Commit 169cdda5 authored by Shabnam Ghasemirad's avatar Shabnam Ghasemirad

Deq Enq SPSC fixed. lemmas added. ghost_var in a separate file.

parent b67e07ce
From iris.algebra Require Import auth frac_auth excl list.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import lib.par proofmode notation lang.
Section Excl_cam.
Definition my_camera := (authR (optionUR (exclR (prodO (listO (prodO (prodO locO ZO) gnameO)) gnameO)))).
Context `{!heapG Σ, !spawnG Σ, !inG Σ my_camera}.
Lemma ghost_var_alloc n :
(|==> γ, own γ ( (Excl' n)) own γ ( (Excl' n)))%I.
Proof.
iMod (own_alloc ( (Excl' n) (Excl' n))) as (γ) "[??]".
- by apply auth_both_valid.
- by eauto with iFrame.
Qed.
Lemma ghost_var_agree γ n m :
own γ ( (Excl' n)) - own γ ( (Excl' m)) - n = m .
Proof.
iIntros "Hγ● Hγ◯".
by iDestruct (own_valid_2 with "Hγ● Hγ◯")
as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid.
Qed.
Lemma ghost_var_update γ n' n m :
own γ ( (Excl' n)) - own γ ( (Excl' m)) ==
own γ ( (Excl' n')) own γ ( (Excl' n')).
Proof.
iIntros "Hγ● Hγ◯".
iMod (own_update_2 _ _ _ ( Excl' n' Excl' n') with "Hγ● Hγ◯") as "[$$]".
{ by apply auth_update, option_local_update, exclusive_local_update. }
done.
Qed.
End Excl_cam.
\ No newline at end of file
......@@ -19,6 +19,14 @@ Proof.
reflexivity.
Qed.
Lemma prefix_app_inv : (A : Type) (l l1 l2 : list A),
l ++ l1 `prefix_of` l ++ l2 l1 `prefix_of` l2.
Proof.
intros. inversion H.
rewrite <- app_assoc in H0. apply app_inv_head in H0.
by exists x.
Qed.
Instance prefix_PO {A: Type}: PartialOrder (@prefix A).
Proof.
split; [apply _|].
......
......@@ -4,7 +4,7 @@ From iris.proofmode Require Import tactics.
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.
From exercises Require Import list_pre ghost_var.
(** Simplified formalization of Michael-Scott queue
thanks to single-writer protocols **)
......@@ -23,7 +23,7 @@ Section MSQueue.
("q" + #tail) <- "s" ;;
"q".
Definition findTail : val :=
(*Definition findTail : val :=
λ: "q",
let: "n" := ("q" + #tail) in
let: "n'" := link "n" in
......@@ -38,16 +38,14 @@ Section MSQueue.
let: "t" := findTail "q" in
if: "t" = #0
then findTail "t"
else "t".
else "t".*)
Definition tryEnq : val :=
λ: "q" "x",
let: "n" := Alloc (Pair #0 #0) in
"n" <- (link "n", "x") ;;
let: "t" := !("q" + #tail) in
if: link "t" = #0
then "t" <- ("n", data "t");; ("q" + #tail) <- "n" ;; #1
else #0.
"t" <- ("n", data "t");; ("q" + #tail) <- "n" ;; #1.
Definition tryDeq : val :=
λ: "q",
......@@ -55,15 +53,11 @@ Section MSQueue.
let: "n" := (link "s") in
if: "n" = #0
then #0
else
if: (CAS ("q" + #head) "s" "n")
then ! (data "n")
else #0.
else ("q" + #head) <- "n";; (data "n").
Section proof.
(* Typeclasses eauto := debug. *)
Definition my_master_camera := (authR (@lpUR (loc * Z * gname) _ _ _ _)).
Definition my_camera := (authR (optionUR (exclR (prodO (listO (prodO (prodO locO ZO) gnameO)) gnameO)))).
Context `{!heapG Σ, !spawnG Σ, !inG Σ my_master_camera, !inG Σ my_camera}.
Context (P : Z iProp Σ).
......@@ -77,7 +71,6 @@ Section MSQueue.
by apply (excl_exclusive (Excl ())) in Valid.
Qed.
Fixpoint queue_inv (h t: loc) (γ: gname) (L: list (loc * Z * gname)): iProp Σ :=
(match L with
| [] => dummy, h = t h (#0, #dummy) (* this will be the sentinel node *)
......@@ -101,32 +94,6 @@ Section MSQueue.
q {1/2} #h own γc ( (Excl' (Lout, γ))) own γm ( (ListSome (Lout ++ Lin))) iTok γ)%I.
Definition Producer (q: loc): iProp Σ := ( (t: loc), (q + 1) {1/2} #t)%I.
Lemma ghost_var_alloc n :
(|==> γ, own γ ( (Excl' n)) own γ ( (Excl' n)))%I.
Proof.
iMod (own_alloc ( (Excl' n) (Excl' n))) as (γ) "[??]".
- by apply auth_both_valid.
- by eauto with iFrame.
Qed.
Lemma ghost_var_agree γ n m :
own γ ( (Excl' n)) - own γ ( (Excl' m)) - n = m .
Proof.
iIntros "Hγ● Hγ◯".
by iDestruct (own_valid_2 with "Hγ● Hγ◯")
as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid.
Qed.
Lemma ghost_var_update γ n' n m :
own γ ( (Excl' n)) - own γ ( (Excl' m)) ==
own γ ( (Excl' n')) own γ ( (Excl' n')).
Proof.
iIntros "Hγ● Hγ◯".
iMod (own_update_2 _ _ _ ( Excl' n' Excl' n') with "Hγ● Hγ◯") as "[$$]".
{ by apply auth_update, option_local_update, exclusive_local_update. }
done.
Qed.
Lemma newQueue_spec:
{{{ True }}}
(newQueue #())
......@@ -211,14 +178,9 @@ Section MSQueue.
wp_load.
iMod ("Hclose" with "[Hhq Htq Ht Hγc● Hγm●]") as "_".
{ iNext. iExists _, _, _, _. iFrame. iExists _. iFrame. iExists _. iFrame. done. }
iModIntro. wp_proj. wp_op. wp_if.
iModIntro. wp_proj.
Admitted.
Lemma prefix_app_inv : (A : Type) (l l1 l2 : list A),
l ++ l1 `prefix_of` l ++ l2 l1 `prefix_of` l2.
Proof.
intros. inversion H. Admitted.
Lemma tryDeq_spec q γc γm:
{{{ Queue q γc γm Consumer q γc γm }}}
tryDeq #q
......@@ -250,22 +212,28 @@ Section MSQueue.
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γ')".
iMod ("Hclose" with "[Hhq Htq Hh Hγc● Hγm● Hγ Hr]") as "_".
{ iNext. iExists h, t, Lout, γ. iFrame. iExists (((l', v), γ') :: L'). iFrame. iExists d, l. iFrame. }
iMod (ghost_var_update _ (Lout, γ') with "Hγc● Hγc◯") as "(Hγc● & Hγc◯)".
iMod ("Hclose" with "[Hhq Htq Hh Hγc● Hγm● Hγ' Hr]") as "_".
{ iNext. iExists h, t, Lout, γ'. iFrame.
iExists ((l', v, γ') :: L'). iFrame. iExists d, l. iFrame. }
iModIntro. wp_proj.
wp_let. wp_op. wp_if.
wp_op. rewrite loc_add_0.
wp_bind (CmpXchg _ _ _).
wp_op. rewrite loc_add_0. wp_bind (_ <- _)%E.
iInv queueN as (h' t' Lout'' γ'') "(>Hhq & >Htq & >Hγc● & HL)" "Hclose".
iDestruct "HL" as (Lin'') "(>Hγm● & Hr)".
iDestruct (mapsto_agree with "Hhc Hhq") as %?. symmetry in H. simplify_eq.
iCombine "Hhc" "Hhq" as "Hh". wp_cmpxchg_suc.
iCombine "Hhc" "Hhq" as "Hh". wp_store.
iDestruct "Hh" as "(Hhc & Hhq)".
iMod (ghost_var_update _ (Lout ++ [(l', v, γ')], γ') with "Hγc● Hγc◯") as "(Hγc● & Hγc◯)".
iDestruct (own_lat_auth_max _ _ with "[Hγm● Hγm◯]") as %Hpre. iFrame.
iMod ("Hclose" with "[Hhq Htq Hr Hγc● Hγm●]") as "_".
{ iNext. iExists l', t', (Lout ++ [(l', v, γ')]), γ'. iFrame. iExists Lin''. iFrame. }
Admitted.
iModIntro. wp_seq. wp_load. wp_proj.
iApply "Post".
iSplitR "Pv".
+ iExists l', (Lout ++ [(l', v, γ')]), L', γ'. iFrame. admit.
+ by iRight.
Admitted.
End proof.
End MSQueue.
......
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