atomic_clhlock.v 5.84 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

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

Ike Mulder's avatar
Ike Mulder committed
126
  Global Program Instance new_lock_spec :
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
    SPEC {{ True }} 
      new_lock #() 
    {{ (l p : loc) γe, RET #l; holds_at_loc l (is_queued_loc γe)  is_queue_head γe p }}.

  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.

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

147
148
  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 _ _ _ _ _ _ _.
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
End spec.