Commit bb9d4d91 authored by Zhen Zhang's avatar Zhen Zhang

I DON\'T KNOW WHAT I\'VE WRITTEN

parent 6580992d
......@@ -6,3 +6,4 @@ flat.v
sync_stack.v
treiber_stack.v
protocol.v
misc.v
From iris.program_logic Require Export weakestpre hoare.
From iris.proofmode Require Import invariants ghost_ownership.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From iris.tests Require Import atomic.
From iris.algebra Require Import dec_agree frac.
From iris.program_logic Require Import auth.
Import uPred.
Section lemmas.
Lemma frac_op': forall (p q: Qp), (p q) = (p + q)%Qp.
Proof. done. Qed.
Lemma pair_l_frac_update (g g': val):
((1 / 2)%Qp, DecAgree g) ((1 / 2)%Qp, DecAgree g) ~~> ((1 / 2)%Qp, DecAgree g') ((1 / 2)%Qp, DecAgree g').
Proof.
repeat rewrite pair_op dec_agree_idemp.
rewrite frac_op' Qp_div_2.
eapply cmra_update_exclusive.
done.
Qed.
Lemma pair_l_frac_op (g g': val):
((((1 / 2)%Qp, DecAgree g') ((1 / 2)%Qp, DecAgree g'))) ~~> (1%Qp, DecAgree g').
Proof. by rewrite pair_op dec_agree_idemp frac_op' Qp_div_2. Qed.
End lemmas.
......@@ -4,6 +4,7 @@ From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import frac excl dec_agree.
From flatcomb Require Import misc.
Definition srv : val :=
rec: "srv" "f" "p" :=
......@@ -62,7 +63,7 @@ Section proof.
(γx γ1 γ2: gname) (p: loc)
(Q: val val Prop): iProp Σ :=
(( (x: val), p InjRV x own γ1 (Excl ()))
( (x: val), p InjLV x own γx ((1/2)%Qp, DecAgree x) own γ2 (Excl ()))
( (x: val), p InjLV x own γx ((1/2)%Qp, DecAgree x) own γ1 (Excl ()))
( (x y: val), p InjRV y own γx ((1/2)%Qp, DecAgree x) Q x y own γ2 (Excl ())))%I.
Lemma srv_inv_timeless γx γ1 γ2 p Q: TimelessP (srv_inv γx γ1 γ2 p Q).
......@@ -72,49 +73,53 @@ Section proof.
heapN N
heap_ctx inv N (srv_inv γx γ1 γ2 p Q)
own γx ((1/2)%Qp, DecAgree x) own γ1 (Excl ())
( y, own γ2 (Excl ()) - own γx (1%Qp, DecAgree x) - Q x y- Φ y)
( x y, own γ2 (Excl ()) - own γx (1%Qp, DecAgree x) - Q x y- Φ y)
WP wait #p {{ Φ }}.
Proof.
iIntros (HN) "(#Hh & #Hsrv & Hx & Hempty & HΦ)".
iLöb as "IH".
wp_rec. wp_bind (! #p)%E.
iInv N as ">[Hinv|[Hinv|Hinv]]" "Hclose".
+ (* collision with Hempty *) admit.
+ (* not finished *)
iDestruct "Hinv" as (x') "(Hp & Hx' & Hissued)".
+ iExFalso. iDestruct "Hinv" as (?) "[_ Ho1]".
iCombine "Hempty" "Ho1" as "Hempty".
by iDestruct (own_valid with "Hempty") as "%".
+ iDestruct "Hinv" as (x') "(Hp & Hx' & Hissued)".
wp_load.
iVs ("Hclose" with "[Hp Hx' Hissued]").
{ iNext. iRight. iLeft. iExists x'. by iFrame. }
iVsIntro. wp_match. by iApply ("IH" with "Hx Hempty").
+ (* finished *)
iDestruct "Hinv" as (x' y) "(Hp & Hx' & % & Hissued)".
(* assert (x = x'). *)
(* { admit. (* should use the properties of agreement monoid to fix this *) } *)
wp_load. iVs ("Hclose" with "[Hp Hx' Hissued]").
{ iNext. iRight. iRight. iExists x', y. by iFrame. }
iVsIntro. wp_match.
wp_bind (_ <- _)%E.
iInv N as ">[Hinv|[Hinv|Hinv]]" "Hclose".
- (* colission *) admit.
- (* impossible ... this is why irreversibility is important *)
admit.
- iDestruct "Hinv" as (x'' y') "(Hp & Hx' & % & Hissued)".
assert (x = x'').
{ admit. (* should use the properties of agreement monoid to fix this *) }
subst. wp_store.
iVs ("Hclose" with "[Hp Hempty]").
{ iNext. iLeft. iExists #0. by iFrame. }
iVsIntro. wp_seq.
assert (y = y').
{ admit. (* exclusivity *) }
subst.
iClear "Hx". iClear "Hx'".
iAssert (own γx (1%Qp, DecAgree x'')) as "Hx".
{ admit. }
iSpecialize ("HΦ" $! y' with "Hissued Hx").
by iApply "HΦ".
Admitted.
+ iDestruct "Hinv" as (x' y') "(Hp & Hx' & % & Hissued)".
wp_load.
destruct (decide (x = x')) as [->|Hneq].
{ subst.
iVs ("Hclose" with "[Hp Hx' Hissued]").
{ iNext. iRight. iRight. iExists x', y'. by iFrame. }
iVsIntro. wp_match.
wp_bind (_ <- _)%E.
iInv N as ">[Hinv|[Hinv|Hinv]]" "Hclose".
- iExFalso. iDestruct "Hinv" as (?) "[_ Ho1]".
iCombine "Hempty" "Ho1" as "Hempty".
iDestruct (own_valid with "Hempty") as "%". done.
- iExFalso. iDestruct "Hinv" as (?) "[_ [_ Ho1]]".
iCombine "Hempty" "Ho1" as "Hempty".
iDestruct (own_valid with "Hempty") as "%". done.
- iDestruct "Hinv" as (x'' y'') "(Hp & Hx'' & % & Hissued)".
iCombine "Hx" "Hx''" as "Hx".
destruct (decide (x' = x'')) as [->|Hneq].
+ wp_store. iVs ("Hclose" with "[Hp Hempty]").
{ iNext. iLeft. iExists #0. by iFrame. }
iVsIntro. wp_seq.
iDestruct (own_update with "Hx") as "Hx"; first by apply pair_l_frac_op.
iVs "Hx". iVsIntro.
by iApply ("HΦ" $! x'' y' with "Hissued Hx").
+ iExFalso. iDestruct (own_valid with "Hx") as "%".
iPureIntro. apply Hneq. destruct H1 as [_ Hag]. apply dec_agree_op_inv in Hag.
by inversion Hag. }
{ iCombine "Hx" "Hx'" as "Hx". iExFalso. iDestruct (own_valid with "Hx") as "%".
iPureIntro. apply Hneq. destruct H0 as [_ Hag]. apply dec_agree_op_inv in Hag.
by inversion Hag. }
Qed.
Lemma mk_srv_spec (f: val) Q:
heapN N
heap_ctx ( x:val, WP f x {{ v, Q x v }})
......
......@@ -6,6 +6,7 @@ From iris.heap_lang.lib Require Import spin_lock.
From iris.tests Require Import atomic.
From iris.algebra Require Import dec_agree frac.
From iris.program_logic Require Import auth.
From flatcomb Require Import misc.
Import uPred.
(* See CaReSL paper §3.2 *)
......@@ -87,7 +88,7 @@ Section proof.
Qed.
End proof.
Definition syncR := authR (optionUR (prodR fracR (dec_agreeR val))). (* FIXME: can't use A instead of val *)
Definition syncR := prodR fracR (dec_agreeR val). (* FIXME: can't use a general A instead of val *)
Class syncG Σ := sync_tokG :> inG Σ syncR.
Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)].
......@@ -99,8 +100,8 @@ Section generic.
Definition A := val.
Definition gFragR g : syncR := Some ((1/2)%Qp, DecAgree g).
Definition gFullR g : syncR := Some ((1/2)%Qp, DecAgree g).
Definition gFragR g : syncR := ((1/2)%Qp, DecAgree g).
Definition gFullR g : syncR := ((1/2)%Qp, DecAgree g).
Definition gFrag (γ: gname) g : iProp Σ := own γ (gFragR g).
Definition gFull (γ: gname) g : iProp Σ := own γ (gFullR g).
......@@ -139,7 +140,7 @@ Section generic.
Φ: val iProp Σ, heapN N
heap_ctx ( (l: val) (γ: gname), ϕ l g - gFull γ g - gFrag γ g - Φ l)
WP f #() {{ Φ }}.
Lemma atomic_spec (f_cons f_seq: val) (ϕ: val A iProp Σ) α β:
(g0: A),
heapN N seq_spec f_seq ϕ α β cons_spec f_cons g0 ϕ
......@@ -175,12 +176,14 @@ Section generic.
iApply H=>//. (* FIXME: name *)
iFrame "Hh Hϕ Hα". iIntros (ret g') "Hϕ' Hβ".
iCombine "HgFull" "HgFrag" as "Hg".
iVs (own_update with "Hg") as "[HgFull HgFrag]".
{ admit . }
rewrite /gFullR /gFragR.
iAssert (|=r=> own γ (((1 / 2)%Qp, DecAgree g') ((1 / 2)%Qp, DecAgree g')))%I with "[Hg]" as "Hupd".
{ iApply (own_update); last by iAssumption. apply pair_l_frac_update. }
iVs "Hupd" as "[HgFull HgFrag]".
iSplitL "HgFull Hϕ'".
- iExists g'. by iFrame.
- by iVs ("Hvs2" $! g' ret with "[HgFrag Hβ]"); first by iFrame.
Admitted.
Qed.
End generic.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment