blob: a239e24f64754ad6c232e3f823dd45db52724be3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
|
(** 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'.
|
