Require Import List Vbase Vlistbase Relations.
Set Implicit Arguments.
Definition immediate X (rel : relation X) (a b: X) :=
rel a b /\ (forall c (R1: rel a c) (R2: rel c b), False).
Definition irreflexive X (rel : relation X) := forall x, rel x x -> False.
Definition acyclic X (rel : relation X) := irreflexive (clos_trans X rel).
Definition is_total X (cond: X -> Prop) (rel: relation X) :=
forall a (IWa: cond a)
b (IWb: cond b) (NEQ: a <> b),
rel a b \/ rel b a.
Definition restr_subset X (cond: X -> Prop) (rel rel': relation X) :=
forall a (IWa: cond a)
b (IWb: cond b) (REL: rel a b),
rel' a b.
Inductive model_type := Model_standard_c11 | Model_hb_rf_acyclic.
Definition with_mt A mt (x y: A) :=
match mt with
| Model_standard_c11 => x
| Model_hb_rf_acyclic => y
end.
Definition actid := nat.
Inductive access_type :=
| ATsc
| ATar
| ATacq
| ATrel
| ATrlx
| ATna.
Inductive act :=
| Askip
| Aalloc (l : nat)
| Aload (typ : access_type) (l : nat) (v : nat)
| Astore (typ : access_type) (l : nat) (v : nat)
| Armw (typ : access_type) (l : nat) (v v': nat).
Definition loc a :=
match a with
| Askip => 0
| Aalloc l
| Aload _ l _
| Astore _ l _
| Armw _ l _ _ => l
end.
Definition is_rmw a :=
match a with
| Askip | Aalloc _ | Aload _ _ _ | Astore _ _ _ => false
| Armw _ _ _ _ => true
end.
Definition is_write a :=
match a with
| Askip | Aalloc _ | Aload _ _ _ => false
| Astore _ _ _ | Armw _ _ _ _ => true
end.
Definition is_access a :=
match a with
| Askip | Aalloc _ => false
| Aload _ _ _ | Astore _ _ _ | Armw _ _ _ _ => true
end.
Definition is_writeL a l :=
match a with
| Astore _ l' _
| Armw _ l' _ _ => l' = l
| _ => False
end.
Definition is_writeLV a l v :=
match a with
| Astore _ l' v'
| Armw _ l' _ v' => l' = l /\ v' = v
| _ => False
end.
Definition is_readLV a l v :=
match a with
| Aload _ l' v'
| Armw _ l' v' _ => l' = l /\ v' = v
| _ => False
end.
Definition is_na a :=
match a with
| Aload ATna _ _
| Astore ATna _ _
| Armw ATna _ _ _ => true
| _ => false
end.
Is the action sequentially consistent?
Definition is_sc a :=
match a with
| Aload ATsc _ _
| Astore ATsc _ _
| Armw ATsc _ _ _ => true
| _ => false
end.
Is the action a release write or stronger?
Definition is_release a :=
match a with
| Astore ATsc _ _
| Astore ATar _ _
| Astore ATrel _ _
| Armw ATsc _ _ _
| Armw ATar _ _ _
| Armw ATrel _ _ _ => true
| _ => false
end.
Is the action an acquire read or stronger?
Definition is_acquire a :=
match a with
| Aload ATsc _ _
| Aload ATar _ _
| Aload ATacq _ _
| Armw ATsc _ _ _
| Armw ATar _ _ _
| Armw ATacq _ _ _ => true
| _ => false
end.
Is the action a relaxed write or an RMW with a relaxed write ?
Definition is_rlx_write a :=
match a with
| Astore ATacq _ _ => true
| Astore ATrlx _ _ => true
| Armw ATacq _ _ _ => true
| Armw ATrlx _ _ _ => true
| _ => false
end.
List of actions
Labeling function
"Sequence before" order
"Reads from" map
Memory order
Sequential consistency order
Definition sameThread (a b : actid) :=
forall c (BAc: clos_refl_trans _ sb a c) (BBc: clos_refl_trans _ sb c b),
(exists! pre, sb pre c) /\ (exists! post, sb c post).
Definition release_seq_elem (a b : actid) :=
sameThread a b \/ is_rmw (lab b).
Definition release_seq (a b : actid) :=
a = b \/
mo a b /\ release_seq_elem a b
/\ forall c (MA: mo a c) (MB: mo c b), release_seq_elem a c.
Definition synchronizes_with (a b : actid) :=
is_release (lab a) /\ is_acquire (lab b) /\
exists c, release_seq a c /\ rf b = Some c.
Definition imm_happens_before a b :=
sb a b \/ synchronizes_with a b.
Definition happens_before :=
clos_trans _ imm_happens_before.
Definition visible l a b :=
happens_before a b /\
(forall c (HB1: happens_before a c) (HB2: happens_before c b),
~ is_writeL (lab c) l).
Definition ExecutionFinite :=
<< CLOlab: forall a, lab a <> Askip -> In a acts >> /\
<< CLOsb : forall a b, sb a b -> In a acts /\ In b acts >>.
Definition ConsistentMO :=
(forall a b (MO: mo a b), exists l, is_writeL (lab a) l /\ is_writeL (lab b) l)
/\ transitive _ mo
/\ (forall l, is_total (fun a => is_writeL (lab a) l) mo)
/\ (forall l, restr_subset (fun a => is_writeL (lab a) l) happens_before mo).
Definition ConsistentSC :=
transitive _ sc
/\ is_total (fun x => is_sc (lab x)) sc
/\ restr_subset (fun x => is_sc (lab x)) happens_before sc
/\ restr_subset (fun x => is_sc (lab x)) mo sc.
Definition ConsistentRF_basic :=
forall a,
match rf a with
| None =>
forall b (HB: happens_before b a)
l v (READ: is_readLV (lab a) l v)
(WRI: is_writeL (lab b) l), False
| Some b =>
exists l v, is_readLV (lab a) l v /\ is_writeLV (lab b) l v
end.
Definition ConsistentRF_no_future :=
forall a b (RF: rf b = Some a) (HB: happens_before b a), False.
Definition ConsistentRF_na :=
forall a b (RF: rf a = Some b) (NA: is_na (lab a) \/ is_na (lab b)),
visible (loc (lab a)) b a.
Definition SCrestriction :=
forall a b (RF: rf b = Some a) (SC: is_sc (lab b)),
immediate sc a b \/
~ is_sc (lab a) /\ (forall x (SC: immediate sc x b) (HB: happens_before a x), False).
Definition CoherentRR :=
forall a b (HB: happens_before a b) (LOC: loc (lab a) = loc (lab 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) (LOC: loc (lab a) = loc (lab b))
c (RF: rf b = Some c) (MO: mo c a),
False.
Definition CoherentRW :=
forall a b (HB: happens_before a b) (LOC: loc (lab a) = loc (lab 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.
Definition ConsistentAlloc :=
forall l a (ALLOCa: lab a = Aalloc l) b (ALLOCb: lab b = Aalloc l),
a = b.
Definition IrreflexiveHB :=
irreflexive happens_before.
Definition AcyclicMedium :=
acyclic (fun a b => happens_before a b \/
rf b = Some a /\ (is_na (lab b) \/ is_na (lab a))).
Definition AcyclicStrong :=
acyclic (fun a b => happens_before a b \/ rf b = Some a).
Definition Consistent mt :=
<< FIN : ExecutionFinite >> /\
<< IRR : IrreflexiveHB >> /\
<< Cmo : ConsistentMO >> /\
<< Csc : ConsistentSC >> /\
<< Crf : ConsistentRF_basic >> /\
<< Crf': with_mt mt ConsistentRF_no_future AcyclicStrong >> /\
<< Cna : ConsistentRF_na >> /\
<< Csc': SCrestriction >> /\
<< Crr : CoherentRR >> /\
<< Cwr : CoherentWR >> /\
<< Crw : CoherentRW >> /\
<< Crmw: AtomicRMW >> /\
<< Ca : ConsistentAlloc >>.
Definition weakConsistent mt :=
<< FIN : ExecutionFinite >> /\
<< IRR : IrreflexiveHB >> /\
<< ACYC: with_mt mt AcyclicMedium AcyclicStrong >> /\
<< Cmo : ConsistentMO >> /\
<< Csc : ConsistentSC >> /\
<< Crf : ConsistentRF_basic >> /\
<< Crf': with_mt mt ConsistentRF_no_future True >> /\
<< Csc': SCrestriction >> /\
<< Crr : CoherentRR >> /\
<< Cwr : CoherentWR >> /\
<< Crw : CoherentRW >> /\
<< Crmw: AtomicRMW >> /\
<< Ca : ConsistentAlloc >>.
Lemma ConsistentWeaken :
Consistent Model_hb_rf_acyclic -> Consistent Model_standard_c11.
Lemma ConsistentWeaken2 mt :
Consistent mt -> weakConsistent mt.
Lemma finiteRF :
forall (FIN: ExecutionFinite)
(Crf: ConsistentRF_basic) a b,
rf a = Some b -> In a acts /\ In b acts.
Definition mem_safe :=
forall a (IN: In a acts) (Aa: is_access (lab a)),
exists b, lab b = Aalloc (loc (lab a)) /\ happens_before b a.
Definition initialized_reads :=
forall a (IN: In a acts) l v (Aa: is_readLV (lab a) l v), rf a <> None.
Definition race_free :=
forall a (INa: In a acts) (Aa: is_access (lab a))
b (INb: In b acts) (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.
This page has been generated by coqdoc Imprint | Data protection