Skip to content

Commit e156d09

Browse files
diaolo01diaolo01
committed
[litmus] Introduce EXS, EIS and EOS variants to litmus
1 parent 9646353 commit e156d09

File tree

11 files changed

+120
-6
lines changed

11 files changed

+120
-6
lines changed

‎catalogue/aarch64-faults/tests/SVC-ifetch.exs1eis0.litmus‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,13 @@
11
AArch64 SVC-ifetch.exs1eis0
22
variant=ifetch,exs
3-
CacheType=DIC
43
{
54
0:X0=instr:"NOP"; 0:X1=P0:L2;
65
}
76
P0 | P0.F ;
87
STR W0,[X1] | ERET ;
8+
DC CVAU, X1 |;
9+
DSB ISH |;
10+
IC IVAU, X1 |;
911
DSB ISH |;
1012
SVC #0 |;
1113
L2: |;

‎catalogue/aarch64-faults/tests/SVC-ifetch.exs1eis1.litmus‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,13 @@
11
AArch64 SVC-ifetch.exs1eis1
22
variant=ifetch,exs,eis
3-
CacheType=DIC
43
{
54
0:X0=instr:"NOP"; 0:X1=P0:L2;
65
}
76
P0 | P0.F ;
87
STR W0,[X1] | ERET ;
8+
DC CVAU, X1 |;
9+
DSB ISH |;
10+
IC IVAU, X1 |;
911
DSB ISH |;
1012
SVC #0 |;
1113
L2: |;

‎litmus/dumpRun.ml‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -139,6 +139,10 @@ end = struct
139139
if flags.Flags.memtag then
140140
"memtag.o"::utils
141141
else utils in
142+
let utils =
143+
if flags.Flags.exs then
144+
"exs.o"::utils
145+
else utils in
142146
let utils =
143147
if flags.Flags.pac then
144148
"auth.o"::utils
@@ -210,10 +214,11 @@ let collect_flags names =
210214
let open Flags in
211215
{ pac = flags.pac || some_flags.pac;
212216
self = flags.self || some_flags.self;
213-
memtag = flags.memtag || some_flags.memtag;}
217+
memtag = flags.memtag || some_flags.memtag;
218+
exs = flags.exs || some_flags.exs;}
214219
| _ -> some_flags)
215220
names
216-
{Flags.pac=false; Flags.self=false; Flags.memtag=false}
221+
{Flags.pac=false; Flags.self=false; Flags.memtag=false; Flags.exs=false}
217222

218223
let run_tests names flags out_chan =
219224

‎litmus/flags.mli‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,4 +21,5 @@ type t =
2121
pac : bool ; (* Requires pointer authentification *)
2222
self : bool ; (* Self modying code *)
2323
memtag : bool ; (* Requires memory tagging *)
24+
exs : bool ; (* Requires ExS helpers *)
2425
}

‎litmus/libdir/_aarch64/_exs.c‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
/****************************************************************************/
2+
/* the diy toolsuite */
3+
/* */
4+
/* Jade Alglave, University College London, UK. */
5+
/* Luc Maranget, INRIA Paris-Rocquencourt, France. */
6+
/* */
7+
/* Copyright 2015-present Institut National de Recherche en Informatique et */
8+
/* en Automatique and the authors. All rights reserved. */
9+
/* */
10+
/* This software is governed by the CeCILL-B license under French law and */
11+
/* abiding by the rules of distribution of free software. You can use, */
12+
/* modify and/ or redistribute the software under the terms of the CeCILL-B */
13+
/* license as circulated by CEA, CNRS and INRIA at the following URL */
14+
/* "http://www.cecill.info". We also give a copy in LICENSE.txt. */
15+
/****************************************************************************/
16+
#include "kvm-headers.h"
17+
#include "exs.h"
18+
19+
int check_exs(const char *tname) {
20+
uint64_t mmfr0;
21+
asm volatile("mrs %0, ID_AA64MMFR0_EL1" : "=r" (mmfr0));
22+
int exs = (mmfr0 >> 44) & 0xf;
23+
if (exs == 0) {
24+
printf("Test %s, ExS not supported on this system\n", tname);
25+
return 0;
26+
}
27+
return 1;
28+
}
29+
30+
void init_exs(int eis_val, int eos_val) {
31+
uint64_t sctlr;
32+
asm volatile("mrs %0, SCTLR_EL1" : "=r" (sctlr));
33+
sctlr = eis_val ? (sctlr | SCTLR_EL1_EIS) : (sctlr & ~SCTLR_EL1_EIS);
34+
sctlr = eos_val ? (sctlr | SCTLR_EL1_EOS) : (sctlr & ~SCTLR_EL1_EOS);
35+
asm volatile("msr SCTLR_EL1, %0" :: "r" (sctlr));
36+
asm volatile("isb");
37+
}

‎litmus/libdir/_aarch64/_exs.h‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
/****************************************************************************/
2+
/* the diy toolsuite */
3+
/* */
4+
/* Jade Alglave, University College London, UK. */
5+
/* Luc Maranget, INRIA Paris-Rocquencourt, France. */
6+
/* */
7+
/* Copyright 2015-present Institut National de Recherche en Informatique et */
8+
/* en Automatique and the authors. All rights reserved. */
9+
/* */
10+
/* This software is governed by the CeCILL-B license under French law and */
11+
/* abiding by the rules of distribution of free software. You can use, */
12+
/* modify and/ or redistribute the software under the terms of the CeCILL-B */
13+
/* license as circulated by CEA, CNRS and INRIA at the following URL */
14+
/* "http://www.cecill.info". We also give a copy in LICENSE.txt. */
15+
/****************************************************************************/
16+
#ifndef _LITMUS_EXS_H
17+
#define _LITMUS_EXS_H 1
18+
19+
int check_exs(const char *tname);
20+
void init_exs(int eis_val, int eos_val);
21+
22+
#endif

‎litmus/objUtil.ml‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -272,6 +272,15 @@ module Make(O:Config)(Tar:Tar.S) =
272272
fnames
273273
end
274274
else fnames in
275+
let fnames =
276+
if flags.Flags.exs then
277+
begin
278+
let sub = dir_of_sysarch O.sysarch in
279+
let fnames = cpy ~sub:sub fnames "exs" ".c" in
280+
let fnames = cpy ~sub:sub fnames "exs" ".h" in
281+
fnames
282+
end
283+
else fnames in
275284
let fnames =
276285
if flags.Flags.pac then
277286
let sub = dir_of_sysarch O.sysarch in

‎litmus/preSi.ml‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -80,6 +80,11 @@ module Make
8080
if Cfg.variant Variant_litmus.ConstPacField && not (Cfg.variant Variant_litmus.Pac) then
8181
Warn.user_error "\"const-pac-field\" variant require \"pac\" variant"
8282

83+
let () =
84+
if (Cfg.variant Variant_litmus.EIS || Cfg.variant Variant_litmus.EOS)
85+
&& not (Cfg.variant Variant_litmus.ExS) then
86+
Warn.user_error "\"eis\"/\"eos\" variants require \"exs\" variant"
87+
8388
module Insert =
8489
ObjUtil.Insert
8590
(struct
@@ -265,6 +270,9 @@ module Make
265270
if Cfg.variant Variant_litmus.MemTag then begin
266271
O.o "#include \"memtag.h\""
267272
end;
273+
if Cfg.variant Variant_litmus.ExS then begin
274+
O.o "#include \"exs.h\""
275+
end;
268276
if Cfg.variant Variant_litmus.Pac then begin
269277
O.o "#include \"auth.h\""
270278
end;
@@ -2161,6 +2169,14 @@ module Make
21612169
in
21622170
O.fi "mte_init(%s);" (pp_tag_check Cfg.tagcheck);
21632171
end;
2172+
if Cfg.variant Variant_litmus.ExS then
2173+
begin
2174+
let eis_val =
2175+
if Cfg.variant Variant_litmus.EIS then 1 else 0 in
2176+
let eos_val =
2177+
if Cfg.variant Variant_litmus.EOS then 1 else 0 in
2178+
O.fi "init_exs(%d, %d);" eis_val eos_val;
2179+
end;
21642180
if Cfg.variant Variant_litmus.Pac then
21652181
O.oi "init_pauth();" ;
21662182
O.oi "int id = smp_processor_id();" ;
@@ -2329,6 +2345,8 @@ module Make
23292345
end ;
23302346
if Cfg.variant Variant_litmus.ConstPacField then
23312347
O.fi "if (!check_const_pac_field_variant(%S)) return 0;" doc.Name.name;
2348+
if Cfg.is_kvm && Cfg.variant Variant_litmus.ExS then
2349+
O.fi "if (!check_exs(%S)) return 0;" doc.Name.name ;
23322350
if Cfg.is_kvm then begin
23332351
match db with
23342352
| None ->

‎litmus/top_litmus.ml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -271,7 +271,8 @@ end = struct
271271
let flags =
272272
{ Flags.pac = O.variant Variant_litmus.Pac;
273273
Flags.self = O.variant Variant_litmus.Self;
274-
Flags.memtag = O.variant Variant_litmus.MemTag } in
274+
Flags.memtag = O.variant Variant_litmus.MemTag;
275+
Flags.exs = O.variant Variant_litmus.ExS } in
275276
dump src doc compiled;
276277
if not OT.is_out then begin
277278
let _utils =

‎litmus/variant_litmus.ml‎

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,9 @@ type t =
2020
| S128 (* 128 bit signed ints*)
2121
| Mixed (* Ignored *)
2222
| Vmsa (* Checked *)
23+
| ExS (* Enhanced Exception Synchronization *)
24+
| EIS (* Set SCTLR_EL1.EIS=1 when variant present *)
25+
| EOS (* Set SCTLR_EL1.EOS=1 when variant present *)
2326
| Telechat (* Telechat idiosyncrasies *)
2427
| SVE (* Do nothing *)
2528
| SME (* Do nothing *)
@@ -37,6 +40,9 @@ let (mode_variants, arch_variants) : t list * t list =
3740
| S128 -> S128
3841
| Mixed -> Mixed
3942
| Vmsa -> Vmsa
43+
| ExS -> ExS
44+
| EIS -> EIS
45+
| EOS -> EOS
4046
| Telechat -> Telechat
4147
| SVE -> SVE
4248
| SME -> SME
@@ -50,7 +56,9 @@ let (mode_variants, arch_variants) : t list * t list =
5056
let base_modes =
5157
List.map f [NoInit; S128; Telechat]
5258
and archs =
53-
List.map f [SVE; SME; Self; Mixed; Vmsa; Pac; FPac; ConstPacField; MemTag;]
59+
List.map f
60+
[SVE; SME; Self; Mixed; Vmsa; ExS; EIS; EOS; Pac; FPac; ConstPacField;
61+
MemTag;]
5462
and mte_precisions =
5563
List.map (fun precision -> f (MTEPrecision precision)) Precision.all
5664
and fault_modes =
@@ -71,6 +79,9 @@ let parse s = match Misc.lowercase s with
7179
| "self" -> Some Self
7280
| "mixed" -> Some Mixed
7381
| "vmsa"|"kvm" -> Some Vmsa
82+
| "exs" -> Some ExS
83+
| "eis" -> Some EIS
84+
| "eos" -> Some EOS
7485
| "telechat" -> Some Telechat
7586
| "sve" -> Some SVE
7687
| "sme" -> Some SME
@@ -104,6 +115,9 @@ let pp = function
104115
| Mixed -> "mixed"
105116
| S128 -> "s128"
106117
| Vmsa -> "vmsa"
118+
| ExS -> "exs"
119+
| EIS -> "eis"
120+
| EOS -> "eos"
107121
| Telechat -> "telechat"
108122
| FaultHandling p -> Fault.Handling.pp p
109123
| SVE -> "sve"

0 commit comments

Comments
 (0)