atomic_clhlock.v 5.98 KB
Newer Older
1
2
From diaframe.heap_lang Require Import stepping_tacs atomic_instances_heaplang.
From diaframe.lib Require Import own_hints.
3
4
From iris.algebra Require Import agree frac excl auth.
From iris.heap_lang Require Import atomic_heap.
5
From diaframe.examples.wip.logatom Require Import atomic_lock.
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82

Definition clh_lock_firstR := prodR (agreeR $ leibnizO loc) fracR.
Definition clh_lock_secondR := authUR $ optionUR $ exclR $ leibnizO loc.
Class clh_lockG Σ := CLHLockG { 
    clh_lock_firstG :> inG Σ clh_lock_firstR; 
    clh_lock_secondG :> inG Σ clh_lock_secondR;
}.
Definition clh_lockΣ : gFunctors := #[GFunctor clh_lock_firstR; GFunctor clh_lock_secondR].

Obligation Tactic := program_smash_verify.

Global Program Instance subG_clh_lockΣ {Σ} : subG clh_lockΣ Σ  clh_lockG Σ.


Section spec.
  Context `{!heapGS Σ, clh_lockG Σ}. 
  (* not specified on top of logically atomic heap, since current definition does not come with array allocation *)

  Definition new_lock : val :=
    λ: "_", ref (ref #false).

  Definition new_node : val :=
    λ: "_", 
      let: "ret" := AllocN #2 NONE in
      "ret" <- ref #false;;
      "ret".

  Definition wait_on : val :=
    rec: "wait_on" "l" :=
      if: ! "l" then 
        "wait_on" "l"
      else 
        #().

  Definition acquire_with : val :=
    λ: "lk" "node",
      let: "l" := ! "node" in
      "l" <- #true;;
      let: "pred" := Xchg "lk" "l" in  (* also called fetch_and_store sometimes *)
      ("node" + #1) <- "pred";;
      wait_on "pred".

  Definition acquire : val :=
    λ: "lk",
      let: "node" := new_node #() in
      acquire_with "lk" "node";;
      "node".

  Definition release_with : val :=
    λ: "lk" "node",
      ! "node" <- #false;;
      "node" <- ! ("node" + #1).

  Definition release : val :=
    λ: "lk" "node",
      release_with "lk" "node" ;;
      Free (! "node") ;; Free "node" ;; Free ("node" + #1).

  Definition N_node := nroot .@ "clh_node".

  Definition free_node n : iProp Σ :=
     (l : loc) v, n  #l  (n + 1)  v  l  #false.

  Instance wait_on_phys (l : loc) :
    SPEC q (b : bool), <<  l {q} #b >>
      wait_on #l
    << RET #(); l {q} #b  b = false >>.
  Proof.
    iStepsS. iLöb as "IH".
    lang_open_tac.
    iStepsS. destruct x3; iSmash.
  Qed.

  Definition holds_at_loc (l : loc) P : iProp Σ :=
     (l' : loc), l  #l'  P l'.

  Definition queued_loc γe l γ : iProp Σ := 
83
    own γ (to_agree l, 1%Qp)  ( (b : bool), l {#1/2} #b  (b = true  (b = false  own γe ( (Excl' l))  own γ (to_agree l, 1/2)%Qp  l {#1/2} #b))).
84

Ike Mulder's avatar
Ike Mulder committed
85
86
87
  Global Instance own_frac_or_as_forall l γ R : 
    IntoForallCareful (own γ (to_agree l, 1%Qp)  R)%I (λ (q : Qp), own γ (to_agree l, q) - (R   own γ (to_agree l, q)))%I.
  Proof. rewrite /IntoForallCareful. by iStepsS. Qed.
88
89
90
91
92
93

  Definition is_queued_loc γe l' : iProp Σ :=
       γ, own γ (to_agree l', 1/2)%Qp  inv N_node (queued_loc γe l' γ).

  Definition is_queue_head γe (p : loc) : iProp Σ := own γe ( (Excl' p)).

94
  Global Instance update_lock_holder_biabd γe l1 l2 E :
95
96
    HINT own γe ( Excl' l1)  [p;  own γe ( Excl' p)]  [fupd E E]; own γe ( Excl' l2)  [own γe ( Excl' l2)  p = l1] | 99.
  Proof. iStepS. iStepS. rewrite comm. iStepsS. Qed.
97

98
99
100
101
102
103
104
105
  Definition acquired_node γe n (p : loc) : iProp Σ :=
    (n + 1)  #p  own γe ( (Excl' p))  p  #false   (l' : loc), n  #l'  is_queued_loc γe l'  l' {#1/2} #true.

  Instance acquire_with_phys (l n : loc) γe :
    SPEC ⟨↑N_node (p : loc), << free_node n ¦  holds_at_loc l (is_queued_loc γe)   is_queue_head γe p >>
      acquire_with #l #n
    << RET #();  holds_at_loc l (is_queued_loc γe)  is_queue_head γe p  acquired_node γe n p >>.
  Proof.
106
    iStepsS. iLeft.
107
    iStepS. iRight.
Ike Mulder's avatar
Ike Mulder committed
108
109
110
    iStepsS; [iSmash| | iSmash].
    iMod "H5" as (p) "[[Hl >Hp] [_ Hcl]]".
    iReIntro "Hp". rewrite left_id.
111
    iMod ("Hcl" with "[Hl H5 H11 H10 H7 H1 H3 H4]") as "HAU"; first (iFrame; iStepsS).
Ike Mulder's avatar
Ike Mulder committed
112
    iSmash.
113
114
115
116
117
118
  Qed.

  Instance release_with_phys (l n : loc) γe p' :
    SPEC ⟨↑N_node (p : loc), <<  acquired_node γe n p' ¦  holds_at_loc l (is_queued_loc γe)   is_queue_head γe p >>
      release_with #l #n
    << (p'' : loc), RET #(); free_node n ¦  holds_at_loc l (is_queued_loc γe)  is_queue_head γe p'' >>.
119
  Proof. iSmash. Qed.
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145

  Global Program Instance new_node_spec :
    SPEC {{ True }} 
      new_node #() 
    {{ (n : loc), RET #n; free_node n }}.

  Global Instance new_lock_spec :
    SPEC {{ True }} 
      new_lock #() 
    {{ (l p : loc) γe, RET #l; holds_at_loc l (is_queued_loc γe)  is_queue_head γe p }}.
    (* this sidecondition occurs since this approach CoAllocs an ● with a ◯, which is unusual *)
  Proof. iSmash. by apply auth_frag_valid. Qed.

  Global Program Instance acquire_spec (l : loc) γe :
    SPEC ⟨↑N_node (p : loc), <<  holds_at_loc l (is_queued_loc γe)   is_queue_head γe p >>
      acquire #l
    << (n : loc), RET #n;  holds_at_loc l (is_queued_loc γe)  is_queue_head γe p  acquired_node γe n p >>.

  Global Program Instance release_spec (l n : loc) γe p' :
    SPEC ⟨↑N_node (p : loc), <<  acquired_node γe n p' ¦  holds_at_loc l (is_queued_loc γe)   is_queue_head γe p >>
      release #l #n
    << (p'' : loc), RET #();  holds_at_loc l (is_queued_loc γe)  is_queue_head γe p'' >>.

  Definition lock_state (γe : gname) (l p : loc) : iProp Σ :=
    holds_at_loc l (is_queued_loc γe)  is_queue_head γe p.

146
147
  Definition locked_at (γe : gname) (p : loc) (v : val) : iProp Σ 
    :=  (n : loc), v = #n  acquired_node γe n p.
148

149
150
  Global Program Instance clh_lock_atomic_lock : atomic_state_freezer.atomic_freezer Σ :=
    atomic_state_freezer.AtomicFreezer _ _ new_lock acquire release gname loc loc (   N_node) (nroot.@ "free") (λ l, #l) lock_state locked_at _ _ _ _ _ _ _.
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
End spec.