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