Program expressions and their semantics


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 xx)
  | Ctx_let K (CTX : eval_ctx K) e2 : eval_ctx (fun xElet (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 nFalse
    | 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 va = 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 eFalse
    | Erepeat e
        a = Askip e' = Elet e (fun xif 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