mcs_lock.v 6.39 KB
Newer Older
1
From iris.heap_lang Require Import proofmode.
2
From diaframe.heap_lang Require Import stepping_tacs.
3
From iris.algebra Require Import agree frac excl auth.
4
From diaframe.lib Require Import loc_map own_hints.
5
6
7
8
9

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

Definition new_node : val :=
Ike Mulder's avatar
Ike Mulder committed
10
  λ: "_", AllocN #2 NONE.
11
12
13
14
15
16
17
18
19
20
21

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

Definition acquire : val :=
  λ: "lk" "node",
    ("node" + #1) <- NONE;;
22
    let: "pred" := Xchg "lk" (SOME "node") in (* this transfers ownership of "node" +ₗ 1 to "lk" *)
23
24
    match: "pred" with
      NONE => #()
25
    | SOME "l" => (* in this case, we have received of "l" +ₗ 1 ↦{1/2} NONEV from enqueue_node "lk" *)
26
27
28
29
30
31
32
33
      "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
34
      NONE => "wait_for" "node" (* after reading SOME, we gain ownership of the location *)
35
36
37
38
39
40
    | SOME "l" => #()
    end.

Definition release : val :=
  λ: "lk" "node",
    let: "free" := 
41
42
      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 *)
43
          #true
44
        else (* someone is in the process of claiming the lock, wait until it has made itself our tail *)
45
46
47
48
49
50
51
52
          wait_for_succ "node";;
          #false
      else
        #false
      in
    if: "free" then
      #()
    else
53
      match: !("node" + #1) with (* here we should have gained ownership and knowledge that it points to SOME *)
54
55
        NONE => #() #() (* unsafe *)
      | SOME "l" =>
56
        "l" <- #false (* returns ownership to "l", and relinquishes lock resource R *)
57
58
      end.

Ike Mulder's avatar
Ike Mulder committed
59
Definition mcs_lockR := prodR (agreeR $ prodO (leibnizO loc) (leibnizO bool)) fracR.
60
Class mcs_lockG Σ := MCSLockG { 
Ike Mulder's avatar
Ike Mulder committed
61
  mcs_lock_tok1G :> inG Σ mcs_lockR; 
62
63
64
  mcs_lock_locmapG :> loc_mapG Σ (option gname);
  mcs_lock_exclG :> inG Σ $ exclR unitO 
}.
Ike Mulder's avatar
Ike Mulder committed
65
Definition mcs_lockΣ : gFunctors := #[GFunctor mcs_lockR; GFunctor $ exclR unitO; loc_mapΣ (option gname)].
66

Ike Mulder's avatar
Ike Mulder committed
67
Local Obligation Tactic := program_smash_verify.
68

69
Global Program Instance subG_mcs_lockΣ {Σ} : subG mcs_lockΣ Σ  mcs_lockG Σ.
70
71
72
73
74
75
76

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
77
  (* l, false is about the boolean, l, true is about the next location *)
78
79

  Definition signal_loc γm γe l n γb R : iProp Σ :=
Ike Mulder's avatar
Ike Mulder committed
80
81
82
83
84
    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)))).
85
86
87
88

  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
89
  Definition lock_inv γm γe lk R : iProp Σ :=
90
91
92
     (v : val), lk  v  val_is_unboxed v  (
      v = NONEV  own γe (Excl ())  R
        
Ike Mulder's avatar
Ike Mulder committed
93
       (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)
94
95
96
    ).

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

99
  Global Instance own_frac_or_as_forall l γ R : 
100
    IntoForallCareful (own γ (to_agree l, 1%Qp)  R)%I (λ (q : Qp), own γ (to_agree l, q) - (  own γ (to_agree l, q)  R))%I.
101
  Proof. rewrite /IntoForallCareful; do 3 iStepS. iFrame. Qed.
102

Ike Mulder's avatar
Ike Mulder committed
103
  Global Program Instance new_lock_spec :
104
    SPEC {{ True }} 
105
106
107
108
      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. *)
109

Ike Mulder's avatar
Ike Mulder committed
110
  Global Program Instance new_node_spec :
111
112
113
114
    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
115
116
  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 }}
117
118
119
120
      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
121
     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).
122

Ike Mulder's avatar
Ike Mulder committed
123
  Global Program Instance acquire_spec R (n : loc) (lk : val) γm γe :
124
125
126
    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
127
128
129

  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 }}
130
      wait_for_succ #n
Ike Mulder's avatar
Ike Mulder committed
131
    {{ (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) }}.
132
133
134
135
136

  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 }}.
137
  Proof. iSmash. Qed.
138

139
  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
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
    := verify. (* Cannot do Lemma _ : _ := verify unfortunately. If proper reuse is wanted this should be a Mergable instance *)
End spec.