Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps rslassn.
Set Implicit Arguments.
Infix "+!+" := hplus (at level 30, right associativity).
Inductive hbcase :=
| hb_sw (e e': nat)
| hb_sb (e e': nat).
Definition hbcase_eq a b :=
match a, b with
| hb_sw a1 a2, hb_sw b1 b2 ⇒ (a1 == b1) && (a2 == b2)
| hb_sb a1 a2, hb_sb b1 b2 ⇒ (a1 == b1) && (a2 == b2)
| _, _ ⇒ false
end.
Lemma hbcase_eqP : Equality.axiom hbcase_eq.
Proof.
induction[] x [y]; ins; vauto; repeat case eqP; ins;
try (constructor; congruence).
Qed.
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_sw e _ | hb_sb e _ ⇒ e end.
Definition hb_snd edge :=
match edge with hb_sw _ e | hb_sb _ e ⇒ e end.
We do not annotate all sw edges, but rather only the rf edges from a
release-write to an acquire-read.
Definition ann_sw lab rf (a b: actid) :=
is_release (lab a) ∧ is_acquire (lab b) ∧ rf b = Some a.
Definition edge_valid lab sb rf edge :=
match edge with
| hb_sb a b ⇒ sb a b
| hb_sw a b ⇒ ann_sw lab rf a b
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 mt lab (sb : relation actid) rf mo (a b: actid) : Prop :=
| hc_edge_sb (HB_SB: sb a b)
| hc_edge_sw (HB_SW: synchronizes_with lab sb rf mo a b)
| hc_edge_rf (HB_RF: rf b = Some a)
(SIDE: mt = Model_hb_rf_acyclic ∨ is_na (lab a) ∨ is_na (lab b)).
Definition hist_closed mt lab sb rf mo (A: list actid) :=
∀ a (IN: In a A) b (HB: hc_edge mt lab sb rf mo b a), In b A.
View shift implication: currently, vshift h h' ↔ h = h', but
we have made most of the proofs not depend directly on this definition,
so as to allow view shifts that change the logical heaps.
We proceed to the definition of local heap annotation validity at a
node e.
Definition hmap_valid lab sb rf (hmap: hbcase → heap) (e: actid) :=
match lab e with
| Astore typ l v ⇒
∃ pre post hf,
<< pU: unique (sb^~ e) pre >> ∧
<< qU: unique (sb e) post >> ∧
<< pEQ : hmap (hb_sb pre e) = Hdef hf >> ∧
<< DISJ :
(<< IV : is_val (hf l) >> ∧
<< qEQ : hmap (hb_sb e post) = Hdef (hupd hf l (HVval v)) >> ∧
<< wEQ : ∀ e', hmap (hb_sw e e') = hemp >>) ∨
(<< NA : typ ≠ ATna >> ∧ ∃ h (P: assn_mod) sws hsink,
<< UPD: vshift (Hdef (initialize hf l))
(hsingl l (HVra (hupd Wemp v P) Remp false true) +!+
hmap (hb_sb e post) +!+
hsum (map hmap (map (hb_sw e) sws)) +!+ hsink) >> ∧
<< TRAN: assn_sem (sval P) h >> ∧
<< swsND: NoDup sws >> ∧
<< swsOK: ∀ x, In x sws ↔ ann_sw lab rf e x >> ∧
<< swsEQ: hsum (map hmap (map (hb_sw e) sws)) +!+ hsink = h >> ∧
<< RLX: typ = ATrlx ∨ typ = ATacq → sval P = Aemp >>) >>
| Aload typ l v ⇒
∃ pre post hf,
<< pU: unique (sb^~ e) pre >> ∧
<< qU: unique (sb e) post >> ∧
<< pEQ: hmap (hb_sb pre e) = Hdef hf >> ∧
<< DISJ :
(<< IV : hf l = HVval v >> ∧
<< qEQ: hmap (hb_sb e post) = hmap (hb_sb pre e) >> ∧
<< wEQ: ∀ e', hmap (hb_sw e' e) = hemp >>) ∨
(<< NA : typ ≠ ATna >> ∧ ∃ sws hw hF P,
<< swsND: NoDup sws >> ∧
<< swsOK: ∀ x, In x sws ↔ ann_sw lab rf x e >> ∧
<< swsEQ: hsum (map hmap (map (hb_sw^~ e) sws)) = Hdef hw >> ∧
<< pEQ': hsingl l (HVra Wemp (hupd Remp v P) false true) +!+ hF
= Hdef hf >> ∧
<< qD : hmap (hb_sb e post) ≠ Hundef >> ∧
<< qEQ: hmap (hb_sb e post) = hsingl l (HVra Wemp Remp false true)
+!+ Hdef hw +!+ hF >> ∧
<< TRAN: assn_sem (sval P) (Hdef hw) >> ∧
<< PREC: precise (sval P) >>) >>
| Askip ⇒
∃ pres posts hf hsink,
<< pND: NoDup pres >> ∧
<< pOK: ∀ x, In x pres ↔ sb x e >> ∧
<< qND: NoDup posts >> ∧
<< qOK: ∀ x, In x posts ↔ sb e x >> ∧
<< pEQ: hsum (map hmap (map (hb_sb^~ e) pres)) = Hdef hf >> ∧
<< qEQ: vshift (Hdef hf)
(hsum (map hmap (map (hb_sb e) posts)) +!+ hsink) >>
| Aalloc l ⇒
∃ pre post hf,
<< pU : unique (sb^~ e) pre >> ∧
<< qU : unique (sb e) post >> ∧
<< pEQ : hmap (hb_sb pre e) = Hdef hf >> ∧
<< NALL: hf l = HVnone >> ∧
<< qEQ : hmap (hb_sb e post) = Hdef (hupd hf l HVuval) ∨ ∃ QQ isrmw,
hmap (hb_sb e post) = Hdef (hupd hf l (HVra QQ QQ isrmw false)) >>
| Armw typ l v v' ⇒
∃ pre post swsIn swsOut,
<< pU: unique (sb^~ e) pre >> ∧
<< qU: unique (sb e) post >> ∧
<< swsInOK: ∀ x, In x swsIn ↔ ann_sw lab rf x e >> ∧
<< swsOutOK: ∀ x, In x swsOut ↔ ann_sw lab rf e x >> ∧
<< swsInND: NoDup swsIn >> ∧
<< swsOutND: NoDup swsOut >> ∧
<< NA : typ ≠ ATna >> ∧
∃ PP QQ PP' hp hi hsink,
<< pEQ: hmap (hb_sb pre e) = Hdef hp >> ∧
<< pEQ': hp l = HVra PP QQ true true >> ∧
<< iEQ: hmap (hb_sb pre e) +!+ hsum (map hmap (map (hb_sw^~ e) swsIn)) = Hdef hi >> ∧
<< UPD: vshift (Hdef hi)
(hsingl l (HVra PP' Remp false false) +!+ hmap (hb_sb e post) +!+
hsum (map hmap (map (hb_sw e) swsOut)) +!+ hsink) >> ∧
<< TRAN: assn_sem (sval (QQ v))
(hsum (map hmap (map (hb_sw^~ e) swsIn))) >> ∧
<< TRAN': assn_sem (sval (PP' v'))
(hsum (map hmap (map (hb_sw e) swsOut)) +!+ hsink) >> ∧
<< RLX: typ = ATrlx ∨ typ = ATacq → sval (PP' v') = Aemp >>
end.
Definition hmap_valids lab sb rf hmap A :=
∀ e (IN: In e A), hmap_valid lab sb rf hmap e.
Configuration safety
Definition agrees lab (sb: relation actid) rf V (hmap hmap': hbcase → heap) :=
∀ a (IN: In a V) b,
(sb a b → hmap (hb_sb a b) = hmap' (hb_sb a b)) ∧
(ann_sw lab rf b a → hmap (hb_sw b a) = hmap' (hb_sw 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 mt acts_cmd acts_ctx lab (sb : relation actid)
rf mo n V hmap lst (Q : heap → 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 mt lab sb rf mo (a :: V)) hmap'
(HEQ : agrees lab sb rf V hmap hmap')
(VALID' : ∀ e (IN: In e (a :: V)),
hmap_valid lab sb rf hmap' e),
safe mt acts_cmd acts_ctx lab sb rf mo n' (a :: V) hmap' lst Q >> ∧
<< GUAR: ∀ a (INcmd: In a acts_cmd) (NIN: ¬ In a V)
(HC': hist_closed mt lab sb rf mo (a :: V)),
∃ hmap',
<< HEQ : agrees lab sb rf V hmap hmap' >> ∧
<< VALID : ∀ e (IN: In e (a :: V)),
hmap_valid lab sb rf hmap' e >> ∧
<< SAFE : safe mt acts_cmd acts_ctx lab sb rf mo 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 o (QQ : nat → heap → Prop) :=
match o with
| None ⇒ fun _ ⇒ True
| Some x ⇒ QQ x
end.
Definition triple mt 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 mt)
(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 mt lab sb rf mo V) hmap
(VALID : ∀ e (IN: In e V), hmap_valid lab sb rf hmap e)
(pDEF : hmap (hb_sb prev fst) ≠ Hundef) hp hFR
(pEQ : hmap (hb_sb prev fst) = hp +!+ hFR)
(pSAT : assn_sem P hp)
(NOREL : with_mt mt (no_rlx_writes_global lab) True),
safe mt acts_cmd acts_ctx lab sb rf mo n V hmap lst
(with_opt res
(fun res h ⇒ ∃ hq, h ≠ Hundef ∧ h = hq +!+ hFR
∧ assn_sem (QQ res) hq))) ∧
with_mt mt (no_rlx_writes acts_cmd lab) True.
This page has been generated by coqdoc Imprint | Data protection