From 22c9b1b34c962cc3c9d02e647dd9b74c763ed04b Mon Sep 17 00:00:00 2001 From: Nikos Nikoleris Date: Fri, 31 Jan 2025 17:41:05 +0000 Subject: [PATCH] [cat] Ensure that ETS3 includes ordering rules that apply for ETS2 Signed-off-by: Nikos Nikoleris --- herd/libdir/aarch64.cat | 2 +- herd/libdir/aarch64hwreqs.cat | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/herd/libdir/aarch64.cat b/herd/libdir/aarch64.cat index 9226781ed..b33c20a16 100644 --- 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 index 7bb734006..ebeab789e 100644 --- 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