Skip to content

Commit d399582

Browse files
KaptchKaptch
committed
counter example
1 parent 01d8d33 commit d399582

3 files changed

Lines changed: 374 additions & 0 deletions

File tree

‎_CoqProject‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,7 @@ theories/lib/factorial.v
4747
theories/lib/iter.v
4848
theories/lib/eq.v
4949
theories/lib/generators.v
50+
theories/lib/counter.v
5051

5152
theories/examples/delim_lang/lang.v
5253
theories/examples/delim_lang/typing.v

‎theories/effects/store.v‎

Lines changed: 112 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -953,6 +953,96 @@ Section wp.
953953
iApply "Hback".
954954
Qed.
955955

956+
Lemma wp_atomic_atomic_hom'
957+
(f : IT -n> prodO IT IT)
958+
(l : loc) E1 E2 s Φ (κ : IT -n> IT) `{!IT_hom κ} :
959+
nclose (nroot.@"storeE") ## E1 →
960+
heap_ctx
961+
-∗ (|={E1,E2}=> ∃ α w1 w2, ▷ pointsto l α
962+
∗ ▷ (f α ≡ (w1, w2))
963+
∗ ▷ ▷ (pointsto l w2
964+
={E2,E1}=∗ WP@{rs} (κ w1) @ s {{ Φ }}))
965+
-∗ WP@{rs} κ (ATOMIC l f) @ s {{ Φ }}.
966+
Proof.
967+
iIntros (Hee) "#Hcxt H".
968+
unfold ATOMIC; simpl.
969+
rewrite hom_vis.
970+
iApply wp_subreify_ctx_indep_lift''.
971+
iInv (nroot.@"storeE") as (σ) "[>Hlc [Hs Hh]]" "Hcl".
972+
iApply (fupd_mask_weaken E1).
973+
{ set_solver. }
974+
iIntros "Hwk".
975+
iMod "H" as (α w1 w2) "[Hp [#Hcond Hback]]".
976+
iApply (lc_fupd_elim_later with "Hlc").
977+
iNext.
978+
iAssert (⌜is_Some (σ !! l)⌝)%I as "%Hdom".
979+
{ iApply (istate_loc_dom with "Hh Hp"). }
980+
destruct Hdom as [x Hx].
981+
iAssert ((σ !! l ≡ Some (Next α)))%I as "#Hlookup".
982+
{ iApply (istate_read with "Hh Hp"). }
983+
destruct (Next_uninj x) as [β' Hb'].
984+
assert (σ !! l ≡ Some (Next β')) as Hx'.
985+
{ by rewrite Hx Hb'. }
986+
iExists σ, (Next w1), (<[l:=Next w2]>σ), (κ w1), [].
987+
iFrame "Hs".
988+
repeat iSplit.
989+
- rewrite /=.
990+
match goal with
991+
| |- context G [_ ≫= ?F] =>
992+
set (F' := F)
993+
end.
994+
iApply (internal_eq_rewrite _ _
995+
(λ x : option (later IT),
996+
(x ≫= F' ≡ Some (Next w1, (<[l:=Next w2]>σ), []))%I)
997+
with "[Hlookup]").
998+
{
999+
intros m ?? G.
1000+
f_equiv.
1001+
apply option_mbind_ne.
1002+
- subst F'.
1003+
intros ?? H.
1004+
solve_proper_prepare.
1005+
do 3 f_equiv.
1006+
+ f_equiv.
1007+
apply Next_contractive.
1008+
destruct m.
1009+
* apply dist_later_0.
1010+
* apply dist_later_S.
1011+
f_equiv.
1012+
apply H; lia.
1013+
+ do 2 f_equiv.
1014+
apply Next_contractive.
1015+
destruct m.
1016+
* apply dist_later_0.
1017+
* apply dist_later_S.
1018+
f_equiv.
1019+
apply H; lia.
1020+
- done.
1021+
}
1022+
{
1023+
iApply internal_eq_sym.
1024+
rewrite Hx'.
1025+
iApply "Hlookup".
1026+
}
1027+
{
1028+
subst F'.
1029+
rewrite /=.
1030+
iRewrite "Hcond".
1031+
rewrite !later_map_Next /=.
1032+
done.
1033+
}
1034+
- iPureIntro. by rewrite /= ofe_iso_21 laterO_map_Next.
1035+
- iNext. iIntros "Hlc Hs".
1036+
iMod (istate_write l α w2 with "Hh Hp") as "[Hh Hp]".
1037+
iMod ("Hback" with "Hp") as "Hback".
1038+
iMod "Hwk" .
1039+
iMod ("Hcl" with "[Hlc Hh Hs]") as "_".
1040+
{ iExists _. rewrite -(fmap_insert to_agree σ). by iFrame. }
1041+
iModIntro.
1042+
iSplit; last done.
1043+
iApply "Hback".
1044+
Qed.
1045+
9561046
Lemma wp_atomic_hom (f : IT -n> prodO IT IT)
9571047
(l : loc) α w1 w2 s Φ (κ : IT -n> IT) `{!IT_hom κ} :
9581048
heap_ctx
@@ -1192,6 +1282,28 @@ Module faa_wp.
11921282
rewrite get_ret_ret /= get_ret_ret /=.
11931283
done.
11941284
Qed.
1285+
1286+
Lemma wp_faa_atomic_hom (f : A -n> A -n> A) (l : loc) (w : A) E1 E2 s Φ
1287+
(κ : IT -n> IT) `{!IT_hom κ} :
1288+
nclose (nroot.@"storeE") ## E1 →
1289+
heap_ctx rs
1290+
-∗ (|={E1,E2}=> ∃ α : A, ▷ pointsto l (Ret α)
1291+
∗ ▷ ▷ (pointsto l (Ret (f w α))
1292+
={E2,E1}=∗ WP@{rs} (κ (Ret α)) @ s {{ Φ }}))
1293+
-∗ WP@{rs} κ (FAA f l (Ret w)) @ s {{ Φ }}.
1294+
Proof.
1295+
iIntros (Hee) "#Hctx H".
1296+
unfold FAA.
1297+
iApply (wp_atomic_atomic_hom' rs (faa_compute f (Ret w)) l E1 E2 s Φ κ Hee
1298+
with "Hctx [H]").
1299+
iMod "H" as (α) "[Hp Hback]".
1300+
iModIntro.
1301+
iExists (Ret α), (Ret α), (Ret (f w α)).
1302+
iFrame "Hp".
1303+
iSplitR "Hback".
1304+
- iNext. simpl. rewrite get_ret_ret /= get_ret_ret /=. done.
1305+
- iApply "Hback".
1306+
Qed.
11951307
End wp.
11961308
#[global] Opaque FAA.
11971309
End faa_wp.

‎theories/lib/counter.v‎

Lines changed: 261 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,261 @@
1+
From gitrees Require Import gitree program_logic.
2+
From gitrees.effects Require Import store fork.
3+
From iris.algebra.lib Require Import excl_auth.
4+
Import faa_wp.
5+
6+
Section counter.
7+
Context {n' : nat} (rs : gReifiers NotCtxDep n').
8+
Context `{!subReifier reify_store rs}.
9+
Context `{!subReifier reify_fork rs}.
10+
Notation F := (gReifiers_ops rs).
11+
Context {R} `{!Cofe R}.
12+
Context `{!SubOfe natO R, !SubOfe unitO R}.
13+
Notation IT := (IT F R).
14+
Notation ITV := (ITV F R).
15+
16+
Program Definition new_counter : (locO -n> IT) -n> IT := ALLOC (Ret 0).
17+
18+
Definition read_counter : locO -n> IT := READ.
19+
20+
Program Definition incr_fun : natO -n> natO -n> natO := λne a b, a + b.
21+
Solve All Obligations with solve_proper.
22+
23+
Program Definition incr : locO -n> IT := λne ℓ, FAA incr_fun ℓ (Ret 1).
24+
Solve All Obligations with solve_proper_please.
25+
26+
Lemma incr_fun_S (m : nat) : incr_fun 1 m = S m.
27+
Proof. reflexivity. Qed.
28+
29+
Section weakestpre.
30+
Context `{!gitreeGS_gen rs R Σ}.
31+
Context `{!heapG rs R Σ}.
32+
Notation iProp := (iProp Σ).
33+
34+
Lemma wp_new_counter (k : locO -n> IT) s Φ `{!NonExpansive Φ} :
35+
heap_ctx rs -∗
36+
▷▷ (∀ ℓ, pointsto ℓ (Ret 0) -∗ WP@{rs} k ℓ @ s {{ Φ }}) -∗
37+
WP@{rs} new_counter k @ s {{ Φ }}.
38+
Proof.
39+
iIntros "#Hctx H".
40+
iApply (wp_alloc with "Hctx H").
41+
Qed.
42+
43+
Lemma wp_read_counter (ℓ : loc) (m : nat) s Φ :
44+
heap_ctx rs -∗
45+
▷ pointsto ℓ (Ret m) -∗
46+
▷▷ (pointsto ℓ (Ret m) -∗ Φ (RetV m)) -∗
47+
WP@{rs} read_counter ℓ @ s {{ Φ }}.
48+
Proof.
49+
iIntros "#Hctx Hp H".
50+
iApply (wp_read with "Hctx Hp").
51+
iNext. iNext. iIntros "Hp".
52+
iApply wp_val. by iApply "H".
53+
Qed.
54+
55+
Lemma wp_incr (ℓ : loc) (m : nat) s Φ :
56+
heap_ctx rs -∗
57+
▷ pointsto ℓ (Ret m) -∗
58+
▷▷ (pointsto ℓ (Ret (S m)) -∗ Φ (RetV m)) -∗
59+
WP@{rs} incr ℓ @ s {{ Φ }}.
60+
Proof.
61+
iIntros "#Hctx Hp H".
62+
iApply (wp_faa_hom rs incr_fun ℓ m 1 s Φ idfun with "Hctx Hp [H]").
63+
do 2 iNext. iIntros "Hp".
64+
iApply wp_val. iModIntro.
65+
assert (incr_fun 1 m = S m) as -> by reflexivity.
66+
by iApply "H".
67+
Qed.
68+
69+
Program Definition count_to_two : IT :=
70+
new_counter $ λne ℓ,
71+
SEQ (incr ℓ) (SEQ (incr ℓ) (read_counter ℓ)).
72+
Solve All Obligations with solve_proper_please.
73+
74+
Lemma wp_count_to_two s :
75+
heap_ctx rs ⊢ WP@{rs} count_to_two @ s {{ βv, βv ≡ RetV 2 }}.
76+
Proof.
77+
iIntros "#Hctx".
78+
rewrite /count_to_two.
79+
iApply (wp_new_counter with "Hctx"). { solve_proper. }
80+
iNext. iNext. iIntros (ℓ) "Hp". simpl.
81+
iApply wp_seq. { solve_proper. }
82+
iApply (wp_incr with "Hctx Hp").
83+
iNext. iNext. iIntros "Hp". simpl.
84+
iApply wp_seq. { solve_proper. }
85+
iApply (wp_incr with "Hctx Hp").
86+
iNext. iNext. iIntros "Hp". simpl.
87+
iApply (wp_read_counter with "Hctx Hp").
88+
iNext. iNext. iIntros "Hp".
89+
done.
90+
Qed.
91+
92+
End weakestpre.
93+
94+
Section concurrent.
95+
Context `{!gitreeGS_gen rs R Σ}.
96+
Context `{!heapG rs R Σ}.
97+
Context `{!inG Σ (excl_authR boolO)}.
98+
Notation iProp := (iProp Σ).
99+
100+
Definition counterN : namespace := nroot .@ "counter".
101+
102+
Lemma bit_agree γ (a b : bool) :
103+
own γ (●E a) -∗ own γ (◯E b) -∗ ⌜a = b⌝.
104+
Proof.
105+
iIntros "H● H◯".
106+
by iDestruct (own_valid_2 with "H● H◯") as %?%excl_auth_agree_L.
107+
Qed.
108+
109+
Lemma bit_update γ (a b a' : bool) :
110+
own γ (●E a) -∗ own γ (◯E b) ==∗ own γ (●E a') ∗ own γ (◯E a').
111+
Proof.
112+
iIntros "H● H◯".
113+
iMod (own_update_2 with "H● H◯") as "[$ $]".
114+
{ apply excl_auth_update. }
115+
done.
116+
Qed.
117+
118+
Definition is_counter (γ0 γ1 : gname) (ℓ : loc) : iProp :=
119+
inv counterN (∃ b0 b1 : bool,
120+
pointsto ℓ (Ret (Nat.b2n b0 + Nat.b2n b1))
121+
∗ own γ0 (●E b0) ∗ own γ1 (●E b1)).
122+
123+
Global Instance is_counter_persistent γ0 γ1 ℓ :
124+
Persistent (is_counter γ0 γ1 ℓ).
125+
Proof. apply _. Qed.
126+
127+
Lemma wp_incr0 (γ0 γ1 : gname) (ℓ : loc) s Ψ :
128+
heap_ctx rs -∗
129+
is_counter γ0 γ1 ℓ -∗
130+
own γ0 (◯E false) -∗
131+
▷ (∀ m : nat, own γ0 (◯E true) -∗ Ψ (RetV m)) -∗
132+
WP@{rs} incr ℓ @ s {{ Ψ }}.
133+
Proof.
134+
iIntros "#Hctx #Hinv Hf H".
135+
rewrite /incr /=.
136+
iApply (wp_faa_atomic_hom rs incr_fun ℓ 1
137+
(⊤ ∖ ↑(nroot.@"storeE")) (⊤ ∖ ↑(nroot.@"storeE") ∖ ↑counterN)
138+
s Ψ idfun with "Hctx").
139+
{ solve_ndisj. }
140+
iInv counterN as (b0 b1) "(Hp & Ha0 & Ha1)" "Hcl".
141+
iModIntro.
142+
iExists (Nat.b2n b0 + Nat.b2n b1). iFrame "Hp".
143+
iNext. iNext. iIntros "Hp".
144+
iAssert (⌜b0 = false⌝)%I as %->.
145+
{ iApply (bit_agree with "Ha0 Hf"). }
146+
iMod (bit_update γ0 false false true with "Ha0 Hf") as "[Ha0 Hf]".
147+
assert (Nat.b2n true + Nat.b2n b1
148+
= incr_fun 1 (Nat.b2n false + Nat.b2n b1)) as Hval.
149+
{ rewrite incr_fun_S. simpl. lia. }
150+
iMod ("Hcl" with "[Hp Ha0 Ha1]") as "_".
151+
{ iNext. iExists true, b1. rewrite Hval. iFrame "Hp Ha0 Ha1". }
152+
iModIntro. simpl.
153+
iApply wp_val.
154+
by iApply ("H" $! _ with "Hf").
155+
Qed.
156+
157+
Lemma wp_incr1 (γ0 γ1 : gname) (ℓ : loc) s Ψ :
158+
heap_ctx rs -∗
159+
is_counter γ0 γ1 ℓ -∗
160+
own γ1 (◯E false) -∗
161+
▷ (∀ m : nat, own γ1 (◯E true) -∗ Ψ (RetV m)) -∗
162+
WP@{rs} incr ℓ @ s {{ Ψ }}.
163+
Proof.
164+
iIntros "#Hctx #Hinv Hf H".
165+
rewrite /incr /=.
166+
iApply (wp_faa_atomic_hom rs incr_fun ℓ 1
167+
(⊤ ∖ ↑(nroot.@"storeE")) (⊤ ∖ ↑(nroot.@"storeE") ∖ ↑counterN)
168+
s Ψ idfun with "Hctx").
169+
{ solve_ndisj. }
170+
iInv counterN as (b0 b1) "(Hp & Ha0 & Ha1)" "Hcl".
171+
iModIntro.
172+
iExists (Nat.b2n b0 + Nat.b2n b1). iFrame "Hp".
173+
iNext. iNext. iIntros "Hp".
174+
iAssert (⌜b1 = false⌝)%I as %->.
175+
{ iApply (bit_agree with "Ha1 Hf"). }
176+
iMod (bit_update γ1 false false true with "Ha1 Hf") as "[Ha1 Hf]".
177+
assert (Nat.b2n b0 + Nat.b2n true
178+
= incr_fun 1 (Nat.b2n b0 + Nat.b2n false)) as Hval.
179+
{ rewrite incr_fun_S. simpl. lia. }
180+
iMod ("Hcl" with "[Hp Ha0 Ha1]") as "_".
181+
{ iNext. iExists b0, true. rewrite Hval. iFrame "Hp Ha0 Ha1". }
182+
iModIntro. simpl.
183+
iApply wp_val.
184+
by iApply ("H" $! _ with "Hf").
185+
Qed.
186+
187+
Lemma wp_read_le (γ0 γ1 : gname) (ℓ : loc) s Ψ :
188+
heap_ctx rs -∗
189+
is_counter γ0 γ1 ℓ -∗
190+
own γ0 (◯E true) -∗
191+
▷ (∀ k : nat, ⌜1 ≤ k ≤ 2⌝ -∗ Ψ (RetV k)) -∗
192+
WP@{rs} read_counter ℓ @ s {{ Ψ }}.
193+
Proof.
194+
iIntros "#Hctx #Hinv Hf H".
195+
rewrite /read_counter.
196+
iApply (wp_read_atomic_hom rs ℓ
197+
(⊤ ∖ ↑(nroot.@"storeE")) (⊤ ∖ ↑(nroot.@"storeE") ∖ ↑counterN)
198+
s Ψ idfun with "Hctx").
199+
{ solve_ndisj. }
200+
iInv counterN as (b0 b1) "(Hp & Ha0 & Ha1)" "Hcl".
201+
iModIntro.
202+
iExists (Ret (Nat.b2n b0 + Nat.b2n b1)). iFrame "Hp".
203+
iNext. iNext. iIntros "Hp".
204+
iAssert (⌜b0 = true⌝)%I as %->.
205+
{ iApply (bit_agree with "Ha0 Hf"). }
206+
iMod ("Hcl" with "[Hp Ha0 Ha1]") as "_".
207+
{ iNext. iExists true, b1. iFrame "Hp Ha0 Ha1". }
208+
iModIntro. simpl.
209+
iApply wp_val.
210+
iApply ("H" $! (Nat.b2n true + Nat.b2n b1)).
211+
iPureIntro. destruct b1; simpl; lia.
212+
Qed.
213+
214+
Program Definition par_incr : IT :=
215+
new_counter $ λne ℓ,
216+
SEQ (FORK (SEQ (incr ℓ) (Ret ())))
217+
(SEQ (incr ℓ) (read_counter ℓ)).
218+
Solve All Obligations with solve_proper_please.
219+
220+
Definition counter_post : ITV → iProp :=
221+
λ βv, (∃ k : nat, ⌜1 ≤ k ≤ 2⌝ ∧ βv ≡ RetV k)%I.
222+
Global Instance counter_post_ne : NonExpansive counter_post.
223+
Proof. solve_proper. Qed.
224+
225+
Lemma wp_par_incr s :
226+
(⊢ fork_post (RetV ())) →
227+
fork_ctx rs -∗
228+
heap_ctx rs -∗
229+
WP@{rs} par_incr @ s {{ counter_post }}.
230+
Proof using All.
231+
iIntros (Hfork) "#Hfctx #Hctx".
232+
rewrite /par_incr.
233+
iApply (wp_new_counter with "Hctx").
234+
iNext. iNext. iIntros (ℓ) "Hp". simpl.
235+
iApply fupd_wp.
236+
iMod (own_alloc (●E false ⋅ ◯E false)) as (γ0) "[Ha0 Hf0]".
237+
{ apply excl_auth_valid. }
238+
iMod (own_alloc (●E false ⋅ ◯E false)) as (γ1) "[Ha1 Hf1]".
239+
{ apply excl_auth_valid. }
240+
iMod (inv_alloc counterN _
241+
(∃ b0 b1 : bool, pointsto ℓ (Ret (Nat.b2n b0 + Nat.b2n b1))
242+
∗ own γ0 (●E b0) ∗ own γ1 (●E b1))
243+
with "[Hp Ha0 Ha1]") as "#Hinv".
244+
{ iNext. iExists false, false. simpl. iFrame "Hp Ha0 Ha1". }
245+
iModIntro.
246+
iApply wp_seq.
247+
iApply (wp_fork with "Hfctx [Hf1] [Hf0]").
248+
- iNext. iApply wp_seq.
249+
iApply (wp_incr1 with "Hctx Hinv Hf1").
250+
iNext. iIntros (m) "_". iApply wp_val. iModIntro. by iApply Hfork.
251+
- iNext. iApply wp_seq.
252+
iApply (wp_incr0 with "Hctx Hinv Hf0").
253+
iNext. iIntros (m) "Hf0".
254+
iApply (wp_read_le with "Hctx Hinv Hf0").
255+
iNext. iIntros (k) "%Hk".
256+
rewrite /counter_post. iExists k. by iSplit.
257+
Qed.
258+
259+
End concurrent.
260+
261+
End counter.

0 commit comments

Comments
 (0)