Commit 123c00a1 authored by Jaehwang Jung's avatar Jaehwang Jung
Browse files

prove spec_abs_graph for msqueue

parent b206e119
......@@ -154,8 +154,9 @@ 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/spec_abs_graph.v
theories/examples/queue/proof_ms_gps.v
theories/examples/queue/proof_ms_graph.v
theories/examples/queue/proof_ms_abs_graph.v
theories/examples/queue/proof_hw_graph.v
theories/examples/queue/proof_per_elem_graph.v
theories/examples/queue/proof_mp_graph.v
......
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).
......
From stdpp Require Import namespaces.
From gpfsl.logic Require Import logatom.
From gpfsl.examples.graph Require Export spec.
From gpfsl.examples.queue Require Export event spec_graph.
Require Import iris.prelude.options.
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 Σ.
Definition QueueInvT Σ : Type :=
gname gname queue graph vProp Σ.
(** Operation specs *)
Definition new_queue_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
(new_queue : val) (QueueLocal : QueueLocalT Σ) (QueueInv : QueueInvT Σ) : Prop :=
N tid,
{{{ True }}}
new_queue [] @ tid;
{{{ γa γg (q: loc), RET #q; QueueLocal N γa γg q QueueInv γa γg [] }}}.
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),
(* PRIVATE PRE *)
V - QueueLocal N γa γg q G1 M - (* G1 is a snapshot of the graph, locally observed by M *)
(* PUBLIC PRE *)
<<< Q G, QueueInv γa γg 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'
G G' M M'
V Venq.(dv_in) Venq.(dv_wrt) = V'
Q' = Q ++ [(v, Venq.(dv_comm))]
(* enq is a new enqueue event with which G' strictly extends G *)
is_enqueue enq v
enqId = length G.(Es)
G'.(Es) = G.(Es) ++ [mkGraphEvent enq Venq M']
G'.(so) = G.(so) G'.(com) = G.(com)
enqId M' (* << M' may also acquire more events that
come with the Enqueue (acquired by reading the Head pointer). *)
enqId M ,
(* RETURN VALUE AT COMMITTING POINT *)
RET #, emp >>>
.
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,
(* PRIVATE PRE *)
V - QueueLocal N γa γg q G1 M -
(* PUBLIC PRE *)
<<< Q G, QueueInv γa γg 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'
G G' M M'
V Vdeq.(dv_in) Vdeq.(dv_comm) = V'
( (* EMPTY case *)
( Q' = Q
v = 0 deq = EmpDeq
deqId = length G.(Es)
G'.(Es) = G.(Es) ++ [mkGraphEvent deq Vdeq M']
G'.(so) = G.(so) G'.(com) = G.(com)
{[deqId]} M M' deqId M)
(* successful case *)
(Q = (v, Venq.(dv_comm)) :: Q'
0 < v is_enqueue enq v is_dequeue deq v
deqId = length G.(Es)
( id, (enqId, id) G.(so))
G'.(Es) = G.(Es) ++ [mkGraphEvent deq Vdeq M']
G'.(so) = {[(enqId, deqId)]} G.(so)
G'.(com) = {[(enqId, deqId)]} G.(com)
enqId M' deqId M' deqId M
eV, G.(Es) !! enqId = Some eV eV.(ge_event) = enq
eV.(ge_view) = Venq eV.(ge_lview) M') ) ,
(* RETURN VALUE AT COMMITTING POINT *)
RET #v, emp >>>
.
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),
(* PRIVATE PRE *)
V - QueueLocal N γa γg q G1 M -
(* PUBLIC PRE *)
<<< Q G, QueueInv γa γg 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'
G G' M M'
V Venq.(dv_in) Venq.(dv_wrt) = V'
if b is false then
Q' = Q G' = G
else
(* enq is a new enqueue event with which G' strictly extends G *)
Q' = Q ++ [(v, Venq.(dv_comm))]
is_enqueue enq v
enqId = length G.(Es)
G'.(Es) = G.(Es) ++ [mkGraphEvent enq Venq M']
G'.(so) = G.(so) G'.(com) = G.(com)
enqId M' enqId M ,
(* RETURN VALUE AT COMMITTING POINT *)
RET #b, emp >>>
.
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,
(* PRIVATE PRE *)
V - QueueLocal N γa γg q G1 M -
<<< (* PUBLIC PRE *)
Q G, (QueueInv γa γg 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'
G G' M M'
V Vdeq.(dv_in) Vdeq.(dv_comm) = V'
(* FAIL case *)
((Q' = Q v < 0 G' = G)
(* EMPTY case *)
( Q' = Q
v = 0 deq = EmpDeq
deqId = length G.(Es)
G'.(Es) = G.(Es) ++ [mkGraphEvent deq Vdeq M']
G'.(so) = G.(so) G'.(com) = G.(com)
{[deqId]} M M' deqId M)
(* successful case *)
(Q = (v, Venq.(dv_comm)) :: Q'
0 < v is_enqueue enq v is_dequeue deq v
deqId = length G.(Es)
( id, (enqId, id) G.(so))
G'.(Es) = G.(Es) ++ [mkGraphEvent deq Vdeq M']
G'.(so) = {[(enqId, deqId)]} G.(so)
G'.(com) = {[(enqId, deqId)]} G.(com)
enqId M' deqId M' deqId M
eV, G.(Es) !! enqId = Some eV eV.(ge_event) = enq
eV.(ge_view) = Venq eV.(ge_lview) M') ) ,
(* RETURN VALUE AT COMMITTING POINT *)
RET #v, emp >>>
.
(** Bundling of specs *)
Record core_queue_spec {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
{QueueConsistent : graph Prop} := QueueSpec {
(* operations *)
new_queue : val;
enqueue : val;
dequeue : val;
(* predicates *)
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_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);
QueueLocal_graph_snap :
N γa γg q G M, QueueLocal N γa γ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);
(* operations specs *)
new_queue_spec : new_queue_spec' new_queue QueueLocal QueueInv;
enqueue_spec : enqueue_spec' enqueue QueueLocal QueueInv;
dequeue_spec : dequeue_spec' dequeue QueueLocal QueueInv;
}.
Arguments core_queue_spec _ {_ _} _.
Record extended_queue_spec Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
(QueueConsistent : graph Prop) := ExtendedQueueSpec {
extended_core_spec :> core_queue_spec Σ QueueConsistent ;
(* extra operations *)
try_enq : val;
try_deq : val;
(* operations specs *)
try_enq_spec :
try_enq_spec' try_enq extended_core_spec.(QueueLocal) extended_core_spec.(QueueInv);
try_deq_spec :
try_deq_spec' try_deq extended_core_spec.(QueueLocal) extended_core_spec.(QueueInv);
}.
(** A strong queue spec *)
Definition strong_queue_spec Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
:= extended_queue_spec Σ StrongQueueConsistent.
(** A Weak queue spec *)
Definition weak_queue_spec Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
:= core_queue_spec Σ WeakQueueConsistent.
(** Basic queue spec *)
Definition basic_queue_spec Σ `{!noprolG Σ, !inG Σ (graphR qevent)}
:= core_queue_spec Σ BasicQueueConsistent.
(** Strong implies Weak *)
Program Definition strong_weak_queue_spec
{Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
(sq : strong_queue_spec Σ) : weak_queue_spec Σ :=
{|
QueueInv_Timeless := sq.(QueueInv_Timeless);
QueueInv_Objective := sq.(QueueInv_Objective);
QueueInv_graph_master_acc := sq.(QueueInv_graph_master_acc);
QueueLocal_graph_snap := sq.(QueueLocal_graph_snap) ;
QueueLocal_Persistent := sq.(QueueLocal_Persistent) ;
new_queue_spec := sq.(new_queue_spec) ;
enqueue_spec := sq.(enqueue_spec) ;
dequeue_spec := sq.(dequeue_spec) ;
|}.
Next Obligation.
iIntros "* QI".
by iDestruct (sq.(QueueInv_QueueConsistent) with "QI") as %SC%strq_wkq_cons.
Qed.
(** Weak implies Basic *)
Program Definition weak_basic_queue_spec
{Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
(wq : weak_queue_spec Σ) : basic_queue_spec Σ :=
{|
QueueInv_Timeless := wq.(QueueInv_Timeless);
QueueInv_Objective := wq.(QueueInv_Objective);
QueueInv_graph_master_acc := wq.(QueueInv_graph_master_acc);
QueueLocal_graph_snap := wq.(QueueLocal_graph_snap) ;
QueueLocal_Persistent := wq.(QueueLocal_Persistent) ;
new_queue_spec := wq.(new_queue_spec) ;
enqueue_spec := wq.(enqueue_spec) ;
dequeue_spec := wq.(dequeue_spec) ;
|}.
Next Obligation.
iIntros "* QI".
by iDestruct (wq.(QueueInv_QueueConsistent) with "QI") as %SC%wkq_bsq_cons.
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