Require Import List Vbase Relations ExtraRelations actions.
Require Import Peano_dec Classical.
Set Implicit Arguments.
Remove Hints plus_n_O.
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: forall 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 >> /\
exists 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 >> /\
exists 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 >> /\
exists 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 >> /\
exists 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: forall a, lab a <> Askip 0 -> In a acts >> /\
<< CLOsb : forall a b, sb a b \/ asw a b -> In a acts /\ In b acts >>.
The modification order, mo, is consistent iff
Definition ConsistentMO :=
<< CmoD: forall a b (MO: mo a b),
exists l, is_writeL (lab a) l /\ is_writeL (lab b) l >>
/\ << CmoT: transitive _ mo >>
/\ << CmoF: forall 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.
Definition ConsistentMOhb :=
forall l, restr_subset (fun a => is_writeL (lab a) l) happens_before mo.
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: forall 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 :=
forall 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 :=
forall a b (RF: rf a = Some b),
exists 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 :=
forall a b (RF: rf a = Some b),
exists 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 :=
forall 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 :=
forall a b (RF: rf b = Some a) (SC: is_sc (lab b)),
immediate sc_restr a b \/
~ is_sc (lab a)
/\ (forall x (SC: sc_restr_cond x b) (HB: happens_before a x), False).
Allocation consistency: the same location cannot be allocated twice.
Definition ConsistentAlloc :=
forall 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 :=
forall a b (HB: happens_before a b) (MO: mo b a),
False.
Definition CoherentRR :=
forall 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 :=
forall a b (HB: happens_before a b)
c (RF: rf b = Some c) (MO: mo c a),
False.
Definition CoherentRW :=
forall a b (HB: happens_before a b)
c (RF: rf a = Some c) (MO: mo b c),
False.
Definition AtomicRMW :=
forall 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
\/ exists 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 :=
(forall a b (SB: sb a b), thread (lab a) = thread (lab b)).
Definition ConsistentDSB :=
inclusion _ dsb (clos_trans _ sb) /\
(forall a b (DSB: dsb a b), is_access (lab a)) /\
(forall 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 :=
forall a (IN: In a acts) (Aa: is_access (lab a)),
exists 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.
Definition initialized_reads :=
forall a (IN: In a acts) l v (Aa: is_readLV (lab a) l v), rf a <> None.
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 :=
exists 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 :=
forall 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 :
forall mt2 lab sb asw rf mo x y,
clos_trans _ sb x y ->
happens_before mt2 lab sb asw rf mo x y.
Proof.
induction 1; vauto.
Qed.
Lemma sb_in_hb :
forall mt2 lab (sb : relation actid) asw rf mo x y,
sb x y ->
happens_before mt2 lab sb asw rf mo x y.
Proof.
vauto.
Qed.
Lemma sw_in_hb :
forall 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.
Proof.
red; eauto using t_step.
Qed.
Lemma asw_in_hb :
forall mt2 lab (sb asw : relation actid) rf mo x y,
asw x y ->
happens_before mt2 lab sb asw rf mo x y.
Proof.
red; eauto using t_step.
Qed.
Lemma t_asw_in_hb :
forall mt2 lab sb asw rf mo x y,
clos_trans actid asw x y -> happens_before mt2 lab sb asw rf mo x y.
Proof.
induction 1; vauto; eapply t_step; eauto.
Qed.
Lemma hb_trans :
forall 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.
Proof.
vauto.
Qed.
Hint Resolve hb_trans sb_in_hb t_sb_in_hb asw_in_hb t_asw_in_hb : hb.
Lemma loceq_mo :
forall lab mo (C: ConsistentMO lab mo) x y (H: mo x y),
loc (lab x) = loc (lab y).
Proof.
ins; apply (proj1 C) in H; desf; destruct (lab x); ins; destruct (lab y); ins; desf.
Qed.
Lemma loceq_rf :
forall lab rf (C: ConsistentRF lab rf) x y (H: rf x = Some y),
loc (lab x) = loc (lab y).
Proof.
ins; apply C in H; desf; destruct (lab x); ins; destruct (lab y); ins; desf.
Qed.
Lemma loceq_com :
forall 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).
Proof.
unfold com; ins; desf;
try (exploit (loceq_mo Cmo); [edone|]);
try (exploit (loceq_rf Crf); [edone|]);
instantiate; congruence.
Qed.
Lemma comD :
forall lab rf mo
(Crf: ConsistentRF lab rf)
(Cmo: ConsistentMO lab mo) x y
(C: com rf mo x y),
exists l, is_accessL (lab x) l /\ is_accessL (lab y) l.
Proof.
unfold com; ins; desf.
by apply (proj1 Cmo) in C; desf; eauto with access.
by apply Crf in C; desf; eauto with access.
apply Crf in C; apply (proj1 Cmo) in C0; desf.
assert (l0 = l) by (destruct (lab z); ins; desf).
desf; eauto with access.
Qed.
Lemma finiteRF :
forall 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.
Proof.
unfold ExecutionFinite; ins; desf.
apply Crf in H; desf.
generalize (CLOlab a); destruct (lab a); ins;
generalize (CLOlab b); destruct (lab b); ins; intuition congruence.
Qed.
Lemma finiteMO :
forall 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.
Proof.
unfold ExecutionFinite; ins; desf.
apply (proj1 Cmo) in H; desf.
generalize (CLOlab a); destruct (lab a); ins;
generalize (CLOlab b); destruct (lab b); ins; intuition congruence.
Qed.
Lemma finiteSW :
forall 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.
Proof.
unfold synchronizes_with; ins; des;
split; apply FIN; intro X; rewrite X in *; ins.
Qed.
Lemma finiteHB :
forall 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.
Proof.
induction 2; desf; eauto using finiteSW; apply FIN; eauto.
Qed.
Lemma finiteCOM :
forall 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.
Proof.
by ins; eapply comD in H; eauto; desc; split; apply FIN; intro X; rewrite X in *.
Qed.
Lemma race_free_iff_not_racy :
forall mt2 lab sb asw rf mo,
race_free mt2 lab sb asw rf mo <-> ~ racy mt2 lab sb asw rf mo.
Proof.
unfold race_free, racy; split; try red; ins; desc; eauto.
eapply H in WRI; eauto; desf.
apply NNPP; intro; destruct H; unnw; repeat (eexists; try edone); tauto.
Qed.
Lemma racy_if_not_race_free :
forall mt2 lab sb asw rf mo,
racy mt2 lab sb asw rf mo <-> ~ race_free mt2 lab sb asw rf mo.
Proof.
ins; rewrite race_free_iff_not_racy; tauto.
Qed.
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.
Proof.
unfold Consistent, Semiconsistent, NW; intuition.
Qed.
Theorem Consistent_orig_hbUrfnaAcyclic :
forall 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.
Proof.
unfold Consistent; ins; desf; intuition.
intros x A; apply (IRR x); revert A; generalize x at 2 4.
unfold rfna; induction 1; desf; eauto; vauto.
Qed.
Theorem Consistent_hbUrfnaAcyclic_orig :
forall 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.
Proof.
unfold Consistent; ins; desf; intuition.
repeat red; ins.
specialize (Crf _ _ RF); desc.
specialize (CrfH _ _ RF).
destruct H0 with (a:=a) (b:=b); ins.
by destruct (lab a).
by destruct (lab b).
by destruct (lab a); ins; desc; destruct (lab b); ins; desc; desf.
by intro; clarify; apply Crmw, proj1, Cmo in RF; ins; destruct (lab b).
by right; destruct (lab b).
Qed.
Theorem Consistent_hbUrfAcyclic_X :
forall 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.
Proof.
unfold Consistent; ins; desf; repeat (split; try done).
red; red in Cdsb; destruct mt; ins;
intros x A; apply (ACYC x); revert A; generalize x at 2 4;
unfold rfna; induction 1; desf; eauto using clos_trans.
by apply t_step; left; eauto with hb.
Qed.
Theorem Consistent_hbUrfAcyclic_orig :
forall 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.
Proof.
unfold Consistent; ins; desf; repeat (split; try done).
red; red; ins.
assert (a <> b).
clear NA; intro; desf.
eapply Crmw, proj1 in RF.
eby eapply Cmo.
by apply Crf in RF; desf; destruct (lab b); ins.
specialize (CrfH _ _ RF).
eapply H0 in NA; eauto using loceq_rf;
eapply Crf in RF; desc; try (by desf).
by destruct (lab a).
by destruct (lab b).
by right; destruct (lab b).
Qed.
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 :
forall acts mt2 mtsc lab sb dsb asw rf mo sc,
Consistent MThbUrfnaAcyclic (MT2sb, mt2) mtsc acts lab sb dsb asw rf mo sc ->
(forall a, no_rlx (lab a)) ->
Consistent MThbUrfAcyclic (MT2sb, mt2) mtsc acts lab sb dsb asw rf mo sc.
Proof.
unfold Consistent; ins; desf; repeat (split; try done).
intros x A; apply (ACYC x); revert A; generalize x at 2 4.
unfold rfna; induction 1; desf; eauto; vauto.
apply t_step; generalize (H0 x), (H0 y), (Crf _ _ H); ins; desf.
case_eq (is_na (lab x)) as EQx; eauto.
case_eq (is_na (lab y)) as EQy; eauto.
ins; left; apply t_step; right; left; left.
unfold release_seq, same_thread, NW; repeat split; desf; repeat eexists;
eauto 10 using release_seq_alt; instantiate; rewrite ?EQx, ?EQy; ins.
by destruct (lab x); ins; desf.
by destruct (lab y); ins; desf.
Qed.
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 :
forall 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.
Proof.
unfold Consistent; ins; des; repeat (split; try done).
repeat red; ins; edestruct Cscr; des; eauto.
right; split; unfold immediate; ins; des; eauto.
Qed.
Changing the mt3 from MT3orig to MT3rf strengthens the model,
under the assumption that every RMW is initialised.
Lemma initialized_rmw_immediate:
forall lab rf mo a b
(Init: forall c, is_rmw (lab c) -> exists 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.
Proof.
ins.
exploit Init; eauto; intros Hinit; destruct Hinit as (d, Hrfdy); rewrite Hrfdy.
f_equal.
dupdes Crf; exploit Crf0; eauto; ins; desf.
dupdes Imm; dupdes Cmo; eapply CmoD in Imm0; eauto; desf.
assert (l = l0).
by destruct (lab b); inversion Imm2; inversion READ; subst; eauto.
subst.
eapply total_immediate_unique; eauto using eq_nat_dec;
by red; eauto with access.
Qed.
Lemma mo_immediate_mo_left:
forall lab mo a b c
(Cmo: ConsistentMO lab mo)
(Neq: a <> b)
(MOac: mo a c)
(Immbc: immediate mo b c),
mo a b.
Proof.
ins; dupdes Cmo; dupdes Immbc.
generalize MOac Immbc0.
eapply CmoD in MOac; eapply CmoD in Immbc0; desf.
assert (l = l0).
by destruct (lab c); inversion MOac0; inversion Immbc2; subst; eauto.
subst.
destruct (CmoF l0 a MOac b Immbc0); eauto.
ins; exfalso; eauto.
Qed.
Lemma release_seq_mt3:
forall mt2 acts lab sb asw rf mo a b
(RS: release_seq (mt2, MT3orig) lab sb rf mo a b)
(Init: forall c, is_rmw (lab c) -> exists 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.
Proof.
ins.
destruct RS; desf; vauto.
exploit clos_trans_imm2; try (dupdes Cmo; eauto using eq_nat_dec).
intros c hac ?; eapply CmoD in hac.
dupdes EF; eapply CLOlab.
destruct (lab c); inversion hac0; discriminate.
intro Hind.
eapply clos_trans_tn1 in Hind; induction Hind.
destruct RSE.
by eapply RS_thr; eauto.
by eapply RS_rmw; eauto using RS_refl, initialized_rmw_immediate.
destruct RSE.
by eapply RS_thr; eauto.
eapply RS_rmw; eauto using initialized_rmw_immediate.
destruct (eq_nat_dec a y).
by subst; eauto using RS_refl.
eapply IHHind.
by eapply mo_immediate_mo_left; eauto.
eapply RSO.
by eapply mo_immediate_mo_left; eauto.
by dupdes H.
ins; dupdes H; eapply RSO;
by eauto.
Qed.
Lemma synchronizes_with_mt3:
forall mt2 acts lab sb asw rf mo flag a b
(SW: synchronizes_with (mt2, MT3orig) lab sb rf mo flag a b)
(Init: forall c, is_rmw (lab c) -> exists 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.
Proof.
unfold synchronizes_with; ins.
repeat (destruct SW as [SW'|SW]; [left|right]);
by intuition; desf; repeat eexists; eauto using release_seq_mt3.
Qed.
Lemma happens_before_mt3:
forall mt2 acts lab sb asw rf mo a b
(HB: happens_before (mt2, MT3orig) lab sb asw rf mo a b)
(Init: forall c, is_rmw (lab c) -> exists 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.
Proof.
ins; induction HB; desf; vauto;
by eapply t_step; eauto using synchronizes_with_mt3.
Qed.
Theorem Semiconsistent_mt3 :
forall 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: forall a, is_rmw (lab a) -> exists b, rf a = Some b),
Semiconsistent mt (mt2, MT3orig) mtsc acts lab sb dsb asw rf mo sc.
Proof.
unfold Semiconsistent; ins; desf; repeat (split; try done; try by dupdes Csc); try red.
by intros x hxx; eapply IRR; eapply happens_before_mt3; eauto.
destruct mt; simpl; intuition;
intros x hxx; eapply ACYC; eapply clos_trans_monotonic; eauto;
by intros y z hyz; desf; eauto using happens_before_mt3.
by unfold ConsistentMOhb, restr_subset in *; ins; eauto using happens_before_mt3.
by dupdes Csc; unfold restr_subset in *; ins; eauto using happens_before_mt3.
unfold SCrestriction in *; ins; eauto.
by exploit Cscr; eauto; ins; desf; eauto using happens_before_mt3.
by unfold ConsistentRF_dom_none in *; ins; eauto using happens_before_mt3.
by unfold ConsistentRFhb; ins; eauto using happens_before_mt3.
by unfold CoherentRR; ins; eauto using happens_before_mt3.
by unfold CoherentWR; ins; eauto using happens_before_mt3.
by unfold CoherentRW; ins; eauto using happens_before_mt3.
Qed.
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.
Proof.
split; red; ins; induction H; desf; vauto; try (by apply t_step; eauto);
[|apply NNPP; intro X; apply X];
(apply t_step; right; left; red in H; desf;
[left | right; left | do 2 right; left | do 3 right]); unnw;
repeat (eexists; eauto); unfold diff_thread, same_thread in *; desf;
intro Y; destruct X; eapply clos_trans_mon; eauto.
Qed.
Taking the transitive closure of sb does not affect consistency
and the safety properties.
Lemma clos_trans_of_clos_trans :
forall X R (a b : X),
clos_trans _ (clos_trans _ R) a b <-> clos_trans _ R a b.
Proof.
split; ins; eauto using t_step; induction H; vauto.
Qed.
Lemma same_thread_of_t_sb :
forall mt2 lab sb a b,
same_thread mt2 lab (clos_trans actid sb) a b
<-> same_thread mt2 lab sb a b.
Proof.
unfold same_thread; split; ins; desf; ins; desf; unnw; eauto using t_step.
induction H; vauto.
Qed.
Lemma release_seq_elem_of_t_sb :
forall mt2 lab sb a b,
release_seq_elem mt2 lab (clos_trans actid sb) a b
<-> release_seq_elem mt2 lab sb a b.
Proof.
by unfold release_seq_elem; ins; rewrite same_thread_of_t_sb; ins.
Qed.
Lemma release_seq_of_t_sb :
forall 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.
Proof.
unfold release_seq; split; red; ins; desf; ins; desf; unnw; eauto;
try rewrite release_seq_elem_of_t_sb in *; eauto.
by right; intuition; rewrite <- release_seq_elem_of_t_sb; eauto.
by induction H; desf; try rewrite same_thread_of_t_sb in *; vauto.
by right; intuition; rewrite release_seq_elem_of_t_sb; eauto.
by induction H; desf; try rewrite <- same_thread_of_t_sb in *; vauto.
Qed.
Lemma sw_of_t_sb :
forall 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.
Proof.
split; ins; repeat (destruct H as [K | H]; [left|right]); desf; unnw;
repeat eexists; rewrite ?release_seq_of_t_sb, ?same_thread_of_t_sb,
?clos_trans_of_clos_trans in *; edone.
Qed.
Lemma hb_of_t_sb :
forall 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.
Proof.
split; ins; induction H; desf; eauto using t_step with hb;
eapply t_step; try rewrite sw_of_t_sb in *; eauto.
Qed.
Lemma Consistent_of_t_sb :
forall 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.
Proof.
unfold Semiconsistent, NW; split; intro M;
repeat first [split; [apply proj1 in M|apply proj2 in M]; unnw; try red; des_if; ins
|destruct M as [M|M]; [left|right]
|exploit M; eauto; clear M; intro M];
desf; repeat red; ins; try rewrite clos_trans_of_clos_trans in *; ins;
try (by first [eapply M | exploit M]; try rewrite hb_of_t_sb in *; eauto using t_step);
try (by eapply M, clos_trans_mon; eauto; instantiate; ins; desf; rewrite ?hb_of_t_sb in *; eauto).
by induction H; desf; eauto.
by eapply hb_of_t_sb; eauto.
by induction SB; eauto; congruence.
Qed.
Lemma mem_safe_of_t_sb :
forall 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.
Proof.
unfold mem_safe; split; ins; desf; exploit H; eauto; desf; intro M; desf;
repeat eexists; try rewrite hb_of_t_sb in *; eauto.
Qed.
Lemma race_free_of_t_sb :
forall mt2 lab sb asw rf mo,
race_free mt2 lab (clos_trans _ sb) asw rf mo <->
race_free mt2 lab sb asw rf mo.
Proof.
unfold race_free; split; ins; desc.
by rewrite <- !hb_of_t_sb with (sb := sb); eauto.
by rewrite !hb_of_t_sb; eauto.
Qed.
Similarly, taking the transitive closure of asw does not affect
consistency and the safety properties.
Lemma hb_of_t_asw :
forall 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.
Proof.
split; ins; induction H; desf; eauto using t_step with hb;
eapply t_step; eauto.
Qed.
Theorem Consistent_of_t_asw :
forall 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.
Proof.
unfold Semiconsistent, NW; split; intro M;
repeat first [split; [apply proj1 in M|apply proj2 in M]; unnw; try red; des_if; ins
|destruct M as [M|M]; [left|right]
|exploit M; eauto; clear M; intro M];
desf; repeat red; ins;
try (by first [eapply M | exploit M]; try rewrite hb_of_t_asw in *; eauto using t_step);
try (by eapply M, clos_trans_mon; eauto; instantiate; ins; desf; rewrite ?hb_of_t_asw in *; eauto).
by induction H; desf; eauto.
by eapply hb_of_t_asw; eauto.
Qed.
Lemma mem_safe_of_t_asw :
forall 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.
Proof.
unfold mem_safe; split; ins; desf; exploit H; eauto; desf; intro M; desf;
repeat eexists; try rewrite hb_of_t_asw in *; eauto.
Qed.
Lemma race_free_of_t_asw :
forall mt2 lab sb asw rf mo,
race_free mt2 lab sb (clos_trans _ asw) rf mo <->
race_free mt2 lab sb asw rf mo.
Proof.
unfold race_free; split; ins; desc.
by rewrite <- !hb_of_t_asw with (asw := asw); eauto.
by rewrite !hb_of_t_asw; eauto.
Qed.
This page has been generated by coqdoc