Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps permission fslassn fslassnsem.
Require Import GpsSepAlg.
Set Implicit Arguments.
Infix "+!+" := hplus (at level 30, right associativity).
Inductive hbcase :=
| hb_sb (e e': nat)
| hb_rf (e e': nat)
| hb_sink (e: nat).
Definition is_sb edge :=
match edge with
| hb_sb _ _ ⇒ True
| _ ⇒ False
end.
Definition is_rf edge :=
match edge with
| hb_sb _ _ ⇒ False
| hb_rf _ _ ⇒ True
| hb_sink _ ⇒ False
end.
Definition is_sink edge :=
match edge with
| hb_sink _ ⇒ true
| _ ⇒ false
end.
Definition hbcase_eq a b :=
match a, b with
| hb_sb a1 a2, hb_sb b1 b2 ⇒ (a1 == b1) && (a2 == b2)
| hb_rf a1 a2, hb_rf b1 b2 ⇒ (a1 == b1) && (a2 == b2)
| hb_sink a1, hb_sink b1 ⇒ a1 == b1
| _, _ ⇒ false
end.
Lemma hbcase_eqP : Equality.axiom hbcase_eq.
Canonical Structure hbcase_eqMixin := EqMixin hbcase_eqP.
Canonical Structure hbcase_eqType := Eval hnf in EqType _ hbcase_eqMixin.
Definition hb_fst edge :=
match edge with hb_sb e _ | hb_rf e _ | hb_sink e ⇒ e end.
Definition hb_snd edge :=
match edge with
| hb_sb _ e | hb_rf _ e ⇒ Some e
| hb_sink _ ⇒ None
end.
Definition ann_sink lab (a : actid) :=
match lab a with
| Aalloc _ ⇒ False
| Afence _ ⇒ False
| _ ⇒ True
end.
Definition edge_valid lab sb rf edge :=
match edge with
| hb_sb a b ⇒ sb a b
| hb_rf a b ⇒ rf b = Some a
| hb_sink a ⇒ ann_sink lab a
end.
A list of nodes A is prefix-closed, hist_closed mt lab sb rf A, if is
closed with respect to incoming happens-before edges.
Inductive hc_edge (sb : relation actid) rf (a b: actid) : Prop :=
| hc_edge_sb (HB_SB: sb a b)
| hc_edge_rf (HB_RF: rf b = Some a).
Definition hist_closed sb rf (A: list actid) :=
∀ a (IN: In a A) b (HB: hc_edge sb rf b a), In b A.
Definition happens_before_union_rf sb rf := clos_trans _ (hc_edge sb rf).
Definition IrreflexiveHBuRF sb rf := irreflexive (happens_before_union_rf sb rf).
We proceed to the definition of local heap annotation validity at a
node e.
Definition RMW_rel_condition PS PSg typ (hrel: heap PS PSg) :=
HlabeledExact hrel HLtriangle ∨ (typ ≠ ATrlx ∧ typ ≠ ATacq ∧ HlabeledExact hrel HLnormal).
Definition RMW_acq_condition PS PSg typ (hacq': heap PS PSg) :=
HlabeledExact hacq' HLnabla ∨ (typ ≠ ATrlx ∧ typ ≠ ATrel ∧ HlabeledExact hacq' HLnormal).
Definition hmap_valid PS PSg lab sb rf (hmap: hbcase → heap PS PSg) (ga : val → option actid) (e: actid) :=
∃ (gnew : ghost_resource), << NG: ∀ x, gnew x ≠ None ↔ ga x = Some e >> ∧
match lab e with
| Astore typ l v ⇒
∃ pre post hf g,
<< pU: unique (sb^~ e) pre >> ∧
<< qU: unique (sb e) post >> ∧
<< pEQ : hmap (hb_sb pre e) = Hdef hf g >> ∧
<< DISJ :
(<< IV : is_lvalue (hf l) >> ∧
<< qEQ : ∃ Perm,
hmap (hb_sb e post) = Hdef (hupd hf l (lvalue _ _ Perm v)) g +!+ gheap _ _ gnew >> ∧
<< DEF : hmap (hb_sb e post) ≠ Hundef >> ∧
<< rEQ : ∀ e', hmap (hb_rf e e') = hemp >> ∧
<< sEQ : hmap (hb_sink e) = hemp >>) ∨
(<< NA : typ ≠ ATna >> ∧ ∃ rfs hr hF (P: assn_mod PS PSg) sbg rfg,
<< UPD: Hdef (initialize hf l) g =
hsingl _ _ l (HVra (hupd Wemp v P) Remp false (Some HLCnormal) (Some HLCnormal))
+!+ hF +!+ hr >> ∧
<< qEQ: hmap (hb_sb e post) =
hsingl _ _ l (HVra (hupd Wemp v P) Remp false (Some HLCnormal) (Some HLCnormal))
+!+ hF +!+ sbg >> ∧
<< DEF: hmap (hb_sb e post) +!+ hsum (map hmap (map (hb_rf e) rfs)) +!+ hmap (hb_sink e)
≠ Hundef >> ∧
<< rfsSIM: Hsim ((hsum (map hmap (map (hb_rf e) rfs))) +!+ hmap (hb_sink e)) (hr +!+ rfg) >> ∧
<< ghostEQ: sbg +!+ rfg = gheap _ _ gnew >> ∧
<< TRAN: assn_sem (Anabla (sval P)) ((hsum (map hmap (map (hb_rf e) rfs))) +!+ hmap (hb_sink e)) >> ∧
<< TYP: HlabeledExact hr HLtriangle ∨
(typ ≠ ATrlx ∧ typ ≠ ATacq ∧ HlabeledExact hr HLnormal) >> ∧
<< rfsND: NoDup rfs >> ∧
<< rfsOK: ∀ x, In x rfs ↔ rf x = Some e >>) >>
| Aload typ l v ⇒
∃ pre post hf g,
<< pU: unique (sb^~ e) pre >> ∧
<< qU: unique (sb e) post >> ∧
<< qD : hmap (hb_sb e post) ≠ Hundef >> ∧
<< pEQ: hmap (hb_sb pre e) = Hdef hf g >> ∧
<< DISJ :
(<< IV : is_rvalueV (hf l) v >> ∧
<< qEQ: hmap (hb_sb e post) = hmap (hb_sb pre e) +!+ gheap _ _ gnew >> ∧
<< rEQ: ∀ e', hmap (hb_rf e' e) = hemp >> ∧
<< sEQ: hmap (hb_sink e) = hemp >>) ∨
(<< NA : typ ≠ ATna >> ∧ ∃ rfs hr hF P,
<< rfsND: NoDup rfs >> ∧
<< rfsOK: ∀ x, In x rfs ↔ rf e = Some x >> ∧
<< TRAN: assn_sem (Anabla (sval P)) (hsum (map hmap (map (hb_rf^~ e) rfs))) >> ∧
<< rfsSIM: Hsim (hsum (map hmap (map (hb_rf^~ e) rfs))) hr >> ∧
<< sEQ: hmap (hb_sink e) = hsingl _ _ l (HVra Wemp (hupd Remp v P) false None None ) >> ∧
<< pEQ': hsingl _ _ l (HVra Wemp (hupd Remp v P) false None (Some HLCnormal)) +!+ hF
= Hdef hf g >> ∧
<< qEQ: hmap (hb_sb e post) = hsingl _ _ l (HVra Wemp Remp false None (Some HLCnormal))
+!+ hr +!+ hF +!+ gheap _ _ gnew >> ∧
<< TYP: HlabeledExact hr HLnabla ∨
(typ ≠ ATrlx ∧ typ ≠ ATrel ∧ HlabeledExact hr HLnormal) >> ∧
<< PREC: precise (sval P) >> ∧
<< NORM: normalizable (sval P) >>) >>
| Askip ⇒
∃ pres posts,
<< pND: NoDup pres >> ∧
<< pOK: ∀ x, In x pres ↔ sb x e >> ∧
<< qND: NoDup posts >> ∧
<< qOK: ∀ x, In x posts ↔ sb e x >> ∧
<< DEF: hsum (map hmap (map (hb_sb e) posts)) +!+ hmap (hb_sink e) ≠ Hundef >> ∧
<< EQ: hsum (map hmap (map (hb_sb^~ e) pres)) +!+ gheap _ _ gnew =
hsum (map hmap (map (hb_sb e) posts)) +!+ hmap (hb_sink e) >>
| Aalloc l ⇒
∃ pre post hf g,
<< pU : unique (sb^~ e) pre >> ∧
<< qU : unique (sb e) post >> ∧
<< pEQ : hmap (hb_sb pre e) = Hdef hf g >> ∧
<< NALL: hf l = HVnone >> ∧
<< DEF : hmap (hb_sb e post) ≠ Hundef >> ∧
<< qEQ : hmap (hb_sb e post) = Hdef (hupd hf l (HVuval HLnormal)) g +!+ gheap _ _ gnew
∨ ∃ QQ isrmw,
hmap (hb_sb e post) = Hdef (hupd hf l (HVra QQ QQ isrmw (Some HLCnormal) None)) g
+!+ gheap _ _ gnew >>
| Armw typ l v v' ⇒
∃ pre post rfsIn rfsOut,
<< AT: typ ≠ ATna >> ∧
<< pU: unique (sb^~ e) pre >> ∧
<< qU: unique (sb e) post >> ∧
<< rfsInND: NoDup rfsIn >> ∧
<< rfsOutND: NoDup rfsOut >> ∧
<< rfsInOK: ∀ x, In x rfsIn ↔ rf e = Some x >> ∧
<< rfsOutOK: ∀ x, In x rfsOut ↔ rf x = Some e >> ∧
<< DEF: hmap (hb_sb e post) +!+ hsum (map hmap (map (hb_rf e) rfsOut)) +!+ hmap (hb_sink e)
≠ Hundef >> ∧
∃ P QQ hrel hrel' hacq hacq' ht hF sbg rfg,
<< pEQ: hmap (hb_sb pre e) = hsingl _ _ l (HVra (hupd Wemp v' P) QQ true (Some HLCnormal) (Some HLCnormal))
+!+ hrel +!+ hF >> ∧
<< rInEQ: hsum (map hmap (map (hb_rf^~ e) rfsIn)) = hacq +!+ ht >> ∧
<< qEQ: hmap (hb_sb e post) = hsingl _ _ l (HVra (hupd Wemp v' P) QQ true (Some HLCnormal) (Some HLCnormal))
+!+ hacq' +!+ hF +!+ sbg >> ∧
<< rOutEQ: hsum (map hmap (map (hb_rf e) rfsOut)) +!+ hmap (hb_sink e) = hrel' +!+ ht +!+ rfg >> ∧
<< ghostEQ: sbg +!+ rfg = gheap _ _ gnew >> ∧
<< TRANin: assn_sem (Anabla (sval (QQ v))) (hacq +!+ ht) >> ∧
<< TRANout: assn_sem (Anabla (sval P)) (hrel' +!+ ht) >> ∧
<< RELsim: Hsim hrel hrel' >> ∧
<< ACQsim: Hsim hacq hacq' >> ∧
<< RELlabel: RMW_rel_condition typ hrel >> ∧
<< ACQlabel: RMW_acq_condition typ hacq' >>
| Afence typ ⇒
∃ pre post,
<< pU: unique (sb^~ e) pre >> ∧
<< qU: unique (sb e) post >> ∧
<< DEF: hmap (hb_sb e post) ≠ Hundef >> ∧
∃ hF hrel hrel' hacq hacq',
<< pEQ: hmap (hb_sb pre e) = hF +!+ hrel +!+ hacq >> ∧
<< qEQ: hmap (hb_sb e post) = hF +!+ hrel' +!+ hacq' +!+ gheap _ _ gnew >> ∧
<< RELlabel : HlabeledExact hrel HLnormal >> ∧
<< RELlabel': HlabeledExact hrel' HLtriangle >> ∧
<< ACQlabel : HlabeledExact hacq HLnabla >> ∧
<< ACQlabel': HlabeledExact hacq' HLnormal >> ∧
<< RELsim: Hsim hrel hrel' >> ∧
<< ACQsim: Hsim hacq hacq' >> ∧
<< NA: typ ≠ ATna >> ∧
<< RLX: typ ≠ ATrlx >> ∧
<< REL: typ = ATrel → hacq = hemp >> ∧
<< ACQ: typ = ATacq → hrel = hemp >>
end.
Definition hmap_valids PS PSg lab sb rf hmap A :=
∃ ga, << GAfin: ∃ max, ∀ n, max < n → ga n = None >> ∧
<< VLD: ∀ e (IN: In e A), @hmap_valid PS PSg lab sb rf hmap ga e >>.
Definition is_sb_out edge A := is_sb edge ∧ In (hb_fst edge) A.
Definition hmap_valids_strong PS PSg lab sb rf hmap A :=
<< VALIDS: hmap_valids lab sb rf hmap A >> ∧
<< RESTR: ∀ e (NIN: ¬ In e A) edge,
(hb_fst edge = e ∨ (hb_snd edge = Some e ∧ ¬ is_sb_out edge A)
→ hmap edge = @hemp PS PSg) >>.
Configuration safety
Definition agrees PS PSg (sb: relation actid) rf V (hmap hmap': hbcase → heap PS PSg) :=
∀ a (IN: In a V) b,
(sb a b → hmap (hb_sb a b) = hmap' (hb_sb a b)) ∧
(rf a = Some b → hmap (hb_rf b a) = hmap' (hb_rf b a)).
A logical configuration is a heap-annotated execution that is locally valid
on a prefix-closed set of nodes, V. Such a logical configuration is safe
for n steps, if n=0 or the following three conditions hold:
Fixpoint safe PS PSg acts_cmd acts_ctx lab (sb : relation actid)
rf n V hmap lst (Q : heap PS PSg → Prop) :=
match n with 0 ⇒ True | S n' ⇒
<< POST: ∀ (IN: In lst V) next (SB: sb lst next),
Q (hmap (hb_sb lst next)) >> ∧
<< RELY: ∀ a (INctx: In a acts_ctx) (NIN: ¬ In a V)
(HC': hist_closed sb rf (a :: V)) hmap'
(HEQ : agrees sb rf V hmap hmap')
(VALID' : hmap_valids_strong lab sb rf hmap' (a :: V)),
safe acts_cmd acts_ctx lab sb rf n' (a :: V) hmap' lst Q >> ∧
<< GUAR: ∀ a (INcmd: In a acts_cmd) (NIN: ¬ In a V)
(HC': hist_closed sb rf (a :: V)),
∃ hmap',
<< HEQ : agrees sb rf V hmap hmap' >> ∧
<< VALID : hmap_valids_strong lab sb rf hmap' (a :: V) >> ∧
<< SAFE : safe acts_cmd acts_ctx lab sb rf n' (a :: V) hmap' lst Q >> >>
end.
Definition no_rlx_writes_global lab :=
∀ x : actid, ¬ is_rlx_write (lab x).
Definition no_rlx_writes (acts : list actid) lab :=
∀ x (IN: In x acts), ¬ is_rlx_write (lab x).
The meaning of an RSL triple {P} C {y. QQ(y)} is defined in terms of
configuration safety as follows.
Definition with_opt PS PSg o (QQ : nat → heap PS PSg → Prop) :=
match o with
| None ⇒ fun _ ⇒ True
| Some x ⇒ QQ x
end.
Definition triple PS PSg P e QQ :=
∀ acts_cmd res lab sb fst lst
(SEM : exp_sem e res acts_cmd lab sb fst lst),
(∀ acts_ctx rf mo sc
(CONS : weakConsistent (acts_cmd ++ acts_ctx) lab sb rf mo sc Model_hb_rf_acyclic)
(UNIQ : NoDup (acts_cmd ++ acts_ctx)) prev
(FST : unique (sb^~ fst) prev) next
(LST : unique (sb lst) next) n V
(V_PREV: In prev V)
(V_CTX : ∀ x, In x V → In x acts_ctx)
(HC : hist_closed sb rf V) hmap
(VALID : hmap_valids_strong lab sb rf hmap V)
(pDEF : hmap (hb_sb prev fst) ≠ @Hundef PS PSg) hp hFR
(pEQ : hmap (hb_sb prev fst) = hp +!+ hFR)
(pSAT : assn_sem P hp),
safe acts_cmd acts_ctx lab sb rf n V hmap lst
(with_opt res
(fun res h ⇒ ∃ hFR' hq, h ≠ @Hundef PS PSg ∧ h = hq +!+ hFR +!+ hFR'
∧ assn_sem (QQ res) hq))).
This page has been generated by coqdoc