Commit d87ccf7a authored by Hai Dang's avatar Hai Dang
Browse files

Closed elimination stack proof

parent ee8a34f6
......@@ -116,6 +116,7 @@ theories/examples/graph/spec.v
theories/examples/linearizability/spec.v
theories/examples/linearizability/events_ghost.v
theories/examples/linearizability/event_list_helper.v
## Message-Passing
theories/examples/mp/code.v
theories/examples/mp/spec.v
......@@ -142,6 +143,7 @@ theories/examples/stack/proof_treiber_gps.v
theories/examples/stack/proof_treiber_graph.v
theories/examples/stack/proof_mp_client.v
theories/examples/stack/proof_elim_graph.v
theories/examples/stack/proof_elim_graph_closed.v
## Queue
theories/examples/queue/spec_per_elem.v
theories/examples/queue/code_ms.v
......@@ -160,11 +162,11 @@ theories/examples/chase_lev/code.v
## Exchanger
theories/examples/exchanger/code.v
theories/examples/exchanger/spec_graph.v
theories/examples/exchanger/spec_graph_piggyback.v
theories/examples/exchanger/spec_lin.v
theories/examples/exchanger/spec_graph_resource.v
theories/examples/exchanger/proof_graph_piggyback.v
theories/examples/exchanger/proof_graph.v
theories/examples/exchanger/proof_graph_resource.v
theories/examples/exchanger/proof_sequential_client.v
theories/examples/exchanger/proof_mp_client.v
theories/examples/exchanger/spec_graph_piggyback.v
theories/examples/exchanger/proof_graph_piggyback.v
This diff is collapsed.
From gpfsl.base_logic Require Import history.
From gpfsl.logic Require Import atomic_cmra.
From gpfsl.logic Require Import readonly_ptsto.
From gpfsl.algebra Require Import mono_list.
From gpfsl.examples.stack Require Import spec_graph.
From gpfsl.examples.stack Require Import proof_treiber_graph proof_elim_graph.
From gpfsl.examples.exchanger Require Import proof_graph_piggyback.
Require Import iris.prelude.options.
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 Σ).
......@@ -52,10 +52,10 @@ Section Stack.
(* Stack Invariant *)
Definition StackInv1 γg γs s: vProp :=
G, stk.(StackInv) γg s G own γs (E (GSet (to_set G.(Es)))).
G, stk.(StackInv) γg s 1%Qp G own γs (E (GSet (to_set G.(Es)))).
Local Existing Instances
StackInv_Objective StackLocal_Persistent
StackInv_Objective StackInv_Timeless StackLocal_Persistent
queue_persistent.
Instance StackInv_obj γg γs s : Objective (StackInv1 γg γs s) := _.
......@@ -136,11 +136,11 @@ Section Stack.
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 (G) "[SI >nodes]".
rewrite StackInv_graph_master_acc. iDestruct "SI" as "[>Gm SI]".
iDestruct (graph_master_consistent with "Gm") as %EGC.
iInv "I" as (G) ">[SI nodes]".
iDestruct (StackLocal_graph_snap with "Q2") as "Gs".
iDestruct (graph_master_snap_included with "Gm Gs") as %SubG2.
iDestruct (StackInv_graph_snap with "SI Gs") as %SubG2.
iDestruct (StackInv_graph_master_acc with "SI") as (q') "[Gm SI]".
iDestruct (graph_master_consistent with "Gm") as %EGC.
iSpecialize ("SI" with "[$Gm]").
iAaccIntro with "SI".
{ iIntros "SI !>". iFrame. iNext. rewrite /StackInv1. iExists G. iFrame. }
......
From iris.bi Require Import lib.fractional.
From iris.algebra Require Import auth gset gmap agree proofmode_classes.
From iris.proofmode Require Import tactics.
......@@ -64,7 +65,7 @@ Record StackProps G T S
#[local] Notation tstk_mapUR := (authUR tstk_mapUR').
Class tstackG Σ := TStackG {
tstk_graphG : inG Σ (graphR sevent) ;
tstk_graphG :> inG Σ (graphR sevent) ;
(* a persistent map of from logical nodes to event ids and locations. *)
tstk_stackG : inG Σ tstk_mapUR ;
}.
......@@ -329,20 +330,22 @@ Definition StackBaseInv γ γh s G T : vProp :=
(* Only share the ghost state with the client.
This carries some properties of T so that they are available without the
internal invariant StackInternalInv *)
Definition StackInv' γg s G γ T : vProp :=
StackConsistent G graph_master γg (1/2) G
Definition StackInv' γg s q G γ T : vProp :=
StackConsistent 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 *)
LTM_masterv γ (1/2)%Qp T.
Definition StackInv γg s G : vProp :=
γ T, StackInv' γg s G γ T.
#[global] Instance StackInv_objective γg s G : Objective (StackInv γg s G) := _.
LTM_masterv γ (q/2)%Qp T.
Definition StackInv γg s q G : vProp :=
γ T, StackInv' γg s q G γ T.
#[global] Instance StackInv_objective γg s q G :
Objective (StackInv γg s q G) := _.
(* Our internal invariant keeps all the physical resources, as well as enough
ghost resources (`StackInv`) to maintain agreement with the client. *)
Definition StackInternalInv γ γh γg s : vProp :=
G T, StackInv' γg s G γ T StackBaseInv γ γh s G T.
G T, StackInv' γg s 1%Qp G γ T StackBaseInv γ γh s G T.
#[global] Instance StackInternalInv_objective γ γh γg s :
Objective (StackInternalInv γ γh γg s) := _.
......@@ -503,25 +506,26 @@ Proof.
+ eapply (SeenPushed_mono _ _ T2); eauto.
Qed.
Lemma StackInv'_map_snap_incl {γg s G γ T T0} :
StackInv' γg s G γ T -
Lemma StackInv'_map_snap_incl {γg s q G γ T T0} :
StackInv' γg s q G γ T -
LTM_snapv γ T0 - T0 T .
Proof.
iDestruct 1 as (SC) "(G & %γh & F & MT & LT)". iIntros "LTm".
by iDestruct (LTM_master_snap_included with "LT LTm") as %?.
Qed.
Lemma StackInv'_graph_snap_incl {γg s G γ T G' M'} :
StackInv' γg s G γ T -
Lemma StackInv'_graph_snap_incl {γg s q G γ T G' M'} :
StackInv' γg s q G γ T -
graph_snap γg G' M' - G' G .
Proof.
iDestruct 1 as (SC) "(G & ?)". iIntros "Gs".
by iDestruct (graph_master_snap_included with "G Gs") as %?.
Qed.
Lemma StackInv'_snapshot {γg s G γ T} :
StackInv' γg s G γ T -
StackConsistent G eventgraph_consistent G LTM_snapv γ T graph_snap γg G .
Lemma StackInv'_snapshot {γg s q G γ T} :
StackInv' γg s q G γ T -
StackConsistent G eventgraph_consistent G
LTM_snapv γ T graph_snap γg G .
Proof.
iDestruct 1 as (SC) "(G & %γh & F & MT & LT)".
iDestruct (graph_master_consistent with "G") as %?.
......@@ -530,8 +534,9 @@ Proof.
done.
Qed.
Lemma StackInv'_agree γg s G γ T G' γ' T' :
StackInv' γg s G γ T - StackInv' γg s G' γ' T' - γ' = γ G' = G T' = T .
Lemma StackInv'_agree γg s q G γ T q' G' γ' T' :
StackInv' γg s q G γ T - StackInv' γg s q' G' γ' T' -
γ' = γ G' = G T' = T .
Proof.
iDestruct 1 as (_) "(G & %γh & _ & MT & LT)".
iDestruct 1 as (_) "(G' & %γh' & _ & MT' & LT')".
......@@ -541,11 +546,43 @@ Proof.
done.
Qed.
Instance StackInv'_fractional γg s G γ T :
Fractional (λ q, StackInv' γg s q G γ T).
Proof.
intros p q. iSplit.
- iDestruct 1 as (SC) "(G & %γh & %EM & #MT & oT)".
rewrite Qp_div_add_distr.
iDestruct "G" as "[Gp Gq]". iDestruct "oT" as "[oTp oTq]".
iSplitL "Gp oTp"; iFrame (SC) "∗"; iExists γh; iFrame (EM) "#".
- iIntros "[S1 S2]".
iDestruct "S1" as (SC) "(Gp & %γh & %EM & #MT & oT)".
iDestruct "S2" as (_) "(Gq & %_ & _ & _ & oT')".
iCombine "Gp Gq" as "G". iCombine "oT oT'" as "oT".
rewrite -Qp_div_add_distr.
iFrame (SC) "G". iExists γh. iFrame (EM) "MT oT".
Qed.
#[global] Instance StackInv_fractional γg s G :
Fractional (λ q, StackInv γg s q G).
Proof.
intros p q. iSplit.
- iDestruct 1 as (γ T) "S".
iDestruct (StackInv'_fractional with "S") as "[S1 S2]".
iSplitL "S1"; iExists γ, T; iFrame.
- iIntros "[S1 S2]".
iDestruct "S1" as (γ T) "S1". iDestruct "S2" as (γ2 T2) "S2".
iDestruct (StackInv'_agree with "S1 S2") as %(-> & _ & ->).
iExists γ, T. iApply StackInv'_fractional. iFrame.
Qed.
#[global] Instance StackInv_asfractional γg s q G :
AsFractional (StackInv γg s q G) (λ q, StackInv γg s q G) q.
Proof. constructor; [done|apply _]. Qed.
Lemma StackInv'_update γg s G γ T G' T' :
eventgraph_consistent G' StackConsistent G'
G G' T T' EM_equiv T' G'.(Es) gmap_inj T'
StackInv' γg s G γ T - StackInv' γg s G γ T ==
StackInv' γg s G' γ T' StackInv' γg s G' γ 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'.
Proof.
intros EGCs' SC' LeG' LeT' EM' INJ'.
iDestruct 1 as (_) "(G1 & %γh & _ & #MT & oT1)".
......@@ -728,18 +765,33 @@ Local Existing Instances tstk_graphG tstk_stackG.
#[local] Notation vProp := (vProp Σ).
Lemma StackInv_StackConsistent_instance :
γg s G, StackInv γg s G StackConsistent G .
γg s q G, StackInv γg s q G StackConsistent G .
Proof. intros. by iDestruct 1 as (???) "?". Qed.
Lemma StackInv_graph_master_acc_instance :
γg s G, StackInv γg s G
graph_master γg (1/2) G
(graph_master γg (1/2) G - StackInv γg s G).
γg s q G, StackInv γg s q G
q', graph_master γg q' G (graph_master γg q' G - StackInv γg s q G).
Proof.
intros. iDestruct 1 as (γ T SC) "[$ ?]".
intros. iDestruct 1 as (γ T SC) "[? ?]". iExists _. iFrame.
iIntros "G". iExists γ, T. by iFrame.
Qed.
Lemma StackInv_graph_snap_instance :
γg s q G G' M',
StackInv γg s q G - graph_snap γg G' M' - G' G .
Proof.
intros. iDestruct 1 as (γ T SC) "[G ?]". iIntros "G'".
by iDestruct (graph_master_snap_included with "G G'") as %?.
Qed.
Lemma StackInv_agree_instance :
γg s q G q' G',
StackInv γg s q G - StackInv γg s q' G' - G' = G .
Proof.
iDestruct 1 as (γ T _) "[G1 _]". iDestruct 1 as (γ' T' _) "[G2 _]".
by iDestruct (graph_master_agree with "G1 G2") as %?.
Qed.
Lemma StackLocal_graph_snap_instance :
N γg s G M, StackLocal N γg s G M graph_snap γg G M.
Proof. by iIntros "* [$ _]". Qed.
......@@ -767,8 +819,8 @@ Proof.
Qed.
Lemma StackLocalLite_upgrade_instance :
γg s G' G M,
StackInv γg s G' - StackLocalLite γg s G M - StackLocalLite γg s G' M.
γg s q G' G M,
StackInv γg s q G' - StackLocalLite γg s G M - StackLocalLite γg s G' M.
Proof.
iIntros "* SI [Gs SS]". iDestruct "SS" as (γ γh) "[SS #MT]".
iDestruct "SI" as (γ' T' SC) "[SI ST]".
......@@ -788,8 +840,8 @@ Proof.
Qed.
Lemma StackLocal_upgrade_instance :
N γg s G' G M,
StackInv γg s G' - StackLocal N γg s G M - StackLocal N γg s G' M.
N γg s q G' G M,
StackInv γg s q G' - StackLocal N γg s G M - StackLocal N γg s G' M.
Proof.
iIntros "* SI #SL".
iDestruct (StackLocalLite_from_instance with "SL") as "-#SLL".
......@@ -798,8 +850,8 @@ Proof.
Qed.
Lemma StackLocal_union_instance :
N γg s G G1 G2 M1 M2,
StackInv γg s G - StackLocal N γg s G1 M1 - StackLocal N γg s G2 M2 -
N γg s q G G1 G2 M1 M2,
StackInv γg s q G - StackLocal N γg s G1 M1 - StackLocal N γg s G2 M2 -
StackLocal N γg s G (M1 M2).
Proof.
iIntros "* SI SL1 SL2".
......@@ -846,7 +898,7 @@ Proof.
have EM0 : EM_equiv []. { intros ?. naive_solver. }
have INJ0 : gmap_inj ( : gmap loc event_id). { by intros ????. }
iAssert (StackInv' γg s γ StackInv' γg s γ )%I
iAssert (StackInv' γg s 1%Qp γ StackInv' γg s 1%Qp γ )%I
with "[LTm1 LTm2 GM1 GM2]" as "[SI1 SI2]".
{ iSplitL "LTm1 GM1"; rewrite /StackInv; iFrame (SC0) "∗";
iExists γh; iFrame "Hms ∗"; by iPureIntro. }
......@@ -881,11 +933,11 @@ Lemma atom_try_push_internal :
V - StackLocal N γg s G0 M -
(n >> next) - - (n >> data) #v -
(* PUBLIC PRE *)
<<< G, StackInv γg s G >>>
<<< G, StackInv γg s 1%Qp G >>>
try_push_internal [ #s ; #n] @ tid; N
<<< (b : bool) V' G' (psId : event_id) ps Vpush M',
(* PUBLIC POST *)
StackInv γg s G'
StackInv γg s 1%Qp G'
V' @{V'} StackLocal N γg s G' M'
( (* FAIL_RACE case *)
b = false G' = G M' = M
......@@ -1365,11 +1417,11 @@ Lemma atom_push_internal :
V - StackLocal N γg s G0 M -
(n >> next) - - (n >> data) #v -
(* PUBLIC PRE *)
<<< G, StackInv γg s G >>>
<<< G, StackInv γg s 1%Qp G >>>
push_internal [ #s ; #n] @ tid; N
<<< V' G' (psId : event_id) ps Vpush M',
(* PUBLIC POST *)
StackInv γg s G'
StackInv γg s 1%Qp G'
V' @{V'} StackLocal N γg s G' M'
G G' M M'
Vpush.(dv_in) = V Vpush.(dv_comm) = V'
......@@ -2097,11 +2149,14 @@ Proof.
Qed.
End proof.
Program Definition treiber_stack_impl
Program Definition treiber_stack_impl Σ
`{!noprolG Σ, !tstackG Σ, !atomicG Σ} : a_stack_spec Σ := {|
spec_graph.StackInv_Objective := StackInv_objective ;
spec_graph.StackInv_Fractional := StackInv_fractional ;
spec_graph.StackInv_StackConsistent := StackInv_StackConsistent_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 ;
spec_graph.StackLocal_graph_snap := StackLocal_graph_snap_instance ;
spec_graph.StackLocal_Persistent := StackLocal_persistent ;
......
From stdpp Require Import namespaces.
From iris.bi Require Import lib.fractional.
From gpfsl.logic Require Import logatom.
From gpfsl.examples.graph Require Export spec.
......@@ -50,14 +53,14 @@ Definition StackLocalT Σ : Type :=
Definition StackLocalNT Σ : Type :=
namespace StackLocalT Σ.
Definition StackInvT Σ : Type :=
gname loc graph vProp Σ.
gname loc frac graph vProp Σ.
Definition new_stack_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR sevent)}
(new_stack : val) (StackLocal : StackLocalNT Σ) (StackInv : StackInvT Σ) : Prop :=
N tid,
{{{ True }}}
new_stack [] @ tid;
{{{ γg (s: loc), RET #s; StackLocal N γg s StackInv γg s }}}.
{{{ γg (s: loc), RET #s; StackLocal N γg s StackInv γg s 1%Qp }}}.
Definition try_push_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR sevent)}
(try_push : val) (StackLocal : StackLocalNT Σ) (StackInv : StackInvT Σ) : Prop :=
......@@ -66,11 +69,11 @@ Definition try_push_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR sevent)}
(* G1 is a snapshot of the graph, locally observed by M *)
V - StackLocal N γg s G1 M -
(* PUBLIC PRE *)
<<< G, StackInv γg s G >>>
<<< G, StackInv γg s 1%Qp G >>>
try_push [ #s ; #v] @ tid; N
<<< (b: bool) V' G' (psId : event_id) ps Vpush M',
(* PUBLIC POST *)
StackInv γg s G'
StackInv γg s 1%Qp G'
V' @{V'} StackLocal N γg s G' M'
(* FAIL_RACE case *)
(b = false G' = G M' = M)
......@@ -95,11 +98,11 @@ Definition push_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR sevent)}
(* G1 is a snapshot of the graph, locally observed by M *)
V - StackLocal N γg s G1 M -
(* PUBLIC PRE *)
<<< G, StackInv γg s G >>>
<<< G, StackInv γg s 1%Qp G >>>
push [ #s ; #v] @ tid; N
<<< V' G' (psId : event_id) ps Vpush M',
(* PUBLIC POST *)
StackInv γg s G'
StackInv γg s 1%Qp G'
V' @{V'} StackLocal N γg s G' M'
G G' M M'
Vpush.(dv_in) = V Vpush.(dv_comm) = V'
......@@ -120,11 +123,11 @@ Definition try_pop_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR sevent)}
(* PRIVATE PRE *)
V - StackLocal N γg s G1 M -
(* PUBLIC PRE *)
<<< G, StackInv γg s G >>>
<<< G, StackInv γg s 1%Qp G >>>
try_pop [ #s] @ tid; N
<<< (v: Z) V' G' (psId ppId : event_id) ps pp Vpp M',
(* PUBLIC POST *)
StackInv γg s G'
StackInv γg s 1%Qp G'
V' @{V'} StackLocal N γg s G' M'
G G' M M'
(* the view after should acquire the view of pop *)
......@@ -159,11 +162,11 @@ Definition pop_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR sevent)}
(* PRIVATE PRE *)
V - StackLocal N γg s G1 M -
(* PUBLIC PRE *)
<<< G, StackInv γg s G >>>
<<< G, StackInv γg s 1%Qp G >>>
pop [ #s] @ tid; N
<<< (v: Z) V' G' (psId ppId : event_id) ps pp Vpp M',
(* PUBLIC POST *)
StackInv γg s G'
StackInv γg s 1%Qp G'
V' @{V'} StackLocal N γg s G' M'
G G' M M'
(* the view after should acquire the view of pop *)
......@@ -203,25 +206,32 @@ Record stack_spec {Σ} `{!noprolG Σ, !inG Σ (graphR sevent)}
StackLocalLite : StackLocalT Σ;
StackInv : StackInvT Σ;
(** predicates properties *)
StackInv_Objective : γg s G, Objective (StackInv γg s G) ;
StackInv_Timeless : γg s G, Timeless (StackInv γg s G) ;
StackInv_Objective : γg s q G, Objective (StackInv γg s q G) ;
StackInv_Timeless : γg s q G, Timeless (StackInv γg s q G) ;
StackInv_Fractional : γg s G, Fractional (λ q, StackInv γg s q G) ;
(* TODO: one might want exclusiveness for StackInv *)
StackInv_StackConsistent : γg s G, StackInv γg s G StackConsistent G ;
StackInv_StackConsistent : γg s q G, StackInv γg s q G StackConsistent G ;
StackInv_graph_master_acc :
γg s G, StackInv γg s G graph_master γg (1/2) G
(graph_master γg (1/2) G - StackInv γg s G) ;
γg s q G, StackInv γg s q G
q', graph_master γg q' G (graph_master γg q' G - StackInv γg s q G) ;
StackInv_graph_snap :
γg s q G G' M',
StackInv γg s q G - graph_snap γg G' M' - G' G ;
StackInv_agree :
γg s q G q' G',
StackInv γg s q G - StackInv γg s q' G' - G' = G ;
StackLocal_Persistent :
N γg s G M, Persistent (StackLocal N γg s G M) ;
StackLocal_graph_snap :
N γg s G M, StackLocal N γg s G M graph_snap γg G M ;
StackLocal_union :
N γg s G G1 G2 M1 M2,
StackInv γg s G - StackLocal N γg s G1 M1 - StackLocal N γg s G2 M2 -
N γg s q G G1 G2 M1 M2,
StackInv γg s q G - StackLocal N γg s G1 M1 - StackLocal N γg s G2 M2 -
StackLocal N γg s G (M1 M2) ;
StackLocal_upgrade :
N γg s G' G M,
StackInv γg s G' - StackLocal N γg s G M - StackLocal N γg s G' M ;
N γg s q G' G M,
StackInv γg s q G' - StackLocal N γg s G M - StackLocal N γg s G' M ;
(* StackLocalLite is the light version of StackLocal that is Timeless *)
StackLocalLite_Timeless :
......@@ -236,8 +246,8 @@ Record stack_spec {Σ} `{!noprolG Σ, !inG Σ (graphR sevent)}
StackLocalLite_graph_snap :
γg s G M, StackLocalLite γg s G M graph_snap γg G M ;
StackLocalLite_upgrade :
γg s G' G M,
StackInv γg s G' - StackLocalLite γg s G M - StackLocalLite γg s G' M ;
γg s q G' G M,
StackInv γg s q G' - StackLocalLite γg s G M - StackLocalLite γg s G' M ;
(* operations specs *)
new_stack_spec : new_stack_spec' new_stack StackLocal StackInv;
......
Supports Markdown
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