[litmus] Introduce EXS, EIS and EOS variants to litmus

diaolo01 · diaolo01 · commit b3b90a64d9f6 · 2026-03-24T15:45:10.000Z
diff --git a/catalogue/aarch64-faults/shelf.py b/catalogue/aarch64-faults/shelf.py
@@ -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",
 ]
diff --git a/catalogue/aarch64-faults/tests/@all b/catalogue/aarch64-faults/tests/@all
@@ -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
diff --git a/catalogue/aarch64-faults/tests/SVC-ifetch.dic0idc0-exs1eis0.litmus b/catalogue/aarch64-faults/tests/SVC-ifetch.dic0idc0-exs1eis0.litmus
@@ -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)
diff --git a/catalogue/aarch64-faults/tests/SVC-ifetch.dic0idc0-exs1eis1.litmus b/catalogue/aarch64-faults/tests/SVC-ifetch.dic0idc0-exs1eis1.litmus
@@ -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)
diff --git a/catalogue/aarch64-faults/tests/kinds.txt b/catalogue/aarch64-faults/tests/kinds.txt
@@ -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
diff --git a/litmus/dumpRun.ml b/litmus/dumpRun.ml
@@ -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
@@ -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 =
 
diff --git a/litmus/flags.mli b/litmus/flags.mli
@@ -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 *)
   }
diff --git a/litmus/libdir/_aarch64/_exs.c b/litmus/libdir/_aarch64/_exs.c
@@ -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");
+}
diff --git a/litmus/libdir/_aarch64/_exs.h b/litmus/libdir/_aarch64/_exs.h
@@ -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
diff --git a/litmus/objUtil.ml b/litmus/objUtil.ml
@@ -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
diff --git a/litmus/preSi.ml b/litmus/preSi.ml
@@ -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
@@ -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;
@@ -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();" ;
@@ -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 ;
         if Cfg.is_kvm then begin
           match db with
           | None ->
diff --git a/litmus/top_litmus.ml b/litmus/top_litmus.ml
@@ -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 =
diff --git a/litmus/variant_litmus.ml b/litmus/variant_litmus.ml
@@ -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 *)
@@ -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
@@ -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 =
@@ -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
@@ -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"
diff --git a/litmus/variant_litmus.mli b/litmus/variant_litmus.mli
@@ -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 *)

Original file line number	Diff line number	Diff line change
`@@ -20,6 +20,8 @@`
`20`	`20`	`"tests/MP+dmb.st+ctrl-svc.exs1eis1.litmus",`
`21`	`21`	`"tests/SVC-ifetch.exs1eis0.litmus",`
`22`	`22`	`"tests/SVC-ifetch.exs1eis1.litmus",`
	`23`	`+ "tests/SVC-ifetch.dic0idc0-exs1eis0.litmus",`
	`24`	`+ "tests/SVC-ifetch.dic0idc0-exs1eis1.litmus",`
`23`	`25`	`# "tests/SVC-pte.exs1eis0.litmus",`
`24`	`26`	`# "tests/SVC-pte.exs1eis1.litmus",`
`25`	`27`	`]`
Original file line number	Diff line number	Diff line change
`@@ -21,4 +21,5 @@ type t =`
`21`	`21`	`pac : bool ; (* Requires pointer authentification *)`
`22`	`22`	`self : bool ; (* Self modying code *)`
`23`	`23`	`memtag : bool ; (* Requires memory tagging *)`
	`24`	`+ exs : bool ; (* Requires ExS helpers *)`
`24`	`25`	`}`