Commit 1d2b34cd authored by William Mansky's avatar William Mansky

Improved graph specs and derived invariant specs from them.

parent b273dd96
This diff is collapsed.
......@@ -91,13 +91,13 @@ Instance graph_bot : @LatBottom graph_lat empty_graph.
Proof. intros G; repeat split; apply empty_subseteq. Qed.
Definition graphR := authR (latUR graph_lat).
Definition emapR := authR (gmapUR event (agreeR (latO view_Lat))).
Definition emapR := authR (gmapUR event (agreeR (leibnizO view))).
Context {Σ : gFunctors}.
Context `{noprolG Σ, graphG : inG Σ graphR, emapG : inG Σ emapR }.
Definition wrap_graph G := to_latT(Lat := graph_lat) G.
Definition wrap_emap (emap : gmap event view) := to_agree <$> (to_latT(Lat := view_Lat) <$> emap).
Definition wrap_emap (emap : gmap event view) : gmapUR event (agreeR (leibnizO view)) := to_agree <$> emap.
(* HAI: I believe `marked` here is the thread's local "view" on the graph? *)
(* William: It's events that the thread has synchronized with, while unmarked are known but not synchronized. *)
......@@ -106,9 +106,52 @@ Definition graph_snap γg γv (G : graph) (emap : gmap event view) (marked : eve
forall e, e G.(E) -> exists Ve, emap !! e = Some Ve /\ (marked e -> Ve V))%I.
Definition graph_master γg γv (G : graph) (emap : gmap event view) : iProp Σ :=
(forall e1 e2, (e1, e2) G.(so) -> exists V1 V2, emap !! e1 = Some V1 /\ emap !! e2 = Some V2 /\ V1 V2
((forall e, e G.(E) -> exists Ve, emap !! e = Some Ve) /\
forall e1 e2, (e1, e2) G.(so) -> exists V1 V2, emap !! e1 = Some V1 /\ emap !! e2 = Some V2 /\ V1 V2
own γg ( wrap_graph G) own γv ( wrap_emap emap))%I.
Section gmap_update.
Local Instance discrete_sqsubseteq A : SqSubsetEq A := eq.
Lemma gmap_sub_local_update : forall `{Countable K} {V} (m1 m2 m' : gmapUR K (agreeR (leibnizO V))),
m1 m' -> m' -> (m1, m2) ~l~> (m', m').
Proof.
intros; apply local_update_unital=> n mf Hmv Hm; simpl in *.
split; first by apply cmra_valid_validN.
apply discrete_iff in Hm; last by typeclasses eauto.
intros j.
rewrite lookup_op.
assert (included (mf !! j) (m1 !! j)) as Hj.
{ apply lookup_included; exists m2.
rewrite cmra_comm; auto. }
setoid_rewrite H2 in Hj.
apply option_included in Hj as [Hnone | Hsome]; first by rewrite Hnone right_id.
destruct Hsome as (? & ? & Hj & Hj' & Hcase).
rewrite Hj Hj' -Some_op; constructor.
rewrite -discrete_iff cmra_comm -agree_included.
destruct Hcase as [->|]; auto.
Qed.
End gmap_update.
Lemma graph_master_snap : forall γg γv G emap V,
graph_master γg γv G emap - |==> graph_master γg γv G emap graph_snap γg γv G emap (fun _ => Logic.False) V.
Proof.
intros; unfold graph_master, graph_snap.
iIntros "(% & G & e)".
iMod (own_master_update with "G") as "[$ $]"; first by auto.
iPoseProof (own_valid with "e") as "%".
iMod (own_update with "e") as "[$ $]".
{ apply auth_update_alloc, gmap_sub_local_update.
* reflexivity.
* by rewrite -auth_auth_valid. }
iIntros "!>"; iPureIntro.
split; auto.
intros ? Hin; destruct H1 as [He _].
destruct (He _ Hin); eexists; split; eauto; contradiction.
Qed.
(* HAI:
- We probably can say more about `enq`? How it is ordered with previous
enques and deques that have been seen by `marked`? *)
......@@ -133,11 +176,12 @@ Definition enqueue_spec
graph_snap γg γv G1 emap1 marked 𝓥.(cur) Queue q 𝓥.(cur) -
<<< G emap, queue_consistent G graph_master γg γv G emap>>>
(mkExpr (enqueue [ #q ; v]) 𝓥) @
<<< 𝓥' G' emap' (marked' : event -> Prop), queue_consistent G' /\ G G' /\ emap emap'⌝
graph_master γg γv G' emap'
(* private *) enq, G1 G /\ emap1 emap /\ is_enqueue enq v /\
(forall e, marked e -> marked' e) /\ enq G'.(E) /\ marked' enq /\
(forall e : event, marked' e -> emap' !! e (emap' !! enq : option view))
<<< 𝓥' G' emap' (marked' : event -> Prop) enq Venq, ⌜𝓥 𝓥' /\ is_enqueue enq v /\ ~enq G.(E) /\
G'.(E) = {[enq]} G.(E) /\ G.(po) G'.(po) /\ G'.(so) = G.(so) /\ G'.(com) = G.(com) /\
queue_consistent G' /\ emap' = <[enq := Venq]>emap /\ 𝓥.(cur) Venq graph_master γg γv G' emap'
(* private *) G1 G /\ emap1 emap /\
(forall e, marked e -> marked' e) /\ marked' enq /\
(forall e : event, marked' e -> emap' !! e Some Venq)
graph_snap γg γv G' emap' marked' 𝓥'.(cur) Queue q 𝓥'.(cur), RET (mkVal # 𝓥') >>>.
Definition dequeue_spec
......@@ -145,12 +189,18 @@ Definition dequeue_spec
graph_snap γg γv G1 emap1 marked 𝓥.(cur) Queue q 𝓥.(cur) -
<<< G emap, queue_consistent G graph_master γg γv G emap>>>
(mkExpr (dequeue [ #q]) 𝓥) @
<<< (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 /\
deq G'.(E) /\ ~(deq E G) /\ (enq, deq) G'.(com) /\ marked' deq /\
(forall e : event, marked' e -> emap' !! e (emap' !! deq : option view))
<<< (v: lit) 𝓥' G' emap' (marked' : event -> Prop) enq deq Vdeq, ⌜𝓥 𝓥' /\ is_enqueue enq #v /\ is_dequeue deq #v
enq G.(E) /\ ~deq G.(E) /\ set_Forall (fun e' => ~(enq, e') G.(com)) G.(E) /\
G'.(E) = {[deq]} G.(E) /\ G.(po) G'.(po) /\ {[(enq, deq)]} G'.(so) = G.(so) /\ G'.(com) = {[(enq, deq)]} G.(com) /\
queue_consistent G' /\ emap' = <[deq := Vdeq]>emap /\ 𝓥.(cur) Vdeq graph_master γg γv G' emap'
(* private *) G1 G /\ emap1 emap /\
(forall e, marked e -> marked' e) /\ marked' enq /\ marked' deq /\
(forall e : event, marked' e -> emap' !! e Some Vdeq)
graph_snap γg γv G' emap' marked' 𝓥'.(cur) Queue q 𝓥'.(cur), RET (mkVal #v 𝓥') >>>.
End Graphs.
Arguments E {_ _ _}.
Arguments po {_ _ _}.
Arguments com {_ _ _}.
Arguments so {_ _ _}.
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