From 5f610c4571cad7fe8ddd97ff9fc8cd267311652c Mon Sep 17 00:00:00 2001 From: Filippo Sestini Date: Wed, 15 Jul 2026 14:27:44 +0100 Subject: [PATCH] [cat] Replace mentions of HU/Hardware Update Effects with Implicit TTD Write Effects --- herd/libdir/aarch64.cat | 8 ++++---- herd/libdir/aarch64deps.cat | 7 +++---- herd/libdir/aarch64hwreqs.cat | 16 +++++++-------- herd/libdir/aarch64util.cat | 3 +-- herd/libdir/catdefinitions.tex | 1 - tools/tests/miaou.t | 36 ++++++++++++++++------------------ 6 files changed, 33 insertions(+), 38 deletions(-) diff --git a/herd/libdir/aarch64.cat b/herd/libdir/aarch64.cat index bfeb957ad6..abd4ca9973 100644 --- a/herd/libdir/aarch64.cat +++ b/herd/libdir/aarch64.cat @@ -61,7 +61,7 @@ with IC-after from (all-IC-Imp_Instr_R-enums local-hw-reqs) (** Explicitly-hazard-ordered-before **) let Exp-haz-ob = - [Exp & R]; (po & same-loc); [Exp & R]; sca-class?; [Exp & R]; (ca & ext); [Exp & W | HU]; sca-class?; [Exp & W | HU] + [Exp & R]; (po & same-loc); [Exp & R]; sca-class?; [Exp & R]; (ca & ext); [Exp & W | Imp & TTD & W]; sca-class?; [Exp & W | Imp & TTD & W] (** TLBI-ordered-before **) @@ -110,11 +110,11 @@ let Tag-obs = (* TLBUncacheable-coherence-after *) let TLBuncacheable-ca = - [range([TLBUncacheable & FAULT]; tr-ib^-1; [Imp & TTD & R])]; ca; [Exp & W | HU] + [range([TLBUncacheable & FAULT]; tr-ib^-1; [Imp & TTD & R])]; ca; [Exp & W | Imp & TTD & W] (* Hardware-update-coherence-after *) let HU-ca = - [Exp & R]; ca; [HU] + [Exp & R]; ca; [Imp & TTD & W] (* TLBI-coherence-after *) let TLBI-ca = @@ -125,7 +125,7 @@ let TTD-obs = [Imp & TTD]; rf | rf; [Imp & TTD] | TLBuncacheable-ca | HU-ca - | [HU]; ca; [W] | [W]; ca; [HU] + | [Imp & TTD & W]; ca; [W] | [W]; ca; [Imp & TTD & W] | TLBI-ca (** Instr-observed-by **) diff --git a/herd/libdir/aarch64deps.cat b/herd/libdir/aarch64deps.cat index 68e3dd63fc..24889634cf 100644 --- a/herd/libdir/aarch64deps.cat +++ b/herd/libdir/aarch64deps.cat @@ -52,7 +52,7 @@ let lrrs = (* Local memory write successor *) let lmws = [Exp & M | Imp & Tag & R]; (po & same-loc); [Exp & W] - | [Imp & TTD & R]; (po & same-loc); [Exp & W | HU] + | [Imp & TTD & R]; (po & same-loc); [Exp & W | Imp & TTD & W] (* Local memory read successor *) let lmrs = [W]; ((po & same-loc) & ~(intervening(W,(po & same-loc)))); [R] @@ -67,7 +67,7 @@ let rec dtrm = (** Data, Address and Control dependencies *) let data = [Exp & R]; dtrm & po; [Rreg]; iico_data & ii_data; [Exp & W] -let addr = [Exp & R]; dtrm & po; [Rreg]; iico_data & ii_addr; [Exp & M | Imp & Tag & R | Imp & TTD & R | HU | TLBI | DC.CVAU | IC.IVAU] +let addr = [Exp & R]; dtrm & po; [Rreg]; iico_data & ii_addr; [Exp & M | Imp & Tag & R | Imp & TTD & M | TLBI | DC.CVAU | IC.IVAU] let ctrl = [Exp & R]; dtrm & po; [Rreg]; iico_data; [BCC]; po (** Pick dependencies *) @@ -80,7 +80,7 @@ let pick-basic-dep = [Exp & R]; pick-dtrm let pick-addr-dep = - [Exp & R]; pick-dtrm & po; [Rreg]; iico_data & ii_addr; [Exp & M | Imp & Tag & R | Imp & TTD & R | HU | TLBI | DC.CVAU | IC.IVAU] + [Exp & R]; pick-dtrm & po; [Rreg]; iico_data & ii_addr; [Exp & M | Imp & Tag & R | Imp & TTD & M | TLBI | DC.CVAU | IC.IVAU] let pick-data-dep = [Exp & R]; pick-dtrm & po; [Rreg]; (iico_data | (iico_data; iico_ctrl)) & ii_data; [Exp & W] let pick-ctrl-dep = @@ -94,4 +94,3 @@ let pick-dep = ) & ~same-instance include "aarch64show.cat" - diff --git a/herd/libdir/aarch64hwreqs.cat b/herd/libdir/aarch64hwreqs.cat index 5e789e714a..82cbb556cb 100644 --- a/herd/libdir/aarch64hwreqs.cat +++ b/herd/libdir/aarch64hwreqs.cat @@ -93,12 +93,12 @@ let IFB-ob = let dob = addr | data - | ctrl; [Exp & W | HU | TLBI | DC.CVAU | IC] - | addr; [Exp & M]; po; [Exp & W | HU] + | ctrl; [Exp & W | Imp & TTD & W | TLBI | DC.CVAU | IC] + | addr; [Exp & M]; po; [Exp & W | Imp & TTD & W] | 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]; tr-ib; [Exp & M]; po; [Exp & W | Imp & TTD & W] + | [Imp & Tag & R]; tc-before; [Exp & M]; po; [Exp & W | Imp & TTD & W] (* Fetch-ordered-before *) let f-ob = @@ -113,16 +113,16 @@ let intr-ob = (* Pick-ordered-before *) let pob = - pick-addr-dep; [Exp & W | HU | TLBI | DC.CVAU | IC] + pick-addr-dep; [Exp & W | Imp & TTD & W | TLBI | DC.CVAU | IC] | pick-data-dep - | pick-ctrl-dep; [Exp & W | HU | TLBI | DC.CVAU | IC] - | pick-addr-dep; [Exp & M]; po; [Exp & W | HU] + | pick-ctrl-dep; [Exp & W | Imp & TTD & W | TLBI | DC.CVAU | IC] + | pick-addr-dep; [Exp & M]; po; [Exp & W | Imp & TTD & W] (* Atomic-ordered-before *) let aob = [Exp & M]; rmw; [Exp & M] | [Exp & M]; rmw; lmrs; [(Exp & R & A) | (Exp & R & Q)] - | [Imp & TTD & R]; rmw; [HU] + | [Imp & TTD & R]; rmw; [Imp & TTD & W] (* Barrier-ordered-before *) let bob = diff --git a/herd/libdir/aarch64util.cat b/herd/libdir/aarch64util.cat index 9b8a779bdf..02e01708a5 100644 --- a/herd/libdir/aarch64util.cat +++ b/herd/libdir/aarch64util.cat @@ -106,8 +106,7 @@ let same-translation-context = (Imp & TTD) * (Imp & TTD) (* HW TTD Updates permitted only for the AF or DB *) -let HU = Imp & TTD & W -assert empty HU \ (AF | DB) +assert empty (Imp & TTD & W) \ (AF | DB) (* * Include aarch64fences.cat to define barriers. diff --git a/herd/libdir/catdefinitions.tex b/herd/libdir/catdefinitions.tex index 61a45de749..1201178bc8 100644 --- a/herd/libdir/catdefinitions.tex +++ b/herd/libdir/catdefinitions.tex @@ -129,7 +129,6 @@ \newcommand{\ImpTTDM}[1]{#1 is an Implicit TTD Memory Effect} \newcommand{\ImpTTDW}[1]{#1 is an Implicit TTD Memory Write Effect} -\newcommand{\HU}[1]{#1 is a Hardware Update Effect} \newcommand{\ImpTTDR}[1]{#1 is an Implicit TTD Memory Read Effect} \newcommand{\ImpInstrM}[1]{#1 is an Implicit Instruction Memory Effect} diff --git a/tools/tests/miaou.t b/tools/tests/miaou.t index 2803c63808..1a83492500 100644 --- a/tools/tests/miaou.t +++ b/tools/tests/miaou.t @@ -334,7 +334,7 @@ \item \expandafter{\MakeUppercase\HUca{E\textsubscript{1}}{E\textsubscript{2}}}. \item All of the following apply: \begin{itemize} - \item \HU{E\textsubscript{1}}. + \item \ImpTTDW{E\textsubscript{1}}. \item \expandafter{\MakeUppercase\ca{E\textsubscript{1}}{E\textsubscript{2}}}. \item \W{E\textsubscript{2}}. \end{itemize} @@ -342,7 +342,7 @@ \begin{itemize} \item \W{E\textsubscript{1}}. \item \expandafter{\MakeUppercase\ca{E\textsubscript{1}}{E\textsubscript{2}}}. - \item \HU{E\textsubscript{2}}. + \item \ImpTTDW{E\textsubscript{2}}. \end{itemize} \item \expandafter{\MakeUppercase\TLBIca{E\textsubscript{1}}{E\textsubscript{2}}}. \end{itemize} @@ -396,8 +396,7 @@ \begin{itemize} \item \ExpM{E\textsubscript{2}}. \item \ImpTagR{E\textsubscript{2}}. - \item \ImpTTDR{E\textsubscript{2}}. - \item \HU{E\textsubscript{2}}. + \item \ImpTTDM{E\textsubscript{2}}. \item \TLBI{E\textsubscript{2}}. \item \DCCVAU{E\textsubscript{2}}. \item \ICIVAU{E\textsubscript{2}}. @@ -428,7 +427,7 @@ \begin{itemize} \item \ImpTTDR{E\textsubscript{1}}. \item \expandafter{\MakeUppercase\rmw{E\textsubscript{1}}{E\textsubscript{2}}}. - \item \HU{E\textsubscript{2}}. + \item \ImpTTDW{E\textsubscript{2}}. \end{itemize} \end{itemize} @@ -591,7 +590,7 @@ \item One of the following applies: \begin{itemize} \item \ExpW{E\textsubscript{2}}. - \item \HU{E\textsubscript{2}}. + \item \ImpTTDW{E\textsubscript{2}}. \item \TLBI{E\textsubscript{2}}. \item \DCCVAU{E\textsubscript{2}}. \item \IC{E\textsubscript{2}}. @@ -605,7 +604,7 @@ \item One of the following applies: \begin{itemize} \item \ExpW{E\textsubscript{2}}. - \item \HU{E\textsubscript{2}}. + \item \ImpTTDW{E\textsubscript{2}}. \end{itemize} \end{itemize} \item All of the following apply: @@ -639,7 +638,7 @@ \item One of the following applies: \begin{itemize} \item \ExpW{E\textsubscript{2}}. - \item \HU{E\textsubscript{2}}. + \item \ImpTTDW{E\textsubscript{2}}. \end{itemize} \end{itemize} \item All of the following apply: @@ -651,7 +650,7 @@ \item One of the following applies: \begin{itemize} \item \ExpW{E\textsubscript{2}}. - \item \HU{E\textsubscript{2}}. + \item \ImpTTDW{E\textsubscript{2}}. \end{itemize} \end{itemize} \end{itemize} @@ -691,7 +690,7 @@ \item One of the following applies: \begin{itemize} \item \ExpW{E\textsubscript{5}}. - \item \HU{E\textsubscript{5}}. + \item \ImpTTDW{E\textsubscript{5}}. \end{itemize} \item One of the following applies: \begin{itemize} @@ -701,7 +700,7 @@ \item One of the following applies: \begin{itemize} \item \ExpW{E\textsubscript{2}}. - \item \HU{E\textsubscript{2}}. + \item \ImpTTDW{E\textsubscript{2}}. \end{itemize} \end{itemize} @@ -809,8 +808,7 @@ \begin{itemize} \item \ExpM{E\textsubscript{2}}. \item \ImpTagR{E\textsubscript{2}}. - \item \ImpTTDR{E\textsubscript{2}}. - \item \HU{E\textsubscript{2}}. + \item \ImpTTDM{E\textsubscript{2}}. \item \TLBI{E\textsubscript{2}}. \item \DCCVAU{E\textsubscript{2}}. \item \ICIVAU{E\textsubscript{2}}. @@ -924,7 +922,7 @@ \item One of the following applies: \begin{itemize} \item \ExpW{E\textsubscript{2}}. - \item \HU{E\textsubscript{2}}. + \item \ImpTTDW{E\textsubscript{2}}. \item \TLBI{E\textsubscript{2}}. \item \DCCVAU{E\textsubscript{2}}. \item \IC{E\textsubscript{2}}. @@ -937,7 +935,7 @@ \item One of the following applies: \begin{itemize} \item \ExpW{E\textsubscript{2}}. - \item \HU{E\textsubscript{2}}. + \item \ImpTTDW{E\textsubscript{2}}. \item \TLBI{E\textsubscript{2}}. \item \DCCVAU{E\textsubscript{2}}. \item \IC{E\textsubscript{2}}. @@ -951,7 +949,7 @@ \item One of the following applies: \begin{itemize} \item \ExpW{E\textsubscript{2}}. - \item \HU{E\textsubscript{2}}. + \item \ImpTTDW{E\textsubscript{2}}. \end{itemize} \end{itemize} \end{itemize} @@ -1087,7 +1085,7 @@ \item One of the following applies: \begin{itemize} \item \ExpW{E\textsubscript{2}}. - \item \HU{E\textsubscript{2}}. + \item \ImpTTDW{E\textsubscript{2}}. \end{itemize} \end{itemize} \end{itemize} @@ -1121,7 +1119,7 @@ \item One of the following applies: \begin{itemize} \item \ExpW{E\textsubscript{2}}. - \item \HU{E\textsubscript{2}}. + \item \ImpTTDW{E\textsubscript{2}}. \end{itemize} \end{itemize} @@ -1130,5 +1128,5 @@ \begin{itemize} \item \ExpR{E\textsubscript{1}}. \item \expandafter{\MakeUppercase\ca{E\textsubscript{1}}{E\textsubscript{2}}}. - \item \HU{E\textsubscript{2}}. + \item \ImpTTDW{E\textsubscript{2}}. \end{itemize}