Skip to content

Commit a28062e

Browse files
simongregersensimongregersen
committed
fix #4 
1 parent a362658 commit a28062e

3 files changed

Lines changed: 203 additions & 22 deletions

File tree

‎exercises/resource_algebra.v‎

Lines changed: 12 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -324,10 +324,9 @@ Proof.
324324
Qed.
325325

326326
Lemma dfrac_valid_discarded : ✓ (DfracDiscarded).
327-
(* Solution *) Proof.
328-
rewrite dfrac_valid.
329-
done.
330-
Qed.
327+
Proof.
328+
(* exercise *)
329+
Admitted.
331330

332331
Lemma dfrac_invalid_own : ¬ (✓ (DfracOwn (2/3) ⋅ DfracOwn (2/3))).
333332
Proof.
@@ -392,16 +391,14 @@ Proof.
392391
Qed.
393392

394393
Lemma dfrac_pre_disc_both : DfracDiscarded ≼ DfracBoth (3/4).
395-
(* Solution *) Proof.
396-
exists (DfracOwn (3/4)).
397-
compute_done.
398-
Qed.
394+
Proof.
395+
(* exercise *)
396+
Admitted.
399397

400398
Lemma dfrac_pre_own_both : DfracOwn (2/4) ≼ DfracBoth (3/4).
401-
(* Solution *) Proof.
402-
exists (DfracBoth (1/4)).
403-
compute_done.
404-
Qed.
399+
Proof.
400+
(* exercise *)
401+
Admitted.
405402

406403
(* ----------------------------------------------------------------- *)
407404
(** *** Frame Preserving Update *)
@@ -748,12 +745,9 @@ Qed.
748745

749746
Lemma agree_valid_opL (a b : A) : ✓ (to_agree a ⋅ to_agree b) →
750747
to_agree a ⋅ to_agree b ≡ to_agree a.
751-
(* Solution *) Proof.
752-
intros Hvalid.
753-
apply to_agree_op_valid in Hvalid.
754-
rewrite Hvalid.
755-
apply agree_idemp.
756-
Qed.
748+
Proof.
749+
(* exercise *)
750+
Admitted.
757751

758752
(**
759753
Due to idempotency and the fact that the combination of equivalent

‎exercises/ticket_lock_advanced.v‎

Lines changed: 187 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,187 @@
1+
From iris.algebra Require Import auth excl gset numbers.
2+
From iris.base_logic.lib Require Export invariants.
3+
From iris.heap_lang Require Import lang proofmode notation.
4+
5+
(* ################################################################# *)
6+
(** * Case Study: Ticket Lock Advanced *)
7+
8+
(**
9+
The implementation, resource algebra, and representation predicates
10+
are identical to the original Ticket Lock chapter. Only the proofs
11+
differ.
12+
*)
13+
14+
(* ================================================================= *)
15+
(** ** Implementation *)
16+
17+
Definition mk_lock : val :=
18+
λ: <>, (ref #0, ref #0).
19+
20+
Definition wait : val :=
21+
rec: "wait" "n" "l" :=
22+
let: "o" := !(Fst "l") in
23+
if: "o" = "n" then #() else "wait" "n" "l".
24+
25+
Definition acquire : val :=
26+
rec: "acquire" "l" :=
27+
let: "n" := !(Snd "l") in
28+
if: CAS (Snd "l") "n" ("n" + #1) then
29+
wait "n" "l"
30+
else
31+
"acquire" "l".
32+
33+
Definition release : val :=
34+
λ: "l", Fst "l" <- ! (Fst "l") + #1.
35+
36+
(* ================================================================= *)
37+
(** ** Representation Predicates *)
38+
39+
Definition RA : cmra :=
40+
authR (prodUR (optionUR (exclR natO)) (gset_disjR nat)).
41+
42+
Section proofs.
43+
Context `{!heapGS Σ, !inG Σ RA}.
44+
Let N := nroot .@ "ticket_lock".
45+
46+
Definition locked_by (γ : gname) (o : nat) : iProp Σ :=
47+
own γ (◯ (Excl' o, GSet ∅)).
48+
49+
Definition locked (γ : gname) : iProp Σ :=
50+
∃ o, locked_by γ o.
51+
52+
Lemma locked_excl γ : locked γ -∗ locked γ -∗ False.
53+
Proof.
54+
iIntros "[%o1 H1] [%o2 H2]".
55+
iDestruct (own_valid_2 with "H1 H2") as %[]%auth_frag_valid_1; done.
56+
Qed.
57+
58+
Definition issued (γ : gname) (x : nat) : iProp Σ :=
59+
own γ (◯ (ε : option (excl nat), GSet {[x]})).
60+
61+
Definition lock_inv (γ : gname) (lo ln : loc) (P : iProp Σ) : iProp Σ :=
62+
∃ o n : nat, lo ↦ #o ∗ ln ↦ #n ∗
63+
own γ (● (Excl' o, GSet (set_seq 0 n))) ∗
64+
(
65+
(locked_by γ o ∗ P) ∨
66+
issued γ o
67+
).
68+
69+
Definition is_lock (γ : gname) (l : val) (P : iProp Σ) : iProp Σ :=
70+
∃ lo ln : loc, ⌜l = (#lo, #ln)%V⌝ ∗ inv N (lock_inv γ lo ln P).
71+
72+
(* ================================================================= *)
73+
(** ** Specifications *)
74+
75+
Lemma mk_lock_spec P :
76+
{{{ P }}} mk_lock #() {{{ γ l, RET l; is_lock γ l P }}}.
77+
Proof.
78+
iIntros "%Φ HP HΦ".
79+
wp_lam.
80+
wp_alloc lo; wp_alloc ln.
81+
wp_pures.
82+
iMod (own_alloc (● (Excl' 0, GSet ∅) ⋅ ◯ (Excl' 0, GSet ∅))) as "(%γ & Hγ & Ho)".
83+
{ by apply auth_both_valid_discrete. }
84+
iApply ("HΦ" $! γ).
85+
iExists _, _; iSplitR; first done.
86+
iApply inv_alloc; iExists 0, 0; eauto with iFrame.
87+
Qed.
88+
89+
Lemma wait_spec γ l P x :
90+
{{{ is_lock γ l P ∗ issued γ x }}}
91+
wait #x l
92+
{{{ RET #(); locked γ ∗ P }}}.
93+
Proof.
94+
iIntros "%Φ [(%lo & %ln & -> & #I) Hx] HΦ".
95+
iLöb as "IH".
96+
wp_rec.
97+
wp_pures.
98+
wp_bind (! _)%E.
99+
iInv "I" as "(%o & %n & Hlo & Hln & Hγ)".
100+
wp_load.
101+
destruct (decide (o = x)) as [->|].
102+
- iDestruct "Hγ" as "[Hγ [[Hexcl HP]|Ho]]".
103+
+ iSplitL "Hlo Hln Hγ Hx"; first by iExists _, _; iFrame.
104+
iModIntro.
105+
wp_pures.
106+
rewrite bool_decide_eq_true_2 //.
107+
wp_pures.
108+
by iApply "HΦ"; iFrame.
109+
+ iDestruct (own_valid_2 with "Hx Ho") as
110+
%[_ Hvl%gset_disj_valid_op]%auth_frag_valid_1;
111+
set_solver.
112+
- iSplitL "Hlo Hln Hγ"; first by iExists _, _; iFrame.
113+
iModIntro.
114+
wp_pures.
115+
rewrite bool_decide_eq_false_2; last naive_solver.
116+
wp_pures.
117+
iApply ("IH" with "Hx HΦ").
118+
Qed.
119+
120+
Lemma acquire_spec γ l P :
121+
{{{ is_lock γ l P }}} acquire l {{{ RET #(); locked γ ∗ P }}}.
122+
Proof.
123+
iIntros "%Φ (%lo & %ln & -> & #I) HΦ".
124+
iLöb as "IH".
125+
wp_rec.
126+
wp_pures.
127+
wp_bind (! _)%E.
128+
iInv "I" as "(%o & %n & Hlo & Hln & Hγ)".
129+
wp_load.
130+
iSplitL "Hlo Hln Hγ"; first by iExists _, _; iFrame.
131+
clear o.
132+
iModIntro.
133+
wp_pures.
134+
wp_bind (CmpXchg _ _ _).
135+
iInv "I" as "(%o & %n' & Hlo & Hln & Hγ)".
136+
destruct (decide (n' = n)) as [->|].
137+
- wp_cmpxchg_suc.
138+
rewrite Z.add_comm -(Nat2Z.inj_add 1) /=.
139+
iDestruct "Hγ" as "[Hγ Hγ']".
140+
iMod (own_update _ _ (● (Excl' o, GSet (set_seq 0 (S n))) ⋅ ◯ (ε, GSet {[n]})) with "Hγ") as "[Hγ Hn]".
141+
{
142+
apply auth_update_alloc, prod_local_update_2.
143+
rewrite set_seq_S_end_union_L /=.
144+
apply gset_disj_alloc_empty_local_update; apply (set_seq_S_end_disjoint 0).
145+
}
146+
iSplitL "Hlo Hln Hγ Hγ'"; first by iExists _, _; iFrame.
147+
iModIntro.
148+
wp_pures.
149+
wp_apply (wait_spec with "[I $Hn]"); first iExists _, _; eauto.
150+
- wp_cmpxchg_fail; first naive_solver.
151+
iModIntro.
152+
iSplitL "Hlo Hln Hγ"; first by iExists _, _; iFrame.
153+
wp_pures.
154+
by iApply "IH".
155+
Qed.
156+
157+
Lemma release_spec γ l P :
158+
{{{ is_lock γ l P ∗ locked γ ∗ P }}} release l {{{ RET #(); True }}}.
159+
Proof.
160+
iIntros "%Φ ((%lo & %ln & -> & #I) & [%o Hexcl] & HP) HΦ".
161+
wp_lam.
162+
wp_pures.
163+
wp_bind (! _)%E.
164+
iInv "I" as "(%o' & %n & Hlo & Hln & [Hγ [[>Hexcl' _]|Ho]])".
165+
{ by iDestruct (own_valid_2 with "Hexcl Hexcl'") as %[]%auth_frag_valid_1. }
166+
wp_load.
167+
iDestruct (own_valid_2 with "Hγ Hexcl") as
168+
%[[<-%Excl_included%leibniz_equiv _]%pair_included _]%auth_both_valid_discrete.
169+
iModIntro.
170+
iSplitL "Hlo Hln Hγ Ho"; first by iFrame.
171+
clear n.
172+
wp_pures.
173+
rewrite Z.add_comm -(Nat2Z.inj_add 1) /=.
174+
iInv "I" as "(%o' & %n & Hlo & Hln & [Hγ [[>Hexcl' _]|Ho]])".
175+
{ by iDestruct (own_valid_2 with "Hexcl Hexcl'") as %[]%auth_frag_valid. }
176+
wp_store.
177+
iDestruct (own_valid_2 with "Hγ Hexcl") as
178+
%[[<-%Excl_included%leibniz_equiv _]%pair_included _]%auth_both_valid_discrete.
179+
iCombine "Hγ Hexcl" as "Hγ".
180+
iMod (own_update _ _ (● (Excl' (S o), GSet (set_seq 0 n)) ⋅ ◯ (Excl' (S o), ε)) with "Hγ") as "[Hγ Hexcl]".
181+
{ by apply auth_update, prod_local_update_1, option_local_update, exclusive_local_update. }
182+
iModIntro.
183+
iSplitR "HΦ"; last by iApply "HΦ".
184+
iExists _, _; eauto with iFrame.
185+
Qed.
186+
187+
End proofs.

‎theories/resource_algebra.v‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -327,7 +327,7 @@ Proof.
327327
Qed.
328328

329329
Lemma dfrac_valid_discarded : ✓ (DfracDiscarded).
330-
(* Solution *) Proof.
330+
(* SOLUTION *) Proof.
331331
rewrite dfrac_valid.
332332
done.
333333
Qed.
@@ -395,13 +395,13 @@ Proof.
395395
Qed.
396396

397397
Lemma dfrac_pre_disc_both : DfracDiscarded ≼ DfracBoth (3/4).
398-
(* Solution *) Proof.
398+
(* SOLUTION *) Proof.
399399
exists (DfracOwn (3/4)).
400400
compute_done.
401401
Qed.
402402

403403
Lemma dfrac_pre_own_both : DfracOwn (2/4) ≼ DfracBoth (3/4).
404-
(* Solution *) Proof.
404+
(* SOLUTION *) Proof.
405405
exists (DfracBoth (1/4)).
406406
compute_done.
407407
Qed.
@@ -762,7 +762,7 @@ Qed.
762762

763763
Lemma agree_valid_opL (a b : A) : ✓ (to_agree a ⋅ to_agree b) →
764764
to_agree a ⋅ to_agree b ≡ to_agree a.
765-
(* Solution *) Proof.
765+
(* SOLUTION *) Proof.
766766
intros Hvalid.
767767
apply to_agree_op_valid in Hvalid.
768768
rewrite Hvalid.

0 commit comments

Comments
 (0)