Skip to content
Snippets Groups Projects
Commit 01b3d024 authored by Jaehwang Jung's avatar Jaehwang Jung
Browse files

port treiber stack graph proof (with some admits)

parent d25ee779
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
theories/examples/event/event.v
+ 1
− 1
View file @ 01b3d024
From gpfsl.lang Require Import lang. From gpfsl.lang Require Import lang.
From gpfsl.examples Require Export list_sqsubseteq. From gpfsl.examples Require Export list_helper.
Set Default Proof Using "Type". Set Default Proof Using "Type".
......
theories/examples/event/ghost.v
+ 1
− 1
View file @ 01b3d024
...@@ -4,8 +4,8 @@ From iris.base_logic.lib Require Import own. ...@@ -4,8 +4,8 @@ From iris.base_logic.lib Require Import own.
From gpfsl.algebra Require Import mono_list. From gpfsl.algebra Require Import mono_list.
From gpfsl.base_logic Require Import vprop. From gpfsl.base_logic Require Import vprop.
From gpfsl.examples Require Import list_helper.
From gpfsl.examples.event Require Import event. From gpfsl.examples.event Require Import event.
From gpfsl.examples.graph Require Import list_helper.
Set Default Proof Using "Type". Set Default Proof Using "Type".
......
theories/examples/graph/graph_extend.v
+ 207
− 205
View file @ 01b3d024
This diff is collapsed.
theories/examples/list_helper.v
+ 20
− 0
View file @ 01b3d024
...@@ -25,6 +25,17 @@ Lemma prefix_app_inv l l1 l2 : ...@@ -25,6 +25,17 @@ Lemma prefix_app_inv l l1 l2 :
l ++ l1 `prefix_of` l ++ l2 → l1 `prefix_of` l2. l ++ l1 `prefix_of` l ++ l2 → l1 `prefix_of` l2.
Proof. intros [ly Eq]. exists ly. by simplify_list_eq. Qed. Proof. intros [ly Eq]. exists ly. by simplify_list_eq. Qed.
Lemma prefix_lookup_inv l1 l2 i x y :
l1 !! i = Some x → l1 `prefix_of` l2 → l2 !! i = Some y → x = y.
Proof. intros Hl1 ? Hl2. eapply prefix_lookup in Hl1; eauto. congruence. Qed.
Lemma prefix_lookup_eq_inv l1 l2 i x :
l1 `prefix_of` l2 → l2 !! i = Some x → is_Some (l1 !! i) → l1 !! i = Some x.
Proof.
intros SUB Eq' [? Eq].
assert (Eqv:=prefix_lookup_inv _ _ _ _ _ Eq SUB Eq'). by subst.
Qed.
Global Instance list_sqsubseteq : SqSubsetEq (list A) := prefix. Global Instance list_sqsubseteq : SqSubsetEq (list A) := prefix.
Global Instance list_sqsubseteq_elem_of_proper a : Global Instance list_sqsubseteq_elem_of_proper a :
...@@ -121,6 +132,15 @@ Proof. ...@@ -121,6 +132,15 @@ Proof.
intros [??]%lookup_last_Some. by simplify_list_eq. intros [??]%lookup_last_Some. by simplify_list_eq.
Qed. Qed.
Lemma lookup_last_ne l i x : (i ≠ length l)%nat → (l ++ [x]) !! i = l !! i.
Proof.
case (decide (i < length l)) as [LT|GE].
- intros _. by apply lookup_app_l.
- case (decide (length l < i)) as [GT|EQ]; [|lia].
intros _. rewrite !lookup_ge_None_2; [done|lia|].
rewrite app_length /=. lia.
Qed.
Lemma elem_of_last_Some l x : Lemma elem_of_last_Some l x :
last l = Some x → ∃ l', l = l' ++ [x]. last l = Some x → ∃ l', l = l' ++ [x].
Proof. Proof.
......
theories/examples/stack/proof_treiber_graph.v
+ 339
− 351
View file @ 01b3d024
This diff is collapsed.
theories/examples/stack/spec_graph.v
+ 110
− 118
View file @ 01b3d024
...@@ -27,12 +27,12 @@ Proof. ...@@ -27,12 +27,12 @@ Proof.
by intros []. by intros [].
Qed. Qed.
Local Notation event_map := (event_map sevent). Local Notation history := (history sevent).
Implicit Type (E : event_map). Implicit Type (E : history).
Definition unmatched_push G E eid : Prop := Definition unmatched_push E eid : Prop :=
(∃ v : Z, ge_event <$> (E !! eid) = Some (Push v)) ∧ (∃ v : Z, ge_event <$> (E.(Es) !! eid) = Some (Push v)) ∧
(∀ id, (eid, id) ∉ G.(so)). (∀ id, (eid, id) ∉ E.(so)).
(** Stack predicates *) (** Stack predicates *)
Definition is_push e v : Prop := e = Push v. Definition is_push e v : Prop := e = Push v.
...@@ -42,159 +42,153 @@ Local Notation EMPTY := 0 (only parsing). ...@@ -42,159 +42,153 @@ Local Notation EMPTY := 0 (only parsing).
Local Notation FAIL_RACE := (-1) (only parsing). Local Notation FAIL_RACE := (-1) (only parsing).
Definition StackLocalT Σ : Type := Definition StackLocalT Σ : Type :=
gname → gname → loc → graph → event_map → logView → vProp Σ. gname → gname → loc → history → logView → vProp Σ.
Definition StackInvT Σ : Type := Definition StackInvT Σ : Type :=
gname → graph → event_map → vProp Σ. gname → history → vProp Σ.
Definition new_stack_spec' {Σ} `{!noprolG Σ, !inG Σ (eventGraphR sevent)} Definition new_stack_spec' {Σ} `{!noprolG Σ, !inG Σ (historyR sevent)}
(new_stack : val) (StackLocal : StackLocalT Σ) (StackInv : StackInvT Σ) : Prop := (new_stack : val) (StackLocal : StackLocalT Σ) (StackInv : StackInvT Σ) : Prop :=
∀ tid, ∀ tid,
{{{ True }}} {{{ True }}}
new_stack [] in tid new_stack [] in tid
{{{ γs γg (s: loc), RET #s; StackLocal γs γg s ∅ ∅ ∅ ∗ StackInv γg ∅ ∅ }}}. {{{ γs γg (s: loc), RET #s; StackLocal γs γg s ∅ ∅ ∗ StackInv γg ∅ }}}.
Definition try_push_spec' {Σ} `{!noprolG Σ, !inG Σ (eventGraphR sevent)} Definition try_push_spec' {Σ} `{!noprolG Σ, !inG Σ (historyR sevent)}
(try_push : val) Eo (StackLocal : StackLocalT Σ) (StackInv : StackInvT Σ) : Prop := (try_push : val) Eo (StackLocal : StackLocalT Σ) (StackInv : StackInvT Σ) : Prop :=
∀ (s: loc) tid γs γg G1 E1 M (V : view) (v : Z) (Posx: 0 < v), ∀ (s: loc) tid γs γg E1 M (V : view) (v : Z) (Posx: 0 < v),
(* PRIVATE PRE *) (* PRIVATE PRE *)
(* (G1,E1) is a snapshot of the graph, locally observed by M *) (* E1 is a snapshot of the history, locally observed by M *)
⊒V -∗ StackLocal γs γg s G1 E1 M -∗ ⊒V -∗ StackLocal γs γg s E1 M -∗
(* PUBLIC PRE *) (* PUBLIC PRE *)
<<< ∀ G E, ▷ StackInv γg G E >>> <<< ∀ E, ▷ StackInv γg E >>>
try_push [ #s ; #v] in tid @ Eo try_push [ #s ; #v] in tid @ Eo
<<< ∃ (b: bool) V' G' E' (psId : event_id) ps Vpush M', <<< ∃ (b: bool) V' E' (psId : event_id) ps Vpush M',
(* PUBLIC POST *) (* PUBLIC POST *)
▷ StackInv γg G' E' ∗ ▷ StackInv γg E' ∗
⊒V' ∗ @{V'} StackLocal γs γg s G' E' M' ∗ ⊒V' ∗ @{V'} StackLocal γs γg s E' M' ∗
⌜ (* FAIL_RACE case *) ⌜ (* FAIL_RACE case *)
(b = false ∧ G' = G ∧ E' = E ∧ M' = M) (b = false ∧ E' = E ∧ M' = M)
∨ (* successful case *) ∨ (* successful case *)
( b = true ∧ E ⊆ E' ∧ M ⊑ M' ∧ ( b = true ∧ E ⊑ E' ∧ M ⊑ M' ∧
Vpush.(dv_in) = V ∧ Vpush.(dv_comm) = V' ∧ Vpush.(dv_in) = V ∧ Vpush.(dv_comm) = V' ∧
(* Vpush.(dv_wrt) = V' ∧ *) (* << only works if the push is also acquiring *) (* Vpush.(dv_wrt) = V' ∧ *) (* << only works if the push is also acquiring *)
(* ps is a new push event with which G' strictly extends G *) (* ps is a new push event with which E' strictly extends E *)
is_push ps v ∧ is_push ps v ∧
set_Forall (λ e', (e' < psId)%nat) G.(Es) ∧ psId ∉ G.(Es) ∧ psId = length E.(Es) ∧
G'.(Es) = {[psId]} ∪ G.(Es) ∧ E'.(Es) = E.(Es) ++ [mkGraphEvent ps Vpush M'] ∧
G'.(so) = G.(so) ∧ G'.(com) = G.(com) ∧ E'.(so) = E.(so) ∧ E'.(com) = E.(com) ∧
E' = <[psId := mkGraphEvent ps Vpush M']>E ∧
psId ∈ M' ) ⌝, psId ∈ M' ) ⌝,
(* RETURN VALUE AT COMMITTING POINT *) (* RETURN VALUE AT COMMITTING POINT *)
RET #b >>> RET #b >>>
. .
Definition push_spec' {Σ} `{!noprolG Σ, !inG Σ (eventGraphR sevent)} Definition push_spec' {Σ} `{!noprolG Σ, !inG Σ (historyR sevent)}
(push : val) Eo (StackLocal : StackLocalT Σ) (StackInv : StackInvT Σ) : Prop := (push : val) Eo (StackLocal : StackLocalT Σ) (StackInv : StackInvT Σ) : Prop :=
∀ (s: loc) tid γs γg G1 E1 M (V : view) (v : Z) (Posx: 0 < v), ∀ (s: loc) tid γs γg E1 M (V : view) (v : Z) (Posx: 0 < v),
(* PRIVATE PRE *) (* PRIVATE PRE *)
(* (G1,E1) is a snapshot of the graph, locally observed by M *) (* E1 is a snapshot of the history, locally observed by M *)
⊒V -∗ StackLocal γs γg s G1 E1 M -∗ ⊒V -∗ StackLocal γs γg s E1 M -∗
(* PUBLIC PRE *) (* PUBLIC PRE *)
<<< ∀ G E, ▷ StackInv γg G E >>> <<< ∀ E, ▷ StackInv γg E >>>
push [ #s ; #v] in tid @ Eo push [ #s ; #v] in tid @ Eo
<<< ∃ V' G' E' (psId : event_id) ps Vpush M', <<< ∃ V' E' (psId : event_id) ps Vpush M',
(* PUBLIC POST *) (* PUBLIC POST *)
▷ StackInv γg G' E' ∗ ▷ StackInv γg E' ∗
⊒V' ∗ @{V'} StackLocal γs γg s G' E' M' ∗ ⊒V' ∗ @{V'} StackLocal γs γg s E' M' ∗
⌜ E ⊆ E' ∧ M ⊑ M' ∧ ⌜ E ⊑ E' ∧ M ⊑ M' ∧
Vpush.(dv_in) = V ∧ Vpush.(dv_comm) = V' ∧ Vpush.(dv_in) = V ∧ Vpush.(dv_comm) = V' ∧
(* Vpush.(dv_wrt) = V' ∧ *) (* << only works if the push is also acquiring *) (* Vpush.(dv_wrt) = V' ∧ *) (* << only works if the push is also acquiring *)
(* ps is a new push event with which G' strictly extends G *) (* ps is a new push event with which E' strictly extends E *)
is_push ps v ∧ is_push ps v ∧
set_Forall (λ e', (e' < psId)%nat) G.(Es) ∧ psId ∉ G.(Es) ∧ psId = length E.(Es) ∧
G'.(Es) = {[psId]} ∪ G.(Es) ∧ E'.(Es) = E.(Es) ++ [mkGraphEvent ps Vpush M'] ∧
G'.(so) = G.(so) ∧ G'.(com) = G.(com) ∧ E'.(so) = E.(so) ∧ E'.(com) = E.(com) ∧
E' = <[psId := mkGraphEvent ps Vpush M']>E ∧
psId ∈ M' ⌝, psId ∈ M' ⌝,
(* RETURN VALUE AT COMMITTING POINT *) (* RETURN VALUE AT COMMITTING POINT *)
RET #☠ >>> RET #☠ >>>
. .
Definition try_pop_spec' {Σ} `{!noprolG Σ, !inG Σ (eventGraphR sevent)} Definition try_pop_spec' {Σ} `{!noprolG Σ, !inG Σ (historyR sevent)}
(try_pop : val) Eo (StackLocal : StackLocalT Σ) (StackInv : StackInvT Σ) : Prop := (try_pop : val) Eo (StackLocal : StackLocalT Σ) (StackInv : StackInvT Σ) : Prop :=
∀ (s: loc) tid γs γg G1 E1 M V, ∀ (s: loc) tid γs γg E1 M V,
(* PRIVATE PRE *) (* PRIVATE PRE *)
⊒V -∗ StackLocal γs γg s G1 E1 M -∗ ⊒V -∗ StackLocal γs γg s E1 M -∗
(* PUBLIC PRE *) (* PUBLIC PRE *)
<<< ∀ G E, ▷ StackInv γg G E >>> <<< ∀ E, ▷ StackInv γg E >>>
try_pop [ #s] in tid @ Eo try_pop [ #s] in tid @ Eo
<<< ∃ (v: Z) V' G' E' (psId ppId : event_id) ps pp Vpp M', <<< ∃ (v: Z) V' E' (psId ppId : event_id) ps pp Vpp M',
(* PUBLIC POST *) (* PUBLIC POST *)
▷ StackInv γg G' E' ∗ ▷ StackInv γg E' ∗
⊒V' ∗ @{V'} StackLocal γs γg s G' E' M' ∗ ⊒V' ∗ @{V'} StackLocal γs γg s E' M' ∗
⌜ E ⊆ E' ∧ M ⊑ M' ∧ ⌜ E ⊑ E' ∧ M ⊑ M' ∧
(* the view after should acquire the view of pop *) (* the view after should acquire the view of pop *)
Vpp.(dv_in) = V ∧ Vpp.(dv_comm) = V' Vpp.(dv_in) = V ∧ Vpp.(dv_comm) = V'
(* V ⊑ Vpp.(dv_wrt) ∧ *) (* << only works if pop is releasing *) ⌝ ∗ (* V ⊑ Vpp.(dv_wrt) ∧ *) (* << only works if pop is releasing *) ⌝ ∗
⌜ (* FAIL_RACE case *) ⌜ (* FAIL_RACE case *)
(v = FAIL_RACE ∧ G' = G ∧ E' = E ∧ M' = M) (v = FAIL_RACE ∧ E' = E ∧ M' = M)
∨ (* EMPTY case *) ∨ (* EMPTY case *)
( v = EMPTY ∧ pp = EmpPop ∧ ( v = EMPTY ∧ pp = EmpPop ∧
set_Forall (λ e', (e' < ppId)%nat) G.(Es) ∧ ppId ∉ G.(Es) ∧ ppId = length E.(Es) ∧
G'.(Es) = {[ppId]} ∪ G.(Es) ∧ E'.(Es) = E.(Es) ++ [mkGraphEvent pp Vpp M'] ∧
G'.(so) = G.(so) ∧ G'.(com) = G.(com) ∧ E'.(so) = E.(so) ∧ E'.(com) = E.(com) ∧
E' = <[ppId := mkGraphEvent pp Vpp M']>E ∧
M' = {[ ppId ]} ∪ M ∧ M' = {[ ppId ]} ∪ M ∧
(* coming from StackConsistent. We have it here for convenience. *) (* coming from StackConsistent. We have it here for convenience. *)
(∀ psId, unmatched_push G' E' psId → psId ∉ M) ) (∀ psId, unmatched_push E' psId → psId ∉ M) )
∨ (* successful case *) ∨ (* successful case *)
( 0 < v ∧ is_push ps v ∧ is_pop pp v ∧ psId ∈ G.(Es) ∧ ( 0 < v ∧ is_push ps v ∧ is_pop pp v ∧ (psId < length E.(Es))%nat ∧
set_Forall (λ e', (e' < ppId)%nat) G.(Es) ∧ ppId ∉ G.(Es) ∧ ppId = length E.(Es) ∧
(∀ id, (psId, id) ∉ G.(so)) ∧ (∀ id, (psId, id) ∉ E.(so)) ∧
G'.(Es) = {[ppId]} ∪ G.(Es) ∧ E'.(Es) = E.(Es) ++ [mkGraphEvent pp Vpp M'] ∧
G'.(so) = {[(psId, ppId)]} ∪ G.(so) ∧ E'.(so) = {[(psId, ppId)]} ∪ E.(so) ∧
G'.(com) = {[(psId, ppId)]} ∪ G.(com) ∧ E'.(com) = {[(psId, ppId)]} ∪ E.(com) ∧
E' = <[ppId := mkGraphEvent pp Vpp M']>E ∧ ∃ eV, E.(Es) !! psId = Some eV ∧ eV.(ge_event) = ps ∧
∃ eV, E !! psId = Some eV ∧ eV.(ge_event) = ps ∧
eV.(ge_lview) ⊆ M' ∧ eV.(ge_lview) ⊆ M' ∧
psId ∈ M' ∧ ppId ∈ M' ) ⌝ , psId ∈ M' ∧ ppId ∈ M' ) ⌝ ,
(* RETURN VALUE AT COMMITTING POINT *) (* RETURN VALUE AT COMMITTING POINT *)
RET #v >>> RET #v >>>
. .
Definition pop_spec' {Σ} `{!noprolG Σ, !inG Σ (eventGraphR sevent)} Definition pop_spec' {Σ} `{!noprolG Σ, !inG Σ (historyR sevent)}
(pop : val) Eo (StackLocal : StackLocalT Σ) (StackInv : StackInvT Σ) : Prop := (pop : val) Eo (StackLocal : StackLocalT Σ) (StackInv : StackInvT Σ) : Prop :=
∀ (s: loc) tid γs γg G1 E1 M V, ∀ (s: loc) tid γs γg E1 M V,
(* PRIVATE PRE *) (* PRIVATE PRE *)
⊒V -∗ StackLocal γs γg s G1 E1 M -∗ ⊒V -∗ StackLocal γs γg s E1 M -∗
(* PUBLIC PRE *) (* PUBLIC PRE *)
<<< ∀ G E, ▷ StackInv γg G E >>> <<< ∀ E, ▷ StackInv γg E >>>
pop [ #s] in tid @ Eo pop [ #s] in tid @ Eo
<<< ∃ (v: Z) V' G' E' (psId ppId : event_id) ps pp Vpp M', <<< ∃ (v: Z) V' E' (psId ppId : event_id) ps pp Vpp M',
(* PUBLIC POST *) (* PUBLIC POST *)
▷ StackInv γg G' E' ∗ ▷ StackInv γg E' ∗
⊒V' ∗ @{V'} StackLocal γs γg s G' E' M' ∗ ⊒V' ∗ @{V'} StackLocal γs γg s E' M' ∗
⌜ E ⊆ E' ∧ M ⊑ M' ∧ ⌜ E ⊑ E' ∧ M ⊑ M' ∧
(* the view after should acquire the view of pop *) (* the view after should acquire the view of pop *)
Vpp.(dv_in) = V ∧ Vpp.(dv_comm) = V' Vpp.(dv_in) = V ∧ Vpp.(dv_comm) = V'
(* V ⊑ Vpp.(dv_wrt) ∧ *) (* << only works if pop is releasing *) ⌝ ∗ (* V ⊑ Vpp.(dv_wrt) ∧ *) (* << only works if pop is releasing *) ⌝ ∗
⌜ (* EMPTY case *) ⌜ (* EMPTY case *)
( v = 0 ∧ pp = EmpPop ∧ ( v = 0 ∧ pp = EmpPop ∧
set_Forall (λ e', (e' < ppId)%nat) G.(Es) ∧ ppId ∉ G.(Es) ∧ ppId = length E.(Es) ∧
G'.(Es) = {[ppId]} ∪ G.(Es) ∧ E'.(Es) = E.(Es) ++ [mkGraphEvent pp Vpp M'] ∧
G'.(so) = G.(so) ∧ G'.(com) = G.(com) ∧ E'.(so) = E.(so) ∧ E'.(com) = E.(com) ∧
E' = <[ppId := mkGraphEvent pp Vpp M']>E ∧
M' = {[ ppId ]} ∪ M ∧ M' = {[ ppId ]} ∪ M ∧
(* coming from StackConsistent. We have it here for convenience. *) (* coming from StackConsistent. We have it here for convenience. *)
(∀ psId, unmatched_push G' E' psId → psId ∉ M) ) (∀ psId, unmatched_push E' psId → psId ∉ M) )
∨ (* successful case *) ∨ (* successful case *)
( 0 < v ∧ is_push ps v ∧ is_pop pp v ∧ psId ∈ G.(Es) ∧ ( 0 < v ∧ is_push ps v ∧ is_pop pp v ∧ (psId < length E.(Es))%nat ∧
set_Forall (λ e', (e' < ppId)%nat) G.(Es) ∧ ppId ∉ G.(Es) ∧ ppId = length E.(Es) ∧
(∀ id, (psId, id) ∉ G.(so)) ∧ (∀ id, (psId, id) ∉ E.(so)) ∧
G'.(Es) = {[ppId]} ∪ G.(Es) ∧ E'.(Es) = E.(Es) ++ [mkGraphEvent pp Vpp M'] ∧
G'.(so) = {[(psId, ppId)]} ∪ G.(so) ∧ E'.(so) = {[(psId, ppId)]} ∪ E.(so) ∧
G'.(com) = {[(psId, ppId)]} ∪ G.(com) ∧ E'.(com) = {[(psId, ppId)]} ∪ E.(com) ∧
E' = <[ppId := mkGraphEvent pp Vpp M']>E ∧ ∃ eV, E.(Es) !! psId = Some eV ∧ eV.(ge_event) = ps ∧
∃ eV, E !! psId = Some eV ∧ eV.(ge_event) = ps ∧
eV.(ge_lview) ⊆ M' ∧ eV.(ge_lview) ⊆ M' ∧
psId ∈ M' ∧ ppId ∈ M' ) ⌝ , psId ∈ M' ∧ ppId ∈ M' ) ⌝ ,
(* RETURN VALUE AT COMMITTING POINT *) (* RETURN VALUE AT COMMITTING POINT *)
RET #v >>> RET #v >>>
. .
Record stack_spec {Σ} `{!noprolG Σ, !inG Σ (eventGraphR sevent)} Record stack_spec {Σ} `{!noprolG Σ, !inG Σ (historyR sevent)}
{Eo} {StackConsistent : graph → event_map → Prop} := StackSpec { {Eo} {StackConsistent : history → Prop} := StackSpec {
(* operations *) (* operations *)
new_stack : val; new_stack : val;
try_push : val; try_push : val;
...@@ -205,15 +199,15 @@ Record stack_spec {Σ} `{!noprolG Σ, !inG Σ (eventGraphR sevent)} ...@@ -205,15 +199,15 @@ Record stack_spec {Σ} `{!noprolG Σ, !inG Σ (eventGraphR sevent)}
StackLocal : StackLocalT Σ; StackLocal : StackLocalT Σ;
StackInv : StackInvT Σ; StackInv : StackInvT Σ;
(** predicates properties *) (** predicates properties *)
StackInv_Objective : ∀ γg G E, Objective (StackInv γg G E); StackInv_Objective : ∀ γg E, Objective (StackInv γg E);
StackInv_StackConsistent : ∀ γg G E, StackInv γg G E ⊢ ⌜ StackConsistent G E ⌝; StackInv_StackConsistent : ∀ γg E, StackInv γg E ⊢ ⌜ StackConsistent E ⌝;
StackInv_graph_master_acc : StackInv_history_master_acc :
∀ γg G E, StackInv γg G E ⊢ graph_master γg (1/2) G E ∗ ∀ γg E, StackInv γg E ⊢ history_master γg (1/2) E ∗
(graph_master γg (1/2) G E -∗ StackInv γg G E); (history_master γg (1/2) E -∗ StackInv γg E);
StackLocal_graph_snap : StackLocal_history_snap :
∀ γs γg s G E M, StackLocal γs γg s G E M ⊢ graph_snap γg G E M; ∀ γs γg s E M, StackLocal γs γg s E M ⊢ history_snap γg E M;
StackLocal_Persistent : StackLocal_Persistent :
∀ γs γg s G E M, Persistent (StackLocal γs γg s G E M); ∀ γs γg s E M, Persistent (StackLocal γs γg s E M);
(* operations specs *) (* operations specs *)
new_stack_spec : new_stack_spec' new_stack StackLocal StackInv; new_stack_spec : new_stack_spec' new_stack StackLocal StackInv;
try_push_spec : try_push_spec' try_push Eo StackLocal StackInv; try_push_spec : try_push_spec' try_push Eo StackLocal StackInv;
...@@ -225,46 +219,44 @@ Record stack_spec {Σ} `{!noprolG Σ, !inG Σ (eventGraphR sevent)} ...@@ -225,46 +219,44 @@ Record stack_spec {Σ} `{!noprolG Σ, !inG Σ (eventGraphR sevent)}
Arguments stack_spec _ {_ _} _ _. Arguments stack_spec _ {_ _} _ _.
Existing Instances StackInv_Objective StackLocal_Persistent. Existing Instances StackInv_Objective StackLocal_Persistent.
Record StackConsistent (G: graph) E : Prop := mkStackConsistent { Record StackConsistent E : Prop := mkStackConsistent {
stk_cons_mo_consec : (* mo is consecutive *)
∃ start len, G.(Es) ≡ list_to_set (seq start len) ;
stk_cons_dview_push : (* push is releasing *) stk_cons_dview_push : (* push is releasing *)
∀ e eV (v: Z), E !! e = Some eV → eV.(ge_event) = Push v → ∀ e eV (v: Z), E.(Es) !! e = Some eV → eV.(ge_event) = Push v →
eV.(ge_view).(dv_comm) ⊑ eV.(ge_view).(dv_wrt) ; eV.(ge_view).(dv_comm) ⊑ eV.(ge_view).(dv_wrt) ;
stk_cons_dview_push_order : (* pushes are ordered by CAS *) stk_cons_dview_push_order : (* pushes are ordered by CAS *)
∀ e1 e2 eV1 eV2 (v1 v2 : Z), ∀ e1 e2 eV1 eV2 (v1 v2 : Z),
E !! e1 = Some eV1 → E !! e2 = Some eV2 → E.(Es) !! e1 = Some eV1 → E.(Es) !! e2 = Some eV2 →
is_push eV1.(ge_event) v1 → is_push eV1.(ge_event) v1 →
is_push eV2.(ge_event) v2 → is_push eV2.(ge_event) v2 →
(e1 < e2)%nat → (e1 < e2)%nat →
¬ eV2.(ge_view).(dv_comm) ⊑ eV1.(ge_view).(dv_comm) ; ¬ eV2.(ge_view).(dv_comm) ⊑ eV1.(ge_view).(dv_comm) ;
stk_cons_dview_pop : (* pop is acquiring *) stk_cons_dview_pop : (* pop is acquiring *)
∀ e eV (v: Z), E !! e = Some eV → eV.(ge_event) = Pop v → ∀ e eV (v: Z), E.(Es) !! e = Some eV → eV.(ge_event) = Pop v →
eV.(ge_view).(dv_wrt) ⊑ eV.(ge_view).(dv_comm) ; eV.(ge_view).(dv_wrt) ⊑ eV.(ge_view).(dv_comm) ;
stk_cons_ps_non_zero : (* 0 is used for Empty Pop *) stk_cons_ps_non_zero : (* 0 is used for Empty Pop *)
∀ e eV (v: Z), E !! e = Some eV → eV.(ge_event) = Push v → 0 < v ; ∀ e eV (v: Z), E.(Es) !! e = Some eV → eV.(ge_event) = Push v → 0 < v ;
(* (1)-(7) Stack spec from POPL'19 Library Correctness paper *) (* (1)-(7) Stack spec from POPL'19 Library Correctness paper *)
(* (1) at most 1 Constructor event: we currently don't have initialization events *) (* (1) at most 1 Constructor event: we currently don't have initialization events *)
stk_cons_matches : stk_cons_matches :
(* (2) There can only be so edges between matching Pushs and Pops *) (* (2) There can only be so edges between matching Pushs and Pops *)
∀ e d, (e, d) ∈ G.(com) → (e < d)%nat ∧ ∀ e d, (e, d) ∈ E.(com) → (e < d)%nat ∧
∃ eV dV (v : Z), E !! e = Some eV ∧ E !! d = Some dV ∧ ∃ eV dV (v : Z), E.(Es) !! e = Some eV ∧ E.(Es) !! d = Some dV ∧
eV.(ge_event) = Push v ∧ dV.(ge_event) = Pop v ∧ eV.(ge_event) = Push v ∧ dV.(ge_event) = Pop v ∧
(* so is synchronizing at commit points *) (* so is synchronizing at commit points *)
eV.(ge_view).(dv_wrt) ⊑ dV.(ge_view).(dv_wrt) ; eV.(ge_view).(dv_wrt) ⊑ dV.(ge_view).(dv_wrt) ;
stk_cons_com_functional : stk_cons_com_functional :
(* (3) com and com^-1 are functional: *) (* (3) com and com^-1 are functional: *)
functional_pair_1 G.(com) ∧ functional_pair_2 G.(com) ; functional_pair_1 E.(com) ∧ functional_pair_2 E.(com) ;
(* (4) an empty Pop cannot be matched: this is already included in (2) *) (* (4) an empty Pop cannot be matched: this is already included in (2) *)
stk_cons_non_empty : stk_cons_non_empty :
(* (5) an empty Pop cannot have a logview that includes unmatched Pushs *) (* (5) an empty Pop cannot have a logview that includes unmatched Pushs *)
(* So our Pop result depends on whether our current view includes an (* So our Pop result depends on whether our current view includes an
unmatched Push *) unmatched Push *)
∀ o oV, E !! o = Some oV → oV.(ge_event) = EmpPop → ∀ o oV, E.(Es) !! o = Some oV → oV.(ge_event) = EmpPop →
∀ u, u ∈ oV.(ge_lview) → ¬ unmatched_push G E u ; ∀ u, u ∈ oV.(ge_lview) → ¬ unmatched_push E u ;
stk_cons_so_com : stk_cons_so_com :
(* (6) so and com agree *) (* (6) so and com agree *)
G.(so) = G.(com) ; E.(so) = E.(com) ;
stk_cons_LIFO_a : stk_cons_LIFO_a :
(* (7) If u1 (push1) happens-before u2 (push2), and o1 (pop1) happens-before (* (7) If u1 (push1) happens-before u2 (push2), and o1 (pop1) happens-before
o2 (pop2), then u2 cannot happen-before o1, because if that were the case, o2 (pop2), then u2 cannot happen-before o1, because if that were the case,
...@@ -274,9 +266,9 @@ Record StackConsistent (G: graph) E : Prop := mkStackConsistent { ...@@ -274,9 +266,9 @@ Record StackConsistent (G: graph) E : Prop := mkStackConsistent {
- [u1 [u2 o2] o1] - [u1 [u2 o2] o1]
The impossible case that is mentioned here: [u1 [u2 o1] o2]. *) The impossible case that is mentioned here: [u1 [u2 o1] o2]. *)
∀ u1 o1 oV1 u2 o2 uV2 oV2, ∀ u1 o1 oV1 u2 o2 uV2 oV2,
(u1, o1) ∈ G.(com) → (u2, o2) ∈ G.(com) → (u1, o1) ∈ E.(com) → (u2, o2) ∈ E.(com) →
u1 ≠ u2 → (* e1 and e2 are distinct *) u1 ≠ u2 → (* e1 and e2 are distinct *)
E !! o1 = Some oV1 → E !! u2 = Some uV2 → E !! o2 = Some oV2 → E.(Es) !! o1 = Some oV1 → E.(Es) !! u2 = Some uV2 → E.(Es) !! o2 = Some oV2 →
u1 ∈ uV2.(ge_lview) → (* u1 happens-before u2 *) u1 ∈ uV2.(ge_lview) → (* u1 happens-before u2 *)
o1 ∈ oV2.(ge_lview) → (* o1 happens-before o2 *) o1 ∈ oV2.(ge_lview) → (* o1 happens-before o2 *)
u2 ∉ oV1.(ge_lview) ; (* u2 doesn't happen-before o1. Stronger: o1 happens-before u1. *) u2 ∉ oV1.(ge_lview) ; (* u2 doesn't happen-before o1. Stronger: o1 happens-before u1. *)
...@@ -284,35 +276,35 @@ Record StackConsistent (G: graph) E : Prop := mkStackConsistent { ...@@ -284,35 +276,35 @@ Record StackConsistent (G: graph) E : Prop := mkStackConsistent {
(* Unpopped item u2 cannot be in between push-pop pairs (u1,o1). (* Unpopped item u2 cannot be in between push-pop pairs (u1,o1).
That is, it cannot be the case that [u1 [u2] o1]. *) That is, it cannot be the case that [u1 [u2] o1]. *)
∀ u1 o1 oV1 u2 uV2, ∀ u1 o1 oV1 u2 uV2,
(u1, o1) ∈ G.(com) → (u1, o1) ∈ E.(com) →
E !! o1 = Some oV1 → E !! u2 = Some uV2 → E.(Es) !! o1 = Some oV1 → E.(Es) !! u2 = Some uV2 →
u1 ∈ uV2.(ge_lview) → (* u1 happens-before u2 *) u1 ∈ uV2.(ge_lview) → (* u1 happens-before u2 *)
u2 ∈ oV1.(ge_lview) → (* u2 happen-before o1 *) u2 ∈ oV1.(ge_lview) → (* u2 happen-before o1 *)
¬ unmatched_push G E u2 ; ¬ unmatched_push E u2 ;
stk_cons_mo_hb : stk_cons_mo_hb :
(* mo must agree with logview-inclusion. (* mo must agree with logview-inclusion.
NOTE: this prevents cycles logical view inclusion, which NOTE: this prevents cycles logical view inclusion, which
doesn't work for exchanger. See also "Benign Synchronisation Cycles" in doesn't work for exchanger. See also "Benign Synchronisation Cycles" in
the POPL'19 paper. *) the POPL'19 paper. *)
∀ e1 e2 eV1 eV2, E !! e1 = Some eV1 → E !! e2 = Some eV2 → ∀ e1 e2 eV1 eV2, E.(Es) !! e1 = Some eV1 → E.(Es) !! e2 = Some eV2 →
e1 ∈ eV2.(ge_lview) → e1 ∈ eV2.(ge_lview) →
(e1 ≤ e2)%nat (e1 ≤ e2)%nat
(* ∧ eV1.(ge_lview) ⊑ eV2.(ge_lview) *) (* ∧ eV1.(ge_lview) ⊑ eV2.(ge_lview) *)
(* ^^ this doesn't work because we are not rel-acq (have relaxed ops). *) (* ^^ this doesn't work because we are not rel-acq (have relaxed ops). *)
}. }.
Definition a_stack_spec Σ `{!noprolG Σ, !inG Σ (eventGraphR sevent)} Eo Definition a_stack_spec Σ `{!noprolG Σ, !inG Σ (historyR sevent)} Eo
:= stack_spec Σ Eo StackConsistent. := stack_spec Σ Eo StackConsistent.
(** Some properties *) (** Some properties *)
Lemma unmatched_push_mono G G' E E' eid : Lemma unmatched_push_mono E E' eid :
G ⊑ G' → E ⊆ E' → is_Some (E !! eid) → E ⊑ E' → is_Some (E.(Es) !! eid) →
unmatched_push G' E' eid → unmatched_push G E eid. unmatched_push E' eid → unmatched_push E eid.
Proof. Proof.
intros LeG' LeE [? Eq] [[v Eq'] FA]. intros [LeEs _ Leso] [? Eq] [[v Eq'] FA].
destruct (E' !! eid) as [[? V]|] eqn:Eq''; [|done]. simpl in Eq'. destruct (E'.(Es) !! eid) as [[? V]|] eqn:Eq''; [|done]. simpl in Eq'.
rewrite (lookup_weaken _ _ _ _ Eq LeE) in Eq''. simplify_eq. rewrite (prefix_lookup _ _ _ _ Eq LeEs) in Eq''. simplify_eq.
split. split.
- exists v. by rewrite Eq. - exists v. by rewrite Eq.
- intros e' ?. apply (FA e'); by apply LeG'. - intros e' ?. apply (FA e'); by apply Leso.
Qed. Qed.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment