[all] Improve the implementation of memory attributes for AArch64

herd/libdir/aarch64bbm.cat

@@ -51,29 +51,29 @@ include "aarch64memattrs.cat"
 let ca = fr | co
 
 let PTE-MT-update =
-  [PTENormal]; ca; [PTEDevice]
-  | [PTEDevice]; ca; [PTENormal]
+  [Normal]; ca; [Device]
+  | [Device]; ca; [Normal]
 
 let PTE-SH-update =
-  [PTENon-shareable]; ca; [PTEInner-shareable | PTEOuter-shareable]
-  | [PTEInner-shareable]; ca; [PTEOuter-shareable | PTENon-shareable]
-  | [PTEOuter-shareable]; ca; [PTENon-shareable | PTEInner-shareable]
+  [NSH]; ca; [ISH | OSH]
+  | [ISH]; ca; [OSH | NSH]
+  | [OSH]; ca; [NSH | ISH]
 
 let PTE-ICH-update =
-  [PTEInner-non-cacheable]; ca; [PTEInner-write-through | PTEInner-write-back]
-  | [PTEInner-write-through]; ca; [PTEInner-write-back | PTEInner-non-cacheable]
-  | [PTEInner-write-back]; ca; [PTEInner-non-cacheable | PTEInner-write-through]
+  [iNC]; ca; [iWT | iWB]
+  | [iWT]; ca; [iWB | iNC]
+  | [iWB]; ca; [iNC | iWT]
 
 let PTE-OCH-update =
-  [PTEOuter-non-cacheable]; ca; [PTEOuter-write-through | PTEOuter-write-back]
-  | [PTEOuter-write-through]; ca; [PTEOuter-write-back | PTEOuter-non-cacheable]
-  | [PTEOuter-write-back]; ca; [PTEOuter-non-cacheable | PTEOuter-write-through]
+  [oNC]; ca; [oWT | oWB]
+  | [oWT]; ca; [oWB | oNC]
+  | [oWB]; ca; [oNC | oWT]
 
 let PTE-DT-update =
-  [PTEDevice-GRE]; ca; [PTEDevice-nGRE | PTEDevice-nGnRE | PTEDevice-nGnRnE]
-  | [PTEDevice-nGRE]; ca; [PTEDevice-GRE | PTEDevice-nGnRE | PTEDevice-nGnRnE]
-  | [PTEDevice-nGnRE]; ca; [PTEDevice-GRE | PTEDevice-nGRE | PTEDevice-nGnRnE]
-  | [PTEDevice-nGnRnE]; ca; [PTEDevice-GRE | PTEDevice-nGRE | PTEDevice-nGnRE]
+  [Device-GRE]; ca; [Device-nGRE | Device-nGnRE | Device-nGnRnE]
+  | [Device-nGRE]; ca; [Device-GRE | Device-nGnRE | Device-nGnRnE]
+  | [Device-nGnRE]; ca; [Device-GRE | Device-nGRE | Device-nGnRnE]
+  | [Device-nGnRnE]; ca; [Device-GRE | Device-nGRE | Device-nGnRE]
 
 let PTE-OA-update = ([PTE]; ca; [PTE & oa-changes(PTE, ca^-1)])
 let PTE-OA-update-writable = PTE-OA-update &

herd/libdir/aarch64fences.cat

@@ -53,9 +53,9 @@ let dsb.ld = DSB.ISHLD | DSB.OSHLD | DSB.LD
 let dsb.st = DSB.ISHST | DSB.OSHST | DSB.ST
 
 (*
- * A further restriction is that standard litmus tests are unable to
- * distinguish between DMB and DSB instructions, so the model treats
- * them as equivalent to each other.
+ * A DSB acts as a stronger barrier than a DMB and all ordering that is
+ * created by a DMB with specific options is also generated by a DSB with
+ * the same options.
  *)
 let dmb.full = DMB.ISH | DMB.OSH | DMB.SY | dsb.full
 let dmb.ld = DMB.ISHLD | DMB.OSHLD | DMB.LD | dsb.ld

herd/libdir/aarch64memattrs.cat

@@ -41,100 +41,83 @@
  * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  *)
 
+let TTD = PTE
+
+procedure conflict(attr, set) =
+  let diff = attr & (set \ attr)
+  assert empty diff as Invalid-Attribute
+end
+
 (*** Device Memory ***)
 
 (* Device Memory Types *)
-let PTEDevice-GRE = try PTEDevice-GRE with emptyset
-let PTEDevice-nGRE = try PTEDevice-nGRE with emptyset
-let PTEDevice-nGnRE = try PTEDevice-nGnRE with emptyset
-let PTEDevice-nGnRnE = try PTEDevice-nGnRnE with emptyset
-
-(* A PTE can only have one of the above Device memory types  *)
-let DeviceMemoryType-conflict = (PTEDevice-GRE & PTEDevice-nGRE)
-                              | (PTEDevice-GRE & PTEDevice-nGnRE)
-                              | (PTEDevice-GRE & PTEDevice-nGnRnE)
-                              | (PTEDevice-nGRE & PTEDevice-nGnRE)
-                              | (PTEDevice-nGRE & PTEDevice-nGnRnE)
-                              | (PTEDevice-nGnRE & PTEDevice-nGnRnE)
-assert empty DeviceMemoryType-conflict as Invalid-Device-Memory-Type
-
-let PTEDevice = try PTEDevice with emptyset
-let PTEDevice = PTEDevice
-              | PTEDevice-GRE | PTEDevice-nGRE | PTEDevice-nGnRE | PTEDevice-nGnRnE
+let Device-GRE = try PTEDevice-GRE with emptyset
+let Device-nGRE = try PTEDevice-nGRE with emptyset
+let Device-nGnRE = try PTEDevice-nGnRE with emptyset
+let Device-nGnRnE = try PTEDevice-nGnRnE with emptyset
+let Device = Device-GRE | Device-nGRE | Device-nGnRE | Device-nGnRnE
+
+call conflict(Device-GRE, Device)
+call conflict(Device-nGRE, Device)
+call conflict(Device-nGnRE, Device)
+call conflict(Device-nGnRnE, Device)
 
 (*** Normal Memory ***)
 
-let PTENon-shareable = try PTENon-shareable with emptyset
-let PTEInner-shareable = try PTEInner-shareable with emptyset
-let PTEOuter-shareable = try PTEOuter-shareable with emptyset
+let NSH = try PTENSH with emptyset
+let ISH = try PTEISH with emptyset
+let OSH = try PTEOSH with emptyset
+let Shareability = NSH | ISH | OSH
 
 (* Memory cannot have more than one Shareability Attribute *)
-let Shareability-conflict = (PTENon-shareable & PTEInner-shareable)
-                          | (PTEInner-shareable & PTEOuter-shareable)
-                          | (PTENon-shareable & PTEOuter-shareable)
-assert empty Shareability-conflict as Invalid-Shareability
+call conflict(NSH, Shareability)
+call conflict(ISH, Shareability)
+call conflict(OSH, Shareability)
 
-let PTEInner-write-back = try PTEInner-write-back with emptyset
-let PTEInner-write-through = try PTEInner-write-through with emptyset
-let PTEInner-non-cacheable = try PTEInner-non-cacheable with emptyset
+let iWB = try PTEiWB with emptyset
+let iWT = try PTEiWT with emptyset
+let iNC = try PTEiNC with emptyset
+let InnerCacheability = iWB | iWT | iNC
 
 (* Memory cannot have more than one Inner Cacheability Attribute *)
-let InnerCacheability-conflict = (PTEInner-write-back & PTEInner-write-through)
-                               | (PTEInner-write-through & PTEInner-non-cacheable)
-                               | (PTEInner-non-cacheable & PTEInner-write-back)
-assert empty InnerCacheability-conflict as Invalid-Inner-Cacheability
+call conflict(iWB, InnerCacheability)
+call conflict(iWT, InnerCacheability)
+call conflict(iNC, InnerCacheability)
 
-let PTEOuter-write-back = try PTEOuter-write-back with emptyset
-let PTEOuter-write-through = try PTEOuter-write-through with emptyset
-let PTEOuter-non-cacheable = try PTEOuter-non-cacheable with emptyset
+let oWB = try PTEoWB with emptyset
+let oWT = try PTEoWT with emptyset
+let oNC = try PTEoNC with emptyset
+let OuterCacheability = oWB | oWT | oNC
 
-(* Memory cannot have more than one Outer Cacheability Attribute *)
-let OuterCacheability-conflict = (PTEOuter-write-back & PTEOuter-write-through)
-                               | (PTEOuter-write-through & PTEOuter-non-cacheable)
-                               | (PTEOuter-non-cacheable & PTEOuter-write-back)
-assert empty OuterCacheability-conflict as Invalid-Outer-Cacheability
+(* Memory cannot have more than one Inner Cacheability Attribute *)
+call conflict(oWB, OuterCacheability)
+call conflict(oWT, OuterCacheability)
+call conflict(oNC, OuterCacheability)
 
-let PTENormal = try PTENormal with emptyset
-let PTETaggedNormal = try PTETaggedNormal with emptyset
+let TaggedNormal = try PTETaggedNormal with emptyset
+let Normal = try PTENormal with emptyset
 
 (*** Common attributes ***)
 let PTEXS = try PTEXS with emptyset
 
 (*** Sanity checks ***)
 
 (* Memory cannot be of type Normal and Device at the same time *)
-let MemoryType-conflict = PTENormal & PTEDevice
+let MemoryType-conflict = Normal & Device
 assert empty MemoryType-conflict as Invalid-Memory-Type
 
+(* Default Type *)
+let Normal = Normal | (TTD \ Device)
+(* Default Shareability *)
+let ISH = ISH | (TTD \ (Device | NSH | OSH))
+(* Default Inner Cacheability *)
+let iWB = iWB | (TTD \ (Device | iWT | iNC))
+(* Default Outer Cacheability *)
+let oWB = oWB | (TTD \ (Device | oWT | oNC))
+
 (* No other memory attribute is allowed *)
 let PTEMemAttr = try PTEMemAttr with emptyset
-let PTEAll-Valid-Mem-Attr = PTENormal | PTETaggedNormal
-                    | PTENon-shareable | PTEInner-shareable | PTEOuter-shareable
-                    | PTEInner-write-back | PTEInner-write-through | PTEInner-non-cacheable
-                    | PTEOuter-write-back | PTEOuter-write-through | PTEOuter-non-cacheable
-                    | PTEDevice
-                    | PTEDevice-GRE | PTEDevice-nGRE | PTEDevice-nGnRE | PTEDevice-nGnRnE | PTEXS
-let Invalid-Memory-Attr = PTEMemAttr \ (PTEAll-Valid-Mem-Attr)
+let Invalid-Memory-Attr = PTEMemAttr \ (Normal | Device)
 assert empty Invalid-Memory-Attr as Invalid-Memory-Attribute
 
-(* Default Shareability *)
-let PTEInner-shareable = PTEInner-shareable
-                       | (PTE \ (PTEDevice | PTENon-shareable | PTEOuter-shareable))
-
-(* Default Inner Cacheability *)
-let PTEInner-write-back = PTEInner-write-back
-                        | (PTE \ (PTEDevice | PTEInner-write-through | PTEInner-non-cacheable))
 
-(* Default Outer Cacheability *)
-let PTEOuter-write-back = PTEOuter-write-back
-                        | (PTE \ (PTEDevice | PTEOuter-write-through | PTEOuter-non-cacheable))
-
-let ISH-WB = PTEInner-shareable & PTEInner-write-back & PTEOuter-write-back
-
-(* Default Memory Type *)
-let PTETaggedNormal = PTETaggedNormal | (if "memtag" then ISH-WB else 0)
-let PTENormal = PTENormal
-              | PTENon-shareable | PTEInner-shareable | PTEOuter-shareable
-              | PTEInner-write-back | PTEInner-write-through | PTEInner-non-cacheable
-              | PTEOuter-write-back | PTEOuter-write-through | PTEOuter-non-cacheable
-let PTENormal = if "memtag" then PTENormal \ ISH-WB else PTENormal

herd/tests/instructions/AArch64.vmsa+mte/A003.litmus.expected

@@ -7,5 +7,5 @@ Positive: 1 Negative: 0
 Flag combining-vmsa-and-memtag-is-not-supported
 Condition forall ([x]=0 /\ fault(P0:L0,x,MMU:Permission))
 Observation A003 Always 1 0
-Hash=e7bf1b4fe19ba1d138df90036a21cbe5
+Hash=3efe96b98430c90f13fcf80595d0338d
 

herd/tests/instructions/AArch64.vmsa+mte/A006.litmus.expected

@@ -7,5 +7,5 @@ Positive: 1 Negative: 0
 Flag combining-vmsa-and-memtag-is-not-supported
 Condition forall ([x]=1)
 Observation A006 Always 1 0
-Hash=7a7266deb5d908ed212b3f3d1182f155
+Hash=a97413e5a5b2e88d218e1808ba12a173
 

herd/tests/instructions/AArch64.vmsa+mte/A010.litmus.expected

@@ -7,5 +7,5 @@ Positive: 1 Negative: 0
 Flag combining-vmsa-and-memtag-is-not-supported
 Condition forall (0:X1=1 /\ not (fault(P0:L0,x,TagCheck)))
 Observation A010 Always 1 0
-Hash=f1f7d09e33e99c0f6d5214cf37835072
+Hash=210f090ffc7d7deff803b031d0c7feaa
 

herd/tests/instructions/AArch64.vmsa+mte/A011.litmus.expected

@@ -9,5 +9,5 @@ Positive: 1 Negative: 2
 Flag combining-vmsa-and-memtag-is-not-supported
 Condition exists ([x]=1 /\ not (fault(P0:L0,x)))
 Observation A011 Sometimes 1 2
-Hash=134d988c72472374b559eaf4c6a4fea8
+Hash=26408ab5c44db94a873ce79b4367a3c4
 

herd/tests/instructions/AArch64.vmsa+mte/A012.litmus.expected

@@ -9,5 +9,5 @@ Positive: 1 Negative: 2
 Flag combining-vmsa-and-memtag-is-not-supported
 Condition exists ([x]=1 /\ not (fault(P0:L0,x)))
 Observation A012 Sometimes 1 2
-Hash=3fce4d56177b06c14bfd934326a0645b
+Hash=9592a0d1b0a4d3eb48961b300a635e90
 

herd/tests/instructions/AArch64.vmsa+mte/A015.litmus.expected

@@ -7,5 +7,5 @@ Positive: 0 Negative: 3
 Flag combining-vmsa-and-memtag-is-not-supported
 Condition exists ([x]=1)
 Observation A014 Never 0 3
-Hash=7241fe036f5d711341ead6574ec6f446
+Hash=42905b4f8e0e4bbaf9d2c9905134fcde
 

lib/AArch64Op.ml

@@ -95,7 +95,7 @@ module
 
     let getel0 = op_get_pteval (fun p -> p.el0 <> 0)
 
-    let gettagged = op_get_pteval (fun p -> Attrs.mem "TaggedNormal" p.attrs)
+    let gettagged = op_get_pteval (fun p -> Attrs.is_tagged p.attrs)
 
     let getoa v =
       let open Constant in