Commit a50a88fc authored by Ralf Jung's avatar Ralf Jung

port most things away from dec_agree

parent 572c37bb
Pipeline #3349 passed with stage
in 8 minutes and 11 seconds
...@@ -2,12 +2,10 @@ ...@@ -2,12 +2,10 @@
From iris.program_logic Require Export weakestpre hoare. From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang proofmode notation. From iris.heap_lang Require Export lang proofmode notation.
From iris.heap_lang.lib Require Import spin_lock. From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import deprecated frac. From iris.algebra Require Import agree frac.
From iris_atomic Require Import atomic sync misc. From iris_atomic Require Import atomic sync misc.
Import dec_agree. Definition syncR := prodR fracR (agreeR valC). (* track the local knowledge of ghost state *)
Definition syncR := prodR fracR (dec_agreeR val). (* track the local knowledge of ghost state *)
Class syncG Σ := sync_tokG :> inG Σ syncR. Class syncG Σ := sync_tokG :> inG Σ syncR.
Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)]. Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)].
...@@ -15,11 +13,13 @@ Instance subG_syncΣ {Σ} : subG syncΣ Σ → syncG Σ. ...@@ -15,11 +13,13 @@ Instance subG_syncΣ {Σ} : subG syncΣ Σ → syncG Σ.
Proof. by intros ?%subG_inG. Qed. Proof. by intros ?%subG_inG. Qed.
Section atomic_sync. Section atomic_sync.
Context `{EqDecision A, !heapG Σ, !lockG Σ, !inG Σ (prodR fracR (dec_agreeR A))}. Context `{EqDecision A, !heapG Σ, !lockG Σ}.
Canonical AC := leibnizC A.
Context `{!inG Σ (prodR fracR (agreeR AC))}.
(* TODO: Rename and make opaque; the fact that this is a half should not be visible (* TODO: Rename and make opaque; the fact that this is a half should not be visible
to the user. *) to the user. *)
Definition gHalf (γ: gname) g : iProp Σ := own γ ((1/2)%Qp, DecAgree g). Definition gHalf (γ: gname) g : iProp Σ := own γ ((1/2)%Qp, to_agree g).
Definition atomic_seq_spec (ϕ: A iProp Σ) α β (f x: val) := Definition atomic_seq_spec (ϕ: A iProp Σ) α β (f x: val) :=
( g, {{ ϕ g α g }} f x {{ v, g', ϕ g' β g g' v }})%I. ( g, {{ ϕ g α g }} f x {{ v, g', ϕ g' β g g' v }})%I.
...@@ -49,8 +49,8 @@ Section atomic_sync. ...@@ -49,8 +49,8 @@ Section atomic_sync.
mk_syncer_spec mk_syncer atomic_syncer_spec mk_syncer. mk_syncer_spec mk_syncer atomic_syncer_spec mk_syncer.
Proof. Proof.
iIntros (Hsync g0 ϕ ret) "Hϕ Hret". iIntros (Hsync g0 ϕ ret) "Hϕ Hret".
iMod (own_alloc (((1 / 2)%Qp, DecAgree g0) ((1 / 2)%Qp, DecAgree g0))) as (γ) "[Hg1 Hg2]". iMod (own_alloc (((1 / 2)%Qp, to_agree g0) ((1 / 2)%Qp, to_agree g0))) as (γ) "[Hg1 Hg2]".
{ by rewrite pair_op dec_agree_idemp. } { by rewrite pair_op agree_idemp. }
iApply (Hsync ( g: A, ϕ g gHalf γ g)%I with "[Hg1 Hϕ]")=>//. iApply (Hsync ( g: A, ϕ g gHalf γ g)%I with "[Hg1 Hϕ]")=>//.
{ iExists g0. by iFrame. } { iExists g0. by iFrame. }
iNext. iIntros (s) "#Hsyncer". iApply "Hret". iNext. iIntros (s) "#Hsyncer". iApply "Hret".
...@@ -76,10 +76,10 @@ Section atomic_sync. ...@@ -76,10 +76,10 @@ Section atomic_sync.
iSpecialize ("Hvs2" $! v). iSpecialize ("Hvs2" $! v).
iDestruct (m_frag_agree' with "[Hg'' Hg1]") as "[Hg %]"; first iFrame. subst. iDestruct (m_frag_agree' with "[Hg'' Hg1]") as "[Hg %]"; first iFrame. subst.
rewrite Qp_div_2. rewrite Qp_div_2.
iAssert (|==> own γ (((1 / 2)%Qp, DecAgree g') ((1 / 2)%Qp, DecAgree g')))%I iAssert (|==> own γ (((1 / 2)%Qp, to_agree g') ((1 / 2)%Qp, to_agree g')))%I
with "[Hg]" as ">[Hg1 Hg2]". with "[Hg]" as ">[Hg1 Hg2]".
{ iApply own_update; last by iAssumption. { iApply own_update; last by iAssumption.
apply cmra_update_exclusive. by rewrite pair_op dec_agree_idemp. } apply cmra_update_exclusive. by rewrite pair_op agree_idemp. }
iMod ("Hvs2" with "[Hg1 Hβ]"). iMod ("Hvs2" with "[Hg1 Hβ]").
{ iExists g'. iFrame. } { iExists g'. iFrame. }
iModIntro. iSplitL "Hg2 Hϕ'"; last done. iModIntro. iSplitL "Hg2 Hϕ'"; last done.
......
...@@ -4,12 +4,10 @@ From iris.program_logic Require Export weakestpre. ...@@ -4,12 +4,10 @@ From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock. From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import auth frac agree excl deprecated gset gmap. From iris.algebra Require Import auth frac agree excl agree gset gmap.
From iris.base_logic Require Import big_op saved_prop. From iris.base_logic Require Import big_op saved_prop.
From iris_atomic Require Import misc peritem sync evmap. From iris_atomic Require Import misc peritem sync evmap.
Import dec_agree.
Definition doOp : val := Definition doOp : val :=
λ: "p", λ: "p",
match: !"p" with match: !"p" with
...@@ -49,7 +47,7 @@ Definition mk_flat : val := ...@@ -49,7 +47,7 @@ Definition mk_flat : val :=
let: "r" := loop "p" "s" "lk" in let: "r" := loop "p" "s" "lk" in
"r". "r".
Definition reqR := prodR fracR (dec_agreeR val). (* request x should be kept same *) Definition reqR := prodR fracR (agreeR valC). (* request x should be kept same *)
Definition toks : Type := gname * gname * gname * gname * gname. (* a bunch of tokens to do state transition *) Definition toks : Type := gname * gname * gname * gname * gname. (* a bunch of tokens to do state transition *)
Definition tokmR : ucmraT := evmapR loc toks unitR. (* tie each slot to tokens *) Definition tokmR : ucmraT := evmapR loc toks unitR. (* tie each slot to tokens *)
Class flatG Σ := FlatG { Class flatG Σ := FlatG {
...@@ -76,17 +74,17 @@ Section proof. ...@@ -76,17 +74,17 @@ Section proof.
Definition installed_s R (ts: toks) (f x: val) := Definition installed_s R (ts: toks) (f x: val) :=
let '(γx, γ1, _, γ4, γq) := ts in let '(γx, γ1, _, γ4, γq) := ts in
( (P: val iProp Σ) Q, ( (P: val iProp Σ) Q,
own γx ((1/2)%Qp, DecAgree x) P x ({{ R P x }} f x {{ v, R Q x v }}) own γx ((1/2)%Qp, to_agree x) P x ({{ R P x }} f x {{ v, R Q x v }})
saved_prop_own γq (Q x) own γ1 (Excl ()) own γ4 (Excl ()))%I. saved_prop_own γq (Q x) own γ1 (Excl ()) own γ4 (Excl ()))%I.
Definition received_s (ts: toks) (x: val) γr := Definition received_s (ts: toks) (x: val) γr :=
let '(γx, _, _, γ4, _) := ts in let '(γx, _, _, γ4, _) := ts in
(own γx ((1/2/2)%Qp, DecAgree x) own γr (Excl ()) own γ4 (Excl ()))%I. (own γx ((1/2/2)%Qp, to_agree x) own γr (Excl ()) own γ4 (Excl ()))%I.
Definition finished_s (ts: toks) (x y: val) := Definition finished_s (ts: toks) (x y: val) :=
let '(γx, γ1, _, γ4, γq) := ts in let '(γx, γ1, _, γ4, γq) := ts in
( Q: val val iProp Σ, ( Q: val val iProp Σ,
own γx ((1/2)%Qp, DecAgree x) saved_prop_own γq (Q x) own γx ((1/2)%Qp, to_agree x) saved_prop_own γq (Q x)
Q x y own γ1 (Excl ()) own γ4 (Excl ()))%I. Q x y own γ1 (Excl ()) own γ4 (Excl ()))%I.
Definition evm := ev loc toks. Definition evm := ev loc toks.
...@@ -131,7 +129,7 @@ Section proof. ...@@ -131,7 +129,7 @@ Section proof.
Definition installed_recp (ts: toks) (x: val) (Q: val iProp Σ) := Definition installed_recp (ts: toks) (x: val) (Q: val iProp Σ) :=
let '(γx, _, γ3, _, γq) := ts in let '(γx, _, γ3, _, γq) := ts in
(own γ3 (Excl ()) own γx ((1/2)%Qp, DecAgree x) saved_prop_own γq Q)%I. (own γ3 (Excl ()) own γx ((1/2)%Qp, to_agree x) saved_prop_own γq Q)%I.
Lemma install_spec Lemma install_spec
R P Q R P Q
...@@ -148,7 +146,7 @@ Section proof. ...@@ -148,7 +146,7 @@ Section proof.
iMod (own_alloc (Excl ())) as (γ1) "Ho1"; first done. iMod (own_alloc (Excl ())) as (γ1) "Ho1"; first done.
iMod (own_alloc (Excl ())) as (γ3) "Ho3"; first done. iMod (own_alloc (Excl ())) as (γ3) "Ho3"; first done.
iMod (own_alloc (Excl ())) as (γ4) "Ho4"; first done. iMod (own_alloc (Excl ())) as (γ4) "Ho4"; first done.
iMod (own_alloc (1%Qp, DecAgree x)) as (γx) "Hx"; first done. iMod (own_alloc (1%Qp, to_agree x)) as (γx) "Hx"; first done.
iMod (saved_prop_alloc (F:=(ofe_funCF val idCF)) Q) as (γq) "#?". iMod (saved_prop_alloc (F:=(ofe_funCF val idCF)) Q) as (γq) "#?".
iInv N as "[Hrs >Hm]" "Hclose". iInv N as "[Hrs >Hm]" "Hclose".
iDestruct "Hm" as (m) "[Hm HRm]". iDestruct "Hm" as (m) "[Hm HRm]".
...@@ -209,8 +207,8 @@ Section proof. ...@@ -209,8 +207,8 @@ Section proof.
+ iDestruct "Hp" as (f' x') "(Hp & Hs)". + iDestruct "Hp" as (f' x') "(Hp & Hs)".
wp_load. destruct ts as [[[[γx γ1] γ3] γ4] γq]. wp_load. destruct ts as [[[[γx γ1] γ3] γ4] γq].
iDestruct "Hs" as (P Q) "(Hx & Hpx & Hf' & HoQ & Ho1 & Ho4)". iDestruct "Hs" as (P Q) "(Hx & Hpx & Hf' & HoQ & Ho1 & Ho4)".
iAssert (|==> own γx (((1/2/2)%Qp, DecAgree x') iAssert (|==> own γx (((1/2/2)%Qp, to_agree x')
((1/2/2)%Qp, DecAgree x')))%I with "[Hx]" as ">[Hx1 Hx2]". ((1/2/2)%Qp, to_agree x')))%I with "[Hx]" as ">[Hx1 Hx2]".
{ iDestruct (own_update with "Hx") as "?"; last by iAssumption. { iDestruct (own_update with "Hx") as "?"; last by iAssumption.
rewrite -{1}(Qp_div_2 (1/2)%Qp). rewrite -{1}(Qp_div_2 (1/2)%Qp).
by apply pair_l_frac_op'. } by apply pair_l_frac_op'. }
...@@ -294,7 +292,7 @@ Section proof. ...@@ -294,7 +292,7 @@ Section proof.
Definition own_γ3 (ts: toks) := let '(_, _, γ3, _, _) := ts in own γ3 (Excl ()). Definition own_γ3 (ts: toks) := let '(_, _, γ3, _, _) := ts in own γ3 (Excl ()).
Definition finished_recp (ts: toks) (x y: val) := Definition finished_recp (ts: toks) (x y: val) :=
let '(γx, _, _, _, γq) := ts in let '(γx, _, _, _, γq) := ts in
( Q, own γx ((1 / 2)%Qp, DecAgree x) saved_prop_own γq (Q x) Q x y)%I. ( Q, own γx ((1 / 2)%Qp, to_agree x) saved_prop_own γq (Q x) Q x y)%I.
Lemma try_srv_spec R (s: loc) (lk: val) (γs γr γm γlk: gname) Φ : Lemma try_srv_spec R (s: loc) (lk: val) (γs γr γm γlk: gname) Φ :
inv N (srv_stack_inv R γs γm γr s srv_tokm_inv γm) inv N (srv_stack_inv R γs γm γr s srv_tokm_inv γm)
...@@ -419,7 +417,8 @@ Section proof. ...@@ -419,7 +417,8 @@ Section proof.
iSpecialize ("Heq" $! a0). by iRewrite "Heq" in "HQ'". iSpecialize ("Heq" $! a0). by iRewrite "Heq" in "HQ'".
- iExFalso. iCombine "Hx" "Hx'" as "Hx". - iExFalso. iCombine "Hx" "Hx'" as "Hx".
iDestruct (own_valid with "Hx") as %[_ H1]. iDestruct (own_valid with "Hx") as %[_ H1].
rewrite pair_op //= dec_agree_ne in H1=>//. rewrite pair_op //= in H1=>//. apply to_agree_comp_valid in H1.
fold_leibniz. done.
Qed. Qed.
End proof. End proof.
...@@ -2,20 +2,20 @@ ...@@ -2,20 +2,20 @@
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation. From iris.heap_lang Require Export lang proofmode notation.
From iris.algebra Require Import auth frac gmap deprecated. From iris.algebra Require Import auth frac gmap agree.
From iris.prelude Require Import countable. From iris.prelude Require Import countable.
From iris.base_logic Require Import big_op auth fractional. From iris.base_logic Require Import big_op auth fractional.
Import uPred dec_agree. Import uPred.
Section lemmas. Section lemmas.
Lemma pair_l_frac_op' (p q: Qp) (g g': val): Lemma pair_l_frac_op' (p q: Qp) (g g': val):
((p + q)%Qp, DecAgree g') ~~> (((p, DecAgree g') (q, DecAgree g'))). ((p + q)%Qp, to_agree g') ~~> (((p, to_agree g') (q, to_agree g'))).
Proof. by rewrite pair_op dec_agree_idemp frac_op'. Qed. Proof. by rewrite pair_op agree_idemp frac_op'. Qed.
Lemma pair_l_frac_op_1' (g g': val): Lemma pair_l_frac_op_1' (g g': val):
(1%Qp, DecAgree g') ~~> (((1/2)%Qp, DecAgree g') ((1/2)%Qp, DecAgree g')). (1%Qp, to_agree g') ~~> (((1/2)%Qp, to_agree g') ((1/2)%Qp, to_agree g')).
Proof. by rewrite pair_op dec_agree_idemp frac_op' Qp_div_2. Qed. Proof. by rewrite pair_op agree_idemp frac_op' Qp_div_2. Qed.
End lemmas. End lemmas.
...@@ -60,26 +60,27 @@ Section big_op_later. ...@@ -60,26 +60,27 @@ Section big_op_later.
End big_op_later. End big_op_later.
Section pair. Section pair.
Context `{EqDecision A, !inG Σ (prodR fracR (dec_agreeR A))}. Context {A : ofeT} `{EqDecision A, !Discrete A, !LeibnizEquiv A, !inG Σ (prodR fracR (agreeR A))}.
Lemma m_frag_agree γm (q1 q2: Qp) (a1 a2: A): Lemma m_frag_agree γm (q1 q2: Qp) (a1 a2: A):
own γm (q1, DecAgree a1) own γm (q2, DecAgree a2) a1 = a2. own γm (q1, to_agree a1) own γm (q2, to_agree a2) a1 = a2.
Proof. Proof.
iIntros "[Ho Ho']". iIntros "[Ho Ho']".
destruct (decide (a1 = a2)) as [->|Hneq]=>//. destruct (decide (a1 = a2)) as [->|Hneq]=>//.
iCombine "Ho" "Ho'" as "Ho". iCombine "Ho" "Ho'" as "Ho".
iDestruct (own_valid with "Ho") as %Hvalid. iDestruct (own_valid with "Ho") as %Hvalid.
exfalso. destruct Hvalid as [_ Hvalid]. exfalso. destruct Hvalid as [_ Hvalid].
simpl in Hvalid. apply dec_agree_op_inv in Hvalid. inversion Hvalid. subst. auto. simpl in Hvalid. apply agree_op_inv in Hvalid. apply (inj to_agree) in Hvalid.
apply Hneq. by fold_leibniz.
Qed. Qed.
Lemma m_frag_agree' γm (q1 q2: Qp) (a1 a2: A): Lemma m_frag_agree' γm (q1 q2: Qp) (a1 a2: A):
own γm (q1, DecAgree a1) own γm (q2, DecAgree a2) own γm (q1, to_agree a1) own γm (q2, to_agree a2)
own γm ((q1 + q2)%Qp, DecAgree a1) a1 = a2. own γm ((q1 + q2)%Qp, to_agree a1) a1 = a2.
Proof. Proof.
iIntros "[Ho Ho']". iIntros "[Ho Ho']".
iDestruct (m_frag_agree with "[Ho Ho']") as %Heq; first iFrame. iDestruct (m_frag_agree with "[Ho Ho']") as %Heq; first iFrame.
subst. iCombine "Ho" "Ho'" as "Ho". subst. iCombine "Ho" "Ho'" as "Ho".
rewrite pair_op frac_op' dec_agree_idemp. by iFrame. rewrite pair_op frac_op' agree_idemp. by iFrame.
Qed. Qed.
End pair. End pair.
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import frac auth gmap deprecated csum. From iris.algebra Require Import frac auth gmap csum.
From iris.base_logic Require Import big_op. From iris.base_logic Require Import big_op.
From iris_atomic Require Export treiber misc evmap. From iris_atomic Require Export treiber misc evmap.
Import dec_agree.
Section defs. Section defs.
Context `{heapG Σ, !evidenceG loc val unitR Σ} (N: namespace). Context `{heapG Σ, !evidenceG loc val unitR Σ} (N: namespace).
Context (R: val iProp Σ) `{ x, TimelessP (R x)}. Context (R: val iProp Σ) `{ x, TimelessP (R x)}.
......
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import frac auth gmap deprecated csum. From iris.algebra Require Import frac auth gmap csum.
From iris.base_logic Require Import big_op. From iris.base_logic Require Import big_op.
From iris_atomic Require Import atomic misc. From iris_atomic Require Import atomic misc.
Import dec_agree.
Definition new_stack: val := λ: <>, ref (ref NONE). Definition new_stack: val := λ: <>, ref (ref NONE).
Definition push: val := Definition push: val :=
......
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