peterson.v 6.92 KB
Newer Older
1
2
From iris_automation.heap_lang Require Import stepping_tacs.
From iris_automation.biabd Require Import biabd_local_updates.
3
From iris_automation.steps Require Import local_post.
4
5
6
From iris.heap_lang Require Import proofmode.
From iris.algebra Require Import proofmode_classes excl csum auth.

7
(* true = left *)
8
9

Definition new_peterson : val :=
10
  λ: <>, 
11
12
13
14
15
16
17
    let: "wl" := ref #false in
    let: "wr" := ref #false in
    let: "first" := ref #true in
    ("first", "wl", "wr").

Definition wait_acquire_l : val :=
  rec: "wait_acquire" "first" "wr" :=
18
19
20
21
    if: (! "wr") && (~ (! "first")) then 
      "wait_acquire" "first" "wr"
    else 
      #().
22
23

Definition acquire_l : val :=
24
25
26
27
  λ: "p",
    let: "first" := Fst (Fst "p") in
    let: "wl" := Snd (Fst "p") in
    let: "wr" := Snd "p" in
28
29
30
31
32
    "wl" <- #true ;;
    "first" <- #false ;;
    wait_acquire_l "first" "wr".

Definition release_l : val :=
33
34
35
36
  λ: "p", (Snd (Fst "p")) <- #false.

Definition wait_acquire_r : val :=
  rec: "wait_acquire" "first" "wl" :=
37
38
39
40
    if: (! "wl") && ((! "first")) then 
      "wait_acquire" "first" "wl"
    else 
      #().
41
42
43
44
45
46
47
48
49
50
51
52

Definition acquire_r : val :=
  λ: "p",
    let: "first" := Fst (Fst "p") in
    let: "wl" := Snd (Fst "p") in
    let: "wr" := Snd "p" in
    "wr" <- #true ;;
    "first" <- #true ;;
    wait_acquire_r "first" "wl".

Definition release_r : val :=
  λ: "p", (Snd "p") <- #false.
53
54
55
56
57

Definition petersonR := authUR $ optionUR $ csumR (exclR $ unitR) (exclR $ unitR).
Class petersonG Σ := PetersonG { peterson_tokG :> inG Σ petersonR }.
Definition petersonΣ : gFunctors := #[GFunctor petersonR].

58
59
Local Obligation Tactic := program_smash_verify.

60
Global Program Instance subG_petersonΣ {Σ} : subG petersonΣ Σ  petersonG Σ.
61
62

Section spec.
63
  Context `{!heapGS Σ, !petersonG Σ}.
64
  Let N := nroot.@"peterson".
65
  Set Default Proof Using "heapGS0 petersonG0".
66
67
68
69
70
71
72
73
74
75
76
77

  (* Cinl is waiting, Cinr is active *)

  Definition peterson_inv waitl waitr first γl γr γR R : iProp Σ :=
     (wl wr f ra la : bool), waitl {#1/2} #wl  waitr {#1/2} #wr  first  #f 
      ((own γl ( (Some $ Cinr $ Excl ()))  la = true  wl = true)  (own γl ( (Some $ Cinl $ Excl ()))  la = false)) 
      ((own γr ( (Some $ Cinr $ Excl ()))  ra = true  wr = true)  (own γr ( (Some $ Cinl $ Excl ()))  ra = false)) 
      (if la && negb ra then f = ra else True)  (* note that we don't know anything when both la and ra are true! *)
      (if ra && negb la then f = negb la else True) 
      ((own γR ( None)  R)  (* If left has it and first = false=right, then right must be inactive *)
       (own γR ( (Some $ Cinl $ Excl ()))  own γl ( (Some $ Cinr $ Excl ()))  f = ra) 
       (own γR ( (Some $ Cinr $ Excl ()))  own γr ( (Some $ Cinr $ Excl ()))  f = negb la)).
78

79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
  Definition is_peterson γl γr γR R p : iProp Σ :=
     (first waitl waitr : loc), p = (#first, #waitl, #waitr)%V  inv N (peterson_inv waitl waitr first γl γr γR R).

  Definition left_released γl (γr γR : gname) p : iProp Σ :=
     (first waitl waitr : loc), p = (#first, #waitl, #waitr)%V 
    waitl {#1/2} #false  own γl ( (Some $ Cinl $ Excl ())).

  Definition left_acquired (γl γr : gname) γR p : iProp Σ :=
     (first waitl waitr : loc), p = (#first, #waitl, #waitr)%V 
    waitl {#1/2} #true  own γR ( (Some $ Cinl $ Excl ())).

  Definition right_released (γl : gname) γr (γR : gname) p : iProp Σ :=
     (first waitl waitr : loc), p = (#first, #waitl, #waitr)%V 
    waitr {#1/2} #false  own γr ( (Some $ Cinl $ Excl ())).

  Definition right_acquired (γl γr : gname) γR p : iProp Σ :=
     (first waitl waitr : loc), p = (#first, #waitl, #waitr)%V 
    waitr {#1/2} #true  own γR ( (Some $ Cinr $ Excl ())).

98
  Global Program Instance new_lock_spec :
99
    SPEC {{ True }}
100
      new_peterson #() 
101
    {{ (p : val), RET p;  R, R ={}=  γl γr γR,
102
103
      is_peterson γl γr γR R p 
      left_released γl γr γR p 
104
      right_released γl γr γR p }}.
105

106
  Instance wait_acquire_l_spec (waitl waitr first : loc) γl γr γR R :
107
108
    SPEC {{ inv N (peterson_inv waitl waitr first γl γr γR R)  own γl ( (Some $ Cinr $ Excl ()))  waitl {#1/2} #true }}
      wait_acquire_l #first #waitr
109
110
    {{ RET #(); waitl {#1/2} #true  own γR ( (Some $ Cinl $ Excl ()))  R }}.
  Proof.
111
    iStepsS. iLöb as "IH".
Ike Mulder's avatar
Ike Mulder committed
112
    wp_lam. do 4 iStepS.
113
    iExpr (! _)%E has post ({{ (b : bool), RET #b; waitl {#1 / 2} #true  
114
        (b = true  own γl ( Some (Cinr (Excl ())))  b = false  own γR ( Some (Cinl (Excl ())))  R) }})%I with ["H2"; "H3"]; 
115
      last iStepsS.
116
117
    - iStepsS; [..|destruct x2]; iSmash.
    - iStepsS; [destruct x3|..]; iSmash.
118
119
  Qed.

120
121
122
123
  Global Instance acquire_l_spec (p : val) γl γr γR R :
    SPEC {{ is_peterson γl γr γR R p  left_released γl γr γR p }}
       acquire_l p
    {{ RET #(); left_acquired γl γr γR p  R }}.
124
  Proof.
Ike Mulder's avatar
Ike Mulder committed
125
    do 25 iStepS.
126
    iExpr (_ <- _)%E has post ({{ RET #(); x3 {#1/2} # true  own γl ( (Some (Cinl (Excl ())))) }})%I with ["H2"; "H3"];
127
    iSmash.
128
129
  Qed.

130
  Global Program Instance release_l_spec (p : val) γl γr γR R :
131
132
133
134
    SPEC {{ is_peterson γl γr γR R p  left_acquired γl γr γR p  R }}
      release_l p 
    {{ RET #(); left_released γl γr γR p }}.

135
136
  Definition acquired_mutual_excl (p : val) γl γr γR :
    left_acquired γl γr γR p  right_acquired γl γr γR p  False := verify.
137

138
  Instance wait_acquire_r_spec (waitl waitr first : loc) γl γr γR R :
139
140
141
    SPEC {{ inv N (peterson_inv waitl waitr first γl γr γR R)  own γr ( (Some $ Cinr $ Excl ()))  waitr {#1/2} #true }}
      wait_acquire_r #first #waitl
    {{ RET #(); waitr {#1/2} #true  own γR ( (Some $ Cinr $ Excl ()))  R }} | 50.
142
  Proof.
143
    iStepsS. iLöb as "IH".
Ike Mulder's avatar
Ike Mulder committed
144
    wp_lam. do 4 iStepS.
145
    iExpr (! _)%E has post ({{ (b : bool), RET #b; waitr {#1 / 2} #true  
146
        (b = true  own γr ( Some (Cinr (Excl ())))  b = false  own γR ( Some (Cinr (Excl ())))  R) }})%I with ["H2"; "H3"];
147
      last iStepsS.
148
149
    - iStepsS; [..|destruct x1]; iSmash.
    - iStepsS; [destruct x3|..]; iSmash.
150
151
152
153
154
155
  Qed.

  Global Instance acquire_r_spec (p : val) γl γr γR R :
    SPEC {{ is_peterson γl γr γR R p  right_released γl γr γR p }}
       acquire_r p
    {{ RET #(); right_acquired γl γr γR p  R }}.
156
  Proof.
Ike Mulder's avatar
Ike Mulder committed
157
    do 25 iStepS.
158
    iExpr (_ <- _)%E has post ({{ RET #(); x4 {#1/2} # true  own γr ( Some (Cinl $ Excl ())) }})%I with ["H2"; "H3"];
159
    iSmash.
160
161
  Qed.

162
  Global Program Instance release_r_spec (p : val) γl γr γR R :
163
164
165
    SPEC {{ is_peterson γl γr γR R p  right_acquired γl γr γR p  R }}
      release_r p 
    {{ RET #(); right_released γl γr γR p }}.
166
167
168
169
170
171
End spec.