Commit 5c4b39ff authored by Hai Dang's avatar Hai Dang
Browse files

Merge branch 'jaehwang/hybrid' into 'graphs_multi'

hybrid spec & abstract state spec of queue

See merge request !24
parents c0dd63f2 4dc23f25
......@@ -152,12 +152,18 @@ theories/examples/queue/spec_per_elem.v
theories/examples/queue/code_ms.v
theories/examples/queue/code_hw.v
theories/examples/queue/code_producer_consumer.v
theories/examples/queue/event.v
theories/examples/queue/spec_graph.v
theories/examples/queue/proof_ms_gps.v
theories/examples/queue/proof_ms_graph.v
theories/examples/queue/spec_abs.v
theories/examples/queue/spec_abs_graph.v
theories/examples/queue/proof_abs_graph_abs.v
theories/examples/queue/proof_abs_graph_graph.v
theories/examples/queue/proof_hw_graph.v
theories/examples/queue/proof_per_elem_graph.v
theories/examples/queue/proof_mp_graph.v
theories/examples/queue/proof_ms_abs_graph.v
theories/examples/queue/proof_ms_closed.v
theories/examples/queue/proof_ms_gps.v
## Chase-Lev Double-ended Queue
theories/examples/chase_lev/code.v
## Exchanger
......
From stdpp Require Import countable.
From gpfsl.lang Require Import lang.
Require Import iris.prelude.options.
(** Abstract state of queue *)
Definition queue := list (Z * view).
(** Queue events *)
Inductive qevent := Enq (v : Z) | Deq (v : Z) | EmpDeq (* | FAIL_DEQ *).
Notation dummy_qevt := (Enq 0).
Local Open Scope Z_scope.
Instance qevent_eq_dec : EqDecision qevent.
Proof. solve_decision. Defined.
Instance qevent_countable : Countable qevent.
Proof.
refine (
inj_countable'
(λ e, match e with
| Enq v => (1, v)
| Deq v => (2, v)
| EmpDeq => (3, 0) end)
(λ x, match x with
| (1, v) => Enq v
| (2, v) => Deq v
| _ => EmpDeq end) _);
by intros [].
Qed.
Definition is_enqueue e v : Prop := e = Enq v.
Definition is_dequeue e v : Prop := e = Deq v.
Definition is_maybe_dequeue e : Prop :=
match e with | Enq _ => False | _ => True end.
From gpfsl.logic Require Import logatom proofmode.
From gpfsl.examples.queue Require Export event spec_abs_graph spec_abs.
Require Import iris.prelude.options.
Local Open Scope Z_scope.
Section abs_graph.
Context `{!noprolG Σ, !inG Σ (graphR qevent)}.
(* We only need an extended spec with Weak Consistency *)
Context (weq : spec_abs_graph.extended_queue_spec Σ WeakQueueConsistent).
Local Existing Instances
spec_abs_graph.QueueInv_Timeless spec_abs_graph.QueueInv_Objective
spec_abs_graph.QueueLocal_Persistent.
Definition isQueue N γq q : vProp Σ := weq.(QueueLocal) N γq q .
Definition Queue γq q Q : vProp Σ := G, weq.(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) := _.
#[global] Instance isQueue_persistent N γq q : Persistent (isQueue N γq q) := _.
Lemma new_queue_spec :
new_queue_spec' weq.(spec_abs_graph.new_queue) isQueue Queue.
Proof.
iIntros (N tid Φ) "_ Post".
iApply (weq.(spec_abs_graph.new_queue_spec) with "[%//]").
iIntros "!> * [#QL LI]". iApply "Post". iFrame "QL". by iExists _.
Qed.
Lemma enqueue_spec :
enqueue_spec' weq.(spec_abs_graph.enqueue) isQueue Queue.
Proof.
intros N DISJ q tid γq V v Posx. iIntros "#⊒V #QL" (Φ) "AU".
awp_apply (weq.(spec_abs_graph.enqueue_spec) with "⊒V QL"); [done..|].
iApply (aacc_aupd_commit with "AU"); [done|].
iIntros (Q) ">Q". iDestruct "Q" as (?) "QI".
iAaccIntro with "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". { by iExists _. }
destruct F as (? & _ & ? & ? & ? & ENQ & HenqId & EsG' & ?).
iExists Venq.(dv_comm), Q'.
iSplitL; [|by auto]. iFrame "Q". iSplitL.
+ subst V'. iApply (monPred_in_mono with "⊒V'"). simpl.
change (enqE.(ge_view).(dv_comm) enqE.(ge_view).(dv_wrt)).
apply: QC.(wkq_cons_enqueue_release G').
* rewrite EsG'. apply lookup_app_1_eq.
* by exists v.
+ iPureIntro. split; [|done]. trans Venq.(dv_in); [done|]. apply dv_in_com.
Qed.
Lemma dequeue_spec :
dequeue_spec' weq.(spec_abs_graph.dequeue) isQueue Queue.
Proof.
intros N DISJ q tid γq V. iIntros "#⊒V #QL" (Φ) "AU".
awp_apply (weq.(spec_abs_graph.dequeue_spec) with "⊒V QL"); [done..|].
iApply (aacc_aupd_commit with "AU"); [done|].
iIntros (Q) ">Q". iDestruct "Q" as (?) "QI".
iAaccIntro with "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". { by iExists _. }
iAssert (⊒∅)%I as "⊒∅". { iApply monPred_in_bot. }
destruct F as (? & _ & ? & ? & [CASE|CASE]).
- destruct CASE as (-> & ? & ?). iExists v, , Q.
iSplitL; [|by auto]. iFrame "Q ⊒∅". iPureIntro. by left.
- destruct CASE as (-> & ? & ENQ & DEQ & ? & ? & EsG' & SoG' & ComG' & ? & ? & ?
& enqE & ? & ? & ? & ?).
rewrite /is_enqueue in ENQ. rewrite /is_dequeue in DEQ. subst enq deq.
iExists v, Venq.(dv_comm), Q'.
iSplitL; [|by auto]. iFrame "Q". iSplitL.
{ iDestruct (view_at_elim with "⊒V' QL'") as "{QL QL'} QL'".
rewrite QueueLocal_graph_snap.
iApply (graph_snap_lookup _ _ _ enqId with "QL'"); [|done].
apply list_lookup_fmap_inv'. exists enqE. split; [done|].
eapply prefix_lookup; [done|by eexists]. }
iPureIntro. by right.
Qed.
Lemma try_enq_spec :
try_enq_spec' weq.(spec_abs_graph.try_enq) isQueue Queue.
Proof.
intros N DISJ q tid γq V v Posx. iIntros "#⊒V #QL" (Φ) "AU".
awp_apply (weq.(spec_abs_graph.try_enq_spec) with "⊒V QL"); [done..|].
iApply (aacc_aupd_commit with "AU"); [done|].
iIntros (Q) ">Q". iDestruct "Q" as (?) "QI".
iAaccIntro with "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". { by iExists _. }
destruct F as (? & _ & ? & ? & CASE). destruct b.
- destruct CASE as (? & ENQ & HenqId & EsG' & ?).
iExists true, Venq.(dv_comm), Q'.
iSplitL; [|by auto]. iFrame "Q". iSplitL.
+ subst V'. iApply (monPred_in_mono with "⊒V'"). simpl.
change (enqE.(ge_view).(dv_comm) enqE.(ge_view).(dv_wrt)).
apply: QC.(wkq_cons_enqueue_release G').
* rewrite EsG'. apply lookup_app_1_eq.
* by exists v.
+ iPureIntro. split; [|done]. trans Venq.(dv_in); [done|]. apply dv_in_com.
- destruct CASE as [-> ->].
iExists false, V, Q.
iSplitL; [|by auto]. iFrame "Q ⊒V". done.
Qed.
Lemma try_deq_spec :
try_deq_spec' weq.(spec_abs_graph.try_deq) isQueue Queue.
Proof.
intros N DISJ q tid γq V.
iIntros "#⊒V #QL" (Φ) "AU".
awp_apply (weq.(spec_abs_graph.try_deq_spec) with "⊒V QL"); [done..|].
iApply (aacc_aupd_commit with "AU"); [done|].
iIntros (Q) ">Q". iDestruct "Q" as (?) "QI".
iAaccIntro with "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". { by iExists _. }
iAssert (⊒∅)%I as "⊒∅". { iApply monPred_in_bot. }
destruct F as (? & _ & ? & ? & [CASE|[CASE|CASE]]).
- destruct CASE as (-> & ? & ->). iExists v, , Q.
iSplitL; [|by auto]. iFrame "Q ⊒∅". iPureIntro. by left.
- destruct CASE as (-> & ? & ?). iExists v, , Q.
iSplitL; [|by auto]. iFrame "Q ⊒∅". iPureIntro. by right; left.
- destruct CASE as (-> & ? & ENQ & DEQ & ? & ? & EsG' & SoG' & ComG' & ? & ? & ?
& enqE & ? & ? & ? & ?).
rewrite /is_enqueue in ENQ. rewrite /is_dequeue in DEQ. subst enq deq.
iExists v, Venq.(dv_comm), Q'.
iSplitL; [|by auto]. iFrame "Q". iSplitL.
{ iDestruct (view_at_elim with "⊒V' QL'") as "{QL QL'} QL'".
rewrite QueueLocal_graph_snap.
iApply (graph_snap_lookup _ _ _ enqId with "QL'"); [|done].
apply list_lookup_fmap_inv'. exists enqE. split; [done|].
eapply prefix_lookup; [done|by eexists]. }
iPureIntro. by right; right.
Qed.
End abs_graph.
Definition abs_graph_abs_queue_spec
Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
(weq : spec_abs_graph.extended_queue_spec Σ WeakQueueConsistent) : queue_spec Σ := {|
spec_abs.Queue := Queue weq ;
spec_abs.isQueue := isQueue weq ;
spec_abs.Queue_Objective := Queue_objective weq ;
spec_abs.Queue_Timeless := Queue_timeless weq ;
spec_abs.isQueue_Persistent := isQueue_persistent weq ;
spec_abs.new_queue_spec := new_queue_spec weq ;
spec_abs.enqueue_spec := enqueue_spec weq ;
spec_abs.dequeue_spec := dequeue_spec weq ;
spec_abs.try_enq_spec := try_enq_spec weq ;
spec_abs.try_deq_spec := try_deq_spec weq ;
|}%I.
From gpfsl.logic Require Import logatom proofmode.
From gpfsl.examples.queue Require Export event spec_abs_graph spec_graph.
Require Import iris.prelude.options.
Local Open Scope Z_scope.
Section abs_graph.
Context `{!noprolG Σ, !inG Σ (graphR qevent)}.
Context `(sq : spec_abs_graph.extended_queue_spec Σ QueueConsistent).
Local Existing Instances
spec_abs_graph.QueueInv_Timeless spec_abs_graph.QueueInv_Objective
spec_abs_graph.QueueLocal_Persistent.
Definition QueueInv γg q G : vProp Σ := Q, sq.(spec_abs_graph.QueueInv) γg q Q G.
Definition QueueLocal N γg q G M : vProp Σ := sq.(spec_abs_graph.QueueLocal) N γg q G M.
#[global] Instance QueueInv_objective γg q Q : Objective (QueueInv γg q Q) := _.
#[global] Instance QueueInv_timeless γg q Q : Timeless (QueueInv γg q Q) := _.
#[global] Instance QueueLocal_persistent N γg q G M : Persistent (QueueLocal N γg q G M) := _.
Lemma QueueInv_StrongQueueConsistent_instance :
γg q G, QueueInv γg q G QueueConsistent G .
Proof.
intros. iDestruct 1 as (?) "QI".
by iApply sq.(spec_abs_graph.QueueInv_QueueConsistent).
Qed.
Lemma QueueInv_graph_master_acc_instance :
γg q G, QueueInv γg q G
graph_master γg (1/2) G
(graph_master γg (1/2) G - QueueInv γg q G).
Proof.
intros. iDestruct 1 as (?) "QI".
iDestruct (sq.(spec_abs_graph.QueueInv_graph_master_acc) with "QI") as "[$ Close]".
iIntros "Gm". iSpecialize ("Close" with "Gm"). by iExists Q.
Qed.
Lemma QueueLocal_graph_snap_instance :
N γg q G M, QueueLocal N γg q G M graph_snap γg G M.
Proof. intros. by iApply sq.(spec_abs_graph.QueueLocal_graph_snap). Qed.
Lemma new_queue_spec :
new_queue_spec' sq.(spec_abs_graph.new_queue) QueueLocal QueueInv.
Proof.
iIntros (N tid Φ) "_ Post".
iApply (sq.(spec_abs_graph.new_queue_spec) with "[%//]").
iIntros "!> * [#QL LI]". iApply "Post". iFrame "QL". by iExists _.
Qed.
Lemma enqueue_spec :
enqueue_spec' sq.(spec_abs_graph.enqueue) QueueLocal QueueInv.
Proof.
intros N DISJ q tid γg G1 M 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 (G) ">QI". iDestruct "QI" as (?) "QI".
iAaccIntro with "QI".
{ iIntros ">QI !>". iSplitL "QI"; [|by auto]. iNext. by iExists _. }
iIntros (V' Q' G' enqId enq Venq M') "(>QI & #⊒V' & #QL' & %F) !>".
iAssert (QueueInv γg q G') with "[QI]" as "QI". { by iExists _. }
destruct F as (? & ? & ? & ? & ? & ENQ & HenqId & EsG' & ? & ? & ? & ?).
iExists V', G', enqId, enq, Venq, M'. iFrame "QI QL' ⊒V'". auto.
Qed.
Lemma dequeue_spec :
dequeue_spec' sq.(spec_abs_graph.dequeue) QueueLocal QueueInv.
Proof.
intros N DISJ q tid γg G1 M 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 (G) ">QI". iDestruct "QI" as (?) "QI".
iAaccIntro with "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) !>".
iAssert (QueueInv γg q G') with "[QI]" as "QI". { by iExists _. }
iExists v, V', G', enqId, deqId, enq, deq, Vdeq. iExists M'.
iFrame "QI QL' ⊒V'". iSplit; [|by auto]. iPureIntro. naive_solver.
Qed.
Lemma try_enq_spec :
try_enq_spec' sq.(spec_abs_graph.try_enq) QueueLocal QueueInv.
Proof.
intros N DISJ q tid γg G1 M 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 (G) ">QI". iDestruct "QI" as (?) "QI".
iAaccIntro with "QI".
{ iIntros ">QI !>". iSplitL "QI"; [|by auto]. iNext. by iExists _. }
iIntros (b V' Q' G' enqId enq Venq M') "(>QI & #⊒V' & #QL' & %F) !>".
iAssert (QueueInv γg q G') with "[QI]" as "QI". { by iExists _. }
destruct F as (? & ? & ? & ? & ?).
iExists b, V', G', enqId, enq, Venq, M'. iFrame "QI QL' ⊒V'".
iSplitL; [|by auto]. iPureIntro. destruct b; naive_solver.
Qed.
Lemma try_deq_spec :
try_deq_spec' sq.(spec_abs_graph.try_deq) QueueLocal QueueInv.
Proof.
intros N DISJ q tid γg G1 M V. 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 (G) ">QI". iDestruct "QI" as (?) "QI".
iAaccIntro with "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) !>".
iAssert (QueueInv γg q G') with "[QI]" as "QI". { by iExists _. }
iExists v, V', G', enqId, deqId, enq, deq, Vdeq. iExists M'.
iFrame "QI QL' ⊒V'". iSplit; [|by auto]. iPureIntro. naive_solver.
Qed.
End abs_graph.
Definition abs_graph_graph_extended_queue_spec
Σ `{!noprolG Σ, !inG Σ (graphR qevent)} {QC}
(sq : spec_abs_graph.extended_queue_spec Σ QC)
: spec_graph.extended_queue_spec Σ QC := {|
spec_graph.extended_core_spec := {|
spec_graph.QueueInv_Objective := QueueInv_objective sq ;
spec_graph.QueueInv_Timeless := QueueInv_timeless sq ;
spec_graph.QueueLocal_Persistent := QueueLocal_persistent sq ;
spec_graph.QueueInv_QueueConsistent := QueueInv_StrongQueueConsistent_instance sq;
spec_graph.QueueInv_graph_master_acc := QueueInv_graph_master_acc_instance sq ;
spec_graph.QueueLocal_graph_snap := QueueLocal_graph_snap_instance sq ;
spec_graph.new_queue_spec := new_queue_spec sq ;
spec_graph.enqueue_spec := enqueue_spec sq ;
spec_graph.dequeue_spec := dequeue_spec sq ;
|} ;
spec_graph.try_enq_spec := try_enq_spec sq ;
spec_graph.try_deq_spec := try_deq_spec sq ;
|}%I.
......@@ -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.
......
From gpfsl.base_logic Require Import history. (* << for noprolG *)
From gpfsl.logic Require Import atomics.
From gpfsl.examples.queue Require Import
proof_abs_graph_abs proof_abs_graph_graph proof_ms_abs_graph.
Definition msqueue_impl_abs_graph_strong
Σ `{!noprolG Σ, !msqueueG Σ, !atomicG Σ} :
spec_abs_graph.strong_queue_spec Σ := {|
spec_abs_graph.extended_core_spec := {|
spec_abs_graph.QueueInv_Objective := QueueInv_objective;
spec_abs_graph.QueueInv_QueueConsistent := QueueInv_StrongQueueConsistent_instance;
spec_abs_graph.QueueInv_graph_master_acc := QueueInv_graph_master_acc_instance;
spec_abs_graph.QueueLocal_graph_snap := QueueLocal_graph_snap_instance;
spec_abs_graph.QueueLocal_Persistent := QueueLocal_persistent;
spec_abs_graph.new_queue_spec := new_queue_spec;
spec_abs_graph.enqueue_spec := enqueue_spec;
spec_abs_graph.dequeue_spec := dequeue_spec;
|} ;
spec_abs_graph.try_enq_spec := try_enq_spec;
spec_abs_graph.try_deq_spec := try_deq_spec;
|}.
Definition msqueue_impl_abs_graph_weak Σ `{!noprolG Σ, !msqueueG Σ, !atomicG Σ} :
spec_abs_graph.weak_queue_spec Σ :=
spec_abs_graph.strong_weak_queue_spec Σ (msqueue_impl_abs_graph_strong _).
Definition msqueue_impl_graph_strong Σ `{!noprolG Σ, !msqueueG Σ, !atomicG Σ} :
spec_graph.strong_queue_spec Σ :=
proof_abs_graph_graph.abs_graph_graph_extended_queue_spec Σ
(msqueue_impl_abs_graph_strong Σ).
Definition msqueue_impl_graph_weak Σ `{!noprolG Σ, !msqueueG Σ, !atomicG Σ} :
spec_graph.weak_queue_spec Σ :=
proof_abs_graph_graph.abs_graph_graph_extended_queue_spec Σ
(extended_strong_weak_queue_spec Σ (msqueue_impl_abs_graph_strong Σ)).
Definition msqueue_impl_abs Σ `{!noprolG Σ, !msqueueG Σ, !atomicG Σ} :
spec_abs.queue_spec Σ :=
proof_abs_graph_abs.abs_graph_abs_queue_spec Σ
(extended_strong_weak_queue_spec Σ (msqueue_impl_abs_graph_strong Σ)).
......@@ -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) :
......@@ -247,13 +247,14 @@ Qed.
End RSL.
From gpfsl.logic Require Import atomic_cmra.
From gpfsl.examples.queue Require Import code_ms proof_ms_graph.
From gpfsl.examples.queue Require Import code_ms proof_ms_abs_graph proof_ms_closed.
(* This proof can also be derived from spec_abs. *)
(* TODO: use ther spec_per_elem one. Need try_enq and try_deq *)
Section RSL_instance.
Context {Σ : gFunctors} `{noprolG Σ, !msqueueG Σ, !atomicG Σ}.
Let is_queue := QueuePerElem (msqueue_impl_weak Σ).
Let is_queue := QueuePerElem (msqueue_impl_graph_weak Σ).
Lemma per_elem_enqueue_inst N P γg q (x: Z) tid
(NZ: (0 < x)%Z) (DISJ: N ## histN) :
......
From stdpp Require Import namespaces.
From gpfsl.logic Require Import logatom.
From gpfsl.examples.queue Require Export event spec_abs_graph.
Require Import iris.prelude.options.
Local Open Scope Z_scope.
Implicit Type (Q : queue) (N : namespace).
(** * Abstract State Specs, similar to Cosmo style. *)
(** Queue predicates *)
Definition isQueueT Σ : Type := namespace gname loc vProp Σ.
Definition QueueT Σ : Type := gname loc queue vProp Σ.
(** Operation specs *)
Definition new_queue_spec' {Σ} `{!noprolG Σ}
(new_queue : val) (isQueue : isQueueT Σ) (Queue : QueueT Σ) : Prop :=
N tid,
{{{ True }}}
new_queue [] @ tid;
{{{ γq (q: loc), RET #q; isQueue N γq q Queue γq q [] }}}.
Definition enqueue_spec' {Σ} `{!noprolG Σ}
(enqueue : val) (isQueue : isQueueT Σ) (Queue : QueueT Σ) : Prop :=
N (DISJ: N ## histN) (q : loc) tid γq (V