mcs_lock.v 7.46 KB
Newer Older
1
2
3
4
From iris.heap_lang Require Import proofmode.
From iris_automation.heap_lang Require Import stepping_tacs.
From iris_automation.biabd Require Import biabd_local_updates.
From iris.algebra Require Import agree frac excl auth.
Ike Mulder's avatar
Ike Mulder committed
5
From iris_automation.lib Require Import loc_map.
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

Definition new_lock : val :=
  λ: "_", ref NONE.

Definition new_node : val :=
  λ: "_", 
    let: "ret" := AllocN #2 NONE in
    "ret".

Definition enqueue_node : val :=
  rec: "enqueue" "lk" "node" :=
    let: "pred" := ! "lk" in
    if: CAS "lk" "pred" (SOME "node") then 
      "pred"
    else 
      "enqueue" "lk" "node".

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

Definition acquire : val :=
  λ: "lk" "node",
    ("node" + #1) <- NONE;;
    let: "pred" := enqueue_node "lk" "node" in (* this transfers ownership of "node" +ₗ 1 to "lk" *)
    match: "pred" with
      NONE => #()
36
    | SOME "l" => (* in this case, we have received of "l" +ₗ 1 ↦{1/2} NONEV from enqueue_node "lk" *)
37
38
39
40
41
42
43
44
      "node" <- #true ;;
      ("l" + #1) <- SOME "node";; (* this transfers ownership of "node" +ₗ 0 to "l" *)
      wait_on "node"
    end.

Definition wait_for_succ : val :=
  rec: "wait_for" "node" :=
    match: !("node" + #1) with
45
      NONE => "wait_for" "node" (* after reading SOME, we gain ownership of the location *)
46
47
48
49
50
51
    | SOME "l" => #()
    end.

Definition release : val :=
  λ: "lk" "node",
    let: "free" := 
52
53
      if: !("node" + #1) = NONE then (* after reading SOME, we gain ownership of the location *)
        if: CAS "lk" (SOME "node") NONE then (* This CAS, if succesful gives us almost the ownership back *)
54
          #true
55
        else (* someone is in the process of claiming the lock, wait until it has made itself our tail *)
56
57
58
59
60
61
62
63
          wait_for_succ "node";;
          #false
      else
        #false
      in
    if: "free" then
      #()
    else
64
      match: !("node" + #1) with (* here we should have gained ownership and knowledge that it points to SOME *)
65
66
        NONE => #() #() (* unsafe *)
      | SOME "l" =>
67
        "l" <- #false (* returns ownership to "l", and relinquishes lock resource R *)
68
69
      end.

Ike Mulder's avatar
Ike Mulder committed
70
Definition mcs_lockR := prodR (agreeR $ prodO (leibnizO loc) (leibnizO bool)) fracR.
71
Class mcs_lockG Σ := MCSLockG { 
Ike Mulder's avatar
Ike Mulder committed
72
  mcs_lock_tok1G :> inG Σ mcs_lockR; 
73
74
75
  mcs_lock_locmapG :> loc_mapG Σ (option gname);
  mcs_lock_exclG :> inG Σ $ exclR unitO 
}.
Ike Mulder's avatar
Ike Mulder committed
76
Definition mcs_lockΣ : gFunctors := #[GFunctor mcs_lockR; GFunctor $ exclR unitO; loc_mapΣ (option gname)].
77

Ike Mulder's avatar
Ike Mulder committed
78
Local Obligation Tactic := program_smash_verify.
79
80
81
82
83
84
85
86
87

Program Instance subG_mcs_lockΣ {Σ} : subG mcs_lockΣ Σ  mcs_lockG Σ.

Section spec.
  Context `{!heapGS Σ, mcs_lockG Σ}.

  Let N := nroot .@ "mcslock".
  Definition N_signal := N .@ "signal".
  Definition N_node := N .@ "node".
Ike Mulder's avatar
Ike Mulder committed
88
  (* l, false is about the boolean, l, true is about the next location *)
89
90

  Definition signal_loc γm γe l n γb R : iProp Σ :=
Ike Mulder's avatar
Ike Mulder committed
91
92
93
94
95
    own γb (to_agree (l, false), 1%Qp)  ( (b : bool), l  #b  (b = true  ( γ, loc_map_elem γm n (DfracOwn $ 1/2)%Qp (Some γ))  b = false  R  own γe (Excl ())  own γb (to_agree (l, false), (1/2)%Qp))).

  Definition waiting_loc_inv γm γn γe (n : loc) R : iProp Σ :=
    own γn (to_agree (n, true), 1%Qp)  ( v, (n + 1) {# 1/2} v  val_is_unboxed v 
        (v = NONEV  ( (n' : loc) γ, v = SOMEV #n'  (n + 1) {# 1/2} v  own γn (to_agree (n, true), (1/2)%Qp)  own γ (to_agree (n', false), (1/2)%Qp)  inv N_signal (signal_loc γm γe n' n γ R)))).
96
97
98
99

  Definition free_node γm n : iProp Σ :=
     v1 v2, n  v1  (n + 1)  v2  loc_map_elem γm n (DfracOwn 1) None.

Ike Mulder's avatar
Ike Mulder committed
100
  Definition lock_inv γm γe lk R : iProp Σ :=
101
102
103
     (v : val), lk  v  val_is_unboxed v  (
      v = NONEV  own γe (Excl ())  R
        
Ike Mulder's avatar
Ike Mulder committed
104
       (l : loc) γn, v = SOMEV #l  (l + 1) {# 1/2} NONEV  own γn (to_agree (l, true), (1/2)%Qp)  loc_map_elem γm l (DfracOwn $ 1/2)%Qp (Some γn)  inv N_node (waiting_loc_inv γm γn γe l R)
105
106
107
    ).

  Definition is_lock γm γe R v : iProp Σ :=
Ike Mulder's avatar
Ike Mulder committed
108
     (lk : loc), v = #lk  global_reg γm  inv N (lock_inv γm γe lk R).
109
110
111
112

  Global Program Instance own_frac_or_as_forall l γ R : 
    IntoForallCareful (own γ (to_agree l, 1%Qp)  R)%I (λ (q : Qp), own γ (to_agree l, q) - (  own γ (to_agree l, q)  R))%I.

Ike Mulder's avatar
Ike Mulder committed
113
  Global Program Instance new_lock_spec :
114
    SPEC {{ True }} 
115
116
117
118
      new_lock #()          (* note that global_reg is not a difficult premise, since one has ⊢ |={E}=> ∃ γm, global_reg γm *)
    {{ (lk : val), RET lk; ( R γm, R  global_reg γm ={}=  γe, is_lock γm γe R lk) }}.
    (* having global_reg γm on the left side of the fupd means multiple mcs_locks can share the same global_reg γm,
       which means free_nodes can be used in any of these locks, as desired. *)
119

Ike Mulder's avatar
Ike Mulder committed
120
  Global Program Instance new_node_spec :
121
122
123
124
    SPEC {{ True }} 
      new_node #() (* global_reg or is_lock? *)
    {{ (n : loc), RET #n;  γm, global_reg γm ={}= free_node γm n }}.

Ike Mulder's avatar
Ike Mulder committed
125
126
  Program Instance enqueue_node_spec (lk n : loc) γm γe R :
    SPEC {{ inv N (lock_inv γm γe lk R)  (n + 1)  NONEV  loc_map_elem γm n (DfracOwn 1) None }}
127
      enqueue_node #lk #n
Ike Mulder's avatar
Ike Mulder committed
128
    {{ (p : val) γn, RET p; inv N_node (waiting_loc_inv γm γn γe n R)  own γn (to_agree (n, true), (1/2))%Qp  loc_map_elem γm n (DfracOwn $ 1/2)%Qp (Some γn)  (
129
130
      p = NONEV  own γe (Excl ())  R
          
Ike Mulder's avatar
Ike Mulder committed
131
       (l : loc) γl, p = SOMEV #l  (l + 1) {# 1/2} NONEV  loc_map_elem γm l (DfracOwn $ 1/2)%Qp (Some γl)  own γl (to_agree (l, true), (1/2)%Qp)  inv N_node (waiting_loc_inv γm γl γe l R)) }}.
132

Ike Mulder's avatar
Ike Mulder committed
133
134
  Program Instance wait_on_spec (n l : loc) γm γe γ R :
    SPEC {{ inv N_signal (signal_loc γm γe n l γ R)  own γ (to_agree (n, false), 1/2)%Qp }}
135
136
137
138
      wait_on #n
    {{ RET #(); R  own γe (Excl ())  n  #false }}.

  Definition acquired_node γm γn γe n R : iProp Σ :=
Ike Mulder's avatar
Ike Mulder committed
139
     v, n  v  inv N_node (waiting_loc_inv γm γn γe n R)  own γe (Excl ())  own γn (to_agree (n, true), (1/2))%Qp  loc_map_elem γm n (DfracOwn $ 1/2)%Qp (Some γn).
140

Ike Mulder's avatar
Ike Mulder committed
141
  Global Program Instance acquire_spec R (n : loc) (lk : val) γm γe :
142
143
144
    SPEC {{ is_lock γm γe R lk  free_node γm n }}
      acquire lk #n
    {{ γn, RET #(); R  acquired_node γm γn γe n R }}.
Ike Mulder's avatar
Ike Mulder committed
145
146
147

  Program Instance wait_for_succ_spec γm γn γe (n : loc) R :
    SPEC {{ inv N_node (waiting_loc_inv γm γn γe n R)  own γn (to_agree (n, true), (1/2))%Qp }}
148
      wait_for_succ #n
Ike Mulder's avatar
Ike Mulder committed
149
    {{ (l : loc) γ, RET #(); (n + 1)  SOMEV #l  own γ (to_agree (l, false), (1/2)%Qp)  inv N_signal (signal_loc γm γe l n γ R) }}.
150
151
152
153
154
155

  Global Instance release_spec R (n : loc) γm γn γe (v : val) :
    SPEC {{ R  acquired_node γm γn γe n R  is_lock γm γe R v }}
      release v #n
    {{ RET #(); free_node γm n }}.
  Proof.
Ike Mulder's avatar
Ike Mulder committed
156
157
158
159
160
    iStepsS; last iSmash.
    iRight.
    iStepsS; last iSmash.
    (* need a revert since a detected equality rewrites the context, causing a Mergable instance to be missed *)
    iRevert "H6". iSmash.
161
162
  Qed.

163
  Definition acquired_mutual_exclusion γm γn1 γn2 γe n m R : acquired_node γm γn1 γe n R  acquired_node γm γn2 γe m R  False
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
    := verify. (* Cannot do Lemma _ : _ := verify unfortunately. If proper reuse is wanted this should be a Mergable instance *)
End spec.