Sketch of graph lin proofs

_CoqProject

@@ -134,6 +134,8 @@ theories/examples/stack/code_elimination.v
 theories/examples/stack/proof_na.v
 theories/examples/stack/proof_treiber_gps.v
 theories/examples/stack/proof_treiber_graph.v
+theories/examples/stack/proof_graph_lin.v
+theories/examples/stack/proof_elim_lin.v
 ## Queue
 theories/examples/queue/code_ms.v
 theories/examples/queue/code_hw.v
@@ -146,6 +148,7 @@ theories/examples/queue/proof_per_elem_graph.v
 theories/examples/queue/proof_mp_graph.v
 theories/examples/queue/proof_mp_lin.v
 theories/examples/queue/proof_exchange_lin.v
+theories/examples/queue/proof_graph_lin.v
 ## Chase-Lev Double-ended Queue
 theories/examples/chase_lev/code.v
 ## Exchanger

theories/examples/stack/proof_graph_lin.v

+Require Import stdpp.namespaces.
+
+From iris.algebra Require Import auth frac_auth gset gmap.
+From iris.bi Require Import lib.atomic weakestpre lib.fractional.
+From iris.proofmode Require Import tactics.
+
+From gpfsl.lang Require Import notation.
+From gpfsl.base_logic Require Import vprop.
+From gpfsl.logic Require Import logatom invariants proofmode.
+
+From gpfsl.examples.graph Require Import graph.
+From gpfsl.examples.linearizability Require Import spec events_ghost event_list_helper.
+From gpfsl.examples.stack Require Import spec_lin spec_graph.
+
+Set Default Proof Using "Type*".
+Set Suggest Proof Using.
+
+Definition graph_stack_nameR := agreeR (prodO (prodO gnameO gnameO) gnameO).
+(* TODO: rename treiber → graph? *)
+Class tstackG Σ := TreiberStackG {
+  tstack_hist_inG :> historyG Σ event_id TryStackInput TryStackOutput;
+  graph_stack_name_inG :> inG Σ graph_stack_nameR;
+}.
+
+Definition tstackΣ : gFunctors :=
+  #[historyΣ event_id TryStackInput TryStackOutput; GFunctor (constRF (graph_stack_nameR))].
+
+Instance subG_tstackΣ {Σ} : subG tstackΣ Σ → tstackG Σ.
+Proof. solve_inG. Qed.
+
+Definition stack_linN := nroot .@ "stack_linN".
+
+Notation graph_stack_event := (graph_event sevent).
+Notation graph_stack_event_map := (event.event_map sevent).
+Notation try_stack_event_map := (try_stack_event_map event_id).
+Notation try_stack_event_set := (gset event_id).
+Notation try_stack_event_order := (event_order event_id).
+
+Section graph_to_hist.
+Context `{!noprolG Σ, !tstackG Σ, !inG Σ (eventGraphR sevent)} (P : Z → vProp Σ).
+#[local] Notation vProp := (vProp Σ).
+
+Variable Eo : coPset.
+Hypothesis SubN : ↑stack_linN ⊆ Eo.
+Hypothesis S : a_stack_spec Σ Eo.
+
+Implicit Types (emap emapM : graph_stack_event_map)
+               (events eventsM : try_stack_event_map)
+               (owned ownedM : try_stack_event_set)
+               (orders ordersM : try_stack_event_order)
+               (eids : list event_id) (hs : list try_stack_event).
+
+(* TODO: graph stack → lin stack
+`-op>` with
++ MO (CAS order)
++ lview inclusion?
+
+VIEW: `X -op> Y ⇒ ¬ (Y -v> X)`.
+- E1 -op> E2: Suppose E2.Vo ⊑ E1.Vi.
+  * E2.Vi ⊑ E2.Vo ⊑ E1.Vi ⊑ E1.Vo ⊑ E1.Vw
+    ⇒ E2.Vo ⊑ E1.Vo. But E2.Vo should have at least seen the write msg of E1
+  * release sequence                E1.Vw ⊑ E2.Vw
+  - if we have E1 ∈ E2.ge_lview → E1.Vo ⊑ E2.Vo → E1.Vo = E2.Vo
+  - if strong stack:
+    - E2.Vi ⊑ E2.Vo ⊑ E1.Vi ⊑ E1.Vo → E2.Vo = E1.Vo
+  * dview_push_order contradicts E2.Vo ⊑ E1.Vo ✓
+
+- E1 -op> D2: Suppose D2.Vo ⊑ E1.Vi
+  * D2.Vi ⊑ D2.Vo ⊑ E1.Vi ⊑ E1.Vo ⊑ E1.Vw
+- D1 -op> E2:
+- D1 -op> D2:
+  - need dview_pop_order → maybe strong stack
+
+NOTE
+X1 -op> X2:
+Suppose X2.Vo ⊑ X1.Vi. Then X2.Vo ⊑ X1.Vi ⊑ X1.Vo
+⇒ X2.Vo ⊑ X1.Vo. But X2.Vo should have at least seen the write msg of X1!
+This holds for any single-loc CAS.
+So we can have `e1 < e2 → ¬ (e2.dv_comm ⊑ e1.dv_comm)`.
+(TODO: name for this?)
+Does this hold for any other DS?
+
+
+release sequence: Vr ⊑ Vw
+
+dataView to Vi Vo
+- push: dv_comm ⊑ dv_wrt
+- pop: dv_wrt ⊑ dv_comm
+- (e, d): e.dv_wrt ⊑ d.dv_wrt
+  ⇒ e.dv_comm ⊑ e.dv_wrt ⊑ d.dv_wrt ⊑ d.dv_comm
+  ⇒ e.Vi ⊑ e.Vo ⊑ d.Vo
+- dview_push_order: e1 < e2 ⇒ ¬ (e2.dv_comm ⊑ e1.dv_comm)
+
+logView
+- @{Vpush.(dv_comm)} SeenLogview E' M'
+  ⇒ ∀ e ∈ M', e.(ev_comm) ⊑ Vpush.(dv_comm)
+- e1 ∈ e2.ge_lview → e1 ≤ e2
+  - e1 > e2 → e1 ¬∈ e2.ge_lview
+- LIFO:  u1 -hb> u2 ∧ o1 -hb> o2 →
+
+- cas order & most relaxed/current spec → view_linearizable doesn't hold
+- Other order? Existence of view_linearizable order?
+- Why head read acq in push? Why acq CAS pop?
+  Does it add synchronization? Let's assume it's relaxed
+- Do something similar to hwqueue ordering? i.e. fix pop order and build push order
+  Add minimal synchronization for pop ordering
+- how to use logView?
+
+*)
+Inductive try_stack_event_equiv : ∀ (ge : graph_stack_event) (he : try_stack_event), Prop :=
+  | try_stack_event_equiv_try_push ge he v
+      (GE_EVENT : ge.(ge_event) = Push v)
+      (HE_INPUT : he.(he_input) = TryStackInput_Push v)
+      (IN_VIEW : he.(he_Vi) = ge.(ge_view).(dv_in))
+      (OUT_VIEW : he.(he_Vo) = ge.(ge_view).(dv_comm))
+      : try_stack_event_equiv ge he
+    .
+
+Definition try_stack_event_map_equiv emap events :=
+  ∀ eid, match (emap !! eid, events !! eid) with
+         | (Some ge, Some he) => try_stack_event_equiv ge he
+         | (None, None) => True
+         | _ => False
+         end.
+
+Definition TStackHandle v γ N f events owned orders : vProp :=
+  ∃ (γs γg γh : gname) (l : loc),
+    (⌜v = #l⌝ ∗ ⎡own γ (to_agree (γs, γg, γh))⎤) ∗
+    inv N (∃ GM emapM eventsM ordersM eids hs stack,
+      S.(StackInv) γg GM emapM ∗
+      AuthEvents γ eventsM ordersM ∗
+      try_stack_resources P stack ∗
+      ⌜ event_list eventsM eids hs ∧
+        eids_complete eventsM eids ∧
+        linearization ordersM eids ∧
+        try_stack_history hs stack ∧
+        try_stack_event_map_equiv emapM eventsM ⌝) ∗
+    ∃ G emap M,
+      S.(StackLocal) γs γg l G emap M ∗
+      FragEvents γ f events owned orders ∗
+      SeenEvents events ∗
+      ⌜ orders_consistent events orders ⌝.
+
+Lemma TStackHandle_info v γ N events owned orders E (MASK : ↑N ⊆ E):
+  TStackHandle v γ N 1 events owned orders
+  ={E}=∗ ⌜∃ eids hs stack,
+            event_list events eids hs ∧
+            eids_complete events eids ∧
+            linearization orders eids ∧
+            try_stack_history hs stack⌝.
+Proof. Admitted.
+
+Lemma TStackHandle_split q γ N f1 f2 events owned1 owned2 orders (DISJ : owned1 ## owned2) :
+  TStackHandle q γ N (f1 + f2) events (owned1 ∪ owned2) orders
+  -∗ TStackHandle q γ N f1 events owned1 orders ∗
+     TStackHandle q γ N f2 events owned2 orders.
+Proof. Admitted.
+
+Lemma TStackHandle_join q γ N f1 f2 events1 events2 owned1 owned2 orders1 orders2 :
+  TStackHandle q γ N f1 events1 owned1 orders1 -∗ TStackHandle q γ N f2 events2 owned2 orders2
+  -∗ TStackHandle q γ N (f1 + f2) (events1 ∪ events2) (owned1 ∪ owned2) (orders1 ∪ orders2) ∗
+     ⌜owned1 ## owned2⌝.
+Proof. Admitted.
+
+Lemma TStackHandle_seen_events q γ N f events owned orders :
+  TStackHandle q γ N f events owned orders ⊢ SeenEvents events.
+Proof.
+  iDestruct 1 as (????) "(_ & _ & Q)".
+  iDestruct "Q" as (???) "(_ & _ & $ & _)".
+Qed.
+
+Lemma TStackHandle_orders q γ N f events owned orders :
+  TStackHandle q γ N f events owned orders ⊢ ⌜ orders_consistent events orders ⌝.
+Proof.
+  iDestruct 1 as (????) "(_ & _ & Q)".
+  iDestruct "Q" as (???) "(_ & _ & _ & $)".
+Qed.
+
+Definition TStackCode (obj : val) input : expr :=
+  match input with
+  | TryStackInput_Push v => S.(try_push) [ obj; #v]%E
+  | TryStackInput_Pop => S.(try_pop) [ obj]%E
+  end.
+
+Lemma tstack_new_spec N tid :
+  {{{ True }}}
+      S.(new_stack) [] in tid
+  {{{ γ s, RET s; TStackHandle s γ N 1 ∅ ∅ ∅ }}}.
+Proof.
+  iIntros (Φ) "_ Post".
+  iApply (S.(new_stack_spec) with "[//]").
+  iIntros "!>" (???) "[Local Inv]".
+  iApply "Post".
+  unfold TStackHandle.
+Admitted.
+
+Lemma tstack_try_push_spec s γ N f events owned orders tid v V :
+  lin_spec_operation_specT
+    event_id TryStackInput TryStackOutput
+    TStackHandle
+    (TryStackInputResource P) (TryStackOutputResource P)
+    s γ N f events owned orders tid V
+    TStackCode
+    (TryStackInput_Push v).
+Proof.
+  iIntros (Φ) "(Handle & (>%NZ & Input) & #V) Post".
+  iDestruct "Handle" as (????) "([-> Names] & #Inv & Local)".
+  iDestruct "Local" as (G1 emap1 M) "(Local & Hist)".
+  iApply (wp_step_fupd with "[Post]"); [done..|iIntros "!>!>!>"; iAccu|]. simpl.
+  iDestruct (view_at_intro_incl True%I V with "[//] [$V]") as (Vi) "(Vi & % & _)".
+  iApply (S.(try_push_spec) _ _ _ _ G1 emap1 M with "Vi Local"); [done|].
+  iAuIntro.
+  iInv "Inv" as (G emap ?????) "(INV & >HistM & Res & >F)".
+  admit.
+  iDestruct "F" as %(EQUIV & EVENTS & LINEAR & INTERP).
+  iAssert (⌜eventgraph_consistent G emap⌝)%I with "[INV]" as "%EGCONS".
+  { admit. }
+
+  iAaccIntro with "INV". admit.
+  { iIntros "INV". iFrame "Names Hist Input". iExists _,_,_,_,_,_,_. by iFrame. }
+
+  Local Opaque graph_snap.
+  simpl. iIntros (b Vo G' emap' enqId enq Venq M') "(INV & sVo & Local & [F|F])".
+Admitted.
+
+Lemma tstack_try_pop_spec s γ N f events owned orders tid Vi :
+  lin_spec_operation_specT
+    event_id TryStackInput TryStackOutput
+    TStackHandle
+    (TryStackInputResource P) (TryStackOutputResource P)
+    s γ N f events owned orders tid Vi
+    TStackCode
+    TryStackInput_Pop.
+Proof. Admitted.
+
+Definition tstack_impl_try_stack_spec : try_stack_spec P := {|
+  try_stack_Eid := event_id;
+  try_stack_new := S.(new_stack);
+  try_stack_try_push := S.(try_push);
+  try_stack_try_pop := S.(try_pop);
+  try_stack_handle := TStackHandle;
+  try_stack_handle_info := TStackHandle_info;
+  try_stack_handle_split := TStackHandle_split;
+  try_stack_handle_join := TStackHandle_join;
+  try_stack_handle_seen_events := TStackHandle_seen_events;
+  try_stack_handle_orders := TStackHandle_orders;
+  try_stack_new_spec := tstack_new_spec;
+  try_stack_try_push_spec := tstack_try_push_spec;
+  try_stack_try_pop_spec := tstack_try_pop_spec;
+|}.
+
+Definition tstack_linearizable : linearizability_spec :=
+  try_stack_linearizable tstack_impl_try_stack_spec.
+End graph_to_hist.