Skip to content

[herd,cat] Tentative ordering requirements for strengthening FEAT_ETS #1689

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

Draft
artkhyzha wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

[herd,cat] Tentative ordering requirements for strengthening FEAT_ETS #1689

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
325e7d1
[cat] Generalizing *-intrinsically-before relations as Immediately-in…
artkhyzha Jan 27, 2026
806e711
[cat] Elaborating the scope of the ordering rules known only to apply…
artkhyzha Jan 27, 2026
f6fb047
[herd,cat] Tentative ordering requirements for FEAT_ETS4
artkhyzha Jan 27, 2026
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
63 changes: 34 additions & 29 deletions herd/libdir/aarch64hwreqs.cat
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,45 +49,45 @@
*)
include "aarch64deps.cat"

(* Tag-Check-before *)
(* Tag-Check-intrinsically-before *)
(* Note: in asynchronous fault handling mode, instruction semantics for
checked memory accesses does not feature the iico_ctrl edge to Exp & M
*)
let tc-before =
[Imp & Tag & R]; iico_data; [B]; iico_ctrl; [Exp & M | TagCheck & FAULT]

(* Tag-Check-intrinsically-before *)
let tc-ib = tc-before; [~(Exp & R)]
let tc-ib = [Imp & Tag & R]; imm-ib; [Exp & W | TagCheck & FAULT]

(* Fetch-intrinsically-before *)
let f-ib =
[Imp & Instr & R]; iico_data; [B]; (iico_ctrl | iico_ctrl; iico_data)
[Imp & Instr & R]; imm-ib

(* DSB-ordered-before *)
(* DSB-ordered-before *)
let DSB-ob =
[M | DC.CVAU | IC | TLBI]; po; [dsb.full]; po; [~(Imp & TTD & M | Imp & Instr & R)]
| (if "ETS2" || "ETS3" then [M | DC.CVAU | IC | TLBI]; po; [dsb.full]; po; [Imp & TTD & M] else 0)
[M | DC.CVAU | IC | TLBI]; po; [dsb.full]; po; [~(Imp & TTD & M | Imp & Instr & R)]
| (if "ETS2" || "ETS3" || "ETS4" then [M | DC.CVAU | IC | TLBI]; po; [dsb.full]; po; [Imp & D-TTD & M] else 0)
| (if "ETS4" then [M | DC.CVAU | IC | TLBI]; po; [dsb.full]; po; [I-MMU & EXC-ENTRY]; imm-ib^-1; [Imp & I-TTD & R] else 0)
| (if "ETS4" then [M | DC.CVAU | IC | TLBI]; po; [dsb.full]; po; [UndefinedInstruction & EXC-ENTRY]; imm-ib^-1; [Imp & Instr & R] else 0)
| [(Exp & R) \ NoRet | Imp & Tag & R]; po; [dsb.ld]; po; [~(Imp & TTD & M | Imp & Instr & R)]
| (if "ETS2" || "ETS3" then [(Exp & R) \ NoRet]; po; [dsb.ld]; po; [Imp & TTD & M] else 0)
| (if "ETS2" || "ETS3" || "ETS4" then [(Exp & R) \ NoRet]; po; [dsb.ld]; po; [Imp & D-TTD & M] else 0)
| (if "ETS4" then [(Exp & R) \ NoRet]; po; [dsb.ld]; po; [I-MMU & EXC-ENTRY]; imm-ib^-1; [Imp & I-TTD & R] else 0)
| (if "ETS4" then [(Exp & R) \ NoRet]; po; [dsb.ld]; po; [UndefinedInstruction & EXC-ENTRY]; imm-ib^-1; [Imp & Instr & R] else 0)
| [Exp & W]; po; [dsb.st]; po; [~(Imp & TTD & M | Imp & Instr & R)]
| (if "ETS2" || "ETS3" then [Exp & W]; po; [dsb.st]; po; [Imp & TTD & M] else 0)
| (if "ETS2" || "ETS3" || "ETS4" then [Exp & W]; po; [dsb.st]; po; [Imp & D-TTD & M] else 0)
| (if "ETS4" then [Exp & W]; po; [dsb.st]; po; [I-MMU & EXC-ENTRY]; imm-ib^-1; [Imp & I-TTD & R] else 0)
| (if "ETS4" then [Exp & W]; po; [dsb.st]; po; [UndefinedInstruction & EXC-ENTRY]; imm-ib^-1; [Imp & Instr & R] else 0)

(* IFB-ordered-before *)
let EXC-ENTRY-IFB = if not "ExS" || "EIS" then EXC-ENTRY else EXC-ENTRY \ SVC
let EXC-RET-IFB = if not "ExS" || "EOS" then EXC-RET else {}
let IFB = ISB | EXC-ENTRY-IFB | EXC-RET-IFB

let IFB-ob =
[Exp & R]; ctrl; [IFB]; po
DSB-ob; [IFB]; po
| [Exp & R]; ctrl; [IFB]; po
| [Exp & R]; pick-ctrl-dep; [IFB]; po
| [Exp & R]; addr; [Exp & M]; po; [IFB]; po
| [Exp & R]; pick-addr-dep; [Exp & M]; po; [IFB]; po
| [Exp & R]; pick-addr-dep; (tc-ib | tr-ib); [IFB]; po
| DSB-ob; [IFB]; po
| [Imp & TTD & R]; tr-ib; [IFB]; po
| [Imp & Tag & R]; tc-ib; [IFB]; po
| [Imp & TTD & R]; tr-ib; [Exp & M]; po; [IFB]; po
| [Imp & Tag & R]; tc-before; [Exp & M]; po; [IFB]; po
| [Exp & R]; pick-addr-dep; [Imp & TTD & R | Imp & Tag & R]; imm-ib; [IFB]; po
| [Imp & TTD & R | Imp & Tag & R]; imm-ib; [IFB]; po
| [Imp & TTD & R | Imp & Tag & R]; imm-ib; [Exp & M]; po; [IFB]; po

(* Dependency-ordered-before *)
let dob =
Expand All @@ -97,8 +97,7 @@ let dob =
| addr; [Exp & M]; po; [Exp & W | HU]
| addr; [Exp & M]; lmrs; [Exp & R | Imp & Tag & R]
| data; [Exp & M]; lmrs; [Exp & R | Imp & Tag & R]
| [Imp & TTD & R]; tr-ib; [Exp & M]; po; [Exp & W | HU]
| [Imp & Tag & R]; tc-before; [Exp & M]; po; [Exp & W | HU]
| [Imp & TTD & R | Imp & Tag & R]; imm-ib; [Exp & M]; po; [Exp & W | HU]

(* Fetch-ordered-before *)
let f-ob =
Expand All @@ -119,15 +118,15 @@ let aob =

(* Barrier-ordered-before *)
let bob =
[Exp & M | Imp & Tag & R]; po; [dmb.full]; po; [Exp & M | Imp & Tag & R | MMU & FAULT]
[Exp & M | Imp & Tag & R]; po; [dmb.full]; po; [Exp & M | Imp & Tag & R | D-MMU & FAULT]
| [Exp & M]; po; [dmb.full]; po; [DC.CVAU]
| [DC.CVAU]; po; [dmb.full]; po; [Exp & M]
| [DC.CVAU]; po; [dmb.full]; po; [DC.CVAU]
| [Exp & (R \ NoRet) | Imp & Tag & R]; po; [dmb.ld]; po; [Exp & M | Imp & Tag & R | MMU & FAULT]
| [Exp & W]; po; [dmb.st]; po; [Exp & W | MMU & FAULT]
| [range([Exp & R & A]; amo; [Exp & W & L])]; po; [Exp & M | Imp & Tag & R | MMU & FAULT]
| [Exp & (R \ NoRet) | Imp & Tag & R]; po; [dmb.ld]; po; [Exp & M | Imp & Tag & R | D-MMU & FAULT]
| [Exp & W]; po; [dmb.st]; po; [Exp & W | D-MMU & FAULT]
| [range([Exp & R & A]; amo; [Exp & W & L])]; po; [Exp & M | Imp & Tag & R | D-MMU & FAULT]
| [Exp & W & L]; po; [Exp & R & A]
| [(Exp & R & A) | (Exp & R & Q)]; po; [Exp & M | Imp & Tag & R | MMU & FAULT]
| [(Exp & R & A) | (Exp & R & Q)]; po; [Exp & M | Imp & Tag & R | D-MMU & FAULT]
| [Exp & R & Q]; iico_order; [Exp & R & Q]
| [Exp & M | Imp & Tag & R]; po; [Exp & W & L]
| [Exp & W & L]; iico_order; [Exp & W & L]
Expand All @@ -142,13 +141,19 @@ let TLBUncacheable = MMU & (Translation | AccessFlag)
(* ETS-ordered-before *)
let ets-ob =
(if "ETS2" then
[Exp & M]; po; [TLBUncacheable & FAULT]; tr-ib^-1; [Imp & TTD & R]
[Exp & M]; po; [TLBUncacheable & D-MMU & EXC-ENTRY]; imm-ib^-1; [Imp & D-TTD & R]
else 0)
| (if "ETS3" then
[Exp & M]; po; [MMU & FAULT]; tr-ib^-1; [Imp & TTD & R]
[Exp & M]; po; [D-MMU & EXC-ENTRY]; imm-ib^-1; [Imp & D-TTD & R]
else 0)
| (if "ETS3" then
[Exp & M]; po; [TagCheck & EXC-ENTRY]; tc-ib^-1; [Imp & Tag & R]
[Exp & M]; po; [TagCheck & EXC-ENTRY]; imm-ib^-1; [Imp & Tag & R]
else 0)
| (if "ETS4" then
[Exp & M]; po; [I-MMU & EXC-ENTRY]; imm-ib^-1; [Imp & I-TTD & R]
else 0)
| (if "ETS4" then
[Exp & M]; po; [UndefinedInstruction & EXC-ENTRY]; imm-ib^-1; [Imp & Instr & R]
else 0)

(* Locally-ordered-before *)
Expand Down
6 changes: 5 additions & 1 deletion herd/libdir/aarch64loc.cat
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,13 @@
(* Same General Purpose Register *)
let same-gpr = [Rreg|Wreg]; loc; [Rreg|Wreg]

(* Immediately-intrinsically-before *)
let imm-ib =
[Imp & R]; iico_data; [B]; iico_ctrl; iico_data?; [Exp & M | Imp & M | EXC-ENTRY]

(* Translation-intrinsically-before *)
let tr-ib =
[Imp & TTD & R]; iico_data; [B]; iico_ctrl; [Exp & M | MMU & FAULT]
[Imp & TTD & R]; imm-ib; [Exp & M | MMU & FAULT]

(* Effect with valid PA *)
let E-valid-PA = M | DC.CVAU | IC
Expand Down
10 changes: 8 additions & 2 deletions herd/variant.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,10 +60,12 @@ type t =
| Instances (* Compute dependencies on instruction instances *)
(*Replaces old KVM -> Virtual memory *)
| VMSA
(* AArch64: Enhanced Translation Synchronization - FEAT_ETS, FEAT_ETS2 *)
(* AArch64: Enhanced Translation Synchronization - FEAT_ETS, FEAT_ETS2,
FEAT_ETS3, FEAT_ETS4 *)
| ETS (*Deprecated*)
| ETS2 (*New feature introduced after deprecating ETS*)
| ETS3 (*A feature further strengthening ETS2*)
| ETS4 (*A feature further strengthening ETS3*)
(* AArch64: Enhanced Exception Synchronization - FEAT_ExS *)
| ExS | EIS | EOS
(* Do not insert branching event between pte read and accesses *)
Expand Down Expand Up @@ -157,6 +159,7 @@ let (mode_variants, arch_variants) : t list * t list =
| ETS -> ETS
| ETS2 -> ETS2
| ETS3 -> ETS3
| ETS4 -> ETS4
| ExS -> ExS
| EIS -> EIS
| EOS -> EOS
Expand Down Expand Up @@ -217,7 +220,7 @@ let (mode_variants, arch_variants) : t list * t list =
Fault.Handling.tags
and arch_feat =
List.map f
[ ETS; ETS2; ETS3;
[ ETS; ETS2; ETS3; ETS4;
ExS; EIS; EOS;
DIC; IDC; NV2;
Mixed; Unaligned; DontCheckMixed; Ifetch;
Expand Down Expand Up @@ -260,6 +263,7 @@ let parse s = match Misc.lowercase s with
| "ets" -> Some ETS
| "ets2" -> Some ETS2
| "ets3" -> Some ETS3
| "ets4" -> Some ETS4
| "exs" -> Some ExS
| "eis" -> Some EIS
| "eos" -> Some EOS
Expand Down Expand Up @@ -365,6 +369,7 @@ let pp = function
| ETS -> "ets"
| ETS2 -> "ets2"
| ETS3 -> "ets3"
| ETS4 -> "ets4"
| ExS -> "exs"
| EIS -> "eis"
| EOS -> "eos"
Expand Down Expand Up @@ -444,6 +449,7 @@ let pp = function
| ETS -> "Enable FEAT_ETS, Enhanced Translation Synchronization (deprecated)"
| ETS2 -> "Enable FEAT_ETS2"
| ETS3 -> "Enable FEAT_ETS3"
| ETS4 -> "Enable FEAT_ETS4"
| ExS -> "Enable FEAT_ExS, Enhanced Exception Synchronization (AArch64 only)"
| EIS -> "If FEAT_ExS is enabled, configure the effect of certain Exception entry events, see SCTLR_ELx.EIS (AArch64 only)"
| EOS -> "If FEAT_ExS is enabled, configure the effect of an Exception return, see SCTLR_ELx.EOS (AArch64 only)"
Expand Down
4 changes: 3 additions & 1 deletion herd/variant.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,10 +58,12 @@ type t =
| Instances (* Compute dependencies on instruction instances *)
(*Replaces old KVM -> Virtual memory *)
| VMSA
(* AArch64: Enhanced Translation Synchronization - FEAT_ETS, FEAT_ETS2, FEAT_ETS3 *)
(* AArch64: Enhanced Translation Synchronization - FEAT_ETS, FEAT_ETS2,
FEAT_ETS3, FEAT_ETS4 *)
| ETS (*Deprecated*)
| ETS2 (*New feature introduced after deprecating ETS*)
| ETS3 (*A feature further strengthening ETS2*)
| ETS4 (*A feature further strengthening ETS3*)
(* AArch64: Enhanced Exception Synchronization - FEAT_ExS *)
| ExS | EIS | EOS
(* Do not insert branching event between pte read and accesses *)
Expand Down
Loading