A concurrent WHILE language


Require Import List Permutation Vbase Relations ExtraRelations.
Require Import actions c11 opsemsets.
Require Import Classical extralib.
Set Implicit Arguments.

Expressions consist of values, memory allocation, loads, stores, compare and swaps (CAS), fences, let (sequential composition), forking of threads, non-deterministic choice, and loops.

Inductive cexp :=
  | Evalue (n: nat)
  | Ealloc (n: nat)
  | Eload (typ: read_access_type) (l : nat)
  | Estore (typ: write_access_type) (l v : nat)
  | Ecas (typ_succ : rmw_access_type) (typ_fail: read_access_type) (l v v' : nat)
  | Efence (typ: fence_access_type)
  | Elet (e1: cexp) (e2: nat → cexp)
  | Efork (e: cexp)
  | Echoice (e1: cexp) (e2: cexp)
  | Erepeat (e : cexp).

We now give the semantics of these expressions as opsemsets. To do so, we first define some combinators for defining opsemsets.

Definition oss_one_div act o :=
  ∃ a,
     ≪ O_Res : Res o = None ≫
  ∧ ≪ O_Tid : Tid o = thread act ≫
  ∧ ≪ O_Acts : Acts o = a :: nil ≫
  ∧ ≪ O_LabA : Lab o a = act ≫
  ∧ ≪ O_LabB : ∀ b (NEQ: b ≠ a), Lab o b = Askip 0 ≫
  ∧ ≪ O_Sb : ∀ a b (SB: Sb o a b), False ≫
  ∧ ≪ O_Dsb : ∀ a b (SB: Dsb o a b), False ≫
  ∧ ≪ O_Asw : ∀ a b (SB: Asw o a b), False ≫.

Definition oss_one res act o :=
  ∃ a,
     ≪ O_Res : Res o = None ∨ Res o = Some res ≫
  ∧ ≪ O_Tid : Tid o = thread act ≫
  ∧ ≪ O_Acts : Acts o = a :: nil ≫
  ∧ ≪ O_LabA : Lab o a = act ≫
  ∧ ≪ O_LabB : ∀ b (NEQ: b ≠ a), Lab o b = Askip 0 ≫
  ∧ ≪ O_Sb : ∀ a b (SB: Sb o a b), False ≫
  ∧ ≪ O_Dsb : ∀ a b (SB: Dsb o a b), False ≫
  ∧ ≪ O_Asw : ∀ a b (SB: Asw o a b), False ≫.

Definition oss_seqcomp o1 o2 o :=
     ≪ O_Res : Res o = Res o2 ≫
  ∧ ≪ O_TidA : Tid o = Tid o1 ≫
  ∧ ≪ O_TidB : Tid o = Tid o2 ≫
  ∧ ≪ O_Acts : Permutation (Acts o) (Acts o1 ++ Acts o2) ≫
  ∧ ≪ O_ND : NoDup (Acts o) ≫
  ∧ ≪ O_LabA : ∀ x (IN: In x (Acts o1)), Lab o x = Lab o1 x ≫
  ∧ ≪ O_LabB : ∀ x (NIN: ¬ In x (Acts o1)), Lab o x = Lab o2 x ≫
  ∧ ≪ O_Sb : same_relation _ (Sb o)
                               (union _ (fun x y ⇒ In x (Acts o1) ∧ In y (Acts o2) ∧
                                                    thread (Lab o1 x) = thread (Lab o2 y))
                                      (union _ (Sb o1) (Sb o2))) ≫
  ∧ ≪ O_DSb : same_relation _ (Dsb o) (union _ (Dsb o1) (Dsb o2)) ≫
  ∧ ≪ O_Asw : same_relation _ (Asw o) (union _ (Asw o1) (Asw o2)) ≫.

Definition oss_fork tid tid' o1 o :=
  ∃ a,
     ≪ O_Res : Res o = None ∨ Res o = Some tid' ≫
  ∧ ≪ O_Tid : Tid o = tid ≫
  ∧ ≪ O_Acts : Permutation (Acts o) (a :: Acts o1) ≫
  ∧ ≪ O_LabA : Lab o a = Askip tid ≫
  ∧ ≪ O_NIN : ¬ In a (Acts o1) ≫
  ∧ ≪ O_LabB : ∀ x (NEQ: x ≠ a), Lab o x = Lab o1 x ≫
  ∧ ≪ O_Sb : same_relation _ (Sb o) (Sb o1) ≫
  ∧ ≪ O_DSb : same_relation _ (Dsb o) (Dsb o1) ≫
  ∧ ≪ O_Asw : same_relation _ (Asw o)
                               (union _ (fun x y ⇒ x = a ∧ In y (Acts o1)) (Asw o1)) ≫.

Fixpoint oss_repeat n f o :=
  match n with
    | 0 ⇒
      Res o ≠ Some 0 ∧ f o
    | S m ⇒
      Res o = None ∧ f o ∨
      ∃ o1 o2,
        Res o1 = Some 0 ∧
        f o1 ∧
        oss_repeat m f o2 ∧
        oss_seqcomp o1 o2 o
  end.

Fixpoint exp_sem (e: cexp) (tid : nat) (o : opsem) :=
  match e with
    | Evalue n ⇒
        oss_one n (Askip tid) o
    | Ealloc n ⇒
        ∃ l, oss_one l (Aalloc tid l n) o
    | Eload typ l ⇒
        ∃ v, oss_one v (Aload tid typ l v) o
    | Estore typ l v ⇒
        oss_one v (Astore tid typ l v) o
    | Ecas typ1 typ2 l v v' ⇒
        oss_one v (Armw tid typ1 l v v') o ∨
        (∃ v'', v'' ≠ v ∧ oss_one v'' (Aload tid typ2 l v'') o) ∨
        (∃ v'', oss_one_div (Aload tid RATrlx l v'') o) ∨
        oss_one_div (Aload tid typ2 l v) o
    | Efence typ ⇒
        oss_one 0 (Afence tid typ) o
    | Elet e1 e2 ⇒
        Res o = None ∧ exp_sem e1 tid o ∨
        ∃ vmid o1 o2,
          Res o1 = Some vmid ∧
          exp_sem e1 tid o1 ∧
          exp_sem (e2 vmid) tid o2 ∧
          oss_seqcomp o1 o2 o
    | Efork e ⇒
        (∃ tid', oss_one tid' (Askip tid) o) ∨
        ∃ tid' o',
          exp_sem e tid' o' ∧
          oss_fork tid tid' o' o
    | Echoice e1 e2 ⇒
        exp_sem e1 tid o ∨ exp_sem e2 tid o
    | Erepeat e ⇒
        ∃ n, oss_repeat n (exp_sem e tid) o
  end.

We now prove that opsemsets returned by exp_sem are valid. We start with a helper lemma, and then prove each property of valid opsemsets in turn.

Lemma oss_one_div_one :
  ∀ act o (D: oss_one_div act o) n, oss_one n act o.

  • The set of actions contains no duplicates.

Theorem NoDup_exp_sem : ∀ e tid o, exp_sem e tid o → NoDup (Acts o).

  • Every execution is finite.

Lemma ExecutionFinite_one :
  ∀ n act o,
    oss_one n act o →
    ExecutionFinite (Acts o) (Lab o) (Sb o) (Asw o).

Lemma ExecutionFinite_one_div :
  ∀ act o,
    oss_one_div act o →
    ExecutionFinite (Acts o) (Lab o) (Sb o) (Asw o).

Lemma ExecutionFinite_seqcomp :
  ∀ o1 o2 o (SEQ : oss_seqcomp o1 o2 o)
    (IH1 : ExecutionFinite (Acts o1) (Lab o1) (Sb o1) (Asw o1))
    (IH2 : ExecutionFinite (Acts o2) (Lab o2) (Sb o2) (Asw o2)),
  ExecutionFinite (Acts o) (Lab o) (Sb o) (Asw o).

Lemma ExecutionFinite_fork :
  ∀ tid tid' o' o (SEQ : oss_fork tid tid' o' o)
    (IH : ExecutionFinite (Acts o') (Lab o') (Sb o') (Asw o')),
  ExecutionFinite (Acts o) (Lab o) (Sb o) (Asw o).

Lemma ExecutionFinite_exp_sem :
  ∀ e tid o,
    exp_sem e tid o →
    ExecutionFinite (Acts o) (Lab o) (Sb o) (Asw o).

Theorem oss_ef_exp_sem e tid : oss_ef (exp_sem e tid).

  • The union of the sb and asw relations is acyclic.

Lemma acyclic_sbw_one n act o : oss_one n act o → acyclic (Sbw o).

Lemma acyclic_sbw_one_div act o : oss_one_div act o → acyclic (Sbw o).

Lemma acyclic_sbw_seqcomp :
  ∀ o1 o2 o (SEQ : oss_seqcomp o1 o2 o)
    e1 tid (X: exp_sem e1 tid o1)
    e2 (Y: exp_sem e2 tid o2)
    (A1 : acyclic (Sbw o1))
    (A2 : acyclic (Sbw o2)),
  acyclic (Sbw o).

Lemma acyclic_sbw_exp_sem : ∀ e tid o, exp_sem e tid o → acyclic (Sbw o).

Theorem oss_sbw_acyc_exp_sem e tid : oss_sbw_acyc (exp_sem e tid).

  • Sequence before relations only events from the same thread.

Lemma ConsistentSB_seqcomp :
  ∀ o1 o2 o (SEQ : oss_seqcomp o1 o2 o)
    e1 tid (X: exp_sem e1 tid o1)
    e2 (Y: exp_sem e2 tid o2)
    (IH1 : ConsistentSB (Lab o1) (Sb o1))
    (IH2 : ConsistentSB (Lab o2) (Sb o2)),
  ConsistentSB (Lab o) (Sb o).

Theorem ConsistentSB_exp_sem :
  ∀ e tid o (OSS: exp_sem e tid o), ConsistentSB (Lab o) (Sb o).

  • Dependent sequence before is a subset of sequenced before and
relates only memory accesses.

Lemma ConsistentDSB_seqcomp :
  ∀ o1 o2 o (SEQ : oss_seqcomp o1 o2 o)
    e1 tid (E1: exp_sem e1 tid o1)
    e2 (E2: exp_sem e2 tid o2)
    (IH1 : ConsistentDSB (Lab o1) (Sb o1) (Dsb o1))
    (IH2 : ConsistentDSB (Lab o2) (Sb o2) (Dsb o2)),
  ConsistentDSB (Lab o) (Sb o) (Dsb o).

Theorem ConsistentDSB_exp_sem :
  ∀ e tid o (OSS: exp_sem e tid o), ConsistentDSB (Lab o) (Sb o) (Dsb o).

  • Executions start with an action with thread identifier tid.

Lemma StartTID_seqcomp :
  ∀ o1 o2 o (SEQ : oss_seqcomp o1 o2 o)
    e1 tid (E1: exp_sem e1 tid o1)
    e2 (E2: exp_sem e2 tid o2)
    a1 (IN1: In a1 (Acts o1)) (T1: thread (Lab o1 a1) = tid)
       (T'1: Tid o1 = tid)
       (N: ¬ (∃ b, Sb o1 b a1))
       (N': ¬ (∃ b, Asw o1 b a1))
       (R1: ∀ b (IN: In b (Acts o1)), clos_refl_trans _ (Sbw o1) a1 b)
    a2 (IN1: In a2 (Acts o2)) (T1: thread (Lab o2 a2) = tid)
       (R2: ∀ b (IN: In b (Acts o2)), clos_refl_trans _ (Sbw o2) a2 b),
  ∃ a, In a (Acts o) ∧ thread (Lab o a) = tid ∧ Tid o = tid ∧
            ¬ (∃ b, Sb o b a) ∧ ¬ (∃ b, Asw o b a) ∧
            (∀ b (IN: In b (Acts o)), clos_refl_trans _ (Sbw o) a b).

Theorem StartTID_exp_sem :
  ∀ e tid o (OSS: exp_sem e tid o),
    ∃ a, In a (Acts o) ∧ thread (Lab o a) = tid ∧ Tid o = tid ∧
      ¬ (∃ b, Sb o b a) ∧ ¬ (∃ b, Asw o b a) ∧
      (∀ b (IN: In b (Acts o)), clos_refl_trans _ (Sbw o) a b).

  • Executions are prefix-closed.

Lemma pref_opsem_one :
  ∀ act n x y,
    oss_one n act y →
    pref_opsem x y →
    oss_one n act x.

Lemma pref_opsem_one_div :
  ∀ act x y,
    oss_one_div act y →
    pref_opsem x y →
    oss_one_div act x.

Lemma Pref_closed_fork :
  ∀ e tid' o'
    (E : exp_sem e tid' o')
    (IH : ∀ x, pref_opsem x o' → exp_sem e tid' x)
    x y (S : pref_opsem x y) tid
    (E0 : oss_fork tid tid' o' y),
    (∃ tid', oss_one tid' (Askip tid) x) ∨
    (∃ (tid'0 : nat) (o'0 : opsem),
      exp_sem e tid'0 o'0 ∧ oss_fork tid tid'0 o'0 x).

Lemma NonEmpty2_exp_sem e tid o : exp_sem e tid o → Acts o ≠ nil.

Lemma upward_closed_sbw :
  ∀ y P
    (U_Sb : upward_closed (Sb y) P)
    (U_Asw : upward_closed (Asw y) P) a
    (H: P a) b
    (C: clos_trans _ (Sbw y) b a),
    P b.

Lemma upward_closed_rt_sbw :
  ∀ y P
    (U_Sb : upward_closed (Sb y) P)
    (U_Asw : upward_closed (Asw y) P) a
    (H: P a) b
    (C: clos_refl_trans _ (Sbw y) b a),
    P b.

Lemma Pref_closed_seqcomp :
  ∀ o1 o2 y (SEQ : oss_seqcomp o1 o2 y)
    e1 tid (E1 : exp_sem e1 tid o1)
    (IH1 : ∀ x, pref_opsem x o1 → exp_sem e1 tid x)
    e2 (E2 : exp_sem e2 tid o2)
    (IH2 : ∀ x, pref_opsem x o2 → exp_sem e2 tid x)
    vmid (RES : Res o1 = Some vmid)
    x (S : pref_opsem x y),
    Res x = None ∧ exp_sem e1 tid x ∨
    (∃ (o0 o3 : opsem),
       Res o0 = Some vmid ∧
       exp_sem e1 tid o0 ∧ exp_sem e2 tid o3 ∧ oss_seqcomp o0 o3 x).

Theorem Pref_closed_exp_sem : ∀ e tid, Pref_closed (exp_sem e tid).

  • Executions are receptive: they are closed under changing the value
returned by maximal read.

Lemma alt_read_final_load :
  ∀ n tid typ l v x y,
    oss_one n (Aload tid typ l v) y →
    alt_read_final_one x y →
    ∃ v', oss_one_div (Aload tid typ l v') x.

Lemma alt_read_final_rmw :
  ∀ n tid typ l v v' x y,
    oss_one n (Armw tid typ l v v') y →
    alt_read_final_one x y →
    ∃ v', oss_one_div (Aload tid RATrlx l v') x.

Lemma alt_read_final_fork :
  ∀ e tid' o'
    (H : exp_sem e tid' o')
    (IH: ∀ x, alt_read_final_one x o' → exp_sem e tid' x)
    tid x y
    (F : oss_fork tid tid' o' y)
    (R : alt_read_final_one x y),
  ∃ o, exp_sem e tid' o ∧ oss_fork tid tid' o x.

Lemma alt_read_final_seqcomp :
  ∀ o1 o2 y (SEQ : oss_seqcomp o1 o2 y)
    e1 tid (E1 : exp_sem e1 tid o1)
    (IH1 : ∀ x, alt_read_final_one x o1 → exp_sem e1 tid x)
    vmid (RES : Res o1 = Some vmid)
    e2 (E2 : exp_sem e2 tid o2)
    (IH2 : ∀ x, alt_read_final_one x o2 → exp_sem e2 tid x)
    x (S : alt_read_final_one x y),
  ∃ (o0 o3 : opsem),
      Res o0 = Some vmid ∧
      exp_sem e1 tid o0 ∧ exp_sem e2 tid o3 ∧ oss_seqcomp o0 o3 x.

Theorem AFR_closed_exp_sem : ∀ e tid, AFR_closed (exp_sem e tid).

This page has been generated by coqdoc