Program expressions and their semantics


Require Import List Vbase Vlistbase Vlist extralib.
Require Import Classical ClassicalDescription Relations.
Require Import c11.
Set Implicit Arguments.

Program expressions are defined inductively as follows:

Inductive cexp :=
  | Evalue (n: nat)
  | Ealloc
  | Eload (typ: access_type) (l : nat)
  | Estore (typ: access_type) (l v : nat)
  | Ecas (typ_succ typ_fail: access_type) (l v v' : nat)
  | Elet (e1: cexp) (e2: nat -> cexp)
  | Epar (e1: cexp) (e2: cexp)
  | Erepeat (e : cexp).

The semantics of expressions is given as a set of tuples containing the return value and a partial execution (the events performed by the expression together with the hb-order among them) with distinguished initial and final nodes.

Definition combine_val (v1 v2 v : option nat) :=
  match v with
    | Some n => v1 = Some n /\ v2 <> None
    | None => v1 = None \/ v2 = None
  end.

Fixpoint exp_sem
  (e: cexp) (res: option nat)
  (acts : list actid)
  (lab : actid -> act)
  (sb : actid -> actid -> Prop) (fst : actid) (lst : actid) :=
  match e with
    | Evalue n => acts = fst :: nil /\ lst = fst /\ lab fst = Askip /\ res = Some n
    | Ealloc => exists l, acts = fst :: nil /\ lst = fst
                          /\ lab fst = Aalloc l /\ res = Some l
    | Eload typ l => exists v,
                       acts = fst :: nil /\ lst = fst /\ lab fst = Aload typ l v /\
                       res = Some v
    | Estore typ l v =>
        acts = fst :: nil /\ lst = fst /\ lab fst = Astore typ l v /\ res = Some v
    | Ecas typ1 typ2 l v v' =>
          acts = fst :: nil /\ lst = fst /\ lab fst = Armw typ1 l v v' /\ res = Some v
      \/ exists v', acts = fst :: nil /\ lst = fst /\ lab fst = Aload typ2 l v'
                    /\ res = Some v' /\ v' <> v
    | Elet e1 e2 =>
        (res = None /\ exp_sem e1 None acts lab sb fst lst) \/
        (exists vmid lst1 fst2 acts1 acts2,
           acts = acts1 ++ acts2 /\
           disjoint acts1 acts2 /\
           sb lst1 fst2 /\
           << U1 : (forall n (SB: sb lst1 n), n = fst2) >> /\
           << U2 : (forall n (SB: sb n fst2), n = lst1) >> /\
           << ESEM1: exp_sem e1 (Some vmid) acts1 lab sb fst lst1 >> /\
           << ESEM2: exp_sem (e2 vmid) res acts2 lab sb fst2 lst >>)
    | Epar e1 e2 =>
        exists res1 fst1 lst1 res2 fst2 lst2 acts1 acts2,
          acts = fst :: lst :: acts1 ++ acts2 /\
          << NODUP: NoDup acts >> /\
          << ESEM1: exp_sem e1 res1 acts1 lab sb fst1 lst1 >> /\
          << ESEM2: exp_sem e2 res2 acts2 lab sb fst2 lst2 >> /\
          << LABF : lab fst = Askip >> /\
          << LABL : lab lst = Askip >> /\
          << SBF1 : sb fst fst1 >> /\
          << SBF2 : sb fst fst2 >> /\
          << SBL1 : sb lst1 lst >> /\
          << SBL2 : sb lst2 lst >> /\
          << UL0 : forall n (SB: sb n lst), lst1 = n \/ lst2 = n >> /\
          << UL1 : forall n (SB: sb lst1 n), n = lst >> /\
          << UL2 : forall n (SB: sb lst2 n), n = lst >> /\
          << UF0 : (forall n (SB: sb fst n), n = fst1 \/ n = fst2) >> /\
          << UF1 : (forall n (SB: sb n fst1), n = fst) >> /\
          << UF2 : (forall n (SB: sb n fst2), n = fst) >> /\
          << CVAL: combine_val res1 res2 res >>
    | Erepeat e =>
        exists sems resI actsI lstI actsF fstF,
          acts = flatten (map (fun x => snd (Datatypes.fst (Datatypes.fst x))) sems) /\
          << ESEM: forall res acts fst lst (IN: In (res, acts, fst, lst) sems),
                     exp_sem e res acts lab sb fst lst >> /\
          << REP: forall prefix res1 acts1 fst1 lst1 res2 acts2 fst2 lst2 suffix
                         (EQ: sems = prefix ++ (res1, acts1, fst1, lst1) ::
                                        (res2, acts2, fst2, lst2) :: suffix),
                         << RES : res1 = Some 0 >> /\
                         << SB : sb lst1 fst2 >> /\
                         << U1 : (forall n (SB: sb lst1 n), n = fst2) >> /\
                         << U2 : (forall n (SB: sb n fst2), n = lst1) >> >> /\
          << NODUP: NoDup acts >> /\
          << GET_I: ohead sems = Some (resI,actsI,fst,lstI) >> /\
          << GET_F: olast sems = Some (res,actsF,fstF,lst) >> /\
          << CVAL: res <> Some 0 >>
  end.

We prove a number of basic well-formedness properties for the expression semantics.
1. The fst and lst nodes belong to the set of actions, act.

Lemma exp_sem_fst :
  forall e res acts lab sb fst lst (SEM: exp_sem e res acts lab sb fst lst),
    In fst acts.

Lemma exp_sem_lst :
  forall e res acts lab sb fst lst (SEM: exp_sem e res acts lab sb fst lst),
    In lst acts.

2. The list of actions contains no duplicate entries.

Lemma exp_sem_nodup :
  forall e res acts lab sb fst lst (SEM: exp_sem e res acts lab sb fst lst),
    NoDup acts.

3. Every node in acts is sb-reachable from the initial node, fst.

Lemma exp_sem_fst_reach :
  forall e res acts lab sb fst lst (SEM: exp_sem e res acts lab sb fst lst)
    x (IN: In x acts), clos_refl_trans _ sb fst x.

4. The final node, lst, is sb-reachable from every node in acts.

Lemma exp_sem_lst_reach :
  forall e res acts lab sb fst lst (SEM: exp_sem e res acts lab sb fst lst)
    x (IN: In x acts), clos_refl_trans _ sb x lst.

5. Nodes other than fst have no incoming sb-edges.

Lemma exp_sem_pre_closed :
  forall e res acts lab sb fst lst (SEM: exp_sem e res acts lab sb fst lst)
    a b (SB: sb a b) (IN: In b acts), b = fst \/ In a acts.

This page has been generated by coqdoc Imprint | Data protection