diff options
Diffstat (limited to 'mppa_k1c/abstractbb/DepExample.v')
| -rw-r--r-- | mppa_k1c/abstractbb/DepExample.v | 151 |
1 files changed, 0 insertions, 151 deletions
diff --git a/mppa_k1c/abstractbb/DepExample.v b/mppa_k1c/abstractbb/DepExample.v deleted file mode 100644 index a239e24f..00000000 --- a/mppa_k1c/abstractbb/DepExample.v +++ /dev/null @@ -1,151 +0,0 @@ -(** Specification of the example illustrating how to use ImpDep. *) - -Require Export ZArith. - -Require Export ZArith. -Require Export List. -Export ListNotations. - -(* Syntax *) - -Definition reg := positive. - -Inductive operand := - | Imm (i:Z) - | Reg (r:reg) - . - -Inductive arith_op := ADD | SUB | MUL. - -Inductive inst := - | MOVE (dest: reg) (src: operand) - | ARITH (dest: reg) (op: arith_op) (src1 src2: operand) - | LOAD (dest base: reg) (offset: operand) - | STORE (src base: reg) (offset: operand) - | MEMSWAP (r base: reg) (offset: operand) - . - -Definition bblock := list inst. - -(* Semantics *) - -Definition value := Z. - -Definition addr := positive. - -Definition mem := addr -> value. - -Definition assign (m: mem) (x:addr) (v: value) := - fun y => if Pos.eq_dec x y then v else (m y). - -Definition regmem := reg -> value. - -Record state := { sm: mem; rm: regmem }. - -Definition operand_eval (x: operand) (rm: regmem): value := - match x with - | Imm i => i - | Reg r => rm r - end. - -Definition arith_op_eval (o: arith_op): value -> value -> value := - match o with - | ADD => Z.add - | SUB => Z.sub - | MUL => Z.mul - end. - -Definition get_addr (base:reg) (offset:operand) (rm: regmem): option addr := - let b := rm base in - let ofs := operand_eval offset rm in - match Z.add b ofs with - | Zpos p => Some p - | _ => None - end. - -(* two-state semantics -- dissociating read from write access. - - all read access on [sin] state - - all register write access modifies [sout] state - - all memory write access modifies [sin] state - => useful for parallel semantics - NB: in this parallel semantics -- there is at most one STORE by bundle - which is non-deterministically chosen... -*) -Definition sem_inst (i: inst) (sin sout: state): option state := - match i with - | MOVE dest src => - let v := operand_eval src (rm sin) in - Some {| sm := sm sout; - rm := assign (rm sout) dest v |} - | ARITH dest op src1 src2 => - let v1 := operand_eval src1 (rm sin) in - let v2 := operand_eval src2 (rm sin) in - let v := arith_op_eval op v1 v2 in - Some {| sm := sm sout; - rm := assign (rm sout) dest v |} - | LOAD dest base offset => - match get_addr base offset (rm sin) with - | Some srce => - Some {| sm := sm sout; - rm := assign (rm sout) dest (sm sin srce) |} - | None => None - end - | STORE srce base offset => - match get_addr base offset (rm sin) with - | Some dest => - Some {| sm := assign (sm sin) dest (rm sin srce); - rm := rm sout |} - | None => None - end - | MEMSWAP x base offset => - match get_addr base offset (rm sin) with - | Some ad => - Some {| sm := assign (sm sin) ad (rm sin x); - rm := assign (rm sout) x (sm sin ad) |} - | None => None - end - end. - -Local Open Scope list_scope. - -(** usual sequential semantics *) -Fixpoint sem_bblock (p: bblock) (s: state): option state := - match p with - | nil => Some s - | i::p' => - match sem_inst i s s with - | Some s' => sem_bblock p' s' - | None => None - end - end. - -Definition state_equiv (s1 s2: state): Prop := - (forall x, sm s1 x = sm s2 x) /\ - (forall x, rm s1 x = rm s2 x). - -(* equalities on bblockram outputs *) -Definition res_equiv (os1 os2: option state): Prop := - match os1 with - | Some s1 => exists s2, os2 = Some s2 /\ state_equiv s1 s2 - | None => os2 = None - end. - - -Definition bblock_equiv (p1 p2: bblock): Prop := - forall s, res_equiv (sem_bblock p1 s) (sem_bblock p2 s). - -(** parallel semantics with in-order writes *) -Fixpoint sem_bblock_par_iw (p: bblock) (sin sout: state): option state := - match p with - | nil => Some sout - | i::p' => - match sem_inst i sin sout with - | Some sout' => sem_bblock_par_iw p' sin sout' - | None => None - end - end. - -(** parallelism semantics with arbitrary order writes *) -Require Import Sorting.Permutation. - -Definition sem_bblock_par (p: bblock) (sin: state) (sout: option state) := exists p', res_equiv sout (sem_bblock_par_iw p' sin sin) /\ Permutation p p'. |