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_c11 ⇒ x
    | Model_hb_rf_acyclic ⇒ y
  end.

Definition actid := nat.

Inductive access_type :=
  | ATsc
  | ATar
  | ATacq
  | ATrel
  | ATrlx
  | ATna.

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

Definition acquire_typ typ := typ = ATacq ∨ 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 ATsc ⇒ true
    | _ ⇒ 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 ATrel ⇒ true
    | Afence ATar ⇒ true
    | Afence ATsc ⇒ true
    | _ ⇒ false
  end.

Is the action an acquire fence or stronger?
Definition is_acquire_fence a :=
  match a with
    | Afence ATacq ⇒ true
    | Afence ATar ⇒ true
    | Afence ATsc ⇒ 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).

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 a ⇒ is_writeL (lab a) l) mo)
  ∧ (∀ 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 :=
  ∀ 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 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.
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