Commit 741c6a8a authored by Ralf Jung's avatar Ralf Jung

Merge branch 'list-agree' into 'master'

Use agree instead of dec_agree

This demonstrates that a list-based agreement could work, and form an OFE. I didn't bother to prove all the functor laws.

Man, this reasoning with about the lists is annoying^^.

What I don't like about this is that un-injection (`agree_car`) is only non-expansive for valid elements. I want to try using a different equivalence relation, maybe I can find one where this works.

Cc @jjourdan @robbertkrebbers

See merge request !22
parents 4800d9e2 45cd995f
Pipeline #3284 passed with stage
in 11 minutes and 29 seconds
...@@ -48,7 +48,6 @@ algebra/base.v ...@@ -48,7 +48,6 @@ algebra/base.v
algebra/dra.v algebra/dra.v
algebra/cofe_solver.v algebra/cofe_solver.v
algebra/agree.v algebra/agree.v
algebra/dec_agree.v
algebra/excl.v algebra/excl.v
algebra/iprod.v algebra/iprod.v
algebra/frac.v algebra/frac.v
......
From iris.algebra Require Export cmra.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ _ !_ /.
Local Arguments pcore _ _ !_ /.
(* This is isomorphic to option, but has a very different RA structure. *)
Inductive dec_agree (A : Type) : Type :=
| DecAgree : A dec_agree A
| DecAgreeBot : dec_agree A.
Arguments DecAgree {_} _.
Arguments DecAgreeBot {_}.
Instance maybe_DecAgree {A} : Maybe (@DecAgree A) := λ x,
match x with DecAgree a => Some a | _ => None end.
Section dec_agree.
Context `{EqDecision A}.
Implicit Types a b : A.
Implicit Types x y : dec_agree A.
Instance dec_agree_valid : Valid (dec_agree A) := λ x,
if x is DecAgree _ then True else False.
Canonical Structure dec_agreeC : ofeT := leibnizC (dec_agree A).
Instance dec_agree_op : Op (dec_agree A) := λ x y,
match x, y with
| DecAgree a, DecAgree b => if decide (a = b) then DecAgree a else DecAgreeBot
| _, _ => DecAgreeBot
end.
Instance dec_agree_pcore : PCore (dec_agree A) := Some.
Definition dec_agree_ra_mixin : RAMixin (dec_agree A).
Proof.
apply ra_total_mixin; apply _ || eauto.
- intros [?|] [?|] [?|]; by repeat (simplify_eq/= || case_match).
- intros [?|] [?|]; by repeat (simplify_eq/= || case_match).
- intros [?|]; by repeat (simplify_eq/= || case_match).
- by intros [?|] [?|] ?.
Qed.
Canonical Structure dec_agreeR : cmraT :=
discreteR (dec_agree A) dec_agree_ra_mixin.
Global Instance dec_agree_total : CMRATotal dec_agreeR.
Proof. intros x. by exists x. Qed.
(* Some properties of this CMRA *)
Global Instance dec_agree_persistent (x : dec_agreeR) : Persistent x.
Proof. by constructor. Qed.
Lemma dec_agree_ne a b : a b DecAgree a DecAgree b = DecAgreeBot.
Proof. intros. by rewrite /= decide_False. Qed.
Lemma dec_agree_idemp (x : dec_agree A) : x x = x.
Proof. destruct x; by rewrite /= ?decide_True. Qed.
Lemma dec_agree_op_inv (x1 x2 : dec_agree A) : (x1 x2) x1 = x2.
Proof. destruct x1, x2; by repeat (simplify_eq/= || case_match). Qed.
Lemma DecAgree_included a b : DecAgree a DecAgree b a = b.
Proof.
split. intros [[c|] [=]%leibniz_equiv]. by simplify_option_eq. by intros ->.
Qed.
End dec_agree.
Arguments dec_agreeC : clear implicits.
Arguments dec_agreeR _ {_}.
From iris.algebra Require Import ofe. From iris.algebra Require Import ofe cmra.
(* Old notation for backwards compatibility. *) (* Old notation for backwards compatibility. *)
(* Deprecated 2016-11-22. Use ofeT instead. *) (* Deprecated 2016-11-22. Use ofeT instead. *)
Notation cofeT := ofeT (only parsing). Notation cofeT := ofeT (only parsing).
(* Deprecated 2016-12-09. Use agree instead. *)
(* The module is called dec_agree_deprecated because if it was just dec_agree,
it would still be imported by "From iris Import dec_agree", and people would
not notice they use sth. deprecated. *)
Module dec_agree_deprecated.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ _ !_ /.
Local Arguments pcore _ _ !_ /.
(* This is isomorphic to option, but has a very different RA structure. *)
Inductive dec_agree (A : Type) : Type :=
| DecAgree : A dec_agree A
| DecAgreeBot : dec_agree A.
Arguments DecAgree {_} _.
Arguments DecAgreeBot {_}.
Instance maybe_DecAgree {A} : Maybe (@DecAgree A) := λ x,
match x with DecAgree a => Some a | _ => None end.
Section dec_agree.
Context `{EqDecision A}.
Implicit Types a b : A.
Implicit Types x y : dec_agree A.
Instance dec_agree_valid : Valid (dec_agree A) := λ x,
if x is DecAgree _ then True else False.
Canonical Structure dec_agreeC : ofeT := leibnizC (dec_agree A).
Instance dec_agree_op : Op (dec_agree A) := λ x y,
match x, y with
| DecAgree a, DecAgree b => if decide (a = b) then DecAgree a else DecAgreeBot
| _, _ => DecAgreeBot
end.
Instance dec_agree_pcore : PCore (dec_agree A) := Some.
Definition dec_agree_ra_mixin : RAMixin (dec_agree A).
Proof.
apply ra_total_mixin; apply _ || eauto.
- intros [?|] [?|] [?|]; by repeat (simplify_eq/= || case_match).
- intros [?|] [?|]; by repeat (simplify_eq/= || case_match).
- intros [?|]; by repeat (simplify_eq/= || case_match).
- by intros [?|] [?|] ?.
Qed.
Canonical Structure dec_agreeR : cmraT :=
discreteR (dec_agree A) dec_agree_ra_mixin.
Global Instance dec_agree_total : CMRATotal dec_agreeR.
Proof. intros x. by exists x. Qed.
(* Some properties of this CMRA *)
Global Instance dec_agree_persistent (x : dec_agreeR) : Persistent x.
Proof. by constructor. Qed.
Lemma dec_agree_ne a b : a b DecAgree a DecAgree b = DecAgreeBot.
Proof. intros. by rewrite /= decide_False. Qed.
Lemma dec_agree_idemp (x : dec_agree A) : x x = x.
Proof. destruct x; by rewrite /= ?decide_True. Qed.
Lemma dec_agree_op_inv (x1 x2 : dec_agree A) : (x1 x2) x1 = x2.
Proof. destruct x1, x2; by repeat (simplify_eq/= || case_match). Qed.
Lemma DecAgree_included a b : DecAgree a DecAgree b a = b.
Proof.
split. intros [[c|] [=]%leibniz_equiv]. by simplify_option_eq. by intros ->.
Qed.
End dec_agree.
Arguments dec_agreeC : clear implicits.
Arguments dec_agreeR _ {_}.
End dec_agree_deprecated.
...@@ -21,6 +21,6 @@ Proof. ...@@ -21,6 +21,6 @@ Proof.
iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh". iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
{ apply: auth_auth_valid. exact: to_gen_heap_valid. } { apply: auth_auth_valid. exact: to_gen_heap_valid. }
iModIntro. iExists (λ σ, own γ ( to_gen_heap σ)); iFrame. iModIntro. iExists (λ σ, own γ ( to_gen_heap σ)); iFrame.
set (Hheap := GenHeapG loc val Σ _ _ _ _ γ). set (Hheap := GenHeapG loc val Σ _ _ _ γ).
iApply (Hwp (HeapG _ _ _)). iApply (Hwp (HeapG _ _ _)).
Qed. Qed.
From iris.algebra Require Import auth gmap frac dec_agree. From iris.algebra Require Import auth gmap frac agree.
From iris.base_logic.lib Require Export own. From iris.base_logic.lib Require Export own.
From iris.base_logic.lib Require Import fractional. From iris.base_logic.lib Require Import fractional.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
Import uPred. Import uPred.
Definition gen_heapUR (L V : Type) `{Countable L, EqDecision V} : ucmraT := Definition gen_heapUR (L V : Type) `{Countable L} : ucmraT :=
gmapUR L (prodR fracR (dec_agreeR V)). gmapUR L (prodR fracR (agreeR (leibnizC V))).
Definition to_gen_heap `{Countable L, EqDecision V} : gmap L V gen_heapUR L V := Definition to_gen_heap {L V} `{Countable L} : gmap L V gen_heapUR L V :=
fmap (λ v, (1%Qp, DecAgree v)). fmap (λ v, (1%Qp, to_agree (v : leibnizC V))).
(** The CMRA we need. *) (** The CMRA we need. *)
Class gen_heapG (L V : Type) (Σ : gFunctors) Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
`{Countable L, EqDecision V} := GenHeapG {
gen_heap_inG :> inG Σ (authR (gen_heapUR L V)); gen_heap_inG :> inG Σ (authR (gen_heapUR L V));
gen_heap_name : gname gen_heap_name : gname
}. }.
Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L, EqDecision V} := Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} :=
{ gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V)) }. { gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V)) }.
Definition gen_heapΣ (L V : Type) `{Countable L, EqDecision V} : gFunctors := Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors :=
#[GFunctor (constRF (authR (gen_heapUR L V)))]. #[GFunctor (constRF (authR (gen_heapUR L V)))].
Instance subG_gen_heapPreG {Σ} `{Countable L, EqDecision V} : Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
subG (gen_heapΣ L V) Σ gen_heapPreG L V Σ. subG (gen_heapΣ L V) Σ gen_heapPreG L V Σ.
Proof. intros ?%subG_inG; split; apply _. Qed. Proof. intros ?%subG_inG; split; apply _. Qed.
...@@ -33,7 +32,7 @@ Section definitions. ...@@ -33,7 +32,7 @@ Section definitions.
own gen_heap_name ( to_gen_heap σ). own gen_heap_name ( to_gen_heap σ).
Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ := Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ :=
own gen_heap_name ( {[ l := (q, DecAgree v) ]}). own gen_heap_name ( {[ l := (q, to_agree (v : leibnizC V)) ]}).
Definition mapsto_aux : { x | x = @mapsto_def }. by eexists. Qed. Definition mapsto_aux : { x | x = @mapsto_def }. by eexists. Qed.
Definition mapsto := proj1_sig mapsto_aux. Definition mapsto := proj1_sig mapsto_aux.
Definition mapsto_eq : @mapsto = @mapsto_def := proj2_sig mapsto_aux. Definition mapsto_eq : @mapsto = @mapsto_def := proj2_sig mapsto_aux.
...@@ -60,14 +59,14 @@ Section gen_heap. ...@@ -60,14 +59,14 @@ Section gen_heap.
Lemma lookup_to_gen_heap_None σ l : σ !! l = None to_gen_heap σ !! l = None. Lemma lookup_to_gen_heap_None σ l : σ !! l = None to_gen_heap σ !! l = None.
Proof. by rewrite /to_gen_heap lookup_fmap=> ->. Qed. Proof. by rewrite /to_gen_heap lookup_fmap=> ->. Qed.
Lemma gen_heap_singleton_included σ l q v : Lemma gen_heap_singleton_included σ l q v :
{[l := (q, DecAgree v)]} to_gen_heap σ σ !! l = Some v. {[l := (q, to_agree v)]} to_gen_heap σ σ !! l = Some v.
Proof. Proof.
rewrite singleton_included=> -[[q' av] [/leibniz_equiv_iff Hl Hqv]]. rewrite singleton_included=> -[[q' av] []].
move: Hl. rewrite /to_gen_heap lookup_fmap fmap_Some=> -[v' [Hl [??]]]; subst. rewrite /to_gen_heap lookup_fmap fmap_Some_equiv => -[v' [Hl [/= -> ->]]].
by move: Hqv=> /Some_pair_included_total_2 [_ /DecAgree_included ->]. move=> /Some_pair_included_total_2 [_] /to_agree_included /leibniz_equiv_iff -> //.
Qed. Qed.
Lemma to_gen_heap_insert l v σ : Lemma to_gen_heap_insert l v σ :
to_gen_heap (<[l:=v]> σ) = <[l:=(1%Qp, DecAgree v)]> (to_gen_heap σ). to_gen_heap (<[l:=v]> σ) = <[l:=(1%Qp, to_agree (v:leibnizC V))]> (to_gen_heap σ).
Proof. by rewrite /to_gen_heap fmap_insert. Qed. Proof. by rewrite /to_gen_heap fmap_insert. Qed.
(** General properties of mapsto *) (** General properties of mapsto *)
...@@ -76,7 +75,7 @@ Section gen_heap. ...@@ -76,7 +75,7 @@ Section gen_heap.
Global Instance mapsto_fractional l v : Fractional (λ q, l {q} v)%I. Global Instance mapsto_fractional l v : Fractional (λ q, l {q} v)%I.
Proof. Proof.
intros p q. by rewrite mapsto_eq -own_op -auth_frag_op intros p q. by rewrite mapsto_eq -own_op -auth_frag_op
op_singleton pair_op dec_agree_idemp. op_singleton pair_op agree_idemp.
Qed. Qed.
Global Instance mapsto_as_fractional l q v : Global Instance mapsto_as_fractional l q v :
AsFractional (l {q} v) (λ q, l {q} v)%I q. AsFractional (l {q} v) (λ q, l {q} v)%I q.
...@@ -86,7 +85,7 @@ Section gen_heap. ...@@ -86,7 +85,7 @@ Section gen_heap.
Proof. Proof.
rewrite mapsto_eq -own_op -auth_frag_op own_valid discrete_valid. rewrite mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
f_equiv=> /auth_own_valid /=. rewrite op_singleton singleton_valid pair_op. f_equiv=> /auth_own_valid /=. rewrite op_singleton singleton_valid pair_op.
by move=> [_ /= /dec_agree_op_inv [?]]. by intros [_ ?%agree_op_inv%(inj to_agree)%leibniz_equiv].
Qed. Qed.
Global Instance heap_ex_mapsto_fractional l : Fractional (λ q, l {q} -)%I. Global Instance heap_ex_mapsto_fractional l : Fractional (λ q, l {q} -)%I.
...@@ -105,8 +104,7 @@ Section gen_heap. ...@@ -105,8 +104,7 @@ Section gen_heap.
rewrite mapsto_eq /mapsto_def own_valid !discrete_valid. rewrite mapsto_eq /mapsto_def own_valid !discrete_valid.
by apply pure_mono=> /auth_own_valid /singleton_valid [??]. by apply pure_mono=> /auth_own_valid /singleton_valid [??].
Qed. Qed.
Lemma mapsto_valid_2 l q1 q2 v1 v2 : Lemma mapsto_valid_2 l q1 q2 v1 v2 : l {q1} v1 l {q2} v2 (q1 + q2)%Qp.
l {q1} v1 l {q2} v2 (q1 + q2)%Qp.
Proof. Proof.
iIntros "[H1 H2]". iDestruct (mapsto_agree with "[$H1 $H2]") as %->. iIntros "[H1 H2]". iDestruct (mapsto_agree with "[$H1 $H2]") as %->.
iApply (mapsto_valid l _ v2). by iFrame. iApply (mapsto_valid l _ v2). by iFrame.
...@@ -118,7 +116,7 @@ Section gen_heap. ...@@ -118,7 +116,7 @@ Section gen_heap.
iIntros (?) "Hσ". rewrite /gen_heap_ctx mapsto_eq /mapsto_def. iIntros (?) "Hσ". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
iMod (own_update with "Hσ") as "[Hσ Hl]". iMod (own_update with "Hσ") as "[Hσ Hl]".
{ eapply auth_update_alloc, { eapply auth_update_alloc,
(alloc_singleton_local_update _ _ (1%Qp, DecAgree v))=> //. (alloc_singleton_local_update _ _ (1%Qp, to_agree (v:leibnizC _)))=> //.
by apply lookup_to_gen_heap_None. } by apply lookup_to_gen_heap_None. }
iModIntro. rewrite to_gen_heap_insert. iFrame. iModIntro. rewrite to_gen_heap_insert. iFrame.
Qed. Qed.
...@@ -138,7 +136,7 @@ Section gen_heap. ...@@ -138,7 +136,7 @@ Section gen_heap.
as %[Hl%gen_heap_singleton_included _]%auth_valid_discrete_2. as %[Hl%gen_heap_singleton_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]". iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
{ eapply auth_update, singleton_local_update, { eapply auth_update, singleton_local_update,
(exclusive_local_update _ (1%Qp, DecAgree v2))=> //. (exclusive_local_update _ (1%Qp, to_agree (v2:leibnizC _)))=> //.
by rewrite /to_gen_heap lookup_fmap Hl. } by rewrite /to_gen_heap lookup_fmap Hl. }
iModIntro. rewrite to_gen_heap_insert. iFrame. iModIntro. rewrite to_gen_heap_insert. iFrame.
Qed. Qed.
......
From iris.program_logic Require Export weakestpre hoare. From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.algebra Require Import excl dec_agree csum. From iris.algebra Require Import excl agree csum.
From iris.heap_lang Require Import assert proofmode notation. From iris.heap_lang Require Import assert proofmode notation.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
...@@ -19,9 +19,9 @@ Definition one_shot_example : val := λ: <>, ...@@ -19,9 +19,9 @@ Definition one_shot_example : val := λ: <>,
end end
end)). end)).
Definition one_shotR := csumR (exclR unitC) (dec_agreeR Z). Definition one_shotR := csumR (exclR unitC) (agreeR ZC).
Definition Pending : one_shotR := (Cinl (Excl ()) : one_shotR). Definition Pending : one_shotR := (Cinl (Excl ()) : one_shotR).
Definition Shot (n : Z) : one_shotR := (Cinr (DecAgree n) : one_shotR). Definition Shot (n : Z) : one_shotR := (Cinr (to_agree n) : one_shotR).
Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }. Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
Definition one_shotΣ : gFunctors := #[GFunctor (constRF one_shotR)]. Definition one_shotΣ : gFunctors := #[GFunctor (constRF one_shotR)].
...@@ -76,8 +76,8 @@ Proof. ...@@ -76,8 +76,8 @@ Proof.
{ iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as %?. } { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as %?. }
wp_load. wp_load.
iCombine "Hγ" "Hγ'" as "Hγ". iCombine "Hγ" "Hγ'" as "Hγ".
iDestruct (own_valid with "Hγ") as %[=->]%dec_agree_op_inv. iDestruct (own_valid with "Hγ") as %?%agree_op_inv%to_agree_inj.
iMod ("Hclose" with "[Hl]") as "_". fold_leibniz. subst. iMod ("Hclose" with "[Hl]") as "_".
{ iNext; iRight; by eauto. } { iNext; iRight; by eauto. }
iModIntro. wp_match. iApply wp_assert. wp_op=>?; simplify_eq/=; eauto. iModIntro. wp_match. iApply wp_assert. wp_op=>?; simplify_eq/=; eauto.
Qed. Qed.
......
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