Skip to content

[litmus] Introduce ExS, EIS and EOS variants #1716

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
diaolo01 wants to merge 1 commit into
base: master
Choose a base branch
from
+159 −4
Open

[litmus] Introduce ExS, EIS and EOS variants #1716

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions catalogue/aarch64-faults/shelf.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,8 @@
"tests/MP+dmb.st+ctrl-svc.exs1eis1.litmus",
"tests/SVC-ifetch.exs1eis0.litmus",
"tests/SVC-ifetch.exs1eis1.litmus",
"tests/SVC-ifetch.dic0idc0-exs1eis0.litmus",
"tests/SVC-ifetch.dic0idc0-exs1eis1.litmus",
# "tests/SVC-pte.exs1eis0.litmus",
# "tests/SVC-pte.exs1eis1.litmus",
]
2 changes: 2 additions & 0 deletions catalogue/aarch64-faults/tests/@all
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,5 +9,7 @@ MP+dmb.st+ctrl-svc.exs1eis0.litmus
MP+dmb.st+ctrl-svc.exs1eis1.litmus
SVC-ifetch.exs1eis0.litmus
SVC-ifetch.exs1eis1.litmus
SVC-ifetch.dic0idc0-exs1eis0.litmus
SVC-ifetch.dic0idc0-exs1eis1.litmus
SVC-pte.exs1eis0.litmus
SVC-pte.exs1eis1.litmus
18 changes: 18 additions & 0 deletions catalogue/aarch64-faults/tests/SVC-ifetch.dic0idc0-exs1eis0.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
AArch64 SVC-ifetch.dic0idc0-exs1eis0.litmus
variant=ifetch,exs
{
0:X0=instr:"NOP"; 0:X1=P0:L2;
}
P0 | P0.F ;
STR W0,[X1] | ERET ;
DC CVAU, X1 |;
DSB ISH |;
IC IVAU, X1 |;
DSB ISH |;
SVC #0 |;
L2: |;
B L1 |;
MOV W9,#1 |;
L1: |;

exists(0:X9=0)
18 changes: 18 additions & 0 deletions catalogue/aarch64-faults/tests/SVC-ifetch.dic0idc0-exs1eis1.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
AArch64 SVC-ifetch.dic0idc0-exs1eis1
variant=ifetch,exs,eis
{
0:X0=instr:"NOP"; 0:X1=P0:L2;
}
P0 | P0.F ;
STR W0,[X1] | ERET ;
DC CVAU, X1 |;
DSB ISH |;
IC IVAU, X1 |;
DSB ISH |;
SVC #0 |;
L2: |;
B L1 |;
MOV W9,#1 |;
L1: |;

exists(0:X9=0)
2 changes: 2 additions & 0 deletions catalogue/aarch64-faults/tests/kinds.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,3 +11,5 @@ SVC-pte.exs1eis0 Allowed
SVC-pte.exs1eis1 Forbid
SVC-ifetch.exs1eis0 Allowed
SVC-ifetch.exs1eis1 Forbid
SVC-ifetch.dic0idc0-exs1eis0 Allowed
SVC-ifetch.dic0idc0-exs1eis1 Forbid
9 changes: 7 additions & 2 deletions litmus/dumpRun.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -139,6 +139,10 @@ end = struct
if flags.Flags.memtag then
"memtag.o"::utils
else utils in
let utils =
if flags.Flags.exs then
"exs.o"::utils
else utils in
let utils =
if flags.Flags.pac then
"auth.o"::utils
Expand Down Expand Up @@ -210,10 +214,11 @@ let collect_flags names =
let open Flags in
{ pac = flags.pac || some_flags.pac;
self = flags.self || some_flags.self;
memtag = flags.memtag || some_flags.memtag;}
memtag = flags.memtag || some_flags.memtag;
exs = flags.exs || some_flags.exs;}
| _ -> some_flags)
names
{Flags.pac=false; Flags.self=false; Flags.memtag=false}
{Flags.pac=false; Flags.self=false; Flags.memtag=false; Flags.exs=false}

let run_tests names flags out_chan =

Expand Down
1 change: 1 addition & 0 deletions litmus/flags.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,4 +21,5 @@ type t =
pac : bool ; (* Requires pointer authentification *)
self : bool ; (* Self modying code *)
memtag : bool ; (* Requires memory tagging *)
exs : bool ; (* Requires ExS helpers *)
}
40 changes: 40 additions & 0 deletions litmus/libdir/_aarch64/_exs.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
/****************************************************************************/
/* the diy toolsuite */
/* */
/* Jade Alglave, University College London, UK. */
/* Luc Maranget, INRIA Paris-Rocquencourt, France. */
/* */
/* Copyright 2026-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. */
/****************************************************************************/
#include "kvm-headers.h"
#include "exs.h"

#define MMFR0_EXS_SHIFT 44
#define MMFR0_EXS_MASK 0xf

int check_exs(const char *tname) {
uint64_t mmfr0;
asm volatile("mrs %0, ID_AA64MMFR0_EL1" : "=r" (mmfr0));
int exs = (mmfr0 >> MMFR0_EXS_SHIFT) & MMFR0_EXS_MASK;
if (exs == 0) {
printf("Test %s, ExS not supported on this system\n", tname);
return 0;
}
return 1;
}

void init_exs(int eis_val, int eos_val) {
uint64_t sctlr;
asm volatile("mrs %0, SCTLR_EL1" : "=r" (sctlr));
sctlr = eis_val ? (sctlr | SCTLR_EL1_EIS) : (sctlr & ~SCTLR_EL1_EIS);
sctlr = eos_val ? (sctlr | SCTLR_EL1_EOS) : (sctlr & ~SCTLR_EL1_EOS);
asm volatile("msr SCTLR_EL1, %0" :: "r" (sctlr));
asm volatile("isb");
}
22 changes: 22 additions & 0 deletions litmus/libdir/_aarch64/_exs.h
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
/****************************************************************************/
/* the diy toolsuite */
/* */
/* Jade Alglave, University College London, UK. */
/* Luc Maranget, INRIA Paris-Rocquencourt, France. */
/* */
/* Copyright 2026-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. */
/****************************************************************************/
#ifndef _LITMUS_EXS_H
#define _LITMUS_EXS_H 1

int check_exs(const char *tname);
void init_exs(int eis_val, int eos_val);

#endif
9 changes: 9 additions & 0 deletions litmus/objUtil.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -272,6 +272,15 @@ module Make(O:Config)(Tar:Tar.S) =
fnames
end
else fnames in
let fnames =
if flags.Flags.exs then
begin
let sub = dir_of_sysarch O.sysarch in
let fnames = cpy ~sub:sub fnames "exs" ".c" in
let fnames = cpy ~sub:sub fnames "exs" ".h" in
fnames
end
else fnames in
let fnames =
if flags.Flags.pac then
let sub = dir_of_sysarch O.sysarch in
Expand Down
18 changes: 18 additions & 0 deletions litmus/preSi.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,6 +80,11 @@ module Make
if Cfg.variant Variant_litmus.ConstPacField && not (Cfg.variant Variant_litmus.Pac) then
Warn.user_error "\"const-pac-field\" variant require \"pac\" variant"

let () =
if (Cfg.variant Variant_litmus.EIS || Cfg.variant Variant_litmus.EOS)
&& not (Cfg.variant Variant_litmus.ExS) then
Warn.user_error "\"eis\"/\"eos\" variants require \"exs\" variant"

module Insert =
ObjUtil.Insert
(struct
Expand Down Expand Up @@ -271,6 +276,9 @@ module Make
if Cfg.variant Variant_litmus.MemTag then begin
O.o "#include \"memtag.h\""
end;
if Cfg.variant Variant_litmus.ExS then begin
O.o "#include \"exs.h\""
end;
if Cfg.variant Variant_litmus.Pac then begin
O.o "#include \"auth.h\""
end;
Expand Down Expand Up @@ -2256,6 +2264,14 @@ module Make
in
O.fi "mte_init(%s);" (pp_tag_check Cfg.tagcheck);
end;
if Cfg.variant Variant_litmus.ExS then
begin
let eis_val =
if Cfg.variant Variant_litmus.EIS then 1 else 0 in
let eos_val =
if Cfg.variant Variant_litmus.EOS then 1 else 0 in
O.fi "init_exs(%d, %d);" eis_val eos_val;
end;
if Cfg.variant Variant_litmus.Pac then
O.oi "init_pauth();" ;
O.oi "int id = smp_processor_id();" ;
Expand Down Expand Up @@ -2424,6 +2440,8 @@ module Make
end ;
if Cfg.variant Variant_litmus.ConstPacField then
O.fi "if (!check_const_pac_field_variant(%S)) return 0;" doc.Name.name;
if Cfg.is_kvm && Cfg.variant Variant_litmus.ExS then
O.fi "if (!check_exs(%S)) return 0;" doc.Name.name ;
Copy link
Copy Markdown
Member

@relokin relokin Feb 23, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

perhaps you could also move the eis and eos handling here as well?

Copy link
Copy Markdown
Contributor Author

@diaolo01 diaolo01 Feb 23, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have followed the split between check for feature and use feature as it's done for PAC. MTE does the check for feature within the mte_init function, which is in the same location in the code as eis/eos handling.

Copy link
Copy Markdown
Collaborator

@murzinv murzinv Feb 23, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

MTE does the check for feature within the mte_init function, which is in the same location in the code as eis/eos handling.

Unrelated to the PR. Perhaps MTE would benefit from the similar check/use split...

if Cfg.is_kvm then begin
match db with
| None ->
Expand Down
3 changes: 2 additions & 1 deletion litmus/top_litmus.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -271,7 +271,8 @@ end = struct
let flags =
{ Flags.pac = O.variant Variant_litmus.Pac;
Flags.self = O.variant Variant_litmus.Self;
Flags.memtag = O.variant Variant_litmus.MemTag } in
Flags.memtag = O.variant Variant_litmus.MemTag;
Flags.exs = O.variant Variant_litmus.ExS } in
dump src doc compiled;
if not OT.is_out then begin
let _utils =
Expand Down
16 changes: 15 additions & 1 deletion litmus/variant_litmus.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,9 @@ type t =
| S128 (* 128 bit signed ints*)
| Mixed (* Ignored *)
| Vmsa (* Checked *)
| ExS (* Enhanced Exception Synchronization *)
| EIS (* Set SCTLR_EL1.EIS=1 when variant present *)
| EOS (* Set SCTLR_EL1.EOS=1 when variant present *)
| Telechat (* Telechat idiosyncrasies *)
| SVE (* Do nothing *)
| SME (* Do nothing *)
Expand All @@ -37,6 +40,9 @@ let (mode_variants, arch_variants) : t list * t list =
| S128 -> S128
| Mixed -> Mixed
| Vmsa -> Vmsa
| ExS -> ExS
| EIS -> EIS
| EOS -> EOS
| Telechat -> Telechat
| SVE -> SVE
| SME -> SME
Expand All @@ -50,7 +56,9 @@ let (mode_variants, arch_variants) : t list * t list =
let base_modes =
List.map f [NoInit; S128; Telechat]
and archs =
List.map f [SVE; SME; Self; Mixed; Vmsa; Pac; FPac; ConstPacField; MemTag;]
List.map f
[SVE; SME; Self; Mixed; Vmsa; ExS; EIS; EOS; Pac; FPac; ConstPacField;
MemTag;]
and mte_precisions =
List.map (fun precision -> f (MTEPrecision precision)) Precision.all
and fault_modes =
Expand All @@ -71,6 +79,9 @@ let parse s = match Misc.lowercase s with
| "ifetch"|"self" -> Some Self
| "mixed" -> Some Mixed
| "vmsa"|"kvm" -> Some Vmsa
| "exs" -> Some ExS
| "eis" -> Some EIS
| "eos" -> Some EOS
| "telechat" -> Some Telechat
| "sve" -> Some SVE
| "sme" -> Some SME
Expand Down Expand Up @@ -104,6 +115,9 @@ let pp = function
| Mixed -> "mixed"
| S128 -> "s128"
| Vmsa -> "vmsa"
| ExS -> "exs"
| EIS -> "eis"
| EOS -> "eos"
| Telechat -> "telechat"
| FaultHandling p -> Fault.Handling.pp p
| SVE -> "sve"
Expand Down
3 changes: 3 additions & 0 deletions litmus/variant_litmus.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,9 @@ type t =
| S128 (* 128 bit signed ints*)
| Mixed (* Ignored *)
| Vmsa (* Checked *)
| ExS (* Enhanced Exception Synchronization *)
| EIS (* Set SCTLR_EL1.EIS=1 when variant present *)
| EOS (* Set SCTLR_EL1.EOS=1 when variant present *)
| Telechat (* Telechat idiosyncrasies *)
| SVE (* Do nothing *)
| SME (* Do nothing *)
Expand Down
Loading