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

Fix graph spec w.r.t. logatomic triple mask change

parent 73df76f7
......@@ -16,34 +16,45 @@ Require Import iris.prelude.options.
Section from_piggyback.
Context `{!noprolG Σ, !inG Σ (graphR xchg_event)}.
Context `(ex_spec : exchanger_piggyback_spec Σ Eo Ei).
Context (N : namespace).
Hypotheses (Sub : N Eo) (DISJ : N ## histN).
Context `(ex_spec : exchanger_piggyback_spec Σ).
Let EI : bool vProp Σ := (λ _, True)%I.
Let ExchangerLocal' := spec_graph_piggyback.ExchangerLocal ex_spec N EI.
Let ExchangerLocal' := spec_graph_piggyback.ExchangerLocal ex_spec EI.
Let ExchangerInv' := spec_graph_piggyback.ExchangerInv ex_spec.
Local Lemma ExchangerInv_ExchangerConsistent_instance :
N γg x q G G' M',
ExchangerInv' γg q G - ExchangerLocal' N γg x G' M'
={N}=
eventgraph_consistent G ExchangerConsistent G ExchangerInv' γg q G.
Proof.
iIntros "* EI EL".
iMod (fupd_mask_subseteq (N xchgUN N)) as "Close"; [solve_ndisj|].
iMod (spec_graph_piggyback.ExchangerInv_ExchangerConsistent with "EI EL")
as "$".
by iMod "Close" as "_".
Qed.
Local Lemma new_exchanger_ex_spec :
new_exchanger_spec' ExchangerLocal' ExchangerInv'
(spec_graph_piggyback.new_exchanger ex_spec).
Proof.
iIntros (tid Φ) "T Post".
iIntros (N tid Φ) "T Post".
iApply wp_fupd.
iApply (spec_graph_piggyback.new_exchanger_spec ex_spec with "T").
iIntros "!>" (γg ex) "[EI EL]".
iMod ("EL" $! _ N EI) as "EL".
iMod ("EL" $! _ EI N) as "EL".
iIntros "!>". iApply ("Post" with "[$EL $EI]").
Qed.
Local Lemma exchange_ex_spec :
exchange_spec' ExchangerLocal' ExchangerInv'
(spec_graph_piggyback.exchange ex_spec) (Eo N).
(spec_graph_piggyback.exchange ex_spec).
Proof using All.
iIntros (ex tid γg G1 M V v1 Posv1) "sV EL".
iIntros (N DISJ x tid γg G1 M V v1 Posv1) "sV EL".
iIntros (Φ) "AU".
iMod (inv_alloc N _ (EI true) with "[//]") as "IE".
iMod (inv_alloc (xchgUN N) _ (EI true) with "[//]") as "IE".
iApply (spec_graph_piggyback.exchange_spec ex_spec with "sV EL IE [] AU");
[done..|].
iIntros "!>".
......@@ -65,7 +76,7 @@ Proof using All.
Qed.
Program Definition exchanger_impl_from_piggyback :
exchanger_spec Σ (Eo N) Ei := {|
exchanger_spec Σ := {|
spec_graph.ExchangerLocal := ExchangerLocal' ;
spec_graph.ExchangerInv := ExchangerInv' ;
......@@ -77,7 +88,8 @@ Program Definition exchanger_impl_from_piggyback :
spec_graph_piggyback.ExchangerInv_Fractional ex_spec;
spec_graph.ExchangerInv_ExchangerConsistent :=
spec_graph_piggyback.ExchangerInv_ExchangerConsistent ex_spec N EI;
ExchangerInv_ExchangerConsistent_instance;
spec_graph.ExchangerInv_graph_master_acc :=
spec_graph_piggyback.ExchangerInv_graph_master_acc ex_spec;
spec_graph.ExchangerInv_graph_snap :=
......@@ -86,9 +98,9 @@ Program Definition exchanger_impl_from_piggyback :
spec_graph_piggyback.ExchangerInv_agree ex_spec;
spec_graph.ExchangerLocal_Persistent :=
spec_graph_piggyback.ExchangerLocal_Persistent ex_spec N EI;
spec_graph_piggyback.ExchangerLocal_Persistent ex_spec EI;
spec_graph.ExchangerLocal_graph_snap :=
spec_graph_piggyback.ExchangerLocal_graph_snap ex_spec N EI;
spec_graph_piggyback.ExchangerLocal_graph_snap ex_spec EI;
spec_graph.new_exchanger_spec := new_exchanger_ex_spec;
spec_graph.exchange_spec := exchange_ex_spec;
......@@ -96,15 +108,9 @@ Program Definition exchanger_impl_from_piggyback :
End from_piggyback.
Definition xchgEN := nroot .@ "xchgEmpty".
(* TODO: mismatch between Eo and Ei *)
Program Definition exchanger_impl Σ `{!noprolG Σ, !xchgG Σ, !atomicG Σ} :
exchanger_spec Σ ( (xchgN offN xchgEN)) (xchgN offN).
exchanger_spec Σ.
Proof.
rewrite -difference_difference_L.
apply exchanger_impl_from_piggyback.
- by apply : proof_graph_piggyback.exchanger_impl.
- apply subseteq_difference_r; [|done]. apply disjoint_union_r; solve_ndisj.
- solve_ndisj.
apply : exchanger_impl_from_piggyback.
apply : proof_graph_piggyback.exchanger_impl.
Defined.
......@@ -23,11 +23,13 @@ Local Arguments lookup_weaken {_ _ _ _ _ _ _ _}.
#[local] Notation graph_event := (graph_event xchg_event).
#[local] Notation graph := (graph xchg_event).
Implicit Types (tid : thread_id) (G : graph) (E : event_list) (γ : gname) (x : loc).
Implicit Types (tid : thread_id) (γ : gname) (x : loc).
Implicit Types (G : graph) (E : event_list).
Implicit Types (N : namespace).
(** Namespace for our internal invariants. *)
Definition xchgN := nroot .@ "xchg".
Definition offN := nroot .@ "offer".
Definition xchgN N := N .@ "xchg".
Definition offN N := N .@ "offer".
(* CMRA we need *)
(* a persistent map of from main offers to its info *)
......@@ -35,7 +37,7 @@ Definition offer_info : Type := gname * gname.
Implicit Types (T : gmap loc offer_info).
#[local] Notation xchg_mapUR' := (gmapUR loc (agreeR (leibnizO offer_info))).
#[local] Notation xchg_mapUR' := (agreeMR loc offer_info).
#[local] Notation xchg_mapUR := (authUR xchg_mapUR').
Class xchgG Σ := XChgG {
......@@ -423,8 +425,6 @@ Proof.
iIntros "G1 G2". by iDestruct (ghost_graph_master_agree with "G1 G2") as %?.
Qed.
Let Eo : coPset := ( (xchgN offN)).
Definition ExchangerSeen γx x : vProp :=
ζx, x sn{γx} ζx.
......@@ -480,15 +480,15 @@ Definition exchange_priv_post' γx γg x v1 (Q : Z → vProp) : exchange_postT :
G''.(so) = {[ (exId1, exId2); (exId2, exId1) ]} G.(so)
G''.(com) = {[ (exId1, exId2); (exId2, exId1) ]} G.(com)
exId1 (elements G'.(so)).*1 exId2 (elements G'.(so)).*1
@{V'}( graph_snap γg G'' M' ExchangerSeen γx x)) - Q v2
@{V'}(graph_snap γg G'' M' ExchangerSeen γx x)) - Q v2
)%I.
Definition exchange_AU_proof' (N : namespace) (EI : bool vProp)
Definition exchange_AU_proof' (EI : bool vProp) (N : namespace)
γx γg x G1 M Vin1 v1
(Q : _ vProp)
{TA' TB' : tele} (α' : TA' vProp) (β' Φ' : TA' TB' vProp)
: vProp :=
atomic_update_proof EI (Eo N) (histN)
atomic_update_proof EI ( N) (histN)
α' β' Φ'
(tele_app (TT:= [tele _]) (exchange_AU_atomic_pre ExchangerInv γg))
(λ b1 b2,
......@@ -523,18 +523,18 @@ Definition offer_rep (o : loc) γo γk v1 t0 V0 P Q : vProp :=
(* Invariant of offer, created by the helpee.
We use invariant to have agreement on P Q; otherwise we would need saved predicate!
(where laters wouldn't be a problem, but ghost names are.) *)
Context (N : namespace).
Context (EI : bool vProp).
Context (N : namespace).
Definition offer_inv γx γg x o γo γk t0 V0 : vProp :=
v P Q, inv offN (offer_rep o γo γk v t0 V0 P Q)
v P Q, inv (offN N) (offer_rep o γo γk v t0 V0 P Q)
M1 Vin1,
@{V0} (
Vin1 (* store the Vin of the helpee *)
G1, graph_snap γg G1 M1
(TA' TB' : tele) (α' : TA' vProp) (β' Φ' : TA' TB' vProp),
( P - atomic_update (Eo N) (histN) α' β' Φ')
(exchange_AU_proof' N EI γx γg x G1 M1 Vin1 v Q α' β' Φ')
( P - atomic_update ( N) (histN) α' β' Φ')
(exchange_AU_proof' EI N γx γg x G1 M1 Vin1 v Q α' β' Φ')
).
(* Main offer is created by the helpee and write to the exchange.
......@@ -575,13 +575,13 @@ Definition ExchangerInternalInv γt γx γg x : vProp :=
#[global] Instance ExchangerInternalInv_objective γt γx γg x :
Objective (ExchangerInternalInv γt γx γg x) := _.
Definition InternInv γt γx γg x := inv xchgN (ExchangerInternalInv γt γx γg x).
Definition InternInv γt γx γg x := inv (xchgN N) (ExchangerInternalInv γt γx γg x).
(** ExchangerLocal assertion, specific to this implementation---------------- *)
Definition ExchangerLocalLite γg x G logV : vProp :=
graph_snap γg G logV
(γt γx : gname), ExchangerSeen γx x
meta x xchgN (γt,γx).
meta x nroot (γt,γx).
#[global] Instance ExchangerLocalLite_persistent γg x G M :
Persistent (ExchangerLocalLite γg x G M) := _.
......@@ -591,7 +591,7 @@ Definition ExchangerLocalLite γg x G logV : vProp :=
Definition ExchangerLocal γg x G logV : vProp :=
graph_snap γg G logV
(γt γx : gname), ExchangerSeen γx x
meta x xchgN (γt,γx)
meta x nroot (γt,γx)
InternInv γt γx γg x.
#[global] Instance ExchangerLocal_persistent γg x G M :
......@@ -755,16 +755,13 @@ Context `{!noprolG Σ, !xchgG Σ, !atomicG Σ}.
Local Existing Instances xchg_graphG xchg_uniqTokG xchg_mapG.
Let Eo : coPset := ( (xchgN offN)).
Let Ei : coPset := (xchgN offN).
Lemma ExchangerInv_ExchangerConsistent_instance :
N EI γg x q G G' M',
ExchangerInv γg q G - ExchangerLocal N EI γg x G' M'
={Ei}= eventgraph_consistent G ExchangerConsistent G
EI N γg x q G G' M',
ExchangerInv γg q G - ExchangerLocal EI N γg x G' M'
={N xchgUN N}= eventgraph_consistent G ExchangerConsistent G
ExchangerInv γg q G.
Proof.
iIntros (N EI γg x q G G' M') "GE [? EL]".
iIntros (EI N γg x q G G' M') "GE [? EL]".
iDestruct "EL" as (γt γx) "(ES & MT & II)".
iInv "II" as (G0) "(>[%F1 %F2] & >GE0 & II)" "HClose".
iDestruct (ExchangerInv_agree with "GE GE0") as %->. iFrame "GE".
......@@ -792,7 +789,7 @@ Proof.
Qed.
Lemma ExchangerLocal_graph_snap_instance :
N EI γg x G M, ExchangerLocal N EI γg x G M graph_snap γg G M.
EI N γg x G M, ExchangerLocal EI N γg x G M graph_snap γg G M.
Proof. by iIntros "* [$ _]". Qed.
Lemma ExchangerLocalLite_graph_snap_instance :
......@@ -800,15 +797,15 @@ Lemma ExchangerLocalLite_graph_snap_instance :
Proof. by iIntros "* [$ _]". Qed.
Lemma ExchangerLocalLite_from_instance :
N EI γg x G M, ExchangerLocal N EI γg x G M ExchangerLocalLite γg x G M.
EI N γg x G M, ExchangerLocal EI N γg x G M ExchangerLocalLite γg x G M.
Proof.
iIntros "* [$ EL]". iDestruct "EL" as (γt γx) "(ES & MT & II)".
iExists γt, γx. iFrame.
Qed.
Lemma ExchangerLocalLite_to_instance :
N EI γg x G' M' G M,
ExchangerLocalLite γg x G M - ExchangerLocal N EI γg x G' M' -
ExchangerLocal N EI γg x G M.
EI N γg x G' M' G M,
ExchangerLocalLite γg x G M - ExchangerLocal EI N γg x G' M' -
ExchangerLocal EI N γg x G M.
Proof.
iIntros "* [$ EL] [_ EL']". iDestruct "EL" as (γt γx) "[ES #MT]".
iExists γt, γx. iFrame.
......@@ -831,9 +828,9 @@ Proof.
Qed.
Lemma ExchangerLocal_upgrade_instance :
N EI γg x q G' G M,
EI N γg x q G' G M,
ExchangerInv γg q G' -
ExchangerLocal N EI γg x G M - ExchangerLocal N EI γg x G' M.
ExchangerLocal EI N γg x G M - ExchangerLocal EI N γg x G' M.
Proof.
iIntros "* EI #EL".
iDestruct (ExchangerLocalLite_from_instance with "EL") as "-#ELL".
......@@ -842,10 +839,10 @@ Proof.
Qed.
Lemma ExchangerLocal_union_instance :
N EI γg x q G G1 G2 M1 M2,
EI N γg x q G G1 G2 M1 M2,
ExchangerInv γg q G -
ExchangerLocal N EI γg x G1 M1 - ExchangerLocal N EI γg x G2 M2 -
ExchangerLocal N EI γg x G (M1 M2).
ExchangerLocal EI N γg x G1 M1 - ExchangerLocal EI N γg x G2 M2 -
ExchangerLocal EI N γg x G (M1 M2).
Proof.
iIntros "* [EI1 EI2] EL1 EL2".
iDestruct (ExchangerLocal_upgrade_instance with "EI1 EL1") as "[Gs1 EL1']".
......@@ -871,7 +868,7 @@ Proof.
iMod (LTM_master_alloc ) as (γt) "LTm".
iMod (LTM_master_fork with "LTm") as "[LTm #LTs]".
iMod graph_master_alloc_empty as (γg) "[[GM1 GM2] Gs]".
iMod (meta_set _ _ (γt, γx) xchgN with "Hm") as "#Hm"; [done|].
iMod (meta_set _ _ (γt, γx) nroot with "Hm") as "#Hm"; [done|].
have EC := ExchangerConsistent_empty.
......@@ -879,8 +876,8 @@ Proof.
iSplitL "GM2".
- (* ExchangerInv *)
by iDestruct (ExchangerInv_graph_master with "GM2") as "[% $]".
- iIntros "!>" (E N EI).
iMod (inv_alloc xchgN _ (ExchangerInternalInv N EI γt γx γg x)
- iIntros "!>" (E EI N).
iMod (inv_alloc (xchgN N) _ (ExchangerInternalInv EI N γt γx γg x)
with "[xA GM1 LTm]") as "#I".
{ iNext. iExists .
iDestruct (ExchangerInv_graph_master with "GM1") as "[% $]". iSplit; [done|].
......@@ -896,9 +893,9 @@ Proof.
Qed.
Lemma atom_exchange :
exchange_piggyback_spec' proof_graph_piggyback.ExchangerLocal ExchangerInv exchange Eo.
exchange_piggyback_spec' ExchangerLocal ExchangerInv exchange.
Proof.
intros x tid γg G1 M V v1 Posv1 N EI OBJ Sub DISJ.
intros EI OBJ N DISJ x tid γg G1 M V v1 Posv1.
iIntros "#sV #(Gs & ES) #EXI" (Φ TA' TB' α' β' Φ') "Pr AU".
iDestruct (bi.persistent_sep_dup with "Pr") as "[#Pr AU']".
iDestruct "ES" as (γt γx) "(ES & MT & EII)".
......@@ -957,7 +954,7 @@ Proof.
(* open invariant *)
iInv "EXI" as "XI" "CloseX".
iInv "EII" as (G3) "(>[%CON3 %EGCs] & GM & EBI)" "Close". { set_solver+Sub. }
iInv "EII" as (G3) "(>[%CON3 %EGCs] & GM & EBI)" "Close".
iDestruct "EBI" as (LVs3 os3 T3) "(LTm & Locs)".
iDestruct "Locs" as (Vb) "([%tx0 >xA] & Offs)".
......@@ -1075,9 +1072,8 @@ Proof.
wp_bind (casʳᵉˡ(_, _, _))%E.
(* open invariant *)
iInv "EXI" as "XI" "CloseX".
clear EGCs. iInv "EII" as (G4) "(>[%CON4 %EGCs] & GM & EBI)" "Close".
{ set_solver+Sub. }
iInv "EXI" as "XI" "CloseX". clear EGCs.
iInv "EII" as (G4) "(>[%CON4 %EGCs] & GM & EBI)" "Close".
rewrite ExchangerBaseInv_unfold_snap.
iDestruct ("EBI" with "[$LT3]") as (LVs4 os4 T4) "[(LTm & Locs) >%LeT3]".
iDestruct "Locs" as (Vb) "([%tx0 >xA] & Offs & >[%Eqos4 %EqD4])".
......@@ -1095,11 +1091,7 @@ Proof.
iDestruct "l2A" as (ζl2) ">l2A".
(* open the l2 offer invariant *)
iInv "l2I" as "HIl2" "Close2".
{ (* TODO: cleanup *)
rewrite difference_difference_L. apply subseteq_difference_r; [|done].
apply disjoint_union_r. split; [set_solver+Sub|solve_ndisj]. }
iDestruct "HIl2" as (s ζl0 V1') "(>[%OHl2 %Posv2] & [%Vlo >l2C] & OR)".
iInv "l2I" as (s ζl0 V1') "(>[%OHl2 %Posv2] & [%Vlo >l2C] & OR)" "Close2".
iDestruct (AtomicPtsTo_AtomicCASer_agree with "l2A l2C") as %->.
(* actual CAS to match the offer *)
wp_apply (AtomicCASer_1_CAS_int l2 γl2 _ _ _ _ _ _ 0 #m tid V3 Vb
......@@ -1266,7 +1258,7 @@ Proof.
by rewrite lookup_insert in FRtl2. }
(* We should get an AU from the offerer here *)
iDestruct "OR" as "(l2D & HP)". iDestruct "AU2" as (G02) "[Gs2 AU2]".
iDestruct "OR" as "[l2D HP]". iDestruct "AU2" as (G02) "[Gs2 AU2]".
iDestruct "AU2" as (TA2' TB2' α2' β2' Φ2') "[AU2 AU2']".
iSpecialize ("AU2" with "HP").
rewrite view_at_except_0. iMod "AU2" as "AU2".
......@@ -1387,7 +1379,7 @@ Proof.
- iApply (view_at_mono with "SL'"); [done|]. by apply SeenLogview_map_mono. }
(* COMMITING both AUs in some order decided by the boolean bv. *)
iAssert (|={ N xchgN offN}=>
iAssert (|={_}=>
@{V'} ( EI true graph_master γg (1/2) G'' Q v1 Φ #v2))%I
with "[GM XI AU AU' AU2 AU2']" as ">(XI & GM & HQ & HΦ)".
{ (* TODO: annoying clean up of the context. *)
......@@ -1428,7 +1420,7 @@ Proof.
{ iExists _; iFrame "xN". }
iAssert (@{V'} graph_snap γg G' M')%I with "[Gs']" as "#Obs'".
{ iFrame "Gs' SL'". }
iAssert (@{V'} ExchangerLocal N EI γg x G' M')%I with "[]" as "#EL'".
iAssert (@{V'} ExchangerLocal EI N γg x G' M')%I with "[]" as "#EL'".
{ iFrame "Obs'". iExists γt, γx. by iFrame "ES MT EII". }
rewrite bi.and_elim_r.
......@@ -1445,7 +1437,7 @@ Proof.
iAssert (@{V'} graph_snap γg G'' M'')%I with "[]" as "#Obs''".
{ iFrame "Gs'' SL''". }
iAssert (@{V'} ExchangerLocal N EI γg x G'' M'')%I with "[]" as "#EL''".
iAssert (@{V'} ExchangerLocal EI N γg x G'' M'')%I with "[]" as "#EL''".
{ iFrame "Obs''". iExists γt, γx. by iFrame "ES MT EII". }
rewrite bi.and_elim_r.
......@@ -1492,7 +1484,7 @@ Proof.
iAssert (@{V'} graph_snap γg G'' M'')%I with "[]" as "#Obs''".
{ iFrame "Gs'' SL''". }
iAssert (@{V'} ExchangerLocal N EI γg x G'' M'')%I with "[]" as "#EL''".
iAssert (@{V'} ExchangerLocal EI N γg x G'' M'')%I with "[]" as "#EL''".
{ iFrame "Obs''". iExists γt, γx. by iFrame "ES MT EII". }
rewrite bi.and_elim_r.
......@@ -1625,7 +1617,7 @@ Proof.
iMod UTok_alloc as (γk) "Tok".
(* allocate the offer inv *)
iAssert (@{V0} exchange_AU_proof' N EI γx γg x G1 M V v1 (λ v2, Φ #v2) α' β' Φ')%I
iAssert (@{V0} exchange_AU_proof' EI N γx γg x G1 M V v1 (λ v2, Φ #v2) α' β' Φ')%I
with "[AU']" as "AU'".
{ rewrite -(view_at_objective_iff (InternInv _ _ _ _ _ _) V0).
rewrite -(view_at_objective_iff (meta _ _ _) V0).
......@@ -1652,12 +1644,12 @@ Proof.
iAssert (@{V0} P, P _)%I with "[AU]" as (AU_later) "[AU #AU_back]".
{ iApply (view_at_mono with "AU"); [done|].
by apply laterable, _. }
iMod (inv_alloc offN _ (offer_rep m γm γk v1 t0 V0 AU_later _)
iMod (inv_alloc (offN N) _ (offer_rep m γm γk v1 t0 V0 AU_later _)
with "[mD mC AU]") as "#mOI".
{ iNext. iExists OfferMatching, _, V0. iSplitR; [by iPureIntro|].
iSplitL "mC". { iExists _; iFrame "mC". }
simpl. iFrame "mD AU". }
iAssert (offer_inv N EI γx γg x m γm γk t0 V0) with "[GE AU']" as "#OI".
iAssert (offer_inv EI N γx γg x m γm γk t0 V0) with "[GE AU']" as "#OI".
{ iExists _, _, _. iFrame "mOI". iExists M, V.
iDestruct "GE" as "($ & Gs' & _)". iExists _. iFrame "Gs'".
iExists TA', TB', α', β', Φ'. iFrame "AU' AU_back". }
......@@ -1694,8 +1686,7 @@ Proof.
+ iExists _; iFrame "mA".
+ iExists t0, V0. iSplitR; [by iPureIntro|by iFrame "OI"].
- iPureIntro. rewrite filter_app Eqos2 2!fmap_app dom_insert list_to_set_app.
split; [done|clear -EqD2;set_solver]. }
clear tx0 FRtx1 Eqζx2 Vb.
split; [done|clear -EqD2;set_solver]. } clear tx0 FRtx1 Eqζx2 Vb.
iIntros "!>". wp_if. wp_op.
rewrite shift_0.
......@@ -1707,7 +1698,7 @@ Proof.
(* open invariant *)
iInv "EXI" as "XI" "CloseX".
iInv "EII" as (G3) "(>[%CON3 %EGCs] & GM & EBI)" "Close". { set_solver+Sub. }
iInv "EII" as (G3) "(>[%CON3 %EGCs] & GM & EBI)" "Close".
rewrite ExchangerBaseInv_unfold_snap.
iDestruct ("EBI" with "[$LT']") as (LVs3 os3 T3) "[(LTm & Locs) >%LeT']".
iDestruct "Locs" as (Vb) "([%tx0 >xA] & Offs & >[%Eqos3 %EqD3])".
......@@ -1724,10 +1715,7 @@ Proof.
eapply lookup_weaken_inv in EqTm';
[..|exact LeT']; [|by rewrite lookup_insert]. by inversion EqTm'. }
(* open the offer invariant *)
iInv "mOI" as "HIm" "Close2".
{ (* TODO: cleanup *)
rewrite difference_difference_L. apply subseteq_difference_r; [|done].
apply disjoint_union_r. split; [set_solver+Sub|solve_ndisj]. }
iInv "mOI" as "HIm" "Close2".
iDestruct "HIm" as (s ζl0 Vl2) "(>[%OHm _] & [%VmC >mC] & OR)".
iDestruct (AtomicPtsTo_AtomicCASer_agree with "mA mC") as %->.
......@@ -1798,7 +1786,7 @@ Proof.
iMod ("Pr" $! true true with "AU XI") as (G3') "[>GM' HClose]".
iDestruct (ExchangerInv_graph_master_agree with "GM GM'")
as "(%Eq & GM & GM')". subst G3'.
as "(-> & GM & GM')".
iCombine "GM GM'" as "GM".
iMod (graph_master_update _ _ _ LeG' EGCs' with "GM") as "[[GM GM'] Gs']".
......@@ -1810,7 +1798,7 @@ Proof.
rewrite -SeenLogview_insert'. iSplitL; [|done].
rewrite SeenLogview_map_mono; [iFrame "SL"|done..]. }
iAssert (@{V'} graph_snap γg G' M')%I with "[Gs']" as "#Gss'".
iAssert (@{V'} graph_snap γg G' M')%I with "[Gs']" as "#Gss' {Gs'}".
{ iFrame "Gs' SL". }
rewrite bi.and_elim_r.
......@@ -1826,8 +1814,8 @@ Proof.
(* close the invariant by switching to CANCELLED *)
iMod ("Close" with "[GM LTm xA mA Obs Off Offs]") as "_".
{ iNext. iExists _.
iDestruct (ExchangerInv_graph_master with "GM") as "[_ $]". iSplit; [done|].
iExists _, os3, _. iFrame "LTm".
iDestruct (ExchangerInv_graph_master with "GM") as "[_ $]".
iSplit; [done|]. iExists _, os3, _. iFrame "LTm".
iExists (Vb V'). iSplitL "xA". { iExists _. by iFrame "xA". }
iSplitL; [|by iPureIntro].
rewrite (view_at_mono Vb (Vb V') (ltac:(solve_lat)) (_ - _)%I);
......@@ -1858,9 +1846,9 @@ Proof.
apply lookup_singleton_Some in Subζm'' as []. simplify_eq.
by inversion NEqvm'.
- simpl. by iDestruct (UTok_unique with "Tok OR") as %?.
- iPureIntro. exists l. split; [done|].
subst ζm. move : Subζm''. rewrite lookup_insert_Some lookup_singleton_Some.
intros [[]|(_&_&?)]; [by simplify_eq|]. simplify_eq. by inversion NEqvm'.
- iPureIntro. exists l. split; [done|]. subst ζm.
move : Subζm''. rewrite lookup_insert_Some lookup_singleton_Some.
intros [[]|(_&_&?)]; simplify_eq; [done|]. by inversion NEqvm'.
- simpl. by iDestruct (UTok_unique with "Tok OR") as %?. }
simpl. simpl in OHm.
......@@ -1961,7 +1949,7 @@ End proof.
Program Definition exchanger_impl
Σ `{!noprolG Σ, !xchgG Σ, !atomicG Σ} :
exchanger_piggyback_spec Σ _ _ := {|
exchanger_piggyback_spec Σ := {|
spec_graph_piggyback.ExchangerInv_ExchangerConsistent :=
ExchangerInv_ExchangerConsistent_instance;
spec_graph_piggyback.ExchangerInv_graph_master_acc :=
......
......@@ -9,15 +9,10 @@ From gpfsl.examples.exchanger Require Import proof_graph_piggyback proof_graph.
Require Import iris.prelude.options.
Lemma exchanger_resource_impl
Σ `{!noprolG Σ, !xchgG Σ, !atomicG Σ, !gset_disjARG Σ event_id}
(N : namespace) :
N ## (xchgN offN xchgEN : coPset)
exchanger_resource_spec Σ ( (xchgN offN xchgEN N)) (xchgN offN).
Program Definition exchanger_resource_impl
Σ `{!noprolG Σ, !xchgG Σ, !atomicG Σ, !gset_disjARG Σ event_id} :
exchanger_resource_spec Σ.
Proof.
intros DISJ. rewrite -difference_difference_L.
apply : exchanger_resource_spec_impl.
- exact : exchanger_impl.
- solve_ndisj.
- by apply disjoint_union_r in DISJ as [].
Qed.
apply : proof_graph_piggyback.exchanger_impl.
Defined.
......@@ -18,7 +18,7 @@ Local Notation flag := 0%Z (only parsing).
Section ex.
Context `{!noprolG Σ, !inG Σ (graphR xchg_event),
eaG: !inG Σ (excl_authR (leibnizO bool)) }.
Context Eo Ei `(ex : exchanger_spec Σ Eo Ei).
Context `(ex : exchanger_spec Σ).
Local Notation vProp := (vProp Σ).
......@@ -63,9 +63,10 @@ Section ex.
Furthermore, it should just work with the full ownership of any graph G, not
just the initial graph ∅. *)
Lemma mp_exchange_spec N γg (e : loc) tid
(SubN: histN N Eo) (DISJ: Ei ## Eo) (DISJN: N ## histN) :
{{{ ex.(ExchangerLocal) γg e ex.(ExchangerInv) γg 1%Qp }}}
Lemma mp_exchange_spec N N'
(DISJ: N ## histN) (DISJ': N' ## histN) (DISJN : N ## N')
γg (e : loc) tid :
{{{ ex.(ExchangerLocal) N γg e ex.(ExchangerInv) γg 1%Qp }}}
mp_exchange [ #e ] @ tid;