Commit db86e0ef authored by Hai Dang's avatar Hai Dang Committed by Jaehwang Jung
Browse files

Use meta instead of encode

parent 467cf3a7
......@@ -12,13 +12,9 @@ Local Existing Instances
spec_abs_graph.QueueInv_Timeless spec_abs_graph.QueueInv_Objective
spec_abs_graph.QueueLocal_Persistent.
Definition isQueue N γq q : vProp Σ := γa γg,
γq = encode (γa, γg)
sq.(QueueLocal) N γa γg q .
Definition isQueue N γq q : vProp Σ := sq.(QueueLocal) N γq q .
Definition Queue γq (_ : loc) Q : vProp Σ := γa γg G,
γq = encode (γa, γg)
sq.(QueueInv) γa γg Q G.
Definition Queue γq q Q : vProp Σ := G, sq.(QueueInv) γq q Q G.
#[global] Instance Queue_objective γq q Q : Objective (Queue γq q Q) := _.
#[global] Instance Queue_timeless γq q Q : Timeless (Queue γq q Q) := _.
......@@ -29,30 +25,22 @@ Lemma new_queue_spec :
Proof.
iIntros (N tid Φ) "_ Post".
iApply (sq.(spec_abs_graph.new_queue_spec) with "[%//]").
iIntros "!> * [#QL LI]".
remember (encode (γa, γg)) as γq eqn:Hγq.
iApply "Post". iSplit.
- iExists _,_. iFrame (Hγq) "QL".
- iExists _,_,_. iFrame (Hγq) "LI".
iIntros "!> * [#QL LI]". iApply "Post". iFrame "QL". by iExists _.
Qed.
Lemma enqueue_spec :
enqueue_spec' sq.(spec_abs_graph.enqueue) isQueue Queue.
Proof.
intros N DISJ q tid γq V v Posx.
iIntros "#⊒V IQ" (Φ) "AU". iDestruct "IQ" as (? ? Hγq) "#QL".
intros N DISJ q tid γq V v Posx. iIntros "#⊒V #QL" (Φ) "AU".
awp_apply (sq.(spec_abs_graph.enqueue_spec) with "⊒V QL"); [done..|].
iApply (aacc_aupd_commit with "AU"); [done|].
iIntros (Q) ">Q". iDestruct "Q" as (??? Hγq') "QI".
rewrite Hγq in Hγq'; apply (inj encode) in Hγq'; injection Hγq' as [= <- <-].
iIntros (Q) ">Q". iDestruct "Q" as (?) "QI".
iAaccIntro with "QI".
{ iIntros ">QI !>". iSplitL "QI"; [|by auto].
iNext. iExists _,_,_. iFrame (Hγq) "QI". }
{ iIntros ">QI !>". iSplitL "QI"; [|by auto]. iNext. by iExists _. }
iIntros (V' Q' G' enqId enq Venq M') "(>QI & #⊒V' & #QL' & %F) !>".
iDestruct (spec_abs_graph.QueueInv_QueueConsistent with "QI") as %QC.
set (enqE := mkGraphEvent enq Venq M') in *.
iAssert (Queue γq q Q') with "[QI]" as "Q".
{ iExists _,_,_. iFrame (Hγq) "QI". }
iAssert (Queue γq q Q') with "[QI]" as "Q". { by iExists _. }
destruct F as (? & _ & ? & ? & ? & ENQ & HenqId & EsG' & ?).
iExists Venq.(dv_comm), Q'.
iSplitL; [|by auto]. iFrame "Q". iSplitL.
......@@ -67,20 +55,16 @@ Qed.
Lemma dequeue_spec :
dequeue_spec' sq.(spec_abs_graph.dequeue) isQueue Queue.
Proof.
intros N DISJ q tid γq V.
iIntros "#⊒V IQ" (Φ) "AU". iDestruct "IQ" as (? ? Hγq) "#QL".
intros N DISJ q tid γq V. iIntros "#⊒V #QL" (Φ) "AU".
awp_apply (sq.(spec_abs_graph.dequeue_spec) with "⊒V QL"); [done..|].
iApply (aacc_aupd_commit with "AU"); [done|].
iIntros (Q) ">Q". iDestruct "Q" as (??? Hγq') "QI".
rewrite Hγq in Hγq'; apply (inj encode) in Hγq'; injection Hγq' as [= <- <-].
iIntros (Q) ">Q". iDestruct "Q" as (?) "QI".
iAaccIntro with "QI".
{ iIntros ">QI !>". iSplitL "QI"; [|by auto].
iNext. iExists _,_,_. iFrame (Hγq) "QI". }
{ iIntros ">QI !>". iSplitL "QI"; [|by auto]. iNext. by iExists _. }
iIntros (v V' Q' G' enqId deqId enq deq Venq Vdeq M') "(>QI & #⊒V' & #QL' & %F) !>".
iDestruct (spec_abs_graph.QueueInv_QueueConsistent with "QI") as %QC.
set (deqE := mkGraphEvent deq Vdeq M') in *.
iAssert (Queue γq q Q') with "[QI]" as "Q".
{ iExists _,_,_. iFrame (Hγq) "QI". }
iAssert (Queue γq q Q') with "[QI]" as "Q". { by iExists _. }
iAssert (⊒∅)%I as "⊒∅". { iApply monPred_in_bot. }
destruct F as (? & _ & ? & ? & [CASE|CASE]).
- destruct CASE as (-> & ? & ?). iExists v, , Q.
......@@ -101,20 +85,16 @@ Qed.
Lemma try_enq_spec :
try_enq_spec' sq.(spec_abs_graph.try_enq _ _) isQueue Queue.
Proof.
intros N DISJ q tid γq V v Posx.
iIntros "#⊒V IQ" (Φ) "AU". iDestruct "IQ" as (? ? Hγq) "#QL".
intros N DISJ q tid γq V v Posx. iIntros "#⊒V #QL" (Φ) "AU".
awp_apply (sq.(spec_abs_graph.try_enq_spec _ _) with "⊒V QL"); [done..|].
iApply (aacc_aupd_commit with "AU"); [done|].
iIntros (Q) ">Q". iDestruct "Q" as (??? Hγq') "QI".
rewrite Hγq in Hγq'; apply (inj encode) in Hγq'; injection Hγq' as [= <- <-].
iIntros (Q) ">Q". iDestruct "Q" as (?) "QI".
iAaccIntro with "QI".
{ iIntros ">QI !>". iSplitL "QI"; [|by auto].
iNext. iExists _,_,_. iFrame (Hγq) "QI". }
{ iIntros ">QI !>". iSplitL "QI"; [|by auto]. iNext. by iExists _. }
iIntros (b V' Q' G' enqId enq Venq M') "(>QI & #⊒V' & #QL' & %F) !>".
iDestruct (spec_abs_graph.QueueInv_QueueConsistent with "QI") as %QC.
set (enqE := mkGraphEvent enq Venq M') in *.
iAssert (Queue γq q Q') with "[QI]" as "Q".
{ iExists _,_,_. iFrame (Hγq) "QI". }
iAssert (Queue γq q Q') with "[QI]" as "Q". { by iExists _. }
destruct F as (? & _ & ? & ? & CASE). destruct b.
- destruct CASE as (? & ENQ & HenqId & EsG' & ?).
iExists true, Venq.(dv_comm), Q'.
......@@ -134,19 +114,16 @@ Lemma try_deq_spec :
try_deq_spec' sq.(spec_abs_graph.try_deq _ _) isQueue Queue.
Proof.
intros N DISJ q tid γq V.
iIntros "#⊒V IQ" (Φ) "AU". iDestruct "IQ" as (? ? Hγq) "#QL".
iIntros "#⊒V #QL" (Φ) "AU".
awp_apply (sq.(spec_abs_graph.try_deq_spec _ _) with "⊒V QL"); [done..|].
iApply (aacc_aupd_commit with "AU"); [done|].
iIntros (Q) ">Q". iDestruct "Q" as (??? Hγq') "QI".
rewrite Hγq in Hγq'; apply (inj encode) in Hγq'; injection Hγq' as [= <- <-].
iIntros (Q) ">Q". iDestruct "Q" as (?) "QI".
iAaccIntro with "QI".
{ iIntros ">QI !>". iSplitL "QI"; [|by auto].
iNext. iExists _,_,_. iFrame (Hγq) "QI". }
{ iIntros ">QI !>". iSplitL "QI"; [|by auto]. iNext. by iExists _. }
iIntros (v V' Q' G' enqId deqId enq deq Venq Vdeq M') "(>QI & #⊒V' & #QL' & %F) !>".
iDestruct (spec_abs_graph.QueueInv_QueueConsistent with "QI") as %QC.
set (deqE := mkGraphEvent deq Vdeq M') in *.
iAssert (Queue γq q Q') with "[QI]" as "Q".
{ iExists _,_,_. iFrame (Hγq) "QI". }
iAssert (Queue γq q Q') with "[QI]" as "Q". { by iExists _. }
iAssert (⊒∅)%I as "⊒∅". { iApply monPred_in_bot. }
destruct F as (? & _ & ? & ? & [CASE|[CASE|CASE]]).
- destruct CASE as (-> & ? & ->). iExists v, , Q.
......
......@@ -779,15 +779,15 @@ Definition QueueBaseInv sz γq q G : vProp :=
γb n L T, QueueInv_no_exist sz γq q γb n L T G.
(* Only share the ghost state with the client. *)
Definition QueueInv γg G : vProp :=
Definition QueueInv γg (q : loc) G : vProp :=
WeakQueueConsistent G graph_master γg (1/2) G.
#[global] Instance QueueInv_objective γg G : Objective (QueueInv γg G) := _.
#[global] Instance QueueInv_objective γg q G : Objective (QueueInv γg q G) := _.
(* Our internal invariant keeps all the physical resources, as well as enough
ghost resources (`QueueInv`) to maintain agreement with the client. *)
Definition QueueInternalInv sz γq γg q : vProp :=
G, QueueInv γg G QueueBaseInv sz γq q G.
G, QueueInv γg q G QueueBaseInv sz γq q G.
#[global] Instance QueueInternalInv_objective sz γq γg q :
Objective (QueueInternalInv sz γq γg q) := _.
......@@ -1518,13 +1518,13 @@ Local Existing Instances hwq_graphG hwq_queueG.
#[local] Notation vProp := (vProp Σ).
Lemma QueueInv_WeakQueueConsistent_instance :
γg G, QueueInv γg G WeakQueueConsistent G .
γg q G, QueueInv γg q G WeakQueueConsistent G .
Proof. by iIntros "* [$ QI]". Qed.
Lemma QueueInv_graph_master_acc_instance :
γg G, QueueInv γg G
γg q G, QueueInv γg q G
graph_master γg (1/2) G
(graph_master γg (1/2) G - QueueInv γg G).
(graph_master γg (1/2) G - QueueInv γg q G).
Proof. by iIntros "* [$ $] $". Qed.
Lemma QueueLocal_graph_snap_instance sz :
......
......@@ -56,14 +56,14 @@ Proof.
by apply excl_auth_valid.
Qed.
Definition QueueInv1 γg γs : vProp :=
G, msq.(QueueInv) γg G QEAuth γs (to_set G.(Es)).
Definition QueueInv1 q γg γs : vProp :=
G, msq.(QueueInv) γg q G QEAuth γs (to_set G.(Es)).
Local Existing Instances
QueueInv_Objective QueueLocal_Persistent
stack_persistent.
Instance QueueInv_obj γg γs : Objective (QueueInv1 γg γs) := _.
Instance QueueInv_obj q γg γs : Objective (QueueInv1 q γg γs) := _.
Definition StackInv q γg γs (v : Z) : vProp :=
(if decide (v = 2)
......@@ -91,7 +91,7 @@ Proof using All.
wp_apply (new_stack_spec _ (StackInv q γg γs) with "[//]").
iIntros (s) "#S".
wp_let.
iMod (inv_alloc (mpN .@ "inv") _ (QueueInv1 γg γs) with "[QI QA]") as "#I".
iMod (inv_alloc (mpN .@ "inv") _ (QueueInv1 q γg γs) with "[QI QA]") as "#I".
{ iNext. iExists _. by iFrame "QI QA". }
(* forking *)
wp_apply (wp_fork with "[nodes]"); first auto.
......
......@@ -45,15 +45,15 @@ Proof.
destruct ge; apply _.
Qed.
Definition QueuePerElemInv P γg : vProp :=
G, msq.(QueueInv) γg G queue_resources P G.
Definition QueuePerElemInv P γg q : vProp :=
G, msq.(QueueInv) γg q G queue_resources P G.
Local Existing Instance QueueInv_Objective.
Instance QueuePerElemInv_objective P γg : Objective (QueuePerElemInv P γg) := _.
Instance QueuePerElemInv_objective P γg q : Objective (QueuePerElemInv P γg q) := _.
Definition QueuePerElem N P γg q : vProp :=
G M, msq.(QueueLocal) (N .@ "que") γg q G M
inv (N .@ "iinv") (QueuePerElemInv P γg).
inv (N .@ "iinv") (QueuePerElemInv P γg q).
(* TODO: we can prove logically-atomic spec here. *)
Lemma per_elem_enqueue N P γg q (x: Z) tid (DISJ: N ## histN) (NZ: 0 < x) :
......
......@@ -11,12 +11,9 @@ Local Open Scope Z_scope.
Local Notation graph := (graph qevent).
Implicit Type (Q : queue) (G : graph) (M : logView).
(** Queue predicates *)
Definition QueueLocalT Σ : Type :=
namespace gname gname loc graph logView vProp Σ.
(** Queue predicate with abstract state *)
Definition QueueInvT Σ : Type :=
gname gname queue graph vProp Σ.
gname loc queue graph vProp Σ.
(** Operation specs *)
Definition new_queue_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
......@@ -24,20 +21,20 @@ Definition new_queue_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
N tid,
{{{ True }}}
new_queue [] @ tid;
{{{ γa γg (q: loc), RET #q; QueueLocal N γa γg q QueueInv γa γg [] }}}.
{{{ γg (q: loc), RET #q; QueueLocal N γg q QueueInv γg q [] }}}.
Definition enqueue_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
(enqueue : val) (QueueLocal : QueueLocalT Σ) (QueueInv : QueueInvT Σ) : Prop :=
N (DISJ: N ## histN) (q : loc) tid γa γg G1 M (V : view) (v : Z) (Posx: 0 < v),
N (DISJ: N ## histN) (q : loc) tid γg G1 M (V : view) (v : Z) (Posx: 0 < v),
(* PRIVATE PRE *)
V - QueueLocal N γa γg q G1 M - (* G1 is a snapshot of the graph, locally observed by M *)
V - QueueLocal N γg q G1 M - (* G1 is a snapshot of the graph, locally observed by M *)
(* PUBLIC PRE *)
<<< Q G, QueueInv γa γg Q G >>>
<<< Q G, QueueInv γg q Q G >>>
enqueue [ #q ; #v] @ tid; N
<<< V' Q' G' (enqId : event_id) enq Venq M',
(* PUBLIC POST *)
QueueInv γa γg Q' G'
V' @{V'} QueueLocal N γa γg q G' M'
QueueInv γg q Q' G'
V' @{V'} QueueLocal N γg q G' M'
G G' M M'
V Venq.(dv_in) Venq.(dv_wrt) = V'
Q' = Q ++ [(v, Venq.(dv_comm))]
......@@ -55,16 +52,16 @@ Definition enqueue_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
Definition dequeue_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
(dequeue : val) (QueueLocal : QueueLocalT Σ) (QueueInv : QueueInvT Σ) : Prop :=
N (DISJ: N ## histN) (q : loc) tid γa γg G1 M V,
N (DISJ: N ## histN) (q : loc) tid γg G1 M V,
(* PRIVATE PRE *)
V - QueueLocal N γa γg q G1 M -
V - QueueLocal N γg q G1 M -
(* PUBLIC PRE *)
<<< Q G, QueueInv γa γg Q G >>>
<<< Q G, QueueInv γg q Q G >>>
dequeue [ #q] @ tid; N
<<< (v: Z) V' Q' G' enqId deqId enq deq Venq Vdeq M',
(* PUBLIC POST *)
QueueInv γa γg Q' G'
V' @{V'} QueueLocal N γa γg q G' M'
QueueInv γg q Q' G'
V' @{V'} QueueLocal N γg q G' M'
G G' M M'
V Vdeq.(dv_in) Vdeq.(dv_comm) = V'
( (* EMPTY case *)
......@@ -92,16 +89,16 @@ Definition dequeue_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
Definition try_enq_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
(try_enq : val) (QueueLocal : QueueLocalT Σ) (QueueInv : QueueInvT Σ) : Prop :=
N (DISJ: N ## histN) (q : loc) tid γa γg G1 M (V : view) (v : Z) (Posx: 0 < v),
N (DISJ: N ## histN) (q : loc) tid γg G1 M (V : view) (v : Z) (Posx: 0 < v),
(* PRIVATE PRE *)
V - QueueLocal N γa γg q G1 M -
V - QueueLocal N γg q G1 M -
(* PUBLIC PRE *)
<<< Q G, QueueInv γa γg Q G >>>
<<< Q G, QueueInv γg q Q G >>>
try_enq [ #q ; #v] @ tid; N
<<< (b: bool) V' Q' G' (enqId : event_id) enq Venq M',
(* PUBLIC POST *)
(QueueInv γa γg Q' G')
V' @{V'} QueueLocal N γa γg q G' M'
(QueueInv γg q Q' G')
V' @{V'} QueueLocal N γg q G' M'
G G' M M'
V Venq.(dv_in) Venq.(dv_wrt) = V'
if b is false then
......@@ -120,16 +117,16 @@ Definition try_enq_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
Definition try_deq_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
(try_deq : val) (QueueLocal : QueueLocalT Σ) (QueueInv : QueueInvT Σ) : Prop :=
N (DISJ: N ## histN) (q : loc) tid γa γg G1 M V,
N (DISJ: N ## histN) (q : loc) tid γg G1 M V,
(* PRIVATE PRE *)
V - QueueLocal N γa γg q G1 M -
V - QueueLocal N γg q G1 M -
<<< (* PUBLIC PRE *)
Q G, (QueueInv γa γg Q G) >>>
Q G, (QueueInv γg q Q G) >>>
try_deq [ #q] @ tid; N
<<< (v: Z) V' Q' G' enqId deqId enq deq Venq Vdeq M',
(* PUBLIC POST *)
(QueueInv γa γg Q' G')
V' @{V'} QueueLocal N γa γg q G' M'
(QueueInv γg q Q' G')
V' @{V'} QueueLocal N γg q G' M'
G G' M M'
V Vdeq.(dv_in) Vdeq.(dv_comm) = V'
(* FAIL case *)
......@@ -167,17 +164,17 @@ Record core_queue_spec {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
QueueLocal : QueueLocalT Σ;
QueueInv : QueueInvT Σ;
(** predicates properties *)
QueueInv_Timeless : γa γg Q G, Timeless (QueueInv γa γg Q G);
QueueInv_Objective : γa γg Q G, Objective (QueueInv γa γg Q G);
QueueInv_QueueConsistent : γa γg Q G, QueueInv γa γg Q G QueueConsistent G ;
QueueInv_Timeless : γg q Q G, Timeless (QueueInv γg q Q G);
QueueInv_Objective : γg q Q G, Objective (QueueInv γg q Q G);
QueueInv_QueueConsistent : γg q Q G, QueueInv γg q Q G QueueConsistent G ;
QueueInv_graph_master_acc :
γa γg Q G, QueueInv γa γg Q G graph_master γg (1/2) G
(graph_master γg (1/2) G - QueueInv γa γg Q G);
γg q Q G, QueueInv γg q Q G graph_master γg (1/2) G
(graph_master γg (1/2) G - QueueInv γg q Q G);
QueueLocal_graph_snap :
N γa γg q G M, QueueLocal N γa γg q G M graph_snap γg G M;
N γg q G M, QueueLocal N γg q G M graph_snap γg G M;
QueueLocal_Persistent :
N γa γg q G M, Persistent (QueueLocal N γa γg q G M);
N γg q G M, Persistent (QueueLocal N γg q G M);
(* operations specs *)
new_queue_spec : new_queue_spec' new_queue QueueLocal QueueInv;
......
......@@ -19,7 +19,7 @@ Definition unmatched_enq G eid : Prop :=
Definition QueueLocalT Σ : Type :=
namespace gname loc graph logView vProp Σ.
Definition QueueInvT Σ : Type :=
gname graph vProp Σ.
gname loc graph vProp Σ.
(** Operation specs *)
......@@ -28,7 +28,7 @@ Definition new_queue_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
N tid,
{{{ True }}}
new_queue [] @ tid;
{{{ γg (q: loc), RET #q; QueueLocal N γg q QueueInv γg }}}.
{{{ γg (q: loc), RET #q; QueueLocal N γg q QueueInv γg q }}}.
Definition enqueue_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
(enqueue : val) (QueueLocal : QueueLocalT Σ) (QueueInv : QueueInvT Σ) : Prop :=
......@@ -36,11 +36,11 @@ Definition enqueue_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
(* PRIVATE PRE *)
V - QueueLocal N γg q G1 M - (* G1 is a snapshot of the graph, locally observed by M *)
(* PUBLIC PRE *)
<<< G, QueueInv γg G >>>
<<< G, QueueInv γg q G >>>
enqueue [ #q ; #v] @ tid; N
<<< V' G' (enqId : event_id) enq Venq M',
(* PUBLIC POST *)
QueueInv γg G'
QueueInv γg q G'
V' @{V'} QueueLocal N γg q G' M'
G G' M M'
V Venq.(dv_in) Venq.(dv_wrt) = V'
......@@ -62,11 +62,11 @@ Definition dequeue_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
(* PRIVATE PRE *)
V - QueueLocal N γg q G1 M -
(* PUBLIC PRE *)
<<< G, QueueInv γg G >>>
<<< G, QueueInv γg q G >>>
dequeue [ #q] @ tid; N
<<< (v: Z) V' G' enqId deqId enq deq Vdeq M',
(* PUBLIC POST *)
QueueInv γg G'
QueueInv γg q G'
V' @{V'} QueueLocal N γg q G' M'
G G' M M'
V Vdeq.(dv_in) Vdeq.(dv_comm) = V'
......@@ -96,11 +96,11 @@ Definition try_enq_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
(* PRIVATE PRE *)
V - QueueLocal N γg q G1 M -
(* PUBLIC PRE *)
<<< G, QueueInv γg G >>>
<<< G, QueueInv γg q G >>>
try_enq [ #q ; #v] @ tid; N
<<< (b: bool) V' G' (enqId : event_id) enq Venq M',
(* PUBLIC POST *)
(QueueInv γg G')
(QueueInv γg q G')
V' @{V'} QueueLocal N γg q G' M'
G G' M M'
V Venq.(dv_in) Venq.(dv_wrt) = V'
......@@ -123,11 +123,11 @@ Definition try_deq_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
(* PRIVATE PRE *)
V - QueueLocal N γg q G1 M -
<<< (* PUBLIC PRE *)
G, (QueueInv γg G) >>>
G, (QueueInv γg q G) >>>
try_deq [ #q] @ tid; N
<<< (v: Z) V' G' enqId deqId enq deq Vdeq M',
(* PUBLIC POST *)
(QueueInv γg G')
(QueueInv γg q G')
V' @{V'} QueueLocal N γg q G' M'
G G' M M'
V Vdeq.(dv_in) Vdeq.(dv_comm) = V'
......@@ -163,12 +163,12 @@ Record core_queue_spec {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
QueueLocal : QueueLocalT Σ;
QueueInv : QueueInvT Σ;
(** predicates properties *)
QueueInv_Timeless : γg G, Timeless (QueueInv γg G);
QueueInv_Objective : γg G, Objective (QueueInv γg G);
QueueInv_QueueConsistent : γg G, QueueInv γg G QueueConsistent G ;
QueueInv_Timeless : γg q G, Timeless (QueueInv γg q G);
QueueInv_Objective : γg q G, Objective (QueueInv γg q G);
QueueInv_QueueConsistent : γg q G, QueueInv γg q G QueueConsistent G ;
QueueInv_graph_master_acc :
γg G, QueueInv γg G graph_master γg (1/2) G
(graph_master γg (1/2) G - QueueInv γg G);
γg q G, QueueInv γg q G graph_master γg (1/2) G
(graph_master γg (1/2) G - QueueInv γg q G);
QueueLocal_graph_snap :
N γg q G M, QueueLocal N γg q G M graph_snap γg G M;
......
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