Commit 23ad44c1 authored by Hai Dang's avatar Hai Dang
Browse files

Rename StackConsistent and make elim stack only depend on simple stack consistency

parent 6d4e6438
This diff is collapsed.
......@@ -14,4 +14,5 @@ Definition elimination_stack_impl_closed
`{!noprolG Σ, !tstackG Σ, !xchgG Σ, !atomicG Σ,
!ro_ptstoG Σ, !inG Σ (mono_listR (leibnizO (event_id + event_id)))}
: basic_stack_spec Σ
:= elimination_stack_impl Σ (treiber_stack_impl Σ) (exchanger_impl Σ).
:= elimination_stack_impl Σ (extended_to_basic_stack_spec Σ (treiber_stack_impl Σ))
(exchanger_impl Σ).
......@@ -31,7 +31,7 @@ Section Stack.
Hypothesis qu : queue_per_elem_spec Σ.
(** Assuming graph-based Stack spec *)
Hypothesis stk : a_stack_spec Σ.
Hypothesis stk : basic_stack_spec Σ.
Definition prog : expr :=
let: "s" := stk.(new_stack) [] in
......@@ -158,10 +158,10 @@ Section Stack.
+ destruct CASE as (-> & -> & Eqde & EsG' & SoG' & ComG' & EqM' & NInM').
rewrite StackInv_StackConsistent.
iDestruct "SI'" as ">%SC". exfalso.
destruct SC as [_ _ _ [_ Hcom _ _ HNE HSoCom _ _] _].
destruct SC as [_ Hcom _ _ HNE HSoCom _ _].
have Eqd : G'.(Es) !! popId = Some (mkGraphEvent EmpPop Vpush M').
{ rewrite Eqde. rewrite EsG'. rewrite lookup_app_1_eq. auto. }
have Ine' : e M'. { set_solver. }
have Ine' : e M'. { set_solver+SubM' Inm. }
have SubG2' : G2 G' by etrans.
assert (EqeV := prefix_lookup _ _ _ _ Eqe (graph_sqsubseteq_E _ _ SubG2')).
......
......@@ -331,7 +331,7 @@ Definition StackBaseInv γ γh s G T : vProp :=
This carries some properties of T so that they are available without the
internal invariant StackInternalInv *)
Definition StackInv' γg s q G γ T : vProp :=
StackConsistent G graph_master γg (q/2) G
ExtendedStackConsistent G graph_master γg (q/2) G
(γh : gname), EM_equiv T G.(Es) gmap_inj T
meta s nroot (γ,γh)
(* LTM_master connects the logical enqueues and the event graph *)
......@@ -524,7 +524,7 @@ Qed.
Lemma StackInv'_snapshot {γg s q G γ T} :
StackInv' γg s q G γ T -
StackConsistent G eventgraph_consistent G
ExtendedStackConsistent G eventgraph_consistent G
LTM_snapv γ T graph_snap γg G .
Proof.
iDestruct 1 as (SC) "(G & %γh & F & MT & LT)".
......@@ -579,7 +579,7 @@ Qed.
Proof. constructor; [done|apply _]. Qed.
Lemma StackInv'_update γg s G γ T G' T' :
eventgraph_consistent G' StackConsistent G'
eventgraph_consistent G' ExtendedStackConsistent G'
G G' T T' EM_equiv T' G'.(Es) gmap_inj T'
StackInv' γg s 1%Qp G γ T - StackInv' γg s 1%Qp G γ T ==
StackInv' γg s 1%Qp G' γ T' StackInv' γg s 1%Qp G' γ T'.
......@@ -764,8 +764,8 @@ Local Existing Instances tstk_graphG tstk_stackG.
#[local] Notation iProp := (iProp Σ).
#[local] Notation vProp := (vProp Σ).
Lemma StackInv_StackConsistent_instance :
γg s q G, StackInv γg s q G StackConsistent G .
Lemma StackInv_ExtendedStackConsistent_instance :
γg s q G, StackInv γg s q G ExtendedStackConsistent G .
Proof. intros. by iDestruct 1 as (???) "?". Qed.
Lemma StackInv_graph_master_acc_instance :
......@@ -890,7 +890,7 @@ Proof.
iDestruct (LTM_master_fork with "LTm1") as "#LTs".
iMod graph_master_alloc_empty as (γg) "([GM1 GM2] & Gs)".
have SC0 := StackConsistent_empty.
have SC0 := ExtendedStackConsistent_empty.
rewrite shift_0.
iMod (meta_set _ _ (γ, γh) nroot with "Hms") as "#Hms"; [done|].
......@@ -1149,7 +1149,7 @@ Proof.
destruct (stk_em _ _ _ SP2 psId) as [[v' Eqv] _]. { by exists n'. }
move : Eqv => /list_lookup_fmap_inv' [? [?]]. intros ?%lookup_lt_Some. lia. }
have SC' : StackConsistent G'.
have SC' : ExtendedStackConsistent G'.
{ have NI : e1 e2, (e1, e2) G'.(com) e1 psId e2 psId.
{ move => ?? /(gcons_com_included G2) [/= ??]. lia. }
destruct SC2 as [SC2DPP SC2DPPO SC2DPO
......@@ -1539,7 +1539,7 @@ Proof.
set E' := G'.(Es).
have LeE0' : E0 E' by apply LeG0'.
have SC' : StackConsistent G'.
have SC' : ExtendedStackConsistent G'.
{ have NI : e1 e2, (e1, e2) G'.(com) e1 ppId e2 ppId.
{ move => ?? /(gcons_com_included G1) [/= ??]. lia. }
destruct SC1 as [SC1PS SC1PSO SC1PP
......@@ -1655,7 +1655,7 @@ Proof.
iSplit; [..|by iPureIntro|].
iPureIntro. right; left. do 8 (split; [done|]).
intros e UM Ine.
eapply (bstk_cons_non_empty _ (stk_cons_basic _ SC') ppId);
eapply (stk_cons_non_empty _ (exstk_cons_basic _ SC') ppId);
[by rewrite lookup_app_1_eq|done| |done].
clear -Ine. rewrite /= elem_of_union. right. exact Ine. }
......@@ -1870,7 +1870,7 @@ Proof.
assert (EqG' := graph_insert_edge_eq psId egV' G2 Lted).
rewrite -/G' in EqG'. destruct EqG' as (_ & EqEs' & EqSo' & EqCo').
have SC' : StackConsistent G'.
have SC' : ExtendedStackConsistent G'.
{ have NI : e1 e2, (e1, e2) G2.(com) e1 ppId e2 ppId.
{ move => ?? /(gcons_com_included G2) [/= ??]. lia. }
constructor; [| | |constructor|..]; [| | | | |split|..].
......@@ -2150,10 +2150,10 @@ Qed.
End proof.
Definition treiber_stack_impl Σ
`{!noprolG Σ, !tstackG Σ, !atomicG Σ} : a_stack_spec Σ := {|
`{!noprolG Σ, !tstackG Σ, !atomicG Σ} : extended_stack_spec Σ := {|
spec_graph.StackInv_Objective := StackInv_objective ;
spec_graph.StackInv_Fractional := StackInv_fractional ;
spec_graph.StackInv_StackConsistent := StackInv_StackConsistent_instance ;
spec_graph.StackInv_StackConsistent := StackInv_ExtendedStackConsistent_instance ;
spec_graph.StackInv_graph_master_acc := StackInv_graph_master_acc_instance ;
spec_graph.StackInv_graph_snap := StackInv_graph_snap_instance ;
spec_graph.StackInv_agree := StackInv_agree_instance ;
......
......@@ -337,55 +337,55 @@ Definition stack_LIFO_empty G : Prop :=
[try_push] and [try_pop] operations, but not [push] and [pop] operations.
The consistency condition of the Weak Stack Spec also does NOT include the
condition (5) below for empty pops. We do NOT encode the Weak Stack Spec here. *)
Record BasicStackConsistent G : Prop := mkBasicStackConsistent {
Record StackConsistent G : Prop := mkStackConsistent {
(* The first one is our side condition *)
bstk_cons_ps_non_zero : (* 0 is used for Empty Pop *) stack_positive_value G ;
stk_cons_ps_non_zero : (* 0 is used for Empty Pop *) stack_positive_value G ;
(* (1) at most 1 Constructor event: we currently don't have initialization events *)
bstk_cons_matches :
stk_cons_matches :
(* (2) There can only be so edges between matching Pushs and Pops *)
stack_matches_value G ;
bstk_cons_com_functional :
stk_cons_com_functional :
(* (3) com and com^-1 are functional: *)
functional_pair G.(com) ;
bstk_cons_empty_pop :
stk_cons_empty_pop :
(* (4) every unmatched pop returns empty: *)
stack_unmatched_pop_empty G ;
bstk_cons_non_empty :
stk_cons_non_empty :
(* (5) a pop with a previous unmatched push cannot return empty.
So our Pop result depends on whether our current view includes an unmatched Push *)
stack_empty_unmatched_push G ;
bstk_cons_so_com :
stk_cons_so_com :
(* (6) so and com agree *)
G.(so) = G.(com) ;
bstk_cons_LIFO :
stk_cons_LIFO :
(* (7) pushed values cannot be popped out of order *)
stack_LIFO G ;
(* The last one prevents circles in eco : eco ⊆ xo *)
bstk_cons_mo_hb : graph_xo_eco G ;
stk_cons_mo_hb : graph_xo_eco G ;
}.
(** Our Stack Consistency adds more physical/logical order information. *)
Record StackConsistent G : Prop := mkStackConsistent {
stk_cons_dview_push : (* push is releasing *) stack_push_releasing G ;
stk_cons_dview_push_order : (* pushes are ordered by CAS *) stack_push_CAS_order G ;
stk_cons_dview_pop : (* pop is acquiring *) stack_pop_acquiring G ;
(** ExtendedStackConsistency adds more physical/logical order information. *)
Record ExtendedStackConsistent G : Prop := mkExtendedStackConsistent {
exstk_cons_dview_push : (* push is releasing *) stack_push_releasing G ;
exstk_cons_dview_push_order : (* pushes are ordered by CAS *) stack_push_CAS_order G ;
exstk_cons_dview_pop : (* pop is acquiring *) stack_pop_acquiring G ;
(* (1)-(7) Stack spec from POPL'19 Library Correctness paper *)
stk_cons_basic : BasicStackConsistent G ;
exstk_cons_basic : StackConsistent G ;
(* The last one is our strengthening that holds for stronger implementation. *)
stk_cons_LIFO_b :
exstk_cons_LIFO_b :
stack_LIFO_empty G ;
}.
Definition basic_stack_spec Σ `{!noprolG Σ, !inG Σ (graphR sevent)}
:= stack_spec Σ BasicStackConsistent.
Definition a_stack_spec Σ `{!noprolG Σ, !inG Σ (graphR sevent)}
:= stack_spec Σ StackConsistent.
Definition extended_stack_spec Σ `{!noprolG Σ, !inG Σ (graphR sevent)}
:= stack_spec Σ ExtendedStackConsistent.
(** Some properties *)
Lemma unmatched_push_mono G G' eid :
G G' is_Some (G.(Es) !! eid) unmatched_push G' eid unmatched_push G eid.
......@@ -398,8 +398,46 @@ Proof.
- intros e' ?. apply (FA e'); by apply LeG'.
Qed.
Lemma BasicStackConsistent_empty : BasicStackConsistent .
Lemma StackConsistent_empty : StackConsistent .
Proof. done. Qed.
Lemma StackConsistent_empty : StackConsistent .
Lemma ExtendedStackConsistent_empty : ExtendedStackConsistent .
Proof. done. Qed.
Program Definition extended_to_basic_stack_spec
Σ `{!noprolG Σ, !inG Σ (graphR sevent)}
(stk : extended_stack_spec Σ) : basic_stack_spec Σ := {|
StackInv_Objective := stk.(StackInv_Objective) ;
StackInv_Timeless := stk.(StackInv_Timeless) ;
StackInv_Fractional := stk.(StackInv_Fractional) ;
StackInv_AsFractional := stk.(StackInv_AsFractional) ;
(* StackInv_StackConsistent := ∀ γg s q G, StackInv γg s q G ⊢ ⌜ StackConsistent G ⌝ ; *)
StackInv_graph_master_acc := stk.(StackInv_graph_master_acc) ;
StackInv_graph_snap := stk.(StackInv_graph_snap) ;
StackInv_agree := stk.(StackInv_agree) ;
StackLocal_Persistent := stk.(StackLocal_Persistent) ;
StackLocal_graph_snap := stk.(StackLocal_graph_snap) ;
StackLocal_union := stk.(StackLocal_union) ;
StackLocal_upgrade := stk.(StackLocal_upgrade) ;
(* StackLocalLite is the light version of StackLocal that is Timeless *)
StackLocalLite_Timeless := stk.(StackLocalLite_Timeless) ;
StackLocalLite_Persistent := stk.(StackLocalLite_Persistent) ;
StackLocalLite_from := stk.(StackLocalLite_from) ;
StackLocalLite_to := stk.(StackLocalLite_to) ;
StackLocalLite_graph_snap := stk.(StackLocalLite_graph_snap) ;
StackLocalLite_upgrade := stk.(StackLocalLite_upgrade) ;
(* operations specs *)
new_stack_spec := stk.(new_stack_spec) ;
try_push_spec := stk.(try_push_spec) ;
push_spec := stk.(push_spec) ;
try_pop_spec := stk.(try_pop_spec) ;
pop_spec := stk.(pop_spec) ;
|}.
Next Obligation.
iIntros "* SI".
by iDestruct (StackInv_StackConsistent with "SI") as%?%exstk_cons_basic.
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