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.

Definition release_typ typ := typ = ATrel typ = ATar typ = ATsc.

Definition acquire_typ typ := typ = ATacq typ = ATar typ = ATsc.

Definition acquire_release_typ typ := typ = ATar typ = ATsc.

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)
  | Afence (typ: access_type).

Definition loc a :=
  match a with
    | Askip ⇒ 0
    | Aalloc l
    | Aload _ l _
    | Astore _ l _
    | Armw _ l _ _l
    | Afence _ ⇒ 0
  end.

Definition is_alloc a :=
  match a with
    | Aalloc _true
    | _false
  end.

Definition is_rmw a :=
  match a with
    | Askip | Aalloc _ | Aload _ _ _ | Astore _ _ _ | Afence _false
    | Armw _ _ _ _true
  end.

Definition is_read a :=
  match a with
    | Askip | Aalloc _ | Astore _ _ _ | Afence _false
    | Aload _ _ _ | Armw _ _ _ _true
  end.

Definition is_write a :=
  match a with
    | Askip | Aalloc _ | Aload _ _ _ | Afence _false
    | Astore _ _ _ | Armw _ _ _ _true
  end.

Definition is_access a :=
  match a with
    | Askip | Aalloc _ | Afence _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.

Definition is_at a :=
  match a with
    | Aload ATna _ _
    | Astore ATna _ _
    | Armw ATna _ _ _false
    | _true
  end.

Is the action sequentially consistent?

Definition is_sc a :=
  match a with
    | Aload ATsc _ _
    | Astore ATsc _ _
    | Armw ATsc _ _ _
    | Afence ATsctrue
    | _false
  end.

Is the action a release write or stronger?

Definition is_release_write 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_read 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.

Is the action a fence?

Definition is_fence a :=
  match a with
    | Afence _true
    | _false
  end.

Is the action a release fence or stronger?

Definition is_release_fence a :=
  match a with
    | Afence ATreltrue
    | Afence ATartrue
    | Afence ATsctrue
    | _false
  end.

Is the action an acquire fence or stronger?

Definition is_acquire_fence a :=
  match a with
    | Afence ATacqtrue
    | Afence ATartrue
    | Afence ATsctrue
    | _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).

We use the alternative definition proposed by the paper of Vafeiadis et al. entitled "Common compiler optimisations are invalid in the C11 memory model and what we can do about it.", POPL'15

Inductive release_seq (a b : actid) : Prop :=
| RS_refl (EQ: a = b)
| RS_thr (RSthr: sb a b)
         (RSmo: mo a b)
| RS_rmw c (RS: release_seq a c)
        (RSrf: rf b = Some c)
        (RSrmw: is_rmw (lab b)).

Definition synchronizes_with (a b : actid) :=
     ( is_release_write (lab a) is_acquire_read (lab b)
        c, release_seq a c rf b = Some c)
   ( is_release_write (lab a) is_acquire_fence (lab b)
        c a', clos_refl_trans _ sb c b release_seq a a' rf c = Some a' )
   ( is_release_fence (lab a) is_acquire_read (lab b)
        c c', clos_refl_trans _ sb a c release_seq c c' rf b = some c' )
   ( is_release_fence (lab a) is_acquire_fence (lab b)
        c c' d, clos_refl_trans _ sb a c clos_refl_trans _ sb d b
                      release_seq c c' rf d = 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.
Proof.
  ins; red; red in H; des; intuition.
  unfold with_mt in *; simpl.
  by intros a b ? ?; eapply (Crf' a), (t_trans _ _ _ b); vauto.
Qed.

Lemma ConsistentWeaken2 mt :
  Consistent mt weakConsistent mt.
Proof.
  ins; red; red in H; des; intuition; destruct mt; ins.
  intros x H; apply (IRR x); revert H; generalize x at 1 3.
  induction 1; desf; vauto; edestruct Cna; eauto using clos_trans.
Qed.

Lemma finiteRF :
   (FIN: ExecutionFinite)
         (Crf: ConsistentRF_basic) a b,
    rf a = Some b In a acts In b acts.
Proof.
  unfold ExecutionFinite; ins; desf.
  specialize (Crf a); desf; desf.
  generalize (CLOlab a); destruct (lab a); ins;
  generalize (CLOlab b); destruct (lab b); ins; intuition congruence.
Qed.

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