C11 concurrency model definition


Require Import List Vbase 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.

Definition actid := nat.

Inductive read_access_type :=
  | RATsc
  | RATacq

  | RATrlx
  | RATna.

Inductive write_access_type :=
  | WATsc
  | WATrel
  | WATrlx
  | WATna.

Inductive rmw_access_type :=
  | UATsc
  | UATacq_rel
  | UATacq
  | UATrel
  | UATrlx .

Inductive access_type :=
  | ATna
  | ATat.

Inductive act :=
  | Askip
  | Aalloc (l n : nat)
  | Aload (typ : read_access_type) (l : nat) (v : nat)
  | Astore (typ : write_access_type) (l : nat) (v : nat)
  | Armw (typ : rmw_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 accesses_loc a l :=
  match a with
    | Askip | Aalloc _ _False
    | Aload _ l' _
    | Astore _ l' _
    | Armw _ l' _ _l = l'
  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 RATna _ _
    | Astore WATna _ _true
    | _false
  end.

Is the action sequentially consistent?

Definition is_sc a :=
  match a with
    | Aload RATsc _ _
    | Astore WATsc _ _
    | Armw UATsc _ _ _true
    | _false
  end.

Is the action a release write or stronger?

Definition is_release_wtyp t :=
   match t with WATsc | WATreltrue | _false end.

Definition is_release_utyp t :=
   match t with UATsc | UATrel | UATacq_reltrue | _false end.

Definition is_release a :=
  match a with
    | Astore typ _ _is_release_wtyp typ
    | Armw typ _ _ _is_release_utyp typ
    | _false
  end.

Is the action an acquire read or stronger?

Definition is_acquire_rtyp t :=
   match t with RATsc | RATacqtrue | _false end.

Definition is_acquire_utyp t :=
   match t with UATsc | UATacq | UATacq_reltrue | _false end.

Definition is_acquire a :=
  match a with
    | Aload typ _ _is_acquire_rtyp typ
    | Armw typ _ _ _is_acquire_utyp typ
    | _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 synchronizes_with (a b : actid) :=
  rf b = Some a is_release (lab a) is_acquire (lab b).

Definition imm_happens_before a b :=
  sb a b synchronizes_with a b.

Definition happens_before :=
  clos_trans _ imm_happens_before.

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)
   irreflexive mo
   ( l, restr_subset (fun ais_writeL (lab a) l) happens_before mo).

Definition ConsistentSC :=
  ( a b (MO: sc a b), is_sc (lab a) is_sc (lab b))
   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.

Restriction of the SC relation for the SCrestriction axiom
Definition sc_restr a b :=
  sc a b is_write (lab a) loc (lab a) = loc (lab b).

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: immediate sc_restr 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 :=
   a la na (ALLOCa: lab a = Aalloc la na)
         b lb nb (ALLOCb: lab b = Aalloc lb nb),
    a = b la + na < lb lb + nb < la.

Definition AcyclicStrong :=
  acyclic (fun a bsb a b rf b = Some a sc a b).

Definition Consistent :=
   FIN : ExecutionFinite
   ACYC: AcyclicStrong
   Cmo : ConsistentMO
   Csc : ConsistentSC
   Cscr: SCrestriction
   Crf : ConsistentRF_basic
   Crr : CoherentRR
   Cwr : CoherentWR
   Crw : CoherentRW
   Crmw: AtomicRMW
   Ca : ConsistentAlloc .

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) l (Aa: accesses_loc (lab a) l),
   b l' n, lab b = Aalloc l' n happens_before b a l' l l' + n.

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