herd: Update aarch64.cat to align with the ARMv8 memory model

Revision B.a of the ARMv8 Architecture Reference Manual revises the
memory model to be "other-multi-copy-atomic" and describes this in an
axiomatic fashion.

This patch updates aarch64.cat to align closely with the published
memory model from ARM.

Signed-off-by: Will Deacon <will.deacon@arm.com>

LICENSE.txt

@@ -1,3 +1,11 @@
+NOTE
+
+This license applies to all files in the distribution, except as stated
+below:
+
+* The file herd/libdir/aarch64.cat, which is courtesy of ARM Ltd.
+
+----------------------------------------
 
 CeCILL-B FREE SOFTWARE LICENSE AGREEMENT
 

herd/libdir/aarch64.cat

@@ -1,74 +1,118 @@
-"AArch64"
-
+(*
+ * The ARMv8 Application Level Memory Model.
+ *
+ * See section B2.3 of the ARMv8 ARM:
+ *   https://developer.arm.com/docs/ddi0487/latest/arm-architecture-reference-manual-armv8-for-armv8-a-architecture-profile
+ *
+ * Author: Will Deacon <will.deacon@arm.com>
+ *
+ * Copyright (C) 2016, ARM Ltd.
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in
+ *       the documentation and/or other materials provided with the
+ *       distribution.
+ *     * Neither the name of ARM nor the names of its contributors may be
+ *       used to endorse or promote products derived from this software
+ *       without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+ * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+ * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+ * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED
+ * TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+"ARMv8 AArch64"
+
+(*
+ * Include the cos.cat file shipped with herd.
+ * This builds the co relation as a total order over writes to the same
+ * location and then consequently defines the fr relation using co and
+ * rf.
+ *)
 include "cos.cat"
 
-(* Uniproc *)
-acyclic po-loc | rf | fr | co as uniproc
-
-(* Utilities *)
-let dd = addr | data
-let rdw = po-loc & (fre;rfe)
-let detour = po-loc & (coe ; rfe)
-let addrpo = addr;po
-let com = fr | co | rf
-
-empty rmw & (fre;coe) as atomic
-
+(*
+ * Include aarch64fences.cat so that barriers show up in generated diagrams.
+ *)
 include "aarch64fences.cat"
 
-let ci0 = ctrlisb | detour
-let ii0 = dd | rfi | rdw
-let cc0 = dd | ctrl | addrpo
-let ic0 = 0
-
-include "ppo.cat"
-
-let acq = (A * M) & po
-let rel = (M * L) & po
-
-let ppo = ppo | acq
-
-let fence = dmb.sy & (M * M)
-	    | dsb.sy & (M * M)
-	    | dmb.st & (W * W)
-	    | dsb.st & (W * W)
-	    | dmb.ld & (R * M)
-	    | dsb.ld & (R * M)
-
-let hb = (R * M) & fence | rfe | ppo
-
-acyclic hb as thin_air
-
-(* Prop is more complex... *)
-
-let B = hb*
-
-let prop =
-  com+;(dmb.sy|dsb.sy);B // Strongest fence, no big deal
-| coe;((dmb.st|dsb.st)&(W*W));B
-| (rfe|coe|(co;rfe))?;rel
-| fence;B
-
-
-
-let come = com & ext
-
-let observer =
-  rfe;(ppo|fence);come
-| come;((L*A&po)|dmb.sy);come
-| coe;(rfe;(dmb.sy));come
-| come;rel;come
-| coe;(rfe;rel);come
-| come;fence;come
-
-let OBS = prop+;observer
-irreflexive OBS as observation
-
-let prop_al = (L * A) & (rf | po)
-	    | (A * L) & fr
-            | (L * L) & co
-
-let xx = (W * W) & (X * X) & po
-
-
-acyclic prop | (co & (X * X)) | xx | (prop_al;hb*) as propagation
+(*
+ * As a restriction of the model, all observers are limited to the same
+ * inner-shareable domain. Consequently, the ISH, OSH and SY barrier
+ * options are all equivalent to each other.
+ *)
+let dsb.full = DSB.ISH | DSB.OSH | DSB.SY
+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.
+ *)
+let dmb.full = DMB.ISH | DMB.OSH | DMB.SY | dsb.full
+let dmb.ld = DMB.ISHLD | DMB.OSHLD | DMB.LD | dsb.ld
+let dmb.st = DMB.ISHST | DMB.OSHST | DMB.ST | dsb.st
+
+(* Flag any use of shareability options, due to the restrictions above. *)
+flag ~empty (dmb.full | dmb.ld | dmb.st) \
+	    (DMB.SY | DMB.LD | DMB.ST | DSB.SY | DSB.LD | DSB.ST)
+	    as Assuming-common-inner-shareable-domain
+
+(* Coherence-after *)
+let ca = fr | co
+
+(* Observed-by *)
+let obs = rfe | fre | coe
+
+(* Dependency-ordered-before *)
+let dob = addr | data
+	| ctrl; [W]
+	| (ctrl | (addr; po)); [ISB]; po; [R]
+	| addr; po; [W]
+	| (ctrl | data); coi
+	| (addr | data); rfi
+
+(* Atomic-ordered-before *)
+let aob = rmw
+	| rmw; rfi
+
+(* Barrier-ordered-before *)
+let bob = po; [dmb.full]; po
+	| [L]; po; [A]
+	| [R]; po; [dmb.ld]; po
+	| [A | Q]; po
+	| [W]; po; [dmb.st]; po; [W]
+	| po; [L]
+	| po; [L]; coi
+
+(* Ordered-before *)
+let rec ob = obs
+	| dob
+	| aob
+	| bob
+	| ob; ob
+
+(* Internal visibility requirement *)
+acyclic po-loc | ca | rf as internal
+
+(* External visibility requirement *)
+irreflexive ob as external
+
+(* Atomic: Basic LDXR/STXR constraint to forbid intervening writes. *)
+empty rmw & (fre; coe) as atomic