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
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
|
(****************************************************************************)
(* the diy toolsuite *)
(* *)
(* Jade Alglave, University College London, UK. *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France. *)
(* *)
(* Copyright 2015-present Institut National de Recherche en Informatique et *)
(* en Automatique and the authors. All rights reserved. *)
(* *)
(* This software is governed by the CeCILL-B license under French law and *)
(* abiding by the rules of distribution of free software. You can use, *)
(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
(* license as circulated by CEA, CNRS and INRIA at the following URL *)
(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *)
(****************************************************************************)
(* Java instruction semantics *)
module
Make
(Conf:Sem.Config)
(V:Value.S with type Cst.Instr.t = JavaBase.instruction and type arch_op = JavaBase.arch_op) = struct
module Java = JavaArch_herd.Make(SemExtra.ConfigToArchConfig(Conf))(V)
module Act = JavaAction.Make(Java)
include SemExtra.Make(Conf)(Java)(Act)
let barriers = []
let isync = None
let nat_sz = V.Cst.Scalar.machsize
let atomic_pair_allowed e1 e2 = (e1.E.iiid == e2.E.iiid)
module Mixed(SZ : ByteSize.S) = struct
let (>>=) = M.(>>=)
let (>>*=) = M.(>>*=)
let (>>|) = M.(>>|)
let (>>!) = M.(>>!)
let (>>>) = M.cseq
let (>>>>) = M.(>>>>)
let no_mo = AccessModes.NA
let read_loc is_data mo =
M.read_loc is_data (fun loc v -> Act.Access (Dir.R, loc, v, mo, nat_sz))
let read_exchange is_data vstored mo =
M.read_loc is_data (fun loc v -> Act.RMW (loc,v,vstored,mo,nat_sz))
let read_reg is_data r ii =
read_loc is_data no_mo (A.Location_reg (ii.A.proc,r)) ii
let read_mem is_data mo a =
read_loc is_data mo (A.Location_global a)
let read_mem_atomic is_data a loc =
M.read_loc is_data
(fun loc v -> Act.Access (Dir.R, loc, v, a, nat_sz))
(A.Location_global loc)
let read_mem_atomic_known is_data a loc v =
M.read_loc is_data
(fun loc _v -> Act.Access (Dir.R, loc, v, a, nat_sz))
(A.Location_global loc)
let write_loc mo loc v ii =
M.mk_singleton_es (Act.Access (Dir.W, loc, v, mo, nat_sz)) ii >>! v
let write_reg r v ii = write_loc no_mo (A.Location_reg (ii.A.proc,r)) v ii
let write_mem mo a = write_loc mo (A.Location_global a)
let write_mem_atomic a loc v ii =
M.mk_singleton_es
(Act.Access (Dir.W, A.Location_global loc, v, a, nat_sz)) ii >>! v
let fetch_op op v am l ii =
M.fetch op v
(fun v vstored ->
Act.RMW (A.Location_global l, v, vstored, am, nat_sz))
ii
let rec build_semantics_expr is_data e ii : V.v M.t =
match e with
| JavaBase.LoadReg reg -> read_reg is_data reg ii
| JavaBase.LoadMem (vh, am) -> (read_reg is_data vh ii) >>=
(fun l -> read_mem is_data am l ii)
| JavaBase.Const i -> M.unitT (V.maybevToV (ParsedConstant.intToV i))
| JavaBase.Op (op, e1, e2) ->
(build_semantics_expr is_data e1 ii >>|
build_semantics_expr is_data e2 ii) >>= fun (v1, v2) ->
M.op op v1 v2
| JavaBase.Rmw (vh, (op, am), e) ->
(read_reg is_data vh ii) >>|
(build_semantics_expr true e ii) >>=
(fun (l , v) -> fetch_op op v am l ii)
| JavaBase.CAS (vh, (read_am, write_am), expect, dest) ->
(read_reg is_data vh ii) >>= fun loc_vh ->
(build_semantics_expr true expect ii) >>= fun v_expect ->
(read_mem true read_am loc_vh ii) >>*= fun v_vh ->
M.altT
((M.neqT v_vh v_expect) >>! v_vh)
((build_semantics_expr true dest ii) >>= fun v_dest ->
(M.mk_singleton_es
(Act.RMW (A.Location_global loc_vh,
v_expect, v_dest,
(match read_am , write_am with
| AccessModes.Acquire, AccessModes.Plain -> read_am
| AccessModes.Plain, AccessModes.Release -> write_am
| _ -> write_am), nat_sz))
ii) >>! v_expect)
let build_cond e ii =
let open Op in
let e = match e with
| JavaBase.Op (_,_,_) -> e
| _ -> JavaBase.Op (Ne,e,Java.Const 0) in
build_semantics_expr false e ii
let rec build_semantics test ii : (A.program_order_index * B.t) M.t =
let ii =
{ii with A.program_order_index = A.next_po_index ii.A.program_order_index} in
match ii.A.inst with
| JavaBase.StoreReg (reg, exp) -> (
(build_semantics_expr true exp ii) >>=
(fun v -> write_reg reg v ii) >>=
(fun _ -> M.unitT (ii.A.program_order_index, B.Next [])))
| JavaBase.StoreMem (vh, am, e) -> (
(read_reg false vh ii) >>|
(build_semantics_expr true e ii) >>=
(fun (l, v) -> write_mem am l v ii) >>=
(fun _ -> M.unitT (ii.A.program_order_index, B.Next [])))
| JavaBase.If (grd, thn, Some e) -> (
build_cond grd ii >>>> fun ret ->
let ii' = {
ii with A.program_order_index =
A.next_po_index ii.A.program_order_index;
} in
let then_branch = build_semantics test {ii' with A.inst = thn} in
let else_branch = build_semantics test {ii' with A.inst = e} in
M.choiceT ret then_branch else_branch
)
| JavaBase.If (grd, thn, None) -> (
build_cond grd ii >>>> fun ret ->
let ii' = {
ii with A.program_order_index =
A.next_po_index ii.A.program_order_index;
} in
let then_branch = build_semantics test {ii' with A.inst = thn} in
M.choiceT ret then_branch
(build_semantics_list test [] ii)
)
| JavaBase.Seq ins_lst ->
build_semantics_list test ins_lst ii
| JavaBase.Fence mo -> M.mk_fence (Act.Fence mo) ii
>>= fun _ -> M.unitT
(ii.A.program_order_index, B.Next [])
| _ -> assert false (* others are not implemented yet *)
and build_semantics_list test insts ii =
match insts with
| [] -> M.unitT (ii.A.program_order_index, B.Next [])
| hd :: tl ->
let ii = {ii with A.inst = hd; } in
(build_semantics test ii) >>> fun (prog_order, _branch) ->
build_semantics_list test tl {ii with A.program_order_index = prog_order;}
let spurious_setaf _ = assert false
end
end
|
