[cat] Ensure that ETS3 includes ordering rules that apply for ETS2

Signed-off-by: Nikos Nikoleris <[email protected]>
herd · Feb 5, 2025 · 22c9b1b · 22c9b1b
1 parent de10a47
commit 22c9b1b
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/herd/libdir/aarch64.cat b/herd/libdir/aarch64.cat
@@ -69,7 +69,7 @@ let Exp-haz-ob =
 let TTD-read-ordered-before =
   TLBI-after; [TLBI]; po; [dsb.full]; po; [~(Imp & M)]
   | TLBI-after; [TLBI]; po; [dsb.full]; po; [IFB]; po; [Imp & M]
-  | (if "ETS2" then TLBI-after; [TLBI]; po; [dsb.full]; po; [Imp & TTD & M] else 0)
+  | (if "ETS2" || "ETS3" then TLBI-after; [TLBI]; po; [dsb.full]; po; [Imp & TTD & M] else 0)
 
 (* TLBI-ordered-before *)
 let TLBI-ob =

diff --git a/herd/libdir/aarch64hwreqs.cat b/herd/libdir/aarch64hwreqs.cat
@@ -66,11 +66,11 @@ let f-ib =
 (* DSB-ordered-before *)
 let DSB-ob =
 [M | DC.CVAU | IC]; po; [dsb.full]; po; [~(Imp & TTD & M | Imp & Instr & R)]
- | (if "ETS2" then [M | DC.CVAU | IC]; po; [dsb.full]; po; [Imp & TTD & M] else 0)
+ | (if "ETS2" || "ETS3" then [M | DC.CVAU | IC]; po; [dsb.full]; po; [Imp & TTD & M] else 0)
  | [(Exp & R) \ NoRet | Imp & Tag & R]; po; [dsb.ld]; po; [~(Imp & TTD & M | Imp & Instr & R)]
- | (if "ETS2" then [(Exp & R) \ NoRet]; po; [dsb.ld]; po; [Imp & TTD & M] else 0)
+ | (if "ETS2" || "ETS3" then [(Exp & R) \ NoRet]; po; [dsb.ld]; po; [Imp & TTD & M] else 0)
  | [Exp & W]; po; [dsb.st]; po; [~(Imp & TTD & M | Imp & Instr & R)]
- | (if "ETS2" then [Exp & W]; po; [dsb.st]; po; [Imp & TTD & M] else 0)
+ | (if "ETS2" || "ETS3" then [Exp & W]; po; [dsb.st]; po; [Imp & TTD & M] else 0)
 
 (* IFB-ordered-before *)
 let EXC-ENTRY-IFB = EXC-ENTRY