Skip to content

Commit ef79f22

Browse files
ambroise-armmaranget
authored andcommitted
Morello (#84)
This PR upstreams support for the Arm Morello architecture (for aarch64) The target specification is the first Morello release (version A.f): https://developer.arm.com/documentation/ddi0606/A-f A new variant has been created: "-variant morello", both for diy7 and for herd7. For diy7, new annotations have been added in order to deal with Morello capabilities: Ct for morello tags Cs for morello seal (object type) P, A, Q and L annotations can be suffixed with "c" to handle capabilities More information can be found in the individual commit messages. The patchset passed "pre-commit run --all-files" as well as the regression tests currently in PR #81 with "make test". * [morello] Add infrastructure Add morello variant. Enabling morello variant also enables mixed variant. Because the implementation of the morello tag uses a separate memory location, the execution of herd is faster that way. Using morello without mixed hasn't been fully implemented and would output incorrect results. Add 128-bit size (S128 in MachSize and V128 for AArch64) Add Capability registers for AArch64 Parse morello initializations * [morello] Add capability constants They hold a boolean for the tag and a 128-bit value for the rest of the capability. Arithmetic operations modifying the capability reset the tag to false. * [lib] Add morello Add a number of morello instructions. Some of which are not particularly useful at the moment given that addresses are represented as strings and not numerical values. This patch includes the implementation of the tag, permissions and object type of capabilities. It doesn't include their bounds and flags. When using morello, the only implemented instruction set is C64. Add the necessary operations on Value to implement those instructions. Add the possibility to use unary and binary operations on Symbolic. Those operation will only make use of the new "capability" field of Symbolic values, and won't have an effect on non-morello variants. * [herd] Expose used value in lift_memop This allows to perform checks on both the address and the value used for memory accesses. * [herd] Add a morello specific CAS semantic This is a temporary implementation that should be unified with the baseline CAS in the future. It uses choiceT instead of altT in order to get a correct behavior with the morello tag memory location. * [herd] Allow delay of non-singleton events Not used for now, but might be useful at some point. * [herd] Add morello Add morello instructions Adapt data processing to fit 128-bit registers Add read/write of capabilities from/to registers and memory Add checks on memory accesses and add permissions to memory operations Enable initialization of capability tag memory location * [gen] Fix memtag generation Warn instead of failing an assert when a Tag annotation is used on xload or xstore. That allows the use of "T" in a relaxlist without failure. * [AArch64 gen] Add an optional annotation modifier This patch adds the means to modify the implementation of some annotations without interfering with their nature. The modification is done by chosing and adding a letter to the annotation. For example, for AArch64, using the morello variation of LDAR is done by using "Ac" instead of "A". * [gen] Add is_addr * [gen] Add morello Add capability annotations for tag "Ct" and seal "Cs". Those annotations correspond to their own Banks, behaving similarly to Ord. A situation of potential Fault is created when using those annotations together with DpAddr. The result of the preceding read is used to modify the address so that it will fault if different from the expected value. Implement the addition of the optional annotation modifier for morello capabilities.
1 parent 8e4b93e commit ef79f22

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

84 files changed

+2202
-348
lines changed

gen/AArch64Arch_gen.ml

Lines changed: 59 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@ module Make
3131

3232
let do_self = C.variant Variant_gen.Self
3333
let do_tag = C.variant Variant_gen.MemTag
34+
let do_morello = C.variant Variant_gen.Morello
3435
open Code
3536
open Printf
3637

@@ -52,16 +53,19 @@ module Mixed =
5253
(* AArch64 has more atoms that others *)
5354
let bellatom = false
5455
type atom_rw = PP | PL | AP | AL
55-
type atom_acc = Plain | Acq | AcqPc | Rel | Atomic of atom_rw | Tag
56+
type atom_acc_opt = Capability
57+
type atom_acc = Plain of atom_acc_opt option | Acq of atom_acc_opt option
58+
| AcqPc of atom_acc_opt option | Rel of atom_acc_opt option
59+
| Atomic of atom_rw | Tag | CapaTag | CapaSeal
5660
type atom = atom_acc * MachMixed.t option
5761

5862
let default_atom = Atomic PP,None
5963

6064
let applies_atom (a,_) d = match a,d with
61-
| Acq,R
62-
| AcqPc,R
63-
| Rel,W
64-
| (Plain|Atomic _|Tag),(R|W)
65+
| Acq _,R
66+
| AcqPc _,R
67+
| Rel _,W
68+
| (Plain _|Atomic _|Tag|CapaTag|CapaSeal),(R|W)
6569
-> true
6670
| _ -> false
6771

@@ -75,20 +79,31 @@ let applies_atom (a,_) d = match a,d with
7579
| AP -> "A"
7680
| AL -> "AL"
7781

82+
let pp_opt = function
83+
| None -> ""
84+
| Some Capability -> "c"
85+
7886
let pp_atom_acc = function
7987
| Atomic rw -> sprintf "X%s" (pp_atom_rw rw)
80-
| Rel -> "L"
81-
| Acq -> "A"
82-
| AcqPc -> "Q"
83-
| Plain -> "P"
88+
| Rel o -> sprintf "L%s" (pp_opt o)
89+
| Acq o -> sprintf "A%s" (pp_opt o)
90+
| AcqPc o -> sprintf "Q%s" (pp_opt o)
91+
| Plain o -> sprintf "P%s" (pp_opt o)
8492
| Tag -> "T"
93+
| CapaTag -> "Ct"
94+
| CapaSeal -> "Cs"
8595

8696
let pp_atom (a,m) = match a with
87-
| Plain ->
97+
| Plain o ->
98+
let prefix = match o with
99+
| None -> ""
100+
| Some Capability -> "Pc" in
88101
begin
89102
match m with
90-
| None -> ""
91-
| Some m -> Mixed.pp_mixed m
103+
| None -> prefix
104+
| Some m -> if String.length prefix > 0
105+
then sprintf "%s.%s" prefix (Mixed.pp_mixed m)
106+
else Mixed.pp_mixed m
92107
end
93108
| _ ->
94109
let pp_acc = pp_atom_acc a in
@@ -101,7 +116,7 @@ let applies_atom (a,_) d = match a,d with
101116

102117
let fold_mixed f r =
103118
Mixed.fold_mixed
104-
(fun m r -> f (Plain,Some m) r)
119+
(fun m r -> f (Plain None,Some m) r)
105120
r
106121

107122
let fold_atom_rw f r = f PP (f PL (f AP (f AL r)))
@@ -110,8 +125,22 @@ let applies_atom (a,_) d = match a,d with
110125
if do_tag then fun f r -> f Tag r
111126
else fun _f r -> r
112127

128+
let fold_morello =
129+
if do_morello then fun f r -> f CapaSeal (f CapaTag r)
130+
else fun _f r -> r
131+
113132
let fold_acc f r =
114-
fold_tag f (f Acq (f AcqPc (f Rel (fold_atom_rw (fun rw -> f (Atomic rw)) r))))
133+
fold_morello f (
134+
fold_tag f (
135+
f (Plain (Some Capability)) (
136+
f (Acq (Some Capability)) (
137+
f (Acq None) (
138+
f (AcqPc (Some Capability)) (
139+
f (AcqPc None) (
140+
f (Rel (Some Capability)) (
141+
f (Rel None) (
142+
fold_atom_rw (fun rw -> f (Atomic rw)) r)
143+
))))))))
115144

116145
let fold_non_mixed f r = fold_acc (fun acc r -> f (acc,None) r) r
117146

@@ -125,25 +154,29 @@ let applies_atom (a,_) d = match a,d with
125154

126155
let worth_final (a,_) = match a with
127156
| Atomic _ -> true
128-
| Acq|AcqPc|Rel|Plain|Tag -> false
157+
| Acq _|AcqPc _|Rel _|Plain _|Tag|CapaTag|CapaSeal -> false
129158

130159

131160
let varatom_dir _d f r = f None r
132161

133162
let merge_atoms a1 a2 = match a1,a2 with
134-
| ((Plain,sz),(a,None))
135-
| ((a,None),(Plain,sz)) -> Some (a,sz)
163+
| ((Plain None,sz),(a,None))
164+
| ((a,None),(Plain None,sz)) -> Some (a,sz)
136165
| ((a1,None),(a2,sz))
137166
| ((a1,sz),(a2,None)) when a1=a2 -> Some (a1,sz)
138-
| ((Plain,sz1),(a,sz2))
139-
| ((a,sz1),(Plain,sz2)) when sz1=sz2 -> Some (a,sz1)
167+
| ((Plain None,sz1),(a,sz2))
168+
| ((a,sz1),(Plain None,sz2)) when sz1=sz2 -> Some (a,sz1)
140169
| _,_ ->
141170
if equal_atom a1 a2 then Some a1 else None
142171

143172
let atom_to_bank = function
144173
| Tag,None -> Code.Tag
145174
| Tag,Some _ -> assert false
146-
| (Plain|Acq|AcqPc|Rel|Atomic (PP|PL|AP|AL)),_
175+
| CapaTag,None -> Code.CapaTag
176+
| CapaTag,Some _ -> assert false
177+
| CapaSeal,None -> Code.CapaSeal
178+
| CapaSeal,Some _ -> assert false
179+
| (Plain _|Acq _|AcqPc _|Rel _|Atomic (PP|PL|AP|AL)),_
147180
-> Code.Ord
148181

149182
(**************)
@@ -161,14 +194,14 @@ let applies_atom (a,_) d = match a,d with
161194
end)
162195

163196
let overwrite_value v ao w = match ao with
164-
| None| Some ((Atomic _|Acq|AcqPc|Rel|Plain|Tag),None)
197+
| None| Some ((Atomic _|Acq _|AcqPc _|Rel _|Plain _|Tag|CapaTag|CapaSeal),None)
165198
-> w (* total overwrite *)
166-
| Some ((Atomic _|Acq|AcqPc|Rel|Plain|Tag),Some (sz,o)) ->
199+
| Some ((Atomic _|Acq _|AcqPc _|Rel _|Plain _|Tag|CapaTag|CapaSeal),Some (sz,o)) ->
167200
ValsMixed.overwrite_value v sz o w
168201

169202
let extract_value v ao = match ao with
170-
| None| Some ((Atomic _|Acq|AcqPc|Rel|Plain|Tag),None) -> v
171-
| Some ((Atomic _|Acq|AcqPc|Rel|Plain|Tag),Some (sz,o)) ->
203+
| None| Some ((Atomic _|Acq _|AcqPc _|Rel _|Plain _|Tag|CapaTag|CapaSeal),None) -> v
204+
| Some ((Atomic _|Acq _|AcqPc _|Rel _|Plain _|Tag|CapaTag|CapaSeal),Some (sz,o)) ->
172205
ValsMixed.extract_value v sz o
173206

174207
(* End of atoms *)
@@ -277,8 +310,8 @@ let fold_rmw f r =
277310
r
278311

279312
let applies_atom_rmw rmw ar aw = match rmw,ar,aw with
280-
| (LrSc|Swp|Cas|LdOp _),(Some (Acq,_)|None),(Some (Rel,_)|None)
281-
| (StOp _),None,(Some (Rel,_)|None)
313+
| (LrSc|Swp|Cas|LdOp _),(Some (Acq _,_)|None),(Some (Rel _,_)|None)
314+
| (StOp _),None,(Some (Rel _,_)|None)
282315
-> true
283316
| _ -> false
284317

0 commit comments

Comments
 (0)