Commit 4ced3d79 authored by Shabnam Ghasemirad's avatar Shabnam Ghasemirad

Master camera added. main program changed accordingly

parent fb37b170
From iris.algebra Require Import cmra auth list.
From iris.base_logic.lib Require Import own.
Lemma eq_app_nil {A: Type} (x y : list A) :
x = x ++ y y = [].
Proof.
revert y. induction x as [|a x IH]; intros y; [done|].
inversion 1. by apply IH.
Qed.
Instance prefix_PO {A: Type}: PartialOrder (@prefix A).
Proof.
split; [apply _|].
intros x y [z Eqx] [u Eqy].
rewrite Eqx in Eqy.
assert (z = [] u = []) as [].
{ rewrite <-app_assoc in Eqy.
apply eq_app_nil in Eqy. by apply app_eq_nil. }
subst. by rewrite app_nil_r.
Qed.
Section ListMaster.
Context {A: Type} `{EqDecision A} {EquivA : Equiv A} `{@Equivalence A EquivA} `{@LeibnizEquiv A EquivA}.
Inductive lpT :=
| ListBot : lpT
| ListSome : list A lpT.
Inductive lpT_equiv : Equiv lpT :=
| ListSome_equiv l l' : l l' ListSome l ListSome l'
| ListBot_equiv : ListBot ListBot.
Existing Instance lpT_equiv.
Instance lp_equiv_equivalence : @Equivalence lpT ().
Proof.
split; intros l.
- destruct l; constructor. reflexivity.
- intros y H1. destruct l, y; try done; try inversion H1.
induction H1; [|constructor]. constructor. subst. rewrite H1. reflexivity.
- intros y z Hly Hyz. destruct l, y, z; try done; try constructor;
try inversion Hly; try inversion Hyz. subst. rewrite H3. auto.
Qed.
Canonical Structure lpO := discreteO lpT.
Instance lp_valid : Valid lpT :=
λ x, if x is ListSome l then True else False.
Instance lp_core : PCore lpT :=
λ x, if x is ListSome l then Some x else None.
Instance lp_op : Op lpT :=
λ x y, match x, y with
| ListSome lx, ListSome ly =>
if (decide (lx `prefix_of` ly)) then ListSome ly
else if (decide (ly `prefix_of` lx)) then ListSome lx
else ListBot
| _, _ => ListBot
end.
Definition lp_ra_mixin : RAMixin lpT.
Proof.
split.
- unfold Proper, "==>". intros.
destruct x0, y; try done; try inversion H1. subst.
induction H4. done. destruct x. done. unfold "⋅", lp_op.
destruct (decide (l0 `prefix_of` x0 :: l)). admit. admit.
- intros. exists cx. split; [|done]. rewrite <- H2.
destruct x, y; try done; try inversion H1. admit.
- unfold Proper, "==>", impl. intros.
destruct x, y; try done; try inversion H2; try inversion H1.
- unfold Assoc. intros. destruct x, y, z; try done. admit. admit.
- unfold Comm. intros. destruct x, y; try done. admit.
- intros. destruct x. done. inversion H1. rewrite H3. admit.
- intros. destruct x. inversion H1. inversion H1. done.
- intros. destruct x eqn:E, y; inversion H2. admit. admit.
- intros. destruct x, y; try inversion H1; try done.
Admitted.
Canonical Structure lpR := discreteR lpT lp_ra_mixin.
Global Instance lpR_cmra_discrete : CmraDiscrete lpR.
Proof. apply discrete_cmra_discrete. Qed.
Instance lpR_unit : Unit lpT := ListSome [].
Lemma lpT_ucmra_mixin : UcmraMixin lpT.
Proof. split; [done| |done]. unfold LeftId. destruct x; done. Qed.
Canonical Structure lpUR : ucmraT := UcmraT lpT lpT_ucmra_mixin.
Lemma lp_absorb (x y : lpT):
x y x y x.
Proof.
split; first by move => <-; apply : cmra_included_r.
intros [z Eq]. revert Eq.
destruct x,y,z; simpl; try done.
- cbn. inversion 1.
- cbn. case decide => ?; cbn.
+ inversion 1; simplify_eq. case decide => ?.
* assert (l1 = l0). by apply (anti_symm (prefix)). by subst.
* by rewrite decide_True.
+ case decide => ?; cbn; inversion 1. simplify_eq.
by rewrite decide_True.
Qed.
Lemma lp_included (x y : list A) : ListSome x ListSome y x `prefix_of` y.
Proof.
split.
- intros IN. apply lp_absorb in IN. revert IN. cbn.
+ case decide => ?.
* by inversion 1; simplify_eq.
* case decide => ?; [done|inversion 1].
- intros ?. exists (ListSome y). cbn. by rewrite decide_True.
Qed.
Lemma lp_local_unit_update (x x': list A) y
(Ext: x `prefix_of` x'):
(ListSome x, y) ~l~> (ListSome x', ListSome x').
Proof.
apply (local_update_unital_discrete (A:=lpUR)) => z Val Eq. split; [done|].
symmetry. apply lp_absorb. etrans; last by apply lp_included, Ext.
rewrite Eq. apply : cmra_included_r.
Qed.
End ListMaster.
Section lp_auth.
Context (A: Type) `{EqDecision A} {EquivA : Equiv A} `{@Equivalence A EquivA} `{@LeibnizEquiv A EquivA}
`{inG Σ (authR (@lpUR A _ _ _ _))}.
Lemma own_lat_auth_update γ (V V': list A) (Ext: V `prefix_of` V'):
own γ ( (ListSome V)) == own γ ( (ListSome V')) own γ ( (ListSome V')).
Proof.
rewrite -own_op /auth_auth (auth_both_op (ListSome V) ε).
by apply own_update, auth_update, lp_local_unit_update.
Qed.
Lemma own_lat_auth_update_fork γ (V: list A):
own γ ( (ListSome V)) == own γ ( (ListSome V)) own γ ( (ListSome V)).
Proof. by apply own_lat_auth_update. Qed.
Lemma own_lat_auth_max γ (V1 V2: list A) :
own γ ( (ListSome V1)) own γ ( (ListSome V2)) V2 `prefix_of` V1.
Proof.
rewrite -own_op own_valid uPred.discrete_valid auth_both_valid lp_included.
by apply bi.pure_mono=>-[? _].
Qed.
End lp_auth.
\ No newline at end of file
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth frac_auth excl.
From iris.algebra Require Import auth frac_auth excl list.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import proofmode notation lib.par lang.
From exercises Require Import list_pre.
(** Simplified formalization of Michael-Scott queue
thanks to single-writer protocols **)
......@@ -44,7 +44,7 @@ Section MSQueue.
λ: "q" "x",
let: "n" := Alloc (Pair #0 #0) in
"n" <- (link "n", "x") ;;
let: "t" := getTail "q" in
let: "t" := ("q" + #tail) (*getTail "q"*) in
if: (CAS (link "t") #0 ("n"))
then ("q" + #tail) <- "n" ;; #1
else #0.
......@@ -61,7 +61,9 @@ Section MSQueue.
else #0.
Section proof.
Context `{!heapG Σ, !spawnG Σ, !inG Σ (authR (optionUR (exclR gnameO)))}.
Definition my_master_camera := (authR (@lpUR (loc * Z) _ _ _)).
Definition my_camera := (authR (optionUR (exclR (prodO (listO (prodO locO ZO)) gnameO)))).
Context `{!heapG Σ, !spawnG Σ, !inG Σ my_master_camera, !inG Σ my_camera}.
Context (P : Z iProp Σ).
......@@ -75,21 +77,26 @@ Section MSQueue.
Qed.
Fixpoint queue_inv (h t: loc) (γc γ: gname) (L: list (prod loc Z)): iProp Σ :=
Fixpoint queue_inv (h t: loc) (γ: gname) (L: list (loc * Z)): iProp Σ :=
(match L with
| [] => dummy, h = t h (#0, #dummy) (* this will be the sentinel node *)
| (l, v) :: L' => dummy next_link γ', h (#l, #dummy) own γc ( (Excl' γ))
(iTok γ (l (#next_link, #v) P(v) own γc ( (Excl' γ')) (queue_inv l t γc γ' L')))
| (l, v) :: L' => dummy next_link γ', h (#l, #dummy)
(iTok γ (l (#next_link, #v) P(v) iTok γ')) (queue_inv l t γ' L')
end)%I.
(*Typeclasses eauto := debug.*)
Definition queue_inv_s (q: loc) (γc: gname): iProp Σ :=
( h t: loc, q {1/2} #h (q + 1) {1/2} #t (L: list (prod loc Z)) (γ: gname), queue_inv h t γc γ L)%I.
( (h t: loc) (Lout: list (loc * Z)) (γ: gname),
q {1/2} #h (q + 1) {1/2} #t own γc ( (Excl' (Lout, γ)))
( (Lin: list (loc * Z)),
own γc ( (ListSome (Lout ++ Lin))) queue_inv h t γ Lin)
)%I.
Definition queueN : namespace := nroot .@ "queue".
Definition Queue (l : loc) (γc: gname): iProp Σ :=
( q: loc, l = q inv queueN (queue_inv_s q γc))%I.
Definition Consumer (q: loc) (γc: gname): iProp Σ := ( (h: loc) (γ: gname), q {1/2} #h own γc ( (Excl' γ)) iTok γ)%I.
Definition Consumer (q: loc) (γc: gname): iProp Σ := ( (h: loc) (Lout: list (loc * Z)) (γ: gname), q {1/2} #h own γc ( (Excl' (Lout, γ))) iTok γ)%I.
Definition Producer (q: loc): iProp Σ := ( (t: loc), (q + 1) {1/2} #t)%I.
Lemma ghost_var_alloc n :
......@@ -126,14 +133,15 @@ Section MSQueue.
intros. iIntros "_ Post". iApply wp_fupd.
wp_lam. wp_alloc l as "Hl".
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (ghost_var_alloc γ) as (γc) "[Hγc● Hγc◯]".
iMod (ghost_var_alloc (nil, γ)) as (γc) "[Hγc● Hγc◯]".
iMod (ghost_var_alloc (nil ++ nil)) as (γc) "[Hγc● Hγc◯]".
wp_let. wp_alloc q as "(Hh & Ht)". lia. rewrite big_sepL_singleton.
wp_let. do 2 (wp_op; wp_store).
rewrite loc_add_0.
iDestruct "Hh" as "[Hhq Hhc]".
iDestruct "Ht" as "(Htq & Htp)".
iMod (inv_alloc queueN _ (queue_inv_s q γc) with "[Hhq Htq Hl]") as "#Hinv".
{ iNext. iExists l, l. iFrame. iExists nil, γ, 0. iFrame. done. }
iMod (inv_alloc queueN _ (queue_inv_s q γc) with "[Hhq Htq Hl Hγc●]") as "#Hinv".
{ iNext. iExists l, l, nil, γ. iFrame. iExists nil. iFrame. done. }
iModIntro. iApply "Post".
iExists γc.
iSplitL "Hinv". iExists q. eauto.
......@@ -141,7 +149,7 @@ Section MSQueue.
iExists l, γ. iFrame.
Qed.
Lemma findTail_spec q γc:
(*Lemma findTail_spec q γc:
{{{ Queue q γc ∗ Producer q }}}
findTail #q
{{{ (n: loc), RET #n; Producer q }}}.
......@@ -150,15 +158,14 @@ Section MSQueue.
iDestruct "Hq" as (l ->) "#Hinv".
iDestruct "Hp" as (t) "Htp".
wp_lam. wp_op. wp_let. wp_bind (!#(l +ₗ 1))%E.
iInv queueN as (h t') "(Hhq & Htq & HL)" "Hclose".
iInv queueN as (h t' γ) "(Hhq & Htq & Hγc● & HL)" "Hclose".
wp_load. iDestruct (mapsto_agree with "Htp Htq") as %?. symmetry in H. simplify_eq.
iDestruct "HL" as (L γ) "HL".
destruct L as [|(l', v') L'].
iDestruct "HL" as ([|(l', v') L']) "HL".
- iDestruct "HL" as (d Ht) "Hh". rewrite <- Ht in *.
admit.
- iDestruct "HL" as (d nl γ') "(Hh & Hp & Hr)".
iMod ("Hclose" with "[Hhq Htq Hh]") as "_".
{ iNext. iExists h, t. iFrame. iExists ((l', v')::L'), γ'.
iMod ("Hclose" with "[Hhq Htq Hh Hγc●]") as "_".
{ iNext. iExists h, t, γ. iFrame. iExists ((l', v')::L'), γ'.
unfold queue_inv. iExists d, 0, γ'. iFrame. admit. }
iModIntro.
Admitted. (*wp_proj. wp_let.
......@@ -169,7 +176,7 @@ Section MSQueue.
{ iNext. iExists γ, n. iFrame. }
iModIntro. wp_op. wp_if.
iApply "Post". done.
Qed.*)
Qed.*)*)
Lemma tryEnq_spec q x γc:
{{{ Queue q γc Producer q P x }}}
......@@ -185,9 +192,9 @@ Section MSQueue.
wp_bind ((rec: "getTail" "q" := _) #q)%V.
wp_rec.
wp_bind (findTail #q).
iApply (findTail_spec q with "[Hq Hp]"). iFrame. done.
(*iApply (findTail_spec q with "[Hq Hp]"). iFrame. done.
iNext. iIntros (t) "_".
wp_let.
wp_let.*)
Admitted.
Instance inhabited_base_lit : Inhabited base_lit := populate (LitUnit).
......@@ -204,36 +211,36 @@ Section MSQueue.
wp_bind (!#l)%E.
wp_load.
wp_let. wp_bind (!#h)%E.
iInv queueN as (h' t) "(>Hhq & >Htq & HL)" "Hclose".
iInv queueN as (h' t γ) "(>Hhq & >Htq & >Hγc● & HL)" "Hclose".
iDestruct (mapsto_agree with "Hhc Hhq") as %?. symmetry in H. simplify_eq.
iDestruct "HL" as (L γ) "Hr".
iDestruct "HL" as (L) "Hr".
destruct L as [|(l',v) L'] eqn:HL.
- iDestruct "Hr" as (d) ">[% Hh]". subst t.
wp_load.
iMod ("Hclose" with "[Hhq Htq Hh]") as "_".
{ iNext. iExists h, h. iFrame. iExists nil, γ, d. iFrame. done. }
iMod ("Hclose" with "[Hhq Htq Hh Hγc●]") as "_".
{ iNext. iExists h, h, γ. iFrame. iExists nil, d. iFrame. done. }
iModIntro. wp_proj.
wp_let. wp_op. wp_if. iApply "Post". iSplitL. iExists h, s. iFrame. by iLeft.
- iDestruct "Hr" as (d l'' γ') "(>Hh & >Hγc● & HTrade)".
- iDestruct "Hr" as (d l'' γ') "(>Hh & HTrade & Hr)".
iDestruct (ghost_var_agree with "Hγc● Hγc◯") as %<-.
wp_load.
iCombine "Hγ" "HTrade" as "HTrade". rewrite bi.sep_or_l.
rewrite unit_tok_exclusive. iDestruct "HTrade" as "[HF|[Hγ Hl']]"; try done.
iDestruct "Hl'" as "(Hl' & Pv & Hγ'c● & HL')".
iMod ("Hclose" with "[Hhq Htq Hh Hγc● Hγ]") as "_".
{ iNext. iExists h, t. iFrame. iExists ((l', v) :: L'), γ, d, l'', γ'. iFrame. }
iDestruct "Hl'" as "(Hl' & Pv & Hγ')".
iMod ("Hclose" with "[Hhq Htq Hh Hγc● Hγ Hr]") as "_".
{ iNext. iExists h, t, γ. iFrame. iExists ((l', v) :: L'), d, l', γ'. iFrame. }
iModIntro. wp_proj.
wp_let. wp_op. wp_if.
wp_op. rewrite loc_add_0.
wp_bind (CmpXchg _ _ _).
iInv queueN as (h' t') "(>Hhq & >Htq & HL)" "Hclose".
iInv queueN as (h' t' γ'') "(>Hhq & >Htq & Hγ'c● & HL)" "Hclose".
iDestruct (mapsto_agree with "Hhc Hhq") as %?. symmetry in H. simplify_eq.
iCombine "Hhc" "Hhq" as "Hh". wp_cmpxchg_suc.
iDestruct "Hh" as "(Hhc & Hhq)".
iDestruct (ghost_var_agree with "Hγ'c● Hγc◯") as %<-.
iMod ("Hclose" with "[Hhq Htq HL HL']") as "_".
{ iNext. iExists l', t'. iFrame. iExists L', γ'. iFrame.
destruct L as [|(l',v) L'] eqn:HL. }
iMod (ghost_var_update _ γ' with "Hγ'c● Hγc◯") as "(Hγc● & Hγc◯)".
iMod ("Hclose" with "[Hhq Htq HL Hγc●]") as "_".
{ iNext. iExists l', t', γ'. iFrame. iExists L', γ'. iFrame. }
Admitted.
End proof.
......
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