Require Import List Vbase extralib.
Require Import Classical ClassicalDescription Relations Permutation.
Require Import c11.
Set Implicit Arguments.
Program expressions are defined inductively as follows:
Inductive exp :=
| Evalue (n: nat)
| Ealloc (n: nat)
| Eload (typ: read_access_type) (l : nat)
| Estore (typ: write_access_type) (l v : nat)
| Ecas (typ1: rmw_access_type) (typ2: read_access_type) (l v v' : nat)
| Elet (e1: exp) (e2: nat → exp)
| Efork (e : exp)
| Erepeat (e : exp).
Evaluation contexts
Inductive eval_ctx : (exp → exp) → Prop :=
| Ctx_id : eval_ctx (fun x ⇒ x)
| Ctx_let K (CTX : eval_ctx K) e2 : eval_ctx (fun x ⇒ Elet (K x) e2).
Machine configuration
Record configuration :=
{ Mtmap : list (actid × exp) ;
Macts : list actid ;
Mamap : actid → act ;
Msb : actid → actid → Prop ;
Mrf : actid → option actid ;
Mmo : actid → actid → Prop ;
Msc : actid → actid → Prop }.
Expression evaluation: Event steps
Fixpoint exp_step (e: exp) (a : act) (e' : exp) :=
match e with
| Evalue n ⇒ False
| Ealloc n ⇒ ∃ l, a = Aalloc l n ∧ e' = Evalue l
| Eload typ l ⇒ ∃ v, a = Aload typ l v ∧ e' = Evalue v
| Estore typ l v ⇒ a = Astore typ l v ∧ e' = Evalue 0
| Ecas typ1 typ2 l v v' ⇒ a = Armw typ1 l v v' ∧ e' = Evalue 1
∨ ∃ vo, a = Aload typ2 l vo ∧ vo ≠ v ∧ e' = Evalue 0
| Elet e1 e2 ⇒
(∃ e1', exp_step e1 a e1' ∧ e' = Elet e1' e2)
∨ (∃ n, e1 = Evalue n ∧ a = Askip ∧ e' = e2 n)
| Efork e ⇒ False
| Erepeat e ⇒
a = Askip ∧ e' = Elet e (fun x ⇒ if x == 0 then Erepeat e else Evalue x)
end.
Machine steps
Inductive m_step (mc mc' : configuration) : Prop :=
| Mstep_plain e alpha e' (STEP: exp_step e alpha e') l1 l2 a a'
(THR: Mtmap mc = l1 ++ (a, e) :: l2)
(THR': Mtmap mc' = l1 ++ (a', e') :: l2)
(ACT: Macts mc' = a' :: Macts mc)
(FRESH: ¬ In a' (Macts mc))
(ACT': Mamap mc' a' = alpha)
(AEQ: ∀ x (IN: In x (Macts mc)), Mamap mc' x = Mamap mc x)
(SB: ∀ x y, Msb mc' x y ↔ Msb mc x y ∨ x = a ∧ y = a')
(RF: ∀ x (NEQ: x ≠ a'), Mrf mc' x = Mrf mc x)
(MO: ∀ x (NEQx: x ≠ a') y (NEQy: y ≠ a'), Mmo mc' x y ↔ Mmo mc x y)
(SC: ∀ x (NEQx: x ≠ a') y (NEQy: y ≠ a'), Msc mc' x y ↔ Msc mc x y)
(CONS: Consistent (Macts mc') (Mamap mc') (Msb mc') (Mrf mc') (Mmo mc') (Msc mc'))
| Mstep_fork K (CTX: eval_ctx K) l1 l2 a e
(THR: Mtmap mc = l1 ++ (a, K (Efork e)) :: l2)
(THR': Mtmap mc'= l1 ++ (a, K (Evalue 0)) :: l2 ++ (a, e) :: nil)
(ACT: Macts mc' = Macts mc)
(AEQ: Mamap mc' = Mamap mc)
(SB: Msb mc' = Msb mc)
(RF: Mrf mc' = Mrf mc)
(MO: Mmo mc' = Mmo mc)
(SC: Msc mc' = Msc mc).
Executions
Definition executions e e' acts amap sb rf mo sc :=
∃ init a l,
clos_refl_trans _ m_step
{| Mtmap := (init, e) :: nil ;
Macts := init :: nil ;
Mamap := fun _ ⇒ Askip ;
Msb := fun _ _ ⇒ False ;
Mrf := fun _ ⇒ None ;
Mmo := fun _ _ ⇒ False ;
Msc := fun _ _ ⇒ False |}
{| Mtmap := (a, e') :: l ;
Macts := acts ;
Mamap := amap ;
Msb := sb ;
Mrf := rf ;
Mmo := mo ;
Msc := sc |} ∧
Consistent acts amap sb rf mo sc.
Alternative definition
Inductive mc_step (mc mc' : configuration) : Prop :=
| MCstep_plain e alpha e' (STEP: exp_step e alpha e') l1 l2 a a'
(THR: Mtmap mc = l1 ++ (a, e) :: l2)
(THR': Mtmap mc' = l1 ++ (a', e') :: l2)
(ACT: Macts mc' = a' :: Macts mc)
(FRESH: ¬ In a' (Macts mc))
(ACT': Mamap mc' a' = alpha)
(AEQ: ∀ x (IN: In x (Macts mc)), Mamap mc' x = Mamap mc x)
(SB: ∀ x y, Msb mc' x y ↔ Msb mc x y ∨ x = a ∧ y = a')
(RF: ∀ x (NEQ: x ≠ a'), Mrf mc' x = Mrf mc x)
(MO: ∀ x (NEQx: x ≠ a') y (NEQy: y ≠ a'), Mmo mc' x y ↔ Mmo mc x y)
(SC: ∀ x (NEQx: x ≠ a') y (NEQy: y ≠ a'), Msc mc' x y ↔ Msc mc x y)
(CONS: Consistent (Macts mc') (Mamap mc') (Msb mc') (Mrf mc') (Mmo mc') (Msc mc'))
| MCstep_fork K (CTX: eval_ctx K) l1 l2 a e
(THR: Mtmap mc = l1 ++ (a, K (Efork e)) :: l2)
(THR': Mtmap mc'= l1 ++ (a, K (Evalue 0)) :: l2 ++ (a, e) :: nil)
(ACT: Macts mc' = Macts mc)
(AEQ: Mamap mc' = Mamap mc)
(SB: Msb mc' = Msb mc)
(RF: Mrf mc' = Mrf mc)
(MO: Mmo mc' = Mmo mc)
(SC: Msc mc' = Msc mc).
Definition cexecutions e e' acts amap sb rf mo sc :=
∃ init a l,
clos_refl_trans _ mc_step
{| Mtmap := (init, e) :: nil ;
Macts := init :: nil ;
Mamap := fun _ ⇒ Askip ;
Msb := fun _ _ ⇒ False ;
Mrf := fun _ ⇒ None ;
Mmo := fun _ _ ⇒ False ;
Msc := fun _ _ ⇒ False |}
{| Mtmap := (a, e') :: l ;
Macts := acts ;
Mamap := amap ;
Msb := sb ;
Mrf := rf ;
Mmo := mo ;
Msc := sc |}.
This page has been generated by coqdoc