Merge branch 'jaehwang/stack-history-mp' into 'graphs_multi'

message passing example using stack history LAT

See merge request iris/gpfsl!23

_CoqProject

@@ -143,7 +143,8 @@ theories/examples/stack/proof_na.v
 theories/examples/stack/proof_treiber_gps.v
 theories/examples/stack/proof_treiber_graph.v
 theories/examples/stack/proof_treiber_history.v
-theories/examples/stack/proof_mp_client.v
+theories/examples/stack/proof_mp_client_graph.v
+theories/examples/stack/proof_mp_client_history.v
 theories/examples/stack/proof_elim_graph.v
 theories/examples/stack/proof_elim_graph_closed.v
 ## Queue

theories/examples/history/ghost.v

@@ -59,30 +59,22 @@ Definition history_snap γg E M : vProp :=
 
 (* Updates *)
 Lemma ghost_history_update γ E E' (Le: E ⊑ E') :
-  history_gmaster γ 1 E ==∗ history_gmaster γ 1 E' ∗ history_gsnap γ E'.
-Proof.
-  rewrite -own_op. apply own_update.
-  rewrite -mono_list_auth_lb_op. by apply mono_list_update.
-Qed.
+  history_gmaster γ 1 E ==∗ history_gmaster γ 1 E'.
+Proof. by apply own_update, mono_list_update. Qed.
 
-Lemma ghost_history_fork γ f E E' (Le: E' ⊑ E) :
-  history_gmaster γ f E ==∗ history_gmaster γ f E ∗ history_gsnap γ E'.
-Proof.
-  rewrite -own_op. apply own_update.
-  rewrite /ghost_history_master /ghost_history_snap.
-  rewrite mono_list_auth_lb_op.
-  rewrite -(assoc _ (●ML{#f} _)) mono_list_lb_op_r; [|done].
-  by rewrite -mono_list_auth_lb_op.
-Qed.
+Lemma ghost_history_master_snap γ f E :
+  history_gmaster γ f E ⊢ history_gsnap γ E.
+Proof. apply own_mono, mono_list_included. Qed.
+
+Lemma ghost_history_snap_sub γ E G' :
+  E ⊑ G' →
+  history_gsnap γ G' -∗ history_gsnap γ E.
+Proof. intros Le. apply own_mono, mono_list_lb_mono, Le. Qed.
 
 (* Alloc *)
 Lemma ghost_history_alloc E :
-  ⊢ |==> ∃ γ, history_gmaster γ 1 E ∗ history_gsnap γ E.
-Proof.
-  iMod (own_alloc (ghost_history_master 1 E)) as (γ) "Hm".
-  - apply mono_list_auth_valid.
-  - iExists γ. by iMod (ghost_history_update with "Hm") as "$".
-Qed.
+  ⊢ |==> ∃ γ, history_gmaster γ 1 E.
+Proof. apply own_alloc, mono_list_auth_valid. Qed.
 
 (* Agreements *)
 Lemma ghost_history_master_agree γ f1 E1 f2 E2  :
@@ -122,14 +114,16 @@ Lemma history_master_update γ E E' :
   history_master γ 1 E' ∗ history_gsnapv γ E'.
 Proof.
   iIntros (SE EC) "[EM %]".
-  by iMod (ghost_history_update with "EM") as "[$ $]".
+  iMod (ghost_history_update with "EM") as "EM"; [exact SE|].
+  iDestruct (ghost_history_master_snap with "EM") as "#$". by iFrame "EM".
 Qed.
 
 Lemma history_master_alloc_empty :
   ⊢ |==> ∃ γ, history_master γ 1 [] ∗ history_gsnapv γ [].
 Proof.
-  iMod (ghost_history_alloc []) as (γ) "[Em Es]".
-  iIntros "!>". iExists γ. iFrame. by iPureIntro.
+  iMod (ghost_history_alloc []) as (γ) "Em".
+  iIntros "!>". iExists γ. iDestruct (ghost_history_master_snap with "Em") as "#$".
+  iFrame. by iPureIntro.
 Qed.
 
 Lemma history_master_wf γg f E :
@@ -145,12 +139,11 @@ Proof.
 Qed.
 
 Lemma history_master_snap γg f E :
-  history_master γg f E ==∗
-  history_master γg f E ∗ history_snap γg E ∅.
+  history_master γg f E ⊢  history_snap γg E ∅.
 Proof.
   iIntros "[E %EGc]".
-  iMod (ghost_history_fork with "E") as "[$ $]"; first by auto.
-  iIntros "!>". iSplit; [done|]. by rewrite -SeenLogview_empty.
+  iDestruct (ghost_history_master_snap with "E") as "$".
+  by rewrite -SeenLogview_empty.
 Qed.
 
 Lemma history_master_snap_included' γg f E E' M V V' :
@@ -161,12 +154,14 @@ Proof.
   by iDestruct (ghost_history_master_snap_included with "E Es") as %?.
 Qed.
 
-Definition history_master_snap_included γg f E E' M
-  := view_at_wand_lr _ _ _ (history_master_snap_included' γg f E E' M).
-Definition history_master_snap_included_2 γg f E E' M
-  := view_at_wand_l _ _ _ (history_master_snap_included' γg f E E' M).
+Lemma history_master_snap_included γg q E E' M :
+  history_master γg q E -∗ history_snap γg E' M -∗ ⌜ E' ⊑ E ⌝.
+Proof. by apply view_at_wand_lr, history_master_snap_included'. Qed.
+Lemma history_master_snap_included_2 γg q E E' M V' :
+  history_master γg q E -∗ @{V'} history_snap γg E' M -∗ ⌜ E' ⊑ E ⌝.
+Proof. by apply view_at_wand_l, history_master_snap_included'. Qed.
 
-Lemma history_snap_mono_marked γg E M E' M'
+Lemma history_snap_mono γg E M E' M'
   (In1: E' ⊑ E) :
   history_snap γg E M -∗ history_snap γg E' M' -∗
   history_snap γg E M'.
@@ -179,6 +174,22 @@ Lemma history_snap_downclosed γg E M M' :
   M' ⊆ M → history_snap γg E M ⊢ history_snap γg E M'.
 Proof. iIntros (SubM') "[$ SL]". by iApply SeenLogview_downclosed. Qed.
 
+Lemma history_snap_union γg E M M' :
+  history_snap γg E M -∗ history_snap γg E M' -∗ history_snap γg E (M ∪ M').
+Proof. iIntros "[$ S1] [E2 S2]". rewrite -SeenLogview_union'. by iFrame. Qed.
+Lemma history_snap_union' γg E M M' :
+  history_snap γg E M ∗ history_snap γg E M' ⊢ history_snap γg E (M ∪ M').
+Proof. iIntros "[S1 S2]". iApply (history_snap_union with "S1 S2"). Qed.
+
+Lemma history_snap_upgrade γg q E' E M :
+  history_master γg q E' -∗ history_snap γg E M -∗ history_snap γg E' M.
+Proof.
+  iIntros "Em Es".
+  iDestruct (history_master_snap_included with "Em Es") as %SubE.
+  iDestruct (history_master_snap with "Em") as "E0".
+  by iApply (history_snap_mono with "E0 Es").
+Qed.
+
 Lemma history_snap_lookup γg E M e dV :
   ge_view <$> E !! e = Some dV → e ∈ M →
   history_snap γg E M -∗ ⊒(dV.(dv_comm)).

theories/examples/stack/proof_mp_client.v → theories/examples/stack/proof_mp_client_graph.v

@@ -99,8 +99,7 @@ Section Stack.
       iDestruct "F" as %(SubG' & SubM' & Sub' & Sub'' & IQ & MAX' &
                         EsG' & SoG' & ComG' & EqM' & _).
       rewrite / is_push in IQ. subst push.
-      iDestruct (own_valid_2 with "nodesA nodes") as %EqL%excl_auth_agree_L.
-      inversion EqL as [EQL].
+      iDestruct (own_valid_2 with "nodesA nodes") as %[= EQL]%excl_auth_agree_L.
 
       iMod (own_update_2 with "nodesA nodes") as "[nodesA nodes]".
       { apply (excl_auth_update _ _ (GSet {[pushId]})). }
@@ -144,13 +143,11 @@ Section Stack.
 
       iIntros (v V' G' pushId popId push1 pop Vpush M') "(SI' & sV' & Local & F)".
       iDestruct "F" as %((SubG' & SubM' & Sub' & Sub'') & CASE).
-      iDestruct (own_valid_2 with "nodes nodes1") as %EqL%excl_auth_agree_L.
-      inversion EqL as [He].
-      have He' := He. apply to_set_singleton in He' as [EqeO EQL]. clear EqL.
+      iDestruct (own_valid_2 with "nodes nodes1") as %[= He]%excl_auth_agree_L.
+      have He' := He. apply to_set_singleton in He' as [EqeO EQL].
 
       iMod (own_update_2 with "nodes nodes1") as "[nodes nodes1]".
       { by apply (excl_auth_update _ _ (GSet (to_set G'.(Es)))). }
-      eapply lookup_weaken in Eqe; last done.
       destruct CASE as [CASE|[Lt0 CASE]].
       + destruct CASE as (-> & -> & Eqde & EsG' & SoG' & ComG' & EqM' & NInM').
         rewrite StackInv_StackConsistent.

theories/examples/stack/proof_mp_client_history.v

+From iris.algebra Require Import excl_auth gset.
+From iris.bi.lib Require Import fractional.
+From iris.proofmode Require Import tactics.
+
+From gpfsl.lang Require Import notation.
+From gpfsl.logic Require Import logatom invariants proofmode.
+
+From gpfsl.examples.stack Require Import spec_history.
+From gpfsl.examples.queue Require Import spec_per_elem.
+From gpfsl.examples Require Import set_helper.
+
+Require Import iris.prelude.options.
+
+Local Notation EMPTY := 0%Z (only parsing).
+
+Definition mpN := nroot .@ "mpN".
+
+Local Notation history := (history sevent).
+
+Implicit Types (E : history) (S : gset event_id).
+
+Section Stack.
+  Context `{!noprolG Σ,
+            !inG Σ (historyR sevent),
+            !inG Σ (excl_authR (gset_disjR event_id))}.
+
+  Local Notation iProp := (iProp Σ).
+  Local Notation vProp := (vProp Σ).
+
+  (** Assuming per-elem Queue spec *)
+  Hypothesis qu : queue_per_elem_spec Σ.
+
+  (** Assuming history-based Stack spec *)
+  Hypothesis stk : a_stack_spec Σ.
+
+  Definition prog  : expr :=
+    let: "s" := stk.(new_stack) [] in
+    let: "q" := qu.(new_queue) [] in 
+    Fork
+      (stk.(push) ["s"; #1 ];;
+       qu.(enqueue) ["q"; #2]);;(* || *)
+                                (* || *)  let: "b" := qu.(dequeue) [ "q" ] in
+                                (* || *)  if: "b" = #2
+                                (* || *)  then stk.(pop) ["s"] else #(-1).
+
+  Lemma Ghost_alloc S :
+    ⊢ |==> ∃ γs, own γs (●E (GSet S)) ∗ own γs (◯E (GSet S)).
+  Proof.
+    setoid_rewrite <- own_op.
+    rewrite -own_alloc; first eauto. by apply excl_auth_valid.
+  Qed.
+
+  (* Stack Invariant *)
+  Definition StackInv1 γs γh γg s: vProp :=
+    ∃ E, stk.(StackInv) γs γh s E ∗ ⎡ own γg (●E (GSet (to_set E)))⎤.
+
+  Local Existing Instances
+    StackInv_Objective StackInv_Timeless StackLocal_Persistent
+    queue_persistent.
+
+  Instance StackInv_obj γs γh γg s : Objective (StackInv1 γs γh γg s) := _.
+
+  Definition QueueInv s γs γh γg (v : Z) : vProp :=
+    ( if decide (v = 2)
+      then ∃ E i e k, ⌜ E !! i = Some e /\ e.(ge_event) = Push 1 /\ i ∈ k⌝ ∗
+                stk.(StackLocal) (mpN .@ "stk") γs γh s E k ∗
+                ⎡ own γg (◯E (GSet {[i]})) ⎤
+      else True)%I.
+
+  Lemma mp_stack_spec tid :
+    {{{ True }}}
+      prog @ tid; ⊤
+    {{{ n, RET #n; ⌜n = 1 ∨ n = -1⌝ }}}.
+  Proof using All.
+    iIntros (Φ) "_ Post".
+    rewrite /prog.
+    wp_apply (new_stack_spec _ (mpN .@ "stk") with "[//]").
+    iIntros (γs γh s) "[#S SI]".
+    iMod (Ghost_alloc ∅) as (γg) "[SA nodes]".
+    wp_let.
+    wp_apply (new_queue_spec _ (QueueInv s γs γh γg) with "[//]").
+    iIntros (q) "#Q".
+    wp_let.
+
+    (* allocate invariants *)
+    iMod (inv_alloc (mpN .@ "inv") _ (StackInv1 γs γh γg s) with "[SI SA]") as "#I".
+    { iModIntro. rewrite / StackInv1. iExists []. iFrame. }
+
+    (*forking *)
+    wp_apply (wp_fork with "[nodes]"); first auto.
+    - (* first thread *)
+      iIntros "!>" (t').
+      iDestruct (monPred_in_intro True%I with "[//]") as (V) "[#InV _]".
+      awp_apply (push_spec with "InV S"); [solve_ndisj|lia|].
+      iInv "I" as (E) "[SI >nodesA]".
+      iAaccIntro with "SI".
+      { iIntros "QI". iModIntro. iFrame "nodes". iNext. iExists E. iFrame. }
+      iIntros (V' E' pushId push Vpush M') "(SI' & sV' & Local & F)".
+      iDestruct "F" as %(? & ? & IP & HpushId & HE' & HM').
+      rewrite /is_push in IP. subst push.
+      iDestruct (own_valid_2 with "nodesA nodes") as %[= EQL]%excl_auth_agree_L.
+      iMod (own_update_2 with "nodesA nodes") as "[nodesA nodes]".
+      { apply (excl_auth_update _ _ (GSet {[pushId]})). }
+      iIntros "!>".
+      iSplitL "SI' nodesA".
+      { iNext. iExists E'. rewrite HE' to_set_append -HpushId EQL right_id_L.
+        iFrame. }
+      iIntros "_". wp_seq.
+      wp_apply (enqueue_spec _ _ _ 2 _ (λ _, True%I) with "[-$Q]"); [|auto].
+      iExists E', pushId, (mkGraphEvent (Push 1) Vpush M'), M'.
+      iFrame. iDestruct (view_at_elim with "sV' Local") as "$".
+      iPureIntro. subst; simpl; split_and!; [by rewrite lookup_app_1_eq|done|set_solver].
+
+    - (* second thread *)
+      iIntros "_".
+      wp_seq.
+      wp_apply (dequeue_spec with "Q").
+      iIntros (v) "R".
+      wp_let. wp_op. rewrite bool_decide_decide.
+      case decide => ?.
+      { subst. wp_if. iApply "Post". iPureIntro; auto. }
+      rewrite {2} /QueueInv.
+      case decide => ?; wp_if; last first.
+      { iApply "Post". auto. }
+
+      subst; simpl.
+      iApply (wp_step_fupd _ _ _ _ (∀ _, _ -∗ _)%I with "[$Post]"); [auto..|].
+
+      iDestruct "R" as (E2 e eV M) "(F & #Q2 & nodes1)".
+      iDestruct "F" as %(Eqe & Eqve & Inm).
+      iDestruct (monPred_in_intro True%I with "[//]") as (V) "[#InV _]".
+      awp_apply (pop_spec with "InV Q2"); [solve_ndisj|].
+      iInv "I" as (E) ">[SI nodes]".
+      iDestruct (StackLocal_history_snap with "Q2") as "Es".
+      iDestruct (StackInv_history_snap with "SI Es") as %SubE2.
+      iDestruct (StackInv_history_master_acc with "SI") as "[Em SI]".
+      iDestruct (history_master_wf with "Em") as %EWF.
+      iSpecialize ("SI" with "[$Em]").
+      iAaccIntro with "SI".
+      { iIntros "SI !>". iFrame. iNext. rewrite /StackInv1. iExists E. iFrame. }
+
+      iIntros (v V' E' pushId popId push1 pop Vpush M') "(SI' & sV' & Local & F)".
+      iDestruct "F" as %((? & ?) & CASE).
+      iDestruct (own_valid_2 with "nodes nodes1") as %[= He]%excl_auth_agree_L.
+      apply to_set_singleton in He as [-> EQL].
+      assert (E = [eV]) as ->; last clear EQL.
+      { eapply prefix_lookup in Eqe; [|done]. destruct E; [done|].
+        clear -Eqe EQL. simplify_list_eq. by apply nil_length_inv in EQL as ->. }
+      iDestruct (StackInv_StackLinearizability with "SI'") as "#>%LIN".
+
+      iMod (own_update_2 with "nodes nodes1") as "[nodes nodes1]".
+      { by apply (excl_auth_update _ _ (GSet (to_set E'))). }
+      destruct CASE as [CASE|[Lt0 CASE]].
+      + exfalso.
+        destruct CASE as (-> & -> & Eqde & HE' & HM').
+        destruct LIN as [? lin ? ? ? _ _ ? _ ?].
+        rewrite HE' app_length /= in XO.
+        assert (lin = (([] ++ [0]) ++ [1]) ∨ lin = [1; 0])%nat as [->| ->].
+        { simpl. apply Permutation_length_2_inv. by subst xo. }
+        * apply stack_interp_snoc_inv in INTERP_LIN as (? & ? & INTERP1 & ? & RUN1).
+          apply stack_interp_snoc_inv in INTERP1 as (? & ? & INTERP0 & ? & RUN0).
+          apply stack_interp_nil_inv in INTERP0 as ->.
+          simplify_list_eq.
+          inversion RUN0; [|congruence].
+          inversion RUN1; simplify_list_eq.
+        * suff ? : (1 <= 0)%nat by lia.
+          subst E'. eapply (HB_LIN 1 0 0 1)%nat; [done..|].
+          simpl. set_solver +HM' Inm.
+      + destruct CASE as (IE & ID & ? & ? & ? & ? & ? & ? & ?).
+        rewrite /is_push in IE. rewrite /is_pop in ID. subst push1 pop.
+        simplify_list_eq. rewrite Eqve in IE. injection IE as <-.
+        iIntros "!>". iSplitL.
+        { iNext. iExists _. by iFrame. }
+        iIntros "_ H". iApply "H"; auto.
+Qed.
+End Stack.

theories/examples/stack/proof_treiber_history.v

@@ -1449,6 +1449,14 @@ Proof.
   intros. iDestruct 1 as (??????????) "[$ ?]". iIntros "$". eauto 11 with iFrame.
 Qed.
 
+Lemma StackInv_history_snap_instance :
+  ∀ γs γg s E E' M',
+    StackInv γs γg s E -∗ history_snap γg E' M' -∗ ⌜ E' ⊑ E ⌝.
+Proof.
+  intros. iDestruct 1 as (??????????) "[E ?]". iIntros "E'".
+  by iDestruct (history_master_snap_included with "E E'") as %?.
+Qed.
+
 Lemma StackLocal_history_snap_instance :
   ∀ N γs γg s E M, StackLocal N γs γg s E M ⊢ history_snap γg E M.
 Proof. intros. iDestruct 1 as (??????) "[$ _]". Qed.
@@ -1535,7 +1543,7 @@ Proof.
     "(E●1 & M●1 & (%Vb1 & at↦1) & StackNodes1 & AllLinks1 & #SeenMsgsAll1 & %Props1)".
   simplify_encode.
   (* get snapshot of E1 *)
-  iMod (history_master_snap with "E●1") as "[E●1 #E◯1]".
+  iDestruct (history_master_snap with "E●1") as "#E◯1".
   iDestruct (history_master_snap_included with "E●1 E◯0") as %SubE01.
   iDestruct (emo_auth_lb_valid with "M●1 M◯0") as %(Subesi01 & Subne01 & Subess01).
   (* read *)
@@ -1613,7 +1621,7 @@ Proof.
   iDestruct "CASE" as "[[F ⊒Vr2]|[F sVw2]]".
   { (* fail CAS *)
     iDestruct "F" as %(-> & NEq & ->).
-    iMod (history_master_snap with "E●2") as "[E●2 #E◯2]".
+    iDestruct (history_master_snap with "E●2") as "#E◯2".
     iDestruct (emo_lb_own_get with "M●2") as "#M◯2".
 
     have bLeVV : bool_decide (V ⊑ V) by eapply bool_decide_unpack; eauto.
@@ -1899,7 +1907,7 @@ Proof.
     "(E●1 & M●1 & (%Vb1 & at↦1) & StackNodes1 & AllLinks1 & #SeenMsgsAll1 & %Props1)".
   simplify_encode.
   (* get snapshot of E1 *)
-  iMod (history_master_snap with "E●1") as "[E●1 #E◯1]".
+  iDestruct (history_master_snap with "E●1") as "#E◯1".
   (* initial snapshot is included in E1 *)
   iPoseProof "E◯0" as "E◯0'".
   iDestruct "E◯0'" as "[_ PSV]".
@@ -2268,7 +2276,7 @@ Proof.
     (* COMMIT with no change *)
     subst b2 ζn2.
     (* take a snapshot *)
-    iMod (history_master_snap with "E●2") as "[E●2 #E◯2]".
+    iDestruct (history_master_snap with "E●2") as "#E◯2".
     iDestruct (emo_lb_own_get with "M●2") as "#M◯2".
 
     set Vpp := mkDView V V2 V2 bLeVV2.
@@ -2589,6 +2597,8 @@ Program Definition treiber_stack_impl `{!noprolG Σ, !tstackG Σ, !atomicG Σ}
     spec_history.StackInv_Objective := StackInv_objective ;
     spec_history.StackInv_StackLinearizability := StackInv_StackLinearizability_instance ;
     spec_history.StackInv_history_master_acc := StackInv_history_master_acc_instance ;
+    spec_history.StackInv_history_snap := StackInv_history_snap_instance ;
+
     spec_history.StackLocal_history_snap := StackLocal_history_snap_instance ;
     spec_history.StackLocal_Persistent := StackLocal_persistent ;
     spec_history.new_stack_spec := new_stack_spec;

theories/examples/stack/spec_history.v

@@ -211,10 +211,14 @@ Record stack_spec {Σ} `{!noprolG Σ, !inG Σ (historyR sevent)} := StackSpec {
   StackInv_history_master_acc :
     ∀ γs γg s E, StackInv γs γg s E ⊢ history_master γg 1 E ∗
                                       (history_master γg 1 E -∗ StackInv γs γg s E);
-  StackLocal_history_snap :
-    ∀ N γs γg s E M, StackLocal N γs γg s E M ⊢ history_snap γg E M;
+  StackInv_history_snap :
+    ∀ γs γg s E E' M',
+      StackInv γs γg s E -∗ history_snap γg E' M' -∗ ⌜ E' ⊑ E ⌝;
+
   StackLocal_Persistent :
     ∀ N γs γg s E M, Persistent (StackLocal N γs γg s E M);
+  StackLocal_history_snap :
+    ∀ N γs γg s E M, StackLocal N γs γg s E M ⊢ history_snap γg E M;
 
   (* operations specs *)
   new_stack_spec : new_stack_spec' new_stack StackLocal StackInv;