C11 concurrency model definition


Require Import List Vbase Vlistbase Relations.
Set Implicit Arguments.

Definition immediate X (rel : relation X) (a b: X) :=
  rel a b ( c (R1: rel a c) (R2: rel c b), False).

Definition irreflexive X (rel : relation X) := 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) :=
   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) :=
   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_c11x
    | Model_hb_rf_acyclicy
  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.

Consistency axioms


Section Consistency.

Variable acts : list actid.
List of actions

Variable lab : actid act.
Labeling function

Variable sb : actid actid Prop.
"Sequence before" order

Variable rf : actid option actid.
"Reads from" map

Variable mo : actid actid Prop.
Memory order

Variable sc : actid actid Prop.
Sequential consistency order

Definition sameThread (a b : actid) :=
   c (BAc: clos_refl_trans _ sb a c) (BBc: clos_refl_trans _ sb c b),
    (! pre, sb pre c) (! 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
     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)
   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
  ( c (HB1: happens_before a c) (HB2: happens_before c b),
    ¬ is_writeL (lab c) l).

Definition ExecutionFinite :=
  << CLOlab: a, lab a Askip In a acts >>
  << CLOsb : a b, sb a b In a acts In b acts >>.

Definition ConsistentMO :=
  ( a b (MO: mo a b), l, is_writeL (lab a) l is_writeL (lab b) l)
   transitive _ mo
   ( l, is_total (fun ais_writeL (lab a) l) mo)
   ( l, restr_subset (fun ais_writeL (lab a) l) happens_before mo).

Definition ConsistentSC :=
  transitive _ sc
   is_total (fun xis_sc (lab x)) sc
   restr_subset (fun xis_sc (lab x)) happens_before sc
   restr_subset (fun xis_sc (lab x)) mo sc.

Definition ConsistentRF_basic :=
   a,
    match rf a with
      | None
         b (HB: happens_before b a)
               l v (READ: is_readLV (lab a) l v)
               (WRI: is_writeL (lab b) l), False
      | Some b
           l v, is_readLV (lab a) l v is_writeLV (lab b) l v
    end.

Definition ConsistentRF_no_future :=
   a b (RF: rf b = Some a) (HB: happens_before b a), False.

Definition ConsistentRF_na :=
   a b (RF: rf a = Some b) (NA: is_na (lab a) is_na (lab b)),
    visible (loc (lab a)) b a.

Definition SCrestriction :=
   a b (RF: rf b = Some a) (SC: is_sc (lab b)),
    immediate sc a b
    ¬ is_sc (lab a) ( x (SC: immediate sc x b) (HB: happens_before a x), False).

Definition CoherentRR :=
   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 :=
   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 :=
   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 :=
   a (RMW: is_rmw (lab a)) b (RF: rf a = Some b),
    immediate mo b a.

Definition ConsistentAlloc :=
   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 bhappens_before a b
                      rf b = Some a (is_na (lab b) is_na (lab a))).

Definition AcyclicStrong :=
  acyclic (fun a bhappens_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 :
   (FIN: ExecutionFinite)
         (Crf: ConsistentRF_basic) a b,
    rf a = Some b In a acts In b acts.

Properties describing the absence of memory errors


Definition mem_safe :=
   a (IN: In a acts) (Aa: is_access (lab a)),
   b, lab b = Aalloc (loc (lab a)) happens_before b a.

Definition initialized_reads :=
   a (IN: In a acts) l v (Aa: is_readLV (lab a) l v), rf a None.

Definition race_free :=
   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