Commit b273dd96 authored by William Mansky's avatar William Mansky

Finished translating graph dequeue spec.

parent 578ff7bc
......@@ -61,3 +61,4 @@ theories/examples/circ_buffer.v
theories/examples/ticket_lock.v
theories/examples/msqueue.v
theories/examples/snapshot.v
theories/examples/graphs.v
......@@ -28,20 +28,30 @@ Definition is_dequeue e v := e = Deq v.
Context {Σ : gFunctors}.
Context `{noprolG Σ, graphG : inG Σ (graphR event), emapG : inG Σ (emapR event) }.
Variable Queue : loc -> view -> iProp Σ.
Variable Queue : loc -> vProp Σ.
Variable queue_consistent : graph event -> Prop.
Variable P : val -> view -> iProp Σ.
Variable P : val -> vProp Σ.
Definition queue_inv N γg γv := inv N ( G emap, queue_consistent G graph_master event γg γv G emap
[ set] e unmatched_enqs G, match e with Enq v => V, emap !! e = Some V P v V | _ => emp end).
Program Definition queue_inv N γg γv : vProp Σ :=
{| monPred_at := fun V => inv N ( G emap, queue_consistent G graph_master event γg γv G emap
[ set] e unmatched_enqs G, match e with Enq v => V, emap !! e = Some V P v V | Deq _ => emp end) |}.
Lemma lift_enqueue : forall enqueue q γg γv x tid,
(forall (q: loc) (v : val) γg γv G1 emap1 marked (𝓥: threadView), enqueue_spec enqueue) ->
Instance queue_inv_persistent N γg γv :
Persistent (queue_inv N γg γv).
Proof.
rewrite /Persistent. iStartProof (iProp Σ).
iIntros (V) "#$".
Qed.
Lemma lift_enqueue : forall enqueue N q γg γv x tid
(HQ : forall (q: loc) (v : val) γg γv G1 emap1 marked (𝓥: threadView), enqueue_spec event Queue queue_consistent is_enqueue enqueue q v γg γv G1 emap1 marked 𝓥),
{{{ Queue q P x queue_inv N γg γv }}}
enqueue [ #q; #x] in tid
{{{ RET # }}}.
enqueue [ #q; x] in tid
{{{ RET #; Queue q }}}.
Proof.
intros; iIntros "(queue & P & #inv) Post".
Admitted.
End Graphs.
\ No newline at end of file
......@@ -148,18 +148,9 @@ Definition dequeue_spec
<<< (v: lit) 𝓥' G' emap' (marked' : event -> Prop), queue_consistent G' /\ G G' /\ emap emap'⌝
graph_master γg γv G' emap'
(* private *) enq deq, G1 G /\ emap1 emap /\ is_enqueue enq #v /\ is_dequeue deq #v
(forall e, marked e -> marked' e) /\ enq G'.(E) /\ marked' enq /\
(forall e : event, marked' e -> emap' !! e (emap' !! enq : option view))
(forall e, marked e -> marked' e) /\ enq G.(E) /\ marked' enq /\
deq G'.(E) /\ ~(deq E G) /\ (enq, deq) G'.(com) /\ marked' deq /\
(forall e : event, marked' e -> emap' !! e (emap' !! deq : option view))
graph_snap γg γv G' emap' marked' 𝓥'.(cur) Queue q 𝓥'.(cur), RET (mkVal #v 𝓥') >>>.
(* atomic_wp (dequeue [ #q]%E)
(λ G, queue_consistent G graph_master g G)%I
(λ G val, V' G' (marked' : event -> Prop), queue_consistent G' /\ graph_incl G G'⌝
graph_master g G'
(* private *) enq deq v, val = #v /\ graph_incl G1 G /\ is_enqueue enq v /\ is_dequeue deq v /\
enq E G /\ deq E G' /\ ~(deq E G) /\ com G' enq deq /\
(forall e, marked e -> marked' e) /\ marked' enq /\ marked' deq /\
(forall e, marked' e -> view_of G' e view_of G' deq)
graph_snap g G' marked' V' Queue q V')%I. *)
End Graphs.
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