Require Import List Vbase Relations ExtraRelations actions.
Require Import Peano_dec Classical.
Set Implicit Arguments.
Inductive modeltyp :=
| MTorig
| MTnaive
| MThbUrfnaAcyclic
| MThbUrfAcyclic
| MTdsbUrfAcyclic.
Inductive modeltyp_threadid :=
| MT2orig
| MT2sb.
Inductive modeltyp_relseq :=
| MT3orig
| MT3rf.
Inductive modeltyp_screads :=
| MTSCorig
| MTSChb.
We parametrise the model with the types
Variable mt : modeltyp.
Variable mt2 : modeltyp_threadid * modeltyp_relseq.
Variable mtsc : modeltyp_screads.
An execution contains:
- a sequence of events (actions identifiers), acts,
- a labeling function, lab, mapping action identifiers to the actions,
- the "sequence before" order, sb,
- the "dependent sequence before" relation, dsb, a subset of sb with semantic dependencies,
- the "additional synchronizes with" relation, asw,
- the "reads from" map, rf,
- the modification order, mo, and
- the sequential consistency order, sc
Variable acts : list actid.
Variable lab : actid → act.
Variable sb : actid → actid → Prop.
Variable dsb : actid → actid → Prop.
Variable asw : actid → actid → Prop.
Variable rf : actid → option actid.
Variable mo : actid → actid → Prop.
Variable sc : actid → actid → Prop.
Definition of when two events belong to the same thread. Depending on the
model parameters, either the thread identifiers must match, or the actions have
to be ordered by sb.
Definition same_thread (a b : actid) :=
match fst mt2 with
| MT2orig ⇒ thread (lab a) = thread (lab b)
| MT2sb ⇒ clos_trans _ sb a b
end.
Definition of when two events can synchronise because they belong to different
threads. Depending on the model parameters, either always, or when the thread
identifiers are different.
Definition diff_thread (a b : actid) :=
match fst mt2 with
| MT2orig ⇒ thread (lab a) ≠ thread (lab b)
| MT2sb ⇒ True
end.
Definition of release sequences
Definition release_seq_elem (a b : actid) :=
same_thread a b ∨ is_rmw (lab b).
Inductive release_seq_alt (a b : actid) : Prop :=
| RS_refl (EQ: a = b)
| RS_thr (RSthr: same_thread a b)
(RSmo: mo a b)
| RS_rmw c (RS: release_seq_alt a c)
(RSrf: rf b = Some c)
(RSrmw: is_rmw (lab b)).
Definition release_seq (a b : actid) :=
match snd mt2 with
| MT3orig ⇒
a = b ∨
≪ RSMO: mo a b ≫ ∧
≪ RSE: release_seq_elem a b ≫ ∧
≪ RSO: ∀ c (MA: mo a c) (MB: mo c b), release_seq_elem a c ≫
| MT3rf ⇒ release_seq_alt a b
end.
Definition of when two events synchronise with one another.
Definition synchronizes_with (flag : bool) (a b : actid) :=
(≪ SWrel: is_release_write (lab a) ≫ ∧
≪ SWacq: is_acquire_read (lab b) ≫ ∧
≪ SWthr: if flag then diff_thread a b else ¬ same_thread a b ≫ ∧
∃ c,
≪ RS: release_seq a c ≫ ∧
≪ RF: rf b = Some c ≫ ∧
≪ AT: ¬ is_na (lab c) ≫)
∨ (≪ SWrel: is_release_write (lab a) ≫ ∧
≪ SWacq: is_acquire_fence (lab b) ≫ ∧
≪ SWthr: if flag then diff_thread a b else ¬ same_thread a b ≫ ∧
∃ c a',
≪ SBR: clos_trans _ sb c b ≫ ∧
≪ RS: release_seq a a' ≫ ∧
≪ RF: rf c = Some a' ≫ ∧
≪ AT: ¬ is_na (lab a') ≫ ∧
≪ AT': ¬ is_na (lab c) ≫)
∨ (≪ SWrel: is_release_fence (lab a) ≫ ∧
≪ SWacq: is_acquire_read (lab b) ≫ ∧
≪ SWthr: if flag then diff_thread a b else ¬ same_thread a b ≫ ∧
∃ c c',
≪ SBW: clos_trans _ sb a c ≫ ∧
≪ RS: release_seq c c' ≫ ∧
≪ RF: rf b = some c' ≫ ∧
≪ AT: ¬ is_na (lab c) ≫ ∧
≪ AT': ¬ is_na (lab c') ≫)
∨ (≪ SWrel: is_release_fence (lab a) ≫ ∧
≪ SWacq: is_acquire_fence (lab b) ≫ ∧
≪ SWthr: if flag then diff_thread a b else ¬ same_thread a b ≫ ∧
∃ c c' d,
≪ SBW : clos_trans _ sb a c ≫ ∧
≪ SBR : clos_trans _ sb d b ≫ ∧
≪ RS: release_seq c c' ≫ ∧
≪ RF: rf d = Some c' ≫ ∧
≪ AT: ¬ is_na (lab c) ≫ ∧
≪ AT': ¬ is_na (lab c') ≫ ∧
≪ AT'': ¬ is_na (lab d) ≫).
Happens-before is defined as the transitive closure of the union of three
relations:
Definition happens_before :=
clos_trans _ (fun a b ⇒ sb a b ∨ synchronizes_with true a b ∨ asw a b).
Definition happens_before_alt :=
clos_trans _ (fun a b ⇒ sb a b ∨ synchronizes_with false a b ∨ asw a b).
We require executions to have a finite domain:
Definition ExecutionFinite :=
≪ CLOlab: ∀ a, lab a ≠ Askip 0 → In a acts ≫ ∧
≪ CLOsb : ∀ a b, sb a b ∨ asw a b → In a acts ∧ In b acts ≫.
The modification order, mo, is consistent iff
Definition ConsistentMO :=
≪ CmoD: ∀ a b (MO: mo a b),
∃ l, is_writeL (lab a) l ∧ is_writeL (lab b) l ≫
∧ ≪ CmoT: transitive _ mo ≫
∧ ≪ CmoF: ∀ l, is_total (fun a ⇒ is_writeL (lab a) l) mo ≫
∧ ≪ CmoI: irreflexive mo ≫.
The modification order must also relate any hb-related writes to
the same location. This requirement is equivalent to CoherentWW.
The sequential consistency order, sc, is consitent iff:
- it relates only SC events;
- it is transitive;
- it is total on SC events;
- it is irreflexive;
- it includes happens_before restricted to SC events; and
- it includes mo restricted to SC events.
Definition ConsistentSC :=
≪ CscD: ∀ a b (MO: sc a b), is_sc (lab a) ∧ is_sc (lab b) ≫
∧ ≪ CscT: transitive _ sc ≫
∧ ≪ CscF: is_total (fun x ⇒ is_sc (lab x)) sc ≫
∧ ≪ CscI: irreflexive sc ≫
∧ ≪ Chbsc: restr_subset (fun x ⇒ is_sc (lab x)) happens_before sc ≫
∧ ≪ Cmosc: restr_subset (fun x ⇒ is_sc (lab x)) mo sc ≫.
ConsistentRF_dom_none is the one direction of ConsistentRFdom saying
that reads that happen after a write to the same location must read from
somewhere.
Definition ConsistentRF_dom_none :=
∀ a (RF: rf a = None) b (HB: happens_before b a)
l (READ: is_readL (lab a) l)
(WRI: is_writeL (lab b) l), False.
ConsistentRF_dom_some is the other direction of ConsistentRFdom saying
that reads that read from somewhere must happen after a write to the same
location.
Definition ConsistentRF_dom_some :=
∀ a b (RF: rf a = Some b),
∃ c l,
≪ HB: happens_before c a ≫ ∧
≪ READ: is_readL (lab a) l ≫ ∧
≪ WRI: is_writeL (lab c) l ≫.
The reads-from map is consistent iff it relates only reads and writes to
the same location and with the same values.
Definition ConsistentRF :=
∀ a b (RF: rf a = Some b),
∃ l v,
≪ READ: is_readLV (lab a) l v ≫ ∧
≪ WRITE: is_writeLV (lab b) l v ≫.
The read cannot read from a write happening after it.
The problematic ConsistentRF_na axiom states that a non-atomic read can
read only from a write that happens before it. Similarly, a non-atomic write
can be read only by reads that happen after it.
Definition ConsistentRF_na :=
∀ a b (RF: rf a = Some b) (NA: is_na (lab a) ∨ is_na (lab b)),
happens_before b a.
Next comes the fairly complex SCrestriction axiom stating whence a
sequentially consistent read can read from.
Definition sc_restr a b :=
sc a b ∧ is_write (lab a) ∧ loc (lab a) = loc (lab b).
Definition sc_restr_cond :=
match mtsc with
| MTSCorig ⇒ immediate sc_restr
| MTSCfixed ⇒ sc_restr
end.
Definition SCrestriction :=
∀ a b (RF: rf b = Some a) (SC: is_sc (lab b)),
immediate sc_restr a b ∨
¬ is_sc (lab a)
∧ (∀ x (SC: sc_restr_cond x b) (HB: happens_before a x), False).
Allocation consistency: the same location cannot be allocated twice.
Definition ConsistentAlloc :=
∀ a tida la na (ALLOCa: lab a = Aalloc tida la na)
b tidb lb nb (ALLOCb: lab b = Aalloc tidb lb nb),
a = b ∨ la + na < lb ∨ lb + nb < la.
We move on to the various coherence axioms:
- CoherentWW: the modification order cannot contradict happens-before
- CoherentRR: two happens-before-related reads cannot read the writes in the reverse order of their modification order.
- CoherentWR: a read cannot read from an overwritten write.
- CoherentRW: a read cannot read from a write far in the future.
- AtomicRMW: an RMW can read only from the write that immediately precedes it.
Definition CoherentWW :=
∀ a b (HB: happens_before a b) (MO: mo b a),
False.
Definition CoherentRR :=
∀ a b (HB: happens_before a b)
c (RFa: rf a = Some c) d (RFb: rf b = Some d) (MO: mo d c),
False.
Definition CoherentWR :=
∀ a b (HB: happens_before a b)
c (RF: rf b = Some c) (MO: mo c a),
False.
Definition CoherentRW :=
∀ a b (HB: happens_before a b)
c (RF: rf a = Some c) (MO: mo b c),
False.
Definition AtomicRMW :=
∀ a (RMW: is_rmw (lab a)) b (RF: rf a = Some b),
immediate mo b a.
An alternative, much more compact, coherence axiom.
Definition com x y :=
mo x y ∨ rf y = Some x
∨ ∃ z, rf x = Some z ∧ mo z y ∧ x ≠ y.
Definition Coherence :=
acyclic
(fun x y ⇒ happens_before x y ∧ loc (lab x) = loc (lab y)
∨ com x y).
Next comes the main acyclicity axiom of the model, which depends on the
model type parameter.
Definition rfna a b :=
rf b = Some a ∧ (is_na (lab a) ∨ is_na (lab b)).
Definition AcyclicityAxiom :=
match mt with
| MTnaive ⇒ True
| MTorig ⇒ ConsistentRF_na
| MThbUrfnaAcyclic ⇒ acyclic (fun a b ⇒ happens_before a b ∨ rfna a b)
| MThbUrfAcyclic ⇒ acyclic (fun a b ⇒ happens_before a b ∨ rf b = Some a)
| MTdsbUrfAcyclic ⇒ acyclic (fun a b ⇒ dsb a b ∨ rf b = Some a)
end.
Consistency properties of sb and dsb:
- sb relates only events of the same thread;
- dsb is included in clos_trans _ sb; and
- dsb relates only memory accesses.
Definition ConsistentSB :=
(∀ a b (SB: sb a b), thread (lab a) = thread (lab b)).
Definition ConsistentDSB :=
inclusion _ dsb (clos_trans _ sb) ∧
(∀ a b (DSB: dsb a b), is_access (lab a)) ∧
(∀ a b (DSB: dsb a b), is_access (lab b)).
Definition of when an execution is <em>consistent</em>.
- The Semiconsistent variants are without the ConsistentRF_dom_some axiom.
- The Alt variants use the alternative coherence axiom.
Definition Consistent :=
≪ FIN : ExecutionFinite ≫ ∧
≪ IRR : irreflexive happens_before ≫ ∧
≪ ACYC: AcyclicityAxiom ≫ ∧
≪ Csb: ConsistentSB ≫ ∧
≪ Cdsb: ConsistentDSB ≫ ∧
≪ Cmo : ConsistentMO ≫ ∧
≪ CmoH: ConsistentMOhb ≫ ∧
≪ Csc : ConsistentSC ≫ ∧
≪ Cscr: SCrestriction ≫ ∧
≪ CrfN: ConsistentRF_dom_none ≫ ∧
≪ CrfS: ConsistentRF_dom_some ≫ ∧
≪ Crf : ConsistentRF ≫ ∧
≪ CrfH: ConsistentRFhb ≫ ∧
≪ Crr : CoherentRR ≫ ∧
≪ Cwr : CoherentWR ≫ ∧
≪ Crw : CoherentRW ≫ ∧
≪ Crmw: AtomicRMW ≫ ∧
≪ Ca : ConsistentAlloc ≫.
Definition Semiconsistent :=
≪ FIN : ExecutionFinite ≫ ∧
≪ IRR : irreflexive happens_before ≫ ∧
≪ ACYC: AcyclicityAxiom ≫ ∧
≪ Csb: ConsistentSB ≫ ∧
≪ Cdsb: ConsistentDSB ≫ ∧
≪ Cmo : ConsistentMO ≫ ∧
≪ CmoH: ConsistentMOhb ≫ ∧
≪ Csc : ConsistentSC ≫ ∧
≪ Cscr: SCrestriction ≫ ∧
≪ CrfN: ConsistentRF_dom_none ≫ ∧
≪ Crf : ConsistentRF ≫ ∧
≪ CrfH: ConsistentRFhb ≫ ∧
≪ Crr : CoherentRR ≫ ∧
≪ Cwr : CoherentWR ≫ ∧
≪ Crw : CoherentRW ≫ ∧
≪ Crmw: AtomicRMW ≫ ∧
≪ Ca : ConsistentAlloc ≫.
Definition ConsistentAlt :=
≪ FIN : ExecutionFinite ≫ ∧
≪ ACYC: AcyclicityAxiom ≫ ∧
≪ Csb: ConsistentSB ≫ ∧
≪ Cdsb: ConsistentDSB ≫ ∧
≪ Cmo : ConsistentMO ≫ ∧
≪ Csc : ConsistentSC ≫ ∧
≪ Cscr: SCrestriction ≫ ∧
≪ CrfN: ConsistentRF_dom_none ≫ ∧
≪ CrfS: ConsistentRF_dom_some ≫ ∧
≪ Crf : ConsistentRF ≫ ∧
≪ Coh : Coherence ≫ ∧
≪ Ca : ConsistentAlloc ≫.
Definition SemiconsistentAlt :=
≪ FIN : ExecutionFinite ≫ ∧
≪ ACYC: AcyclicityAxiom ≫ ∧
≪ Csb: ConsistentSB ≫ ∧
≪ Cdsb: ConsistentDSB ≫ ∧
≪ Cmo : ConsistentMO ≫ ∧
≪ Csc : ConsistentSC ≫ ∧
≪ Cscr: SCrestriction ≫ ∧
≪ CrfN: ConsistentRF_dom_none ≫ ∧
≪ Crf : ConsistentRF ≫ ∧
≪ Coh : Coherence ≫ ∧
≪ Ca : ConsistentAlloc ≫.
Properties describing the absence of memory errors
Definition mem_safe :=
∀ a (IN: In a acts) (Aa: is_access (lab a)),
∃ b tid l n,
lab b = Aalloc tid l n ∧
happens_before b a ∧
l ≤ loc (lab a) ≤ l + n.
An execution has no unitialised reads if every read reads from some write,
which for a consistent execution by the ConsistentRF_dom_none axiom means
that there was a write that happened before the read.
An execution is racy if there are two concurrent accesses to the same
location, at least one of which is a write, and at least one of which is
non-atomic.
Definition racy :=
∃ a b,
≪ NEQ: a ≠ b ≫ ∧
≪ Aa: is_access (lab a) ≫ ∧
≪ Ab: is_access (lab b) ≫ ∧
≪ LOC: loc (lab a) = loc (lab b) ≫ ∧
≪ WRI: is_write (lab a) ∨ is_write (lab b) ≫ ∧
≪ NA: is_na (lab a) ∨ is_na (lab b) ≫ ∧
≪ NHB1 : ¬ happens_before a b ≫ ∧
≪ NHB2 : ¬ happens_before b a ≫.
An execution is race-free iff it is not racy.
Definition race_free :=
∀ a (Aa: is_access (lab a))
b (Ab: is_access (lab b))
(LOC: loc (lab a) = loc (lab b)) (NEQ: a ≠ b)
(WRI: is_write (lab a) ∨ is_write (lab b))
(NA: is_na (lab a) ∨ is_na (lab b)),
happens_before a b ∨ happens_before b a.
End Consistency.
Lemma t_sb_in_hb :
∀ mt2 lab sb asw rf mo x y,
clos_trans _ sb x y →
happens_before mt2 lab sb asw rf mo x y.
Lemma sb_in_hb :
∀ mt2 lab (sb : relation actid) asw rf mo x y,
sb x y →
happens_before mt2 lab sb asw rf mo x y.
Lemma sw_in_hb :
∀ mt2 lab (sb asw : relation actid) rf mo x y,
synchronizes_with mt2 lab sb rf mo true x y →
happens_before mt2 lab sb asw rf mo x y.
Lemma asw_in_hb :
∀ mt2 lab (sb asw : relation actid) rf mo x y,
asw x y →
happens_before mt2 lab sb asw rf mo x y.
Lemma t_asw_in_hb :
∀ mt2 lab sb asw rf mo x y,
clos_trans actid asw x y → happens_before mt2 lab sb asw rf mo x y.
Lemma hb_trans :
∀ mt2 lab sb asw rf mo x y z,
happens_before mt2 lab sb asw rf mo x y →
happens_before mt2 lab sb asw rf mo y z →
happens_before mt2 lab sb asw rf mo x z.
Hint Resolve hb_trans sb_in_hb t_sb_in_hb asw_in_hb t_asw_in_hb : hb.
Lemma loceq_mo :
∀ lab mo (C: ConsistentMO lab mo) x y (H: mo x y),
loc (lab x) = loc (lab y).
Lemma loceq_rf :
∀ lab rf (C: ConsistentRF lab rf) x y (H: rf x = Some y),
loc (lab x) = loc (lab y).
Lemma loceq_com :
∀ lab rf (Crf: ConsistentRF lab rf)
mo (Cmo: ConsistentMO lab mo)
x y (H: com rf mo x y),
loc (lab x) = loc (lab y).
Lemma comD :
∀ lab rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo) x y
(C: com rf mo x y),
∃ l, is_accessL (lab x) l ∧ is_accessL (lab y) l.
Lemma finiteRF :
∀ acts lab sb asw
(FIN: ExecutionFinite acts lab sb asw) rf
(Crf: ConsistentRF lab rf) a b,
rf a = Some b → In a acts ∧ In b acts.
Lemma finiteMO :
∀ acts lab sb asw
(FIN: ExecutionFinite acts lab sb asw) mo
(Cmo: ConsistentMO lab mo) a b,
mo a b → In a acts ∧ In b acts.
Lemma finiteSW :
∀ acts lab sb asw
(FIN: ExecutionFinite acts lab sb asw) mt2 rf mo a b,
synchronizes_with mt2 lab sb rf mo true a b → In a acts ∧ In b acts.
Lemma finiteHB :
∀ acts lab sb asw
(FIN: ExecutionFinite acts lab sb asw) mt2 rf mo a b,
happens_before mt2 lab sb asw rf mo a b → In a acts ∧ In b acts.
Lemma finiteCOM :
∀ acts lab sb asw
(FIN: ExecutionFinite acts lab sb asw) rf
(Crf: ConsistentRF lab rf) mo
(Cmo: ConsistentMO lab mo) a b,
com rf mo a b → In a acts ∧ In b acts.
Lemma race_free_iff_not_racy :
∀ mt2 lab sb asw rf mo,
race_free mt2 lab sb asw rf mo ↔ ¬ racy mt2 lab sb asw rf mo.
Lemma racy_if_not_race_free :
∀ mt2 lab sb asw rf mo,
racy mt2 lab sb asw rf mo ↔ ¬ race_free mt2 lab sb asw rf mo.
Tactics to kill inconsistent goals
Ltac kill_incons Aa Ab :=
match goal with
| Crf : ConsistentRF _ ?rf ,
Cmo : ConsistentMO _ ?mo ,
Csc : ConsistentSC _ _ _ _ ?rf ?mo ?sc |- _ ⇒
try by repeat match goal with
| H : sc _ _ |- _ ⇒ apply Csc in H; desc
| H : rf _ = _ |- _ ⇒ apply Crf in H; desc
| H : mo _ _ |- _ ⇒ apply Cmo in H; desc
| H : com rf mo _ _ |- _ ⇒ apply (comD Crf Cmo) in H; desc end;
try rewrite Aa in *; try rewrite Ab in *; ins; desf; eauto
end.
Ltac kill_incons2 Aa Ab :=
match goal with
| Crf : ConsistentRF ?lab ?rf ,
Cmo : ConsistentMO ?lab ?mo |- _ ⇒
try by repeat match goal with
| H : rf _ = _ |- _ ⇒ apply Crf in H; desc
| H : mo _ _ |- _ ⇒ apply Cmo in H; desc
| H : com rf mo _ _ |- _ ⇒ apply (comD Crf Cmo) in H; desc end;
try rewrite Aa in *; try rewrite Ab in *; ins; desf; eauto
end.
Duplicate and destruct:
Ltac dupdes H :=
let H' := fresh H in
assert (H' := H); red in H'; desc.
Theorem Consistent_weaken mt mt2 mtsc acts lab sb dsb asw rf mo sc :
Consistent mt mt2 mtsc acts lab sb dsb asw rf mo sc →
Semiconsistent mt mt2 mtsc acts lab sb dsb asw rf mo sc.
Theorem Consistent_orig_hbUrfnaAcyclic :
∀ mt2 mtsc acts lab sb dsb asw rf mo sc,
Consistent MTorig mt2 mtsc acts lab sb dsb asw rf mo sc →
Consistent MThbUrfnaAcyclic mt2 mtsc acts lab sb dsb asw rf mo sc.
Theorem Consistent_hbUrfnaAcyclic_orig :
∀ mt2 mtsc acts lab sb dsb asw rf mo sc,
Consistent MThbUrfnaAcyclic mt2 mtsc acts lab sb dsb asw rf mo sc →
race_free mt2 lab sb asw rf mo →
Consistent MTorig mt2 mtsc acts lab sb dsb asw rf mo sc.
Theorem Consistent_hbUrfAcyclic_X :
∀ mt (MT: mt ≠ MTorig) mt2 mtsc acts lab sb dsb asw rf mo sc,
Consistent MThbUrfAcyclic mt2 mtsc acts lab sb dsb asw rf mo sc →
Consistent mt mt2 mtsc acts lab sb dsb asw rf mo sc.
Theorem Consistent_hbUrfAcyclic_orig :
∀ mt2 mtsc acts lab sb dsb asw rf mo sc,
Consistent MThbUrfAcyclic mt2 mtsc acts lab sb dsb asw rf mo sc →
race_free mt2 lab sb asw rf mo →
Consistent MTorig mt2 mtsc acts lab sb dsb asw rf mo sc.
Definition no_rlx a :=
match a with
| Aload _ RATrlx _ _ ⇒ false
| Astore _ WATrlx _ _ ⇒ false
| Armw _ UATrlx _ _ _ ⇒ false
| Armw _ UATrel _ _ _ ⇒ false
| Armw _ UATacq _ _ _ ⇒ false
| _ ⇒ true
end.
Theorem Consistent_hbUrfnaAcyclic_hbUrfAcyclic :
∀ acts mt2 mtsc lab sb dsb asw rf mo sc,
Consistent MThbUrfnaAcyclic (MT2sb, mt2) mtsc acts lab sb dsb asw rf mo sc →
(∀ a, no_rlx (lab a)) →
Consistent MThbUrfAcyclic (MT2sb, mt2) mtsc acts lab sb dsb asw rf mo sc.
Changing the mtsc from MTSCorig to MTSChb strengthens the model:
happens-before remains the same (it does not depend on mtsc), while
fewer executions are consistent.
Theorem Consistent_mtsc :
∀ acts mt mt2 lab sb dsb asw rf mo sc,
Consistent mt mt2 MTSChb acts lab sb dsb asw rf mo sc →
Consistent mt mt2 MTSCorig acts lab sb dsb asw rf mo sc.
Changing the mt3 from MT3orig to MT3rf strengthens the model,
under the assumption that every RMW is initialised.
Lemma initialized_rmw_immediate:
∀ lab rf mo a b
(Init: ∀ c, is_rmw (lab c) → ∃ d, rf c = Some d)
(Armw: AtomicRMW lab rf mo)
(Imm: immediate mo a b)
(Rmw: is_rmw (lab b))
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo),
rf b = Some a.
Lemma mo_immediate_mo_left:
∀ lab mo a b c
(Cmo: ConsistentMO lab mo)
(Neq: a ≠ b)
(MOac: mo a c)
(Immbc: immediate mo b c),
mo a b.
Lemma release_seq_mt3:
∀ mt2 acts lab sb asw rf mo a b
(RS: release_seq (mt2, MT3orig) lab sb rf mo a b)
(Init: ∀ c, is_rmw (lab c) → ∃ d, rf c = Some d)
(EF: ExecutionFinite acts lab sb asw)
(Armw: AtomicRMW lab rf mo)
(Cmo: ConsistentMO lab mo)
(Crf: ConsistentRF lab rf),
release_seq (mt2, MT3rf) lab sb rf mo a b.
Lemma synchronizes_with_mt3:
∀ mt2 acts lab sb asw rf mo flag a b
(SW: synchronizes_with (mt2, MT3orig) lab sb rf mo flag a b)
(Init: ∀ c, is_rmw (lab c) → ∃ d, rf c = Some d)
(EF: ExecutionFinite acts lab sb asw)
(Armw: AtomicRMW lab rf mo)
(Cmo: ConsistentMO lab mo)
(Crf: ConsistentRF lab rf),
synchronizes_with (mt2, MT3rf) lab sb rf mo flag a b.
Lemma happens_before_mt3:
∀ mt2 acts lab sb asw rf mo a b
(HB: happens_before (mt2, MT3orig) lab sb asw rf mo a b)
(Init: ∀ c, is_rmw (lab c) → ∃ d, rf c = Some d)
(EF: ExecutionFinite acts lab sb asw)
(Armw: AtomicRMW lab rf mo)
(Cmo: ConsistentMO lab mo)
(Crf: ConsistentRF lab rf),
happens_before (mt2, MT3rf) lab sb asw rf mo a b.
Theorem Semiconsistent_mt3 :
∀ acts mt mt2 mtsc lab sb dsb asw rf mo sc
(MT: mt ≠ MTorig)
(CONS: Semiconsistent mt (mt2, MT3rf) mtsc acts lab sb dsb asw rf mo sc)
(Init: ∀ a, is_rmw (lab a) → ∃ b, rf a = Some b),
Semiconsistent mt (mt2, MT3orig) mtsc acts lab sb dsb asw rf mo sc.
The definition of happens-before as shown in the paper is equivalent
to the one used here.
Theorem happens_before_altE mt2 lab sb asw rf mo :
happens_before_alt mt2 lab sb asw rf mo
<-→ happens_before mt2 lab sb asw rf mo.
Taking the transitive closure of sb does not affect consistency
and the safety properties.
Lemma clos_trans_of_clos_trans :
∀ X R (a b : X),
clos_trans _ (clos_trans _ R) a b ↔ clos_trans _ R a b.
Lemma same_thread_of_t_sb :
∀ mt2 lab sb a b,
same_thread mt2 lab (clos_trans actid sb) a b
↔ same_thread mt2 lab sb a b.
Lemma release_seq_elem_of_t_sb :
∀ mt2 lab sb a b,
release_seq_elem mt2 lab (clos_trans actid sb) a b
↔ release_seq_elem mt2 lab sb a b.
Lemma release_seq_of_t_sb :
∀ mt2 lab sb rf mo a b,
release_seq mt2 lab (clos_trans actid sb) rf mo a b
↔ release_seq mt2 lab sb rf mo a b.
Lemma sw_of_t_sb :
∀ mt2 lab sb rf mo flag a b,
synchronizes_with mt2 lab (clos_trans _ sb) rf mo flag a b
↔ synchronizes_with mt2 lab sb rf mo flag a b.
Lemma hb_of_t_sb :
∀ mt2 lab sb asw rf mo a b,
happens_before mt2 lab (clos_trans _ sb) asw rf mo a b
↔ happens_before mt2 lab sb asw rf mo a b.
Lemma Consistent_of_t_sb :
∀ mt mt2 mtsc acts lab sb dsb asw rf mo sc,
Semiconsistent mt mt2 mtsc acts lab (clos_trans _ sb) dsb asw rf mo sc ↔
Semiconsistent mt mt2 mtsc acts lab sb dsb asw rf mo sc.
Lemma mem_safe_of_t_sb :
∀ mt2 acts lab sb asw rf mo,
mem_safe mt2 acts lab (clos_trans _ sb) asw rf mo ↔
mem_safe mt2 acts lab sb asw rf mo.
Lemma race_free_of_t_sb :
∀ mt2 lab sb asw rf mo,
race_free mt2 lab (clos_trans _ sb) asw rf mo ↔
race_free mt2 lab sb asw rf mo.
Similarly, taking the transitive closure of asw does not affect
consistency and the safety properties.
Lemma hb_of_t_asw :
∀ mt2 lab sb asw rf mo a b,
happens_before mt2 lab sb (clos_trans _ asw) rf mo a b
↔ happens_before mt2 lab sb asw rf mo a b.
Theorem Consistent_of_t_asw :
∀ mt mt2 mtsc acts lab sb dsb asw rf mo sc,
Semiconsistent mt mt2 mtsc acts lab sb dsb (clos_trans _ asw) rf mo sc ↔
Semiconsistent mt mt2 mtsc acts lab sb dsb asw rf mo sc.
Lemma mem_safe_of_t_asw :
∀ mt2 acts lab sb asw rf mo,
mem_safe mt2 acts lab sb (clos_trans _ asw) rf mo ↔
mem_safe mt2 acts lab sb asw rf mo.
Lemma race_free_of_t_asw :
∀ mt2 lab sb asw rf mo,
race_free mt2 lab sb (clos_trans _ asw) rf mo ↔
race_free mt2 lab sb asw rf mo.
This page has been generated by coqdoc