From de4d82aa3558fef911878a113eac105b5e980023 Mon Sep 17 00:00:00 2001
From: Thomas Haas <tomy.haas@t-online.de>
Date: Thu, 12 Feb 2026 16:38:42 +0100
Subject: [PATCH 01/17] Update aarch64.cat

---
 cat/aarch64.cat | 32 ++++++++++++++++++--------------
 1 file changed, 18 insertions(+), 14 deletions(-)

diff --git a/cat/aarch64.cat b/cat/aarch64.cat
index f5944bad5a..9f5d35c545 100644
--- a/cat/aarch64.cat
+++ b/cat/aarch64.cat
@@ -65,8 +65,8 @@ 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
+        (DMB.SY | DMB.LD | DMB.ST | DSB.SY | DSB.LD | DSB.ST)
+        as Assuming-common-inner-shareable-domain
 *)
 
 (* Coherence-after *)
@@ -83,29 +83,33 @@ let obs = rfe | fre | coe
 
 (* Dependency-ordered-before *)
 let dob = (addr | data)
-	| ctrl; [W]
-	| (ctrl | (addr; po)); [ISB]; po; [R]
-	| addr; po; [W]
-	| (addr | data); lrs
+    | ctrl; [W]
+    | (ctrl | (addr; po)); [ISB]; po; [R]
+    | addr; po; [W]
+    | (addr | data); lrs
 
 (* Atomic-ordered-before *)
 let aob = rmw
-	| [range(rmw)]; lrs; [A | Q]
+    | [range(rmw)]; lrs; [A | Q]
 
 (* Barrier-ordered-before *)
 let bob = po; [dmb.full]; po
-	| po; ([A];amo;[L]); po
-	| [L]; po; [A]
-	| [R]; po; [dmb.ld]; po
-	| [A | Q]; po
-	| [W]; po; [dmb.st]; po; [W]
-	| po; [L]
+    | po; ([A];amo;[L]); po
+    | [L]; po; [A]
+    | [R \ NoRet]; po; [dmb.ld]; po
+    | [A | Q]; po
+    | [W]; po; [dmb.st]; po; [W]
+    | po; [L]
 
 (* Locally-ordered-before *)
 let lob = lws; si | dob | aob | bob
 
+(** Hazard-ordered-before **)
+let haz-ob =
+  [R]; (po & loc); [R]; si?; [R]; (ca & ext); [W]; si?; [W]
+
 (* Ordered-before *)
-let ob = obs; si | lob
+let ob = obs; si | lob | haz-ob
 
 (* Internal visibility requirement *)
 acyclic po-loc | ca | rf as internal

From c1b02c4230b6c534361685a0bf6e45b529c25d93 Mon Sep 17 00:00:00 2001
From: Thomas Haas <tomy.haas@t-online.de>
Date: Thu, 12 Feb 2026 16:38:59 +0100
Subject: [PATCH 02/17] Add Armv8.NoRet tag to Loads into zero registers

---
 .../parsers/program/utils/ProgramBuilder.java | 34 ++++++++++++-------
 .../dat3m/dartagnan/program/event/Tag.java    |  1 +
 .../processing/compilation/VisitorArm8.java   |  9 ++++-
 3 files changed, 30 insertions(+), 14 deletions(-)

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java
index 880eb08671..088d5ca9a7 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java
@@ -9,11 +9,12 @@
 import com.dat3m.dartagnan.expression.type.FunctionType;
 import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.program.*;
-import com.dat3m.dartagnan.program.Thread;
 import com.dat3m.dartagnan.program.Program.SourceLanguage;
+import com.dat3m.dartagnan.program.Thread;
 import com.dat3m.dartagnan.program.event.Event;
 import com.dat3m.dartagnan.program.event.EventFactory;
 import com.dat3m.dartagnan.program.event.RegWriter;
+import com.dat3m.dartagnan.program.event.Tag;
 import com.dat3m.dartagnan.program.event.core.Label;
 import com.dat3m.dartagnan.program.event.core.threading.ThreadStart;
 import com.dat3m.dartagnan.program.event.metadata.OriginalId;
@@ -93,21 +94,28 @@ public static void processAfterParsing(Program program) {
 
     public static void replaceZeroRegisters(Program program, List<String> zeroRegNames) {
         for (Function func : Iterables.concat(program.getThreads(), program.getFunctions())) {
-            if (func.hasBody()) {
-                for (String zeroRegName : zeroRegNames) {
-                    Register zr = func.getRegister(zeroRegName);
-                    if (zr != null) {
-                        for (RegWriter rw : func.getEvents(RegWriter.class)) {
-                            if (rw.getResultRegister().equals(zr)) {
-                                Register dummy = rw.getThread().getOrNewRegister("__zeroRegDummy_" + zr.getName(), zr.getType());
-                                rw.setResultRegister(dummy);
-                            }
+            if (!func.hasBody()) {
+                continue;
+            }
+
+            for (String zeroRegName : zeroRegNames) {
+                Register zr = func.getRegister(zeroRegName);
+                if (zr == null) {
+                    continue;
+                }
+
+                for (RegWriter rw : func.getEvents(RegWriter.class)) {
+                    if (rw.getResultRegister().equals(zr)) {
+                        Register dummy = rw.getThread().getOrNewRegister("__zeroRegDummy_" + zr.getName(), zr.getType());
+                        rw.setResultRegister(dummy);
+                        if (rw.hasTag(Tag.VISIBLE)) {
+                            rw.addTags(Tag.ARMv8.NO_RET);
                         }
-                        // This comes after the loop to avoid the renaming in the initialization event
-                        Event initToZero = EventFactory.newLocal(zr, expressions.makeGeneralZero(zr.getType()));
-                        func.getEntry().insertAfter(initToZero);
                     }
                 }
+                // This comes after the loop to avoid the renaming in the initialization event
+                Event initToZero = EventFactory.newLocal(zr, expressions.makeGeneralZero(zr.getType()));
+                func.getEntry().insertAfter(initToZero);
             }
         }
     }
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java
index 3f194e8dff..825c8e4642 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java
@@ -51,6 +51,7 @@ private ARMv8() {
         public static final String MO_REL       = "L";
         public static final String MO_ACQ       = "A";
         public static final String MO_ACQ_PC    = "Q";
+        public static final String NO_RET       = "NoRet";
 
         public static String extractStoreMoFromCMo(String cMo) {
             return cMo.equals(C11.MO_SC) || cMo.equals(C11.MO_RELEASE) || cMo.equals(C11.MO_ACQUIRE_RELEASE) ? MO_REL : "";
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java
index f1603c7fd0..bbced2b57c 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java
@@ -50,11 +50,18 @@ public List<Event> visitXchg(Xchg xchg) {
         String storeMo = xchg.hasTag(ARMv8.MO_REL) ? ARMv8.MO_REL : "";
 
         return eventSequence(
-                newRMWLoadExclusiveWithMo(resultRegister, address, loadMo),
+                propagateNoRet(xchg, newRMWLoadExclusiveWithMo(resultRegister, address, loadMo)),
                 newRMWStoreExclusiveWithMo(address, xchg.getValue(), true, storeMo)
         );
     }
 
+    private <T extends Load> T propagateNoRet(Event orig, T newEv) {
+        if (orig.hasTag(ARMv8.NO_RET)) {
+            newEv.addTags(Tag.ARMv8.NO_RET);
+        }
+        return newEv;
+    }
+
     // =============================================================================================
     // =========================================== LLVM ============================================
     // =============================================================================================

From 4632428d777f11229900e6ba05f5f4bba906e933 Mon Sep 17 00:00:00 2001
From: Thomas Haas <tomy.haas@t-online.de>
Date: Thu, 12 Feb 2026 17:10:42 +0100
Subject: [PATCH 03/17] Move NoRet annotation code into right place (AARCH64
 visitor rather than generic ProgramBuilder). Remove A/Q tags from Loads into
 zero regs (XZR/WZR)

---
 .../parsers/program/utils/ProgramBuilder.java    |  4 ----
 .../program/visitors/VisitorLitmusAArch64.java   | 16 +++++++++++++++-
 2 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java
index 088d5ca9a7..195bc738fc 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java
@@ -14,7 +14,6 @@
 import com.dat3m.dartagnan.program.event.Event;
 import com.dat3m.dartagnan.program.event.EventFactory;
 import com.dat3m.dartagnan.program.event.RegWriter;
-import com.dat3m.dartagnan.program.event.Tag;
 import com.dat3m.dartagnan.program.event.core.Label;
 import com.dat3m.dartagnan.program.event.core.threading.ThreadStart;
 import com.dat3m.dartagnan.program.event.metadata.OriginalId;
@@ -108,9 +107,6 @@ public static void replaceZeroRegisters(Program program, List<String> zeroRegNam
                     if (rw.getResultRegister().equals(zr)) {
                         Register dummy = rw.getThread().getOrNewRegister("__zeroRegDummy_" + zr.getName(), zr.getType());
                         rw.setResultRegister(dummy);
-                        if (rw.hasTag(Tag.VISIBLE)) {
-                            rw.addTags(Tag.ARMv8.NO_RET);
-                        }
                     }
                 }
                 // This comes after the loop to avoid the renaming in the initialization event
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
index 3f743fee51..f39e7e8b7c 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
@@ -14,6 +14,8 @@
 import com.dat3m.dartagnan.program.Register;
 import com.dat3m.dartagnan.program.event.Event;
 import com.dat3m.dartagnan.program.event.EventFactory;
+import com.dat3m.dartagnan.program.event.MemoryEvent;
+import com.dat3m.dartagnan.program.event.RegWriter;
 import com.dat3m.dartagnan.program.event.arch.Xchg;
 import com.dat3m.dartagnan.program.event.core.Label;
 import com.dat3m.dartagnan.program.event.metadata.CustomPrinting;
@@ -55,10 +57,22 @@ public Object visitMain(MainContext ctx) {
         visitInstructionList(ctx.program().instructionList());
         VisitorLitmusAssertions.parseAssertions(programBuilder, ctx.assertionList(), ctx.assertionFilter());
         Program prog = programBuilder.build();
-        replaceZeroRegisters(prog, Arrays.asList("XZR", "WZR"));
+
+        final List<String> zeroRegs = Arrays.asList("XZR", "WZR");
+        markLoadsIntoZeroRegisters(prog, zeroRegs);
+        replaceZeroRegisters(prog, zeroRegs);
         return prog;
     }
 
+    private void markLoadsIntoZeroRegisters(Program prog, List<String> zeroRegs) {
+        for (MemoryEvent memEvent : prog.getThreadEvents(MemoryEvent.class)) {
+            if (memEvent instanceof RegWriter writer && zeroRegs.contains(writer.getResultRegister().getName())) {
+                memEvent.addTags(NO_RET);
+                memEvent.removeTags(MO_ACQ, MO_ACQ_PC);
+            }
+        }
+    }
+
     // ----------------------------------------------------------------------------------------------------------------
     // Variable declarator list, e.g., { 0:EAX=0; 1:EAX=1; x=2; }
 

From 46c55c16d28516109b5bc3db7393d84a40754bbf Mon Sep 17 00:00:00 2001
From: Thomas Haas <tomy.haas@t-online.de>
Date: Thu, 12 Feb 2026 18:12:50 +0100
Subject: [PATCH 04/17] Add new AARCH64 litmus tests: some are disabled due to
 missing grammar/parser support

---
 dartagnan/src/test/resources/ARM8-expected.csv  | 17 +++++++++++++++++
 .../AARCH64/NoRet/MP+rel+CAS-ok-dmb.ld.litmus   | 13 +++++++++++++
 .../AARCH64/NoRet/MP+rel+CASacq-noret-ok.litmus | 12 ++++++++++++
 litmus/AARCH64/NoRet/MP+rel+CASacq-ok.litmus    | 12 ++++++++++++
 .../NoRet/MP+rel+CASnoret-ok-dmb.ld.litmus      | 12 ++++++++++++
 litmus/AARCH64/NoRet/MP+rel+LDADD-dmb.ld.litmus | 12 ++++++++++++
 .../NoRet/MP+rel+LDADDnoret-dmb.ld.litmus       | 11 +++++++++++
 litmus/AARCH64/NoRet/MP+rel+SWP-dmb.ld.litmus   | 12 ++++++++++++
 litmus/AARCH64/NoRet/MP+rel+SWPacq-noret.litmus | 12 ++++++++++++
 litmus/AARCH64/NoRet/MP+rel+SWPacq.litmus       | 12 ++++++++++++
 .../AARCH64/NoRet/MP+rel+SWPnoret-dmb.ld.litmus | 12 ++++++++++++
 .../mixed/CoRR+amo.swph0h0-posh0a.w0+w0.litmus  | 14 ++++++++++++++
 .../mixed/CoRR+rmwh0h0-posh0a.w0+w0.litmus      | 15 +++++++++++++++
 13 files changed, 166 insertions(+)
 create mode 100644 litmus/AARCH64/NoRet/MP+rel+CAS-ok-dmb.ld.litmus
 create mode 100644 litmus/AARCH64/NoRet/MP+rel+CASacq-noret-ok.litmus
 create mode 100644 litmus/AARCH64/NoRet/MP+rel+CASacq-ok.litmus
 create mode 100644 litmus/AARCH64/NoRet/MP+rel+CASnoret-ok-dmb.ld.litmus
 create mode 100644 litmus/AARCH64/NoRet/MP+rel+LDADD-dmb.ld.litmus
 create mode 100644 litmus/AARCH64/NoRet/MP+rel+LDADDnoret-dmb.ld.litmus
 create mode 100644 litmus/AARCH64/NoRet/MP+rel+SWP-dmb.ld.litmus
 create mode 100644 litmus/AARCH64/NoRet/MP+rel+SWPacq-noret.litmus
 create mode 100644 litmus/AARCH64/NoRet/MP+rel+SWPacq.litmus
 create mode 100644 litmus/AARCH64/NoRet/MP+rel+SWPnoret-dmb.ld.litmus
 create mode 100644 litmus/AARCH64/mixed/CoRR+amo.swph0h0-posh0a.w0+w0.litmus
 create mode 100644 litmus/AARCH64/mixed/CoRR+rmwh0h0-posh0a.w0+w0.litmus

diff --git a/dartagnan/src/test/resources/ARM8-expected.csv b/dartagnan/src/test/resources/ARM8-expected.csv
index 604a66cb13..a687755a8f 100644
--- a/dartagnan/src/test/resources/ARM8-expected.csv
+++ b/dartagnan/src/test/resources/ARM8-expected.csv
@@ -7863,3 +7863,20 @@ litmus/AARCH64/mixed/WW+R+dmb.sysw4w0+q0+BIS.litmus,0
 litmus/AARCH64/mixed/WW+R+dmb.sysw4w0+q0.litmus,0
 litmus/AARCH64/mixed/WW+R+posq0w0+q0+SIMPLE.litmus,0
 litmus/AARCH64/mixed/WW+RR-variant.litmus,0
+litmus/AARCH64/mixed/WW+RR-variant.litmus,0
+litmus/AARCH64/mixed/WW+RR-variant.litmus,0
+litmus/AARCH64/mixed/CoRR+amo.swph0h0-posh0a.w0+w0.litmus,0
+litmus/AARCH64/mixed/CoRR+rmwh0h0-posh0a.w0+w0.litmus,0
+
+// Not yet supported due to grammar/parser limitations
+//litmus/AARCH64/NoRet/MP+rel+CAS-ok-dmb.ld.litmus,0
+//litmus/AARCH64/NoRet/MP+rel+CASnoret-ok-dmb.ld.litmus,1
+//litmus/AARCH64/NoRet/MP+rel+CASacq-noret-ok.litmus,1
+//litmus/AARCH64/NoRet/MP+rel+CASacq-ok.litmus,0
+//litmus/AARCH64/NoRet/MP+rel+LDADD-dmb.ld.litmus,0
+//litmus/AARCH64/NoRet/MP+rel+LDADDnoret-dmb.ld.litmus,1
+
+litmus/AARCH64/NoRet/MP+rel+SWPacq.litmus,0
+litmus/AARCH64/NoRet/MP+rel+SWPacq-noret.litmus,1
+litmus/AARCH64/NoRet/MP+rel+SWP-dmb.ld.litmus,0
+litmus/AARCH64/NoRet/MP+rel+SWPnoret-dmb.ld.litmus,1
\ No newline at end of file
diff --git a/litmus/AARCH64/NoRet/MP+rel+CAS-ok-dmb.ld.litmus b/litmus/AARCH64/NoRet/MP+rel+CAS-ok-dmb.ld.litmus
new file mode 100644
index 0000000000..edcee99c0c
--- /dev/null
+++ b/litmus/AARCH64/NoRet/MP+rel+CAS-ok-dmb.ld.litmus
@@ -0,0 +1,13 @@
+AArch64 MP+rel+CAS-ok-dmb.ld
+{
+ y=2;
+ 0:X1=x; 0:X3=y;
+ 1:X1=x; 1:X3=y;
+}
+ P0           | P1             ;
+ MOV W0,#1    | MOV W4,#1      ;
+ STR W0,[X1]  | MOV W2,#0      ;
+ MOV W2,#0    | CAS W2,W4,[X3] ;
+ STLR W2,[X3] | DMB LD         ;
+              | LDR W0,[X1]    ;
+exists (y=1 /\ 1:X0=0)
diff --git a/litmus/AARCH64/NoRet/MP+rel+CASacq-noret-ok.litmus b/litmus/AARCH64/NoRet/MP+rel+CASacq-noret-ok.litmus
new file mode 100644
index 0000000000..2a19c199d9
--- /dev/null
+++ b/litmus/AARCH64/NoRet/MP+rel+CASacq-noret-ok.litmus
@@ -0,0 +1,12 @@
+AArch64 MP+rel+CASacq-noret-ok
+{
+ y=2;
+ 0:X1=x; 0:X3=y;
+ 1:X1=x; 1:X3=y;
+}
+ P0           | P1                ;
+ MOV W0,#1    | MOV W4,#1         ;
+ STR W0,[X1]  | CASA WZR,W4,[X3]  ;
+ MOV W2,#0    | LDR W0,[X1]       ;
+ STLR W2,[X3] |                   ;
+exists (y=1 /\ 1:X0=0)
diff --git a/litmus/AARCH64/NoRet/MP+rel+CASacq-ok.litmus b/litmus/AARCH64/NoRet/MP+rel+CASacq-ok.litmus
new file mode 100644
index 0000000000..2626620342
--- /dev/null
+++ b/litmus/AARCH64/NoRet/MP+rel+CASacq-ok.litmus
@@ -0,0 +1,12 @@
+AArch64 MP+rel+CASacq-ok
+{
+ y=2;
+ 0:X1=x; 0:X3=y;
+ 1:X1=x; 1:X3=y;
+}
+ P0           | P1               ;
+ MOV W0,#1    | MOV W4,#1        ;
+ STR W0,[X1]  | MOV W2,#0        ;
+ MOV W2,#0    | CASA W2,W4,[X3]  ;
+ STLR W2,[X3] | LDR W0,[X1]      ;
+exists (y=1 /\ 1:X0=0)
diff --git a/litmus/AARCH64/NoRet/MP+rel+CASnoret-ok-dmb.ld.litmus b/litmus/AARCH64/NoRet/MP+rel+CASnoret-ok-dmb.ld.litmus
new file mode 100644
index 0000000000..4038d75332
--- /dev/null
+++ b/litmus/AARCH64/NoRet/MP+rel+CASnoret-ok-dmb.ld.litmus
@@ -0,0 +1,12 @@
+AArch64 MP+rel+CASnoret-ok-dmb.ld
+{
+ y=2;
+ 0:X1=x; 0:X3=y;
+ 1:X1=x; 1:X3=y;
+}
+ P0           | P1              ;
+ MOV W0,#1    | MOV W4,#1       ;
+ STR W0,[X1]  | CAS WZR,W4,[X3] ;
+ MOV W2,#0    | DMB LD          ;
+ STLR W2,[X3] | LDR W0,[X1]     ;
+exists (y=1 /\ 1:X0=0)
diff --git a/litmus/AARCH64/NoRet/MP+rel+LDADD-dmb.ld.litmus b/litmus/AARCH64/NoRet/MP+rel+LDADD-dmb.ld.litmus
new file mode 100644
index 0000000000..34a9f6d0e7
--- /dev/null
+++ b/litmus/AARCH64/NoRet/MP+rel+LDADD-dmb.ld.litmus
@@ -0,0 +1,12 @@
+AArch64 MP+rel+LDADD-dmb.ld
+{
+ z=0;
+ 0:X1=x; 0:X3=y;
+ 1:X1=x; 1:X3=y; 1:X6=z;
+}
+ P0           | P1               ;
+ MOV W0,#1    | MOV W4,#1        ;
+ STR W0,[X1]  | LDADD W4,W2,[X3] ;
+ MOV W2,#1    | DMB LD           ;
+ STLR W2,[X3] | LDR W0,[X1]      ;
+exists (y=2 /\ 1:X0=0)
diff --git a/litmus/AARCH64/NoRet/MP+rel+LDADDnoret-dmb.ld.litmus b/litmus/AARCH64/NoRet/MP+rel+LDADDnoret-dmb.ld.litmus
new file mode 100644
index 0000000000..468431aad5
--- /dev/null
+++ b/litmus/AARCH64/NoRet/MP+rel+LDADDnoret-dmb.ld.litmus
@@ -0,0 +1,11 @@
+AArch64 MP+rel+LDADDnoret-dmb.ld
+{
+ 0:X1=x; 0:X3=y;
+ 1:X1=x; 1:X3=y;
+}
+ P0           | P1                ;
+ MOV W0,#1    | MOV W4,#1         ;
+ STR W0,[X1]  | LDADD W4,WZR,[X3] ;
+ MOV W2,#1    | DMB LD            ;
+ STLR W2,[X3] | LDR W0,[X1]       ;
+exists (y=2 /\ 1:X0=0)
diff --git a/litmus/AARCH64/NoRet/MP+rel+SWP-dmb.ld.litmus b/litmus/AARCH64/NoRet/MP+rel+SWP-dmb.ld.litmus
new file mode 100644
index 0000000000..fdaee81f64
--- /dev/null
+++ b/litmus/AARCH64/NoRet/MP+rel+SWP-dmb.ld.litmus
@@ -0,0 +1,12 @@
+AArch64 MP+rel+SWP-dmb.ld
+{
+ z=0;
+ 0:X1=x; 0:X3=y;
+ 1:X1=x; 1:X3=y; 1:X6=z;
+}
+ P0           | P1             ;
+ MOV W0,#1    | MOV W4,#2      ;
+ STR W0,[X1]  | SWP W4,W2,[X3] ;
+ MOV W2,#1    | DMB LD         ;
+ STLR W2,[X3] | LDR W0,[X1]    ;
+exists (y=2 /\ 1:X0=0)
diff --git a/litmus/AARCH64/NoRet/MP+rel+SWPacq-noret.litmus b/litmus/AARCH64/NoRet/MP+rel+SWPacq-noret.litmus
new file mode 100644
index 0000000000..56b2c8e33f
--- /dev/null
+++ b/litmus/AARCH64/NoRet/MP+rel+SWPacq-noret.litmus
@@ -0,0 +1,12 @@
+AArch64 MP+rel+SWPacq-noret
+{
+ z=0;
+ 0:X1=x; 0:X3=y;
+ 1:X1=x; 1:X3=y;
+}
+ P0           | P1               ;
+ MOV W0,#1    | MOV W4,#2        ;
+ STR W0,[X1]  | SWPA W4,WZR,[X3] ;
+ MOV W2,#1    | LDR W0,[X1]      ;
+ STLR W2,[X3] |                  ;
+exists (y=2 /\ 1:X0=0)
diff --git a/litmus/AARCH64/NoRet/MP+rel+SWPacq.litmus b/litmus/AARCH64/NoRet/MP+rel+SWPacq.litmus
new file mode 100644
index 0000000000..c80479d32b
--- /dev/null
+++ b/litmus/AARCH64/NoRet/MP+rel+SWPacq.litmus
@@ -0,0 +1,12 @@
+AArch64 MP+rel+SWPacq
+{
+ z=0;
+ 0:X1=x; 0:X3=y;
+ 1:X1=x; 1:X3=y; 1:X6=z;
+}
+ P0           | P1              ;
+ MOV W0,#1    | MOV W4,#2       ;
+ STR W0,[X1]  | SWPA W4,W2,[X3] ;
+ MOV W2,#1    | LDR W0,[X1]     ;
+ STLR W2,[X3] |                 ;
+exists (y=2 /\ 1:X0=0)
diff --git a/litmus/AARCH64/NoRet/MP+rel+SWPnoret-dmb.ld.litmus b/litmus/AARCH64/NoRet/MP+rel+SWPnoret-dmb.ld.litmus
new file mode 100644
index 0000000000..12e4cfe888
--- /dev/null
+++ b/litmus/AARCH64/NoRet/MP+rel+SWPnoret-dmb.ld.litmus
@@ -0,0 +1,12 @@
+AArch64 MP+rel+SWPnoret-dmb.ld
+{
+ z=0;
+ 0:X1=x; 0:X3=y;
+ 1:X1=x; 1:X3=y;
+}
+ P0           | P1              ;
+ MOV W0,#1    | MOV W4,#2       ;
+ STR W0,[X1]  | SWP W4,WZR,[X3] ;
+ MOV W2,#1    | DMB LD          ;
+ STLR W2,[X3] | LDR W0,[X1]     ;
+exists (y=2 /\ 1:X0=0)
diff --git a/litmus/AARCH64/mixed/CoRR+amo.swph0h0-posh0a.w0+w0.litmus b/litmus/AARCH64/mixed/CoRR+amo.swph0h0-posh0a.w0+w0.litmus
new file mode 100644
index 0000000000..ce88a41242
--- /dev/null
+++ b/litmus/AARCH64/mixed/CoRR+amo.swph0h0-posh0a.w0+w0.litmus
@@ -0,0 +1,14 @@
+AArch64 CoRR+amo.swph0h0-posh0a.w0+w0
+Variant=mixed
+{
+ uint32_t 0:X3; uint32_t 0:X2;
+ 0:X0=x;
+ uint32_t 1:X1=0xccddeeff; 1:X0=x;
+}
+ P0              | P1          ;
+ MOV W2,#42      | STR W1,[X0] ;
+ SWPH W2,W1,[X0] |             ;
+ LDAR W3,[X0]    |             ;
+exists (0:X1=0xeeff /\ 0:X3=42)
+
+(* Linux's qspinlock for systems without FEAT_LSE requires that this is forbidden *)
diff --git a/litmus/AARCH64/mixed/CoRR+rmwh0h0-posh0a.w0+w0.litmus b/litmus/AARCH64/mixed/CoRR+rmwh0h0-posh0a.w0+w0.litmus
new file mode 100644
index 0000000000..92395cd3e1
--- /dev/null
+++ b/litmus/AARCH64/mixed/CoRR+rmwh0h0-posh0a.w0+w0.litmus
@@ -0,0 +1,15 @@
+AArch64 CoRR+rmwh0h0-posh0a.w0+w0
+Variant=mixed
+{
+ uint32_t 0:X3; uint32_t 0:X2;
+ 0:X0=x;
+ uint32_t 1:X1=0xccddeeff; 1:X0=x;
+}
+ P0               | P1          ;
+ MOV W2,#42       | STR W1,[X0] ;
+ LDXRH W1,[X0]    |             ;
+ STXRH W4,W2,[X0] |             ;
+ LDAR W3,[X0]     |             ;
+exists (0:X1=0xeeff /\ 0:X3=42 /\ 0:X4=0)
+
+(* Linux's qspinlock for systems without FEAT_LSE requires that this is forbidden *)

From 32f53ae35c4266bea9246ce8b5a744c38ba7db24 Mon Sep 17 00:00:00 2001
From: Thomas Haas <tomy.haas@t-online.de>
Date: Thu, 12 Feb 2026 18:15:38 +0100
Subject: [PATCH 05/17] Updated expected value of store-to-load-forwarding1.c
 (PASS on new aarch64.cat version)

---
 benchmarks/mixed/store-to-load-forwarding1.c                    | 2 +-
 dartagnan/src/test/java/com/dat3m/dartagnan/llvm/MixedTest.java | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/benchmarks/mixed/store-to-load-forwarding1.c b/benchmarks/mixed/store-to-load-forwarding1.c
index f7700bae39..4cf7dd017f 100644
--- a/benchmarks/mixed/store-to-load-forwarding1.c
+++ b/benchmarks/mixed/store-to-load-forwarding1.c
@@ -2,7 +2,7 @@
 #include <stdatomic.h>
 #include <assert.h>
 // Issue: Store-to-Load Forwarding may cause mixed-size atomic accesses to appear non-atomic.
-// Expected: FAIL on ARMv8
+// Expected: PASS on ARMv8 (FAIL on older, unpatched version of ARMv8)
 
 union { atomic_ushort full; struct { atomic_uchar half0; atomic_uchar half1; }; } lock;
 
diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/llvm/MixedTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/llvm/MixedTest.java
index f56693a775..e9c465887b 100644
--- a/dartagnan/src/test/java/com/dat3m/dartagnan/llvm/MixedTest.java
+++ b/dartagnan/src/test/java/com/dat3m/dartagnan/llvm/MixedTest.java
@@ -66,7 +66,7 @@ public static Iterable<Object[]> data() throws IOException {
             {"memtrack3-pass", ARM8, PASS},
             {"mixed-local1", ARM8, PASS},
             {"mixed-local2", ARM8, FAIL},
-            {"store-to-load-forwarding1", ARM8, FAIL},
+            {"store-to-load-forwarding1", ARM8, PASS}, // FAIL on the older version of aarch64.cat
             {"floats_msa_1", ARM8, PASS},
             {"floats_msa_2", ARM8, PASS},
         });

From 59aa61c9209b7651aed5d458b98130586bdc9163 Mon Sep 17 00:00:00 2001
From: Thomas Haas <tomy.haas@t-online.de>
Date: Thu, 12 Feb 2026 18:20:43 +0100
Subject: [PATCH 06/17] Add reference to aarch64 patch that changed behavior of
 a benchmark.

---
 benchmarks/mixed/store-to-load-forwarding1.c | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/benchmarks/mixed/store-to-load-forwarding1.c b/benchmarks/mixed/store-to-load-forwarding1.c
index 4cf7dd017f..d310441d66 100644
--- a/benchmarks/mixed/store-to-load-forwarding1.c
+++ b/benchmarks/mixed/store-to-load-forwarding1.c
@@ -2,7 +2,8 @@
 #include <stdatomic.h>
 #include <assert.h>
 // Issue: Store-to-Load Forwarding may cause mixed-size atomic accesses to appear non-atomic.
-// Expected: PASS on ARMv8 (FAIL on older, unpatched version of ARMv8)
+// Expected: PASS on ARMv8, but FAIL on older, unpatched version of ARMv8, see
+//           https://github.com/herd/herdtools7/commit/2b7921a
 
 union { atomic_ushort full; struct { atomic_uchar half0; atomic_uchar half1; }; } lock;
 

From 006dde01e4de368f45b1dd93a0cef302f63f140f Mon Sep 17 00:00:00 2001
From: Thomas Haas <tomy.haas@t-online.de>
Date: Thu, 12 Feb 2026 21:24:50 +0100
Subject: [PATCH 07/17] Add new CAS event common for hardware models Add
 support for AARCH64 CAS instructions

---
 dartagnan/src/main/antlr4/LitmusAArch64.g4    | 36 +++++++++++
 .../visitors/VisitorLitmusAArch64.java        | 61 ++++++++++++++++---
 .../dartagnan/program/event/EventFactory.java |  6 +-
 .../dartagnan/program/event/EventVisitor.java |  2 +
 .../dartagnan/program/event/arch/CAS.java     | 32 ++++++++++
 .../processing/compilation/VisitorArm8.java   | 44 +++++++++++++
 .../src/test/resources/ARM8-expected.csv      | 18 +++---
 7 files changed, 180 insertions(+), 19 deletions(-)
 create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/CAS.java

diff --git a/dartagnan/src/main/antlr4/LitmusAArch64.g4 b/dartagnan/src/main/antlr4/LitmusAArch64.g4
index 1c8f2d4710..aea606a508 100644
--- a/dartagnan/src/main/antlr4/LitmusAArch64.g4
+++ b/dartagnan/src/main/antlr4/LitmusAArch64.g4
@@ -64,6 +64,7 @@ instruction
     |   storePair
     |   storeExclusive
     |   swap
+    |   cas
     |   cmp
     |   branch
     |   branchRegister
@@ -123,6 +124,11 @@ swap
     |   swapInstruction rS64 = register64 Comma rD64 = register64 Comma LBracket address RBracket
     ;
 
+cas
+    :   casInstruction rS32 = register32 Comma rT32 = register32 Comma LBracket address RBracket
+    |   casInstruction rS64 = register64 Comma rT64 = register64 Comma LBracket address RBracket
+    ;
+
 fence locals [String opt]
     :   Fence {$opt = "SY";}
     |   Fence FenceOpt {$opt = $FenceOpt.text;}
@@ -200,6 +206,21 @@ swapInstruction locals [boolean acquire, boolean release, boolean byteSize, bool
     | SWPALH {$acquire = true; $release = true; $halfWordSize = true;}
     ;
 
+casInstruction locals [boolean acquire, boolean release, boolean byteSize, boolean halfWordSize]
+    : CAS
+    | CASB {$byteSize = true;}
+    | CASH {$halfWordSize = true;}
+    | CASA {$acquire = true;}
+    | CASAB {$acquire = true; $byteSize = true;}
+    | CASAH {$acquire = true; $halfWordSize = true;}
+    | CASL {$release = true;}
+    | CASLB {$release = true; $byteSize = true;}
+    | CASLH {$release = true; $halfWordSize = true;}
+    | CASAL {$acquire = true; $release = true;}
+    | CASALB {$acquire = true; $release = true; $byteSize = true;}
+    | CASALH {$acquire = true; $release = true; $halfWordSize = true;}
+    ;
+
 arithmeticInstruction locals [IntBinaryOp op]
     :   ADD     { $op = IntBinaryOp.ADD; }
 //    |   ADDS    { throw new RuntimeException("Instruction ADDS is not implemented"); }
@@ -396,6 +417,21 @@ SWPAL  :   'SWPAL'  ;
 SWPALB :   'SWPALB' ;
 SWPALH :   'SWPALH' ;
 
+// CAS instructions
+
+CAS    :   'CAS'    ;
+CASB   :   'CASB'   ;
+CASH   :   'CASH'   ;
+CASA   :   'CASA'   ;
+CASAB  :   'CASAB'  ;
+CASAH  :   'CASAH'  ;
+CASL   :   'CASL'   ;
+CASLB  :   'CASLB'  ;
+CASLH  :   'CASLH'  ;
+CASAL  :   'CASAL'  ;
+CASALB :   'CASALB' ;
+CASALH :   'CASALH' ;
+
 MovInstruction
     :   'MOV'
     ;
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
index f39e7e8b7c..d9a8781b3a 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
@@ -16,6 +16,7 @@
 import com.dat3m.dartagnan.program.event.EventFactory;
 import com.dat3m.dartagnan.program.event.MemoryEvent;
 import com.dat3m.dartagnan.program.event.RegWriter;
+import com.dat3m.dartagnan.program.event.arch.CAS;
 import com.dat3m.dartagnan.program.event.arch.Xchg;
 import com.dat3m.dartagnan.program.event.core.Label;
 import com.dat3m.dartagnan.program.event.metadata.CustomPrinting;
@@ -277,8 +278,6 @@ public Object visitStoreExclusive(StoreExclusiveContext ctx) {
         return Optional.of(String.format("SWP%s%s %s, %s, [%s]", acq, rel, value, loadReg, address));
     };
 
-    // FIXME: SWP into a zero register (WZR or XZR) acts like a store, in particular SWPA(L) does not give
-    //  acquire semantics then.
     @Override
     public Object visitSwap(SwapContext ctx) {
         final SwapInstructionContext inst = ctx.swapInstruction();
@@ -307,6 +306,48 @@ public Object visitSwap(SwapContext ctx) {
         return null;
     }
 
+    private static final CustomPrinting CAS_PRINTER = e -> {
+        if (!(e instanceof CAS cas)) {
+            return Optional.empty();
+        }
+        final String acq = e.hasTag(MO_ACQ) ? "A" : "";
+        final String rel = e.hasTag(MO_REL) ? "L" : "";
+        final Expression value = cas.getStoreValue();
+        final Register loadReg = cas.getResultRegister();
+        final Expression address = cas.getAddress();
+
+        return Optional.of(String.format("CAS%s%s %s, %s, [%s]", acq, rel, loadReg, value, address));
+    };
+
+    @Override
+    public Object visitCas(CasContext ctx) {
+        final CasInstructionContext inst = ctx.casInstruction();
+
+        final Register rs64 = parseRegister64(ctx.rS32, ctx.rS64);
+        final Register rt64 = parseRegister64(ctx.rT32, ctx.rT64);
+
+        final Register rs = shrinkRegister(rs64, ctx.rS32, inst.halfWordSize, inst.byteSize);
+        final Expression cmpVal = expressions.makeCast(rs64, rs.getType(), false);
+        final Expression val = expressions.makeCast(rt64, rs.getType(), false);
+        final Expression address = parseAddress(ctx.address());
+
+        final List<String> mo = new ArrayList<>();
+        if (inst.acquire) {
+            mo.add(MO_ACQ);
+        }
+        if (inst.release) {
+            mo.add(MO_REL);
+        }
+
+        final CAS cas = EventFactory.Common.newCAS(rs, address, cmpVal, val);
+        cas.addTags(mo);
+        cas.setMetadata(CAS_PRINTER);
+
+        add(cas);
+        addRegister64Update(rs64, rs);
+        return null;
+    }
+
 
     @Override
     public Object visitBranch(BranchContext ctx) {
@@ -442,16 +483,18 @@ private IntLiteral parseValue(ConstantContext ctx, IntegerType type) {
         return expressions.parseValue(ctx.getText(), type);
     }
 
-    private Register shrinkRegister(Register other, Register32Context ctx, boolean halfWordSize, boolean byteSize) {
-        checkArgument(other.getType().equals(i64), "Non-64-bit %s", other);
+    private Register shrinkRegister(Register r64, Register32Context ctx, boolean halfWordSize, boolean byteSize) {
+        checkArgument(r64.getType().equals(i64), "Non-64-bit %s", r64);
         checkArgument(!byteSize | !halfWordSize, "Inconclusive access size");
         if (byteSize) {
-            return programBuilder.getOrNewRegister(mainThread, "B" + other.getName().substring(1), i8);
-        }
-        if (halfWordSize) {
-            return programBuilder.getOrNewRegister(mainThread, "H" + other.getName().substring(1), i16);
+            return programBuilder.getOrNewRegister(mainThread, "B" + r64.getName().substring(1), i8);
+        } else if (halfWordSize) {
+            return programBuilder.getOrNewRegister(mainThread, "H" + r64.getName().substring(1), i16);
+        } else if (ctx != null) {
+            return programBuilder.getOrNewRegister(mainThread, "W" + r64.getName().substring(1), i32);
+        } else {
+            return r64;
         }
-        return ctx == null ? other : programBuilder.getOrNewRegister(mainThread, ctx.getText(), i32);
     }
 
     private void addRegister64Update(Register r64, Register value) {
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java
index 79b2b8ca5b..719611f6f4 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java
@@ -11,6 +11,7 @@
 import com.dat3m.dartagnan.program.Function;
 import com.dat3m.dartagnan.program.Register;
 import com.dat3m.dartagnan.program.Thread;
+import com.dat3m.dartagnan.program.event.arch.CAS;
 import com.dat3m.dartagnan.program.event.arch.StoreExclusive;
 import com.dat3m.dartagnan.program.event.arch.Xchg;
 import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomCAS;
@@ -25,7 +26,6 @@
 import com.dat3m.dartagnan.program.event.core.annotations.FunCallMarker;
 import com.dat3m.dartagnan.program.event.core.annotations.FunReturnMarker;
 import com.dat3m.dartagnan.program.event.core.annotations.StringAnnotation;
-import com.dat3m.dartagnan.program.event.core.InstructionBoundary;
 import com.dat3m.dartagnan.program.event.core.special.StateSnapshot;
 import com.dat3m.dartagnan.program.event.core.threading.*;
 import com.dat3m.dartagnan.program.event.functions.AbortIf;
@@ -403,6 +403,10 @@ public static StoreExclusive newExclusiveStore(Register register, Expression add
         public static Xchg newXchg(Register register, Expression address, Expression storeValue) {
             return new Xchg(register, address, storeValue);
         }
+
+        public static CAS newCAS(Register srcReg, Expression address, Expression cmpVal, Expression storeValue) {
+            return new CAS(srcReg, address, cmpVal, storeValue);
+        }
     }
 
     // =============================================================================================
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java
index 598a97dc3e..2dfafe40c3 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java
@@ -1,5 +1,6 @@
 package com.dat3m.dartagnan.program.event;
 
+import com.dat3m.dartagnan.program.event.arch.CAS;
 import com.dat3m.dartagnan.program.event.arch.StoreExclusive;
 import com.dat3m.dartagnan.program.event.arch.Xchg;
 import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomCAS;
@@ -54,6 +55,7 @@ public interface EventVisitor<T> {
     // ------------------ Common Events ------------------
     default T visitStoreExclusive(StoreExclusive e) { return visitMemEvent(e); }
     default T visitXchg(Xchg xchg) { return visitMemEvent(xchg); };
+    default T visitCas(CAS cas) { return visitMemEvent(cas); };
 
     // ------------------ Linux Events ------------------
     default T visitLKMMAddUnless(LKMMAddUnless e) { return visitMemEvent(e); }
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/CAS.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/CAS.java
new file mode 100644
index 0000000000..455f7bd73b
--- /dev/null
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/CAS.java
@@ -0,0 +1,32 @@
+package com.dat3m.dartagnan.program.event.arch;
+
+import com.dat3m.dartagnan.expression.Expression;
+import com.dat3m.dartagnan.program.Register;
+import com.dat3m.dartagnan.program.event.EventVisitor;
+import com.dat3m.dartagnan.program.event.common.RMWCmpXchgBase;
+
+public class CAS extends RMWCmpXchgBase {
+
+    public CAS(Register register, Expression address, Expression cmpVal, Expression value) {
+        super(register, address, cmpVal, value, true, "");
+    }
+
+    private CAS(CAS other){
+        super(other);
+    }
+
+    @Override
+    public String defaultString() {
+        return String.format("%s = cas(%s, %s)", resultRegister, address, storeValue);
+    }
+
+    @Override
+    public CAS getCopy(){
+        return new CAS(this);
+    }
+
+    @Override
+    public <T> T accept(EventVisitor<T> visitor) {
+        return visitor.visitCas(this);
+    }
+}
\ No newline at end of file
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java
index bbced2b57c..b832951328 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java
@@ -9,6 +9,7 @@
 import com.dat3m.dartagnan.program.event.Tag;
 import com.dat3m.dartagnan.program.event.Tag.ARMv8;
 import com.dat3m.dartagnan.program.event.Tag.C11;
+import com.dat3m.dartagnan.program.event.arch.CAS;
 import com.dat3m.dartagnan.program.event.arch.StoreExclusive;
 import com.dat3m.dartagnan.program.event.arch.Xchg;
 import com.dat3m.dartagnan.program.event.core.*;
@@ -55,6 +56,49 @@ public List<Event> visitXchg(Xchg xchg) {
         );
     }
 
+    @Override
+    public List<Event> visitCas(CAS cas) {
+        final Register resultRegister = cas.getResultRegister();
+        final Expression address = cas.getAddress();
+
+        final String loadMo = cas.hasTag(ARMv8.MO_ACQ) ? ARMv8.MO_ACQ : "";
+        final String storeMo = cas.hasTag(ARMv8.MO_REL) ? ARMv8.MO_REL : "";
+
+        Expression cmpValue = cas.getExpectedValue();
+        Local captureCmpVal = null;
+        if (cmpValue.getRegs().contains(resultRegister)) {
+            Register tmpReg = cas.getFunction().newRegister(resultRegister.getType());
+            captureCmpVal = newLocal(tmpReg, cmpValue);
+            cmpValue = tmpReg;
+        }
+
+        Expression newValue = cas.getStoreValue();
+        Local captureNewVal = null;
+        if (newValue.getRegs().contains(resultRegister)) {
+            Register tmpReg = cas.getFunction().newRegister(resultRegister.getType());
+            captureNewVal = newLocal(tmpReg, newValue);
+            newValue = tmpReg;
+        }
+
+        Label casEnd = newLabel("CAS_end");
+        final Expression cmp = expressions.makeEQ(resultRegister, cmpValue);
+        CondJump branchOnCasCmpResult = newJumpUnless(cmp, casEnd);
+
+        Load load = propagateNoRet(cas, newRMWLoadWithMo(resultRegister, address, loadMo));
+        Store store = newRMWStoreWithMo(load, address, newValue, storeMo);
+
+        return eventSequence(
+                captureCmpVal,
+                captureNewVal,
+                load,
+                branchOnCasCmpResult,
+                store,
+                casEnd
+        );
+
+
+    }
+
     private <T extends Load> T propagateNoRet(Event orig, T newEv) {
         if (orig.hasTag(ARMv8.NO_RET)) {
             newEv.addTags(Tag.ARMv8.NO_RET);
diff --git a/dartagnan/src/test/resources/ARM8-expected.csv b/dartagnan/src/test/resources/ARM8-expected.csv
index a687755a8f..277d70d3b6 100644
--- a/dartagnan/src/test/resources/ARM8-expected.csv
+++ b/dartagnan/src/test/resources/ARM8-expected.csv
@@ -7868,15 +7868,15 @@ litmus/AARCH64/mixed/WW+RR-variant.litmus,0
 litmus/AARCH64/mixed/CoRR+amo.swph0h0-posh0a.w0+w0.litmus,0
 litmus/AARCH64/mixed/CoRR+rmwh0h0-posh0a.w0+w0.litmus,0
 
-// Not yet supported due to grammar/parser limitations
-//litmus/AARCH64/NoRet/MP+rel+CAS-ok-dmb.ld.litmus,0
-//litmus/AARCH64/NoRet/MP+rel+CASnoret-ok-dmb.ld.litmus,1
-//litmus/AARCH64/NoRet/MP+rel+CASacq-noret-ok.litmus,1
-//litmus/AARCH64/NoRet/MP+rel+CASacq-ok.litmus,0
-//litmus/AARCH64/NoRet/MP+rel+LDADD-dmb.ld.litmus,0
-//litmus/AARCH64/NoRet/MP+rel+LDADDnoret-dmb.ld.litmus,1
-
+litmus/AARCH64/NoRet/MP+rel+CAS-ok-dmb.ld.litmus,0
+litmus/AARCH64/NoRet/MP+rel+CASnoret-ok-dmb.ld.litmus,1
+litmus/AARCH64/NoRet/MP+rel+CASacq-noret-ok.litmus,1
+litmus/AARCH64/NoRet/MP+rel+CASacq-ok.litmus,0
 litmus/AARCH64/NoRet/MP+rel+SWPacq.litmus,0
 litmus/AARCH64/NoRet/MP+rel+SWPacq-noret.litmus,1
 litmus/AARCH64/NoRet/MP+rel+SWP-dmb.ld.litmus,0
-litmus/AARCH64/NoRet/MP+rel+SWPnoret-dmb.ld.litmus,1
\ No newline at end of file
+litmus/AARCH64/NoRet/MP+rel+SWPnoret-dmb.ld.litmus,1
+
+// Not yet supported due to grammar/parser limitations
+//litmus/AARCH64/NoRet/MP+rel+LDADD-dmb.ld.litmus,0
+//litmus/AARCH64/NoRet/MP+rel+LDADDnoret-dmb.ld.litmus,1
\ No newline at end of file

From 1d87202980c58eb703a9486ad3072bf4fcf047cd Mon Sep 17 00:00:00 2001
From: Thomas Haas <tomy.haas@t-online.de>
Date: Fri, 13 Feb 2026 10:58:08 +0100
Subject: [PATCH 08/17] Added support for parsing LDOP (Aarch64) Added two new
 common Events RMWOp and RMWFetchOp

---
 dartagnan/src/main/antlr4/LitmusAArch64.g4    | 83 +++++++++++++++++++
 .../expression/ExpressionFactory.java         |  4 +
 .../visitors/VisitorLitmusAArch64.java        | 79 ++++++++++++++++++
 .../dartagnan/program/event/EventFactory.java |  8 ++
 .../dartagnan/program/event/EventVisitor.java |  8 +-
 .../program/event/arch/RMWFetchOp.java        | 33 ++++++++
 .../dartagnan/program/event/arch/RMWOp.java   | 32 +++++++
 .../processing/compilation/VisitorArm8.java   | 45 +++++++++-
 .../src/test/resources/ARM8-expected.csv      |  6 +-
 9 files changed, 289 insertions(+), 9 deletions(-)
 create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/RMWFetchOp.java
 create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/RMWOp.java

diff --git a/dartagnan/src/main/antlr4/LitmusAArch64.g4 b/dartagnan/src/main/antlr4/LitmusAArch64.g4
index aea606a508..796da6474e 100644
--- a/dartagnan/src/main/antlr4/LitmusAArch64.g4
+++ b/dartagnan/src/main/antlr4/LitmusAArch64.g4
@@ -63,6 +63,7 @@ instruction
     |   store
     |   storePair
     |   storeExclusive
+    |   loadOp
     |   swap
     |   cas
     |   cmp
@@ -119,6 +120,11 @@ storeExclusive
     |   storeExclusiveInstruction rS32 = register32 Comma rV64 = register64 Comma LBracket address RBracket
     ;
 
+loadOp
+    :   loadOpInstruction rS32 = register32 Comma rD32 = register32 Comma LBracket address RBracket
+    |   loadOpInstruction rS64 = register64 Comma rD64 = register64 Comma LBracket address RBracket
+    ;
+
 swap
     :   swapInstruction rS32 = register32 Comma rD32 = register32 Comma LBracket address RBracket
     |   swapInstruction rS64 = register64 Comma rD64 = register64 Comma LBracket address RBracket
@@ -173,6 +179,25 @@ loadExclusiveInstruction locals [boolean acquire, boolean byteSize, boolean half
     |   LDAXRH   {$acquire = true; $halfWordSize = true;}
     ;
 
+loadOpInstruction locals [IntBinaryOp op, boolean acquire, boolean release, boolean byteSize, boolean halfWordSize]
+    // ADD
+    :   LDADD | LDADDA | LDADDL | LDADDAL
+    |   LDADDH | LDADDAH | LDADDLH | LDADDALH
+    |   LDADDB | LDADDAB | LDADDLB | LDADDALB
+    // EOR
+    |   LDEOR | LDEORA | LDEORL | LDEORAL
+    |   LDEORH | LDEORAH | LDEORLH | LDEORALH
+    |   LDEORB | LDEORAB | LDEORLB | LDEORALB
+    // SET
+    |   LDSET | LDSETA | LDSETL | LDSETAL
+    |   LDSETH | LDSETAH | LDSETLH | LDSETALH
+    |   LDSETB | LDSETAB | LDSETLB | LDSETALB
+    // CLR
+    |   LDCLR | LDCLRA | LDCLRL | LDCLRAL
+    |   LDCLRH | LDCLRAH | LDCLRLH | LDCLRALH
+    |   LDCLRB | LDCLRAB | LDCLRLB | LDCLRALB
+    ;
+
 storeInstruction locals [boolean release, boolean byteSize, boolean halfWordSize]
     :   STR
     |   STRB    {$byteSize = true;}
@@ -402,6 +427,64 @@ STLXR  :   'STLXR'  ;
 STLXRB :   'STLXRB' ;
 STLXRH :   'STLXRH' ;
 
+// Load Op instructions
+// Add
+LDADD        :   'LDADD'      ;
+LDADDA       :   'LDADDA'     ;
+LDADDL       :   'LDADDL'     ;
+LDADDAL      :   'LDADDAL'    ;
+LDADDH       :   'LDADDH'     ;
+LDADDAH      :   'LDADDAH'    ;
+LDADDLH      :   'LDADDLH'    ;
+LDADDALH     :   'LDADDALH'   ;
+LDADDB       :   'LDADDB'     ;
+LDADDAB      :   'LDADDAB'    ;
+LDADDLB      :   'LDADDLB'    ;
+LDADDALB     :   'LDADDALB'   ;
+
+// EOR (XOR)
+LDEOR        :   'LDEOR'      ;
+LDEORA       :   'LDEORA'     ;
+LDEORL       :   'LDEORL'     ;
+LDEORAL      :   'LDEORAL'    ;
+LDEORH       :   'LDEORH'     ;
+LDEORAH      :   'LDEORAH'    ;
+LDEORLH      :   'LDEORLH'    ;
+LDEORALH     :   'LDEORALH'   ;
+LDEORB       :   'LDEORB'     ;
+LDEORAB      :   'LDEORAB'    ;
+LDEORLB      :   'LDEORLB'    ;
+LDEORALB     :   'LDEORALB'   ;
+
+// SET (OR)
+LDSET        :   'LDSET'      ;
+LDSETA       :   'LDSETA'     ;
+LDSETL       :   'LDSETL'     ;
+LDSETAL      :   'LDSETAL'    ;
+LDSETH       :   'LDSETH'     ;
+LDSETAH      :   'LDSETAH'    ;
+LDSETLH      :   'LDSETLH'    ;
+LDSETALH     :   'LDSETALH'   ;
+LDSETB       :   'LDSETB'     ;
+LDSETAB      :   'LDSETAB'    ;
+LDSETLB      :   'LDSETLB'    ;
+LDSETALB     :   'LDSETALB'   ;
+
+// CLR (AND with complement)
+LDCLR        :   'LDCLR'      ;
+LDCLRA       :   'LDCLRA'     ;
+LDCLRL       :   'LDCLRL'     ;
+LDCLRAL      :   'LDCLRAL'    ;
+LDCLRH       :   'LDCLRH'     ;
+LDCLRAH      :   'LDCLRAH'    ;
+LDCLRLH      :   'LDCLRLH'    ;
+LDCLRALH     :   'LDCLRALH'   ;
+LDCLRB       :   'LDCLRB'     ;
+LDCLRAB      :   'LDCLRAB'    ;
+LDCLRLB      :   'LDCLRLB'    ;
+LDCLRALB     :   'LDCLRALB'   ;
+
+
 // Swap word instructions (~ Exchange)
 
 SWP    :   'SWP'    ;
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java
index 8f0140f382..9856b693c8 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java
@@ -119,6 +119,10 @@ public Expression makeGTE(Expression leftOperand, Expression rightOperand, boole
         return makeIntCmp(leftOperand, signed ? IntCmpOp.GTE : IntCmpOp.UGTE, rightOperand);
     }
 
+    public Expression makeIntNot(Expression operand) {
+        return makeIntUnary(IntUnaryOp.NOT, operand);
+    }
+
     public Expression makeNeg(Expression operand) {
         return makeIntUnary(IntUnaryOp.MINUS, operand);
     }
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
index d9a8781b3a..404388ec75 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
@@ -4,7 +4,9 @@
 import com.dat3m.dartagnan.exception.ParsingException;
 import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.expression.ExpressionFactory;
+import com.dat3m.dartagnan.expression.integers.IntBinaryOp;
 import com.dat3m.dartagnan.expression.integers.IntLiteral;
+import com.dat3m.dartagnan.expression.integers.IntUnaryExpr;
 import com.dat3m.dartagnan.expression.type.IntegerType;
 import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.parsers.LitmusAArch64BaseVisitor;
@@ -17,6 +19,7 @@
 import com.dat3m.dartagnan.program.event.MemoryEvent;
 import com.dat3m.dartagnan.program.event.RegWriter;
 import com.dat3m.dartagnan.program.event.arch.CAS;
+import com.dat3m.dartagnan.program.event.arch.RMWFetchOp;
 import com.dat3m.dartagnan.program.event.arch.Xchg;
 import com.dat3m.dartagnan.program.event.core.Label;
 import com.dat3m.dartagnan.program.event.metadata.CustomPrinting;
@@ -348,6 +351,82 @@ public Object visitCas(CasContext ctx) {
         return null;
     }
 
+    private static final CustomPrinting LDOP_PRINTER = e -> {
+        if (!(e instanceof RMWFetchOp ldop)) {
+            return Optional.empty();
+        }
+        final String acq = e.hasTag(MO_ACQ) ? "A" : "";
+        final String rel = e.hasTag(MO_REL) ? "L" : "";
+        final String op = switch (ldop.getOperator()) {
+            case ADD -> "ADD";
+            case XOR -> "EOR";
+            case OR  -> "SET";
+            case AND -> "CLR";
+            default -> throw new RuntimeException("Invalid load op: " + ldop.getOperator());
+        };
+        final String size = switch (((IntegerType)ldop.getResultRegister().getType()).getBitWidth()) {
+            case 16 -> "H";
+            case 8  -> "B";
+            default -> "";
+        };
+        final Expression operand = ldop.getOperand() instanceof IntUnaryExpr expr ?  expr.getOperand() : ldop.getOperand();
+        final Register loadReg = ldop.getResultRegister();
+        final Expression address = ldop.getAddress();
+
+        return Optional.of(String.format("LD%s%s%s%s %s, %s, [%s]", op, acq, rel, size, loadReg, operand, address));
+    };
+
+    @Override
+    public Object visitLoadOp(LoadOpContext ctx) {
+        String instr = ctx.loadOpInstruction().getText();
+        instr = instr.substring(2); // Skip LD
+
+        // TODO: Maybe the following logic can be implemented in the grammar without
+        //  an explicit case distinction over all 48 (or more?) variants of LD
+        // Operation
+        final String opCode = instr.substring(0, 3);
+        final IntBinaryOp op = switch (opCode) {
+            case "ADD" -> IntBinaryOp.ADD;
+            case "EOR" -> IntBinaryOp.XOR;
+            case "SET" -> IntBinaryOp.OR;
+            case "CLR" -> IntBinaryOp.AND;
+            default -> throw new ParsingException("Invalid load op: " + instr);
+        };
+        instr = instr.substring(3);
+
+        // Memory order
+        final boolean acquire = instr.startsWith("A");
+        if (acquire) {
+            instr = instr.substring(1);
+        }
+        final boolean release = instr.startsWith("L");
+        if (release) {
+            instr = instr.substring(1);
+        }
+
+        // Access size
+        assert instr.length() <= 1;
+        final boolean isHalfSize = instr.startsWith("H");
+        final boolean isByteSize = instr.startsWith("B");
+
+
+        final Register rs64 = parseRegister64(ctx.rS32, ctx.rS64);
+        final Register rt64 = parseRegister64(ctx.rD32, ctx.rD64);
+        final Register rt = shrinkRegister(rt64, ctx.rD32, isHalfSize, isByteSize);
+        Expression operand = expressions.makeCast(rs64, rt.getType(), false);
+        if (opCode.equals("CLR")) {
+            operand = expressions.makeIntNot(operand);
+        }
+
+        final Expression address = parseAddress(ctx.address());
+        final RMWFetchOp ldOp = EventFactory.Common.newRmwFetchOp(rt, address, op, operand);
+        ldOp.addTags(release ? MO_REL : null, acquire ? MO_ACQ : null);
+        ldOp.setMetadata(LDOP_PRINTER);
+
+        add(ldOp);
+        addRegister64Update(rt64, rt);
+        return null;
+    }
 
     @Override
     public Object visitBranch(BranchContext ctx) {
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java
index 719611f6f4..f9597d6523 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java
@@ -407,6 +407,14 @@ public static Xchg newXchg(Register register, Expression address, Expression sto
         public static CAS newCAS(Register srcReg, Expression address, Expression cmpVal, Expression storeValue) {
             return new CAS(srcReg, address, cmpVal, storeValue);
         }
+
+        public static RMWFetchOp newRmwFetchOp(Register resultReg, Expression address, IntBinaryOp op, Expression operand) {
+            return new RMWFetchOp(resultReg, address, op, operand);
+        }
+
+        public static RMWOp newRmwOp(Expression address, IntBinaryOp op, Expression operand) {
+            return new RMWOp(address, op, operand);
+        }
     }
 
     // =============================================================================================
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java
index 2dfafe40c3..38a18f0fdb 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java
@@ -3,6 +3,8 @@
 import com.dat3m.dartagnan.program.event.arch.CAS;
 import com.dat3m.dartagnan.program.event.arch.StoreExclusive;
 import com.dat3m.dartagnan.program.event.arch.Xchg;
+import com.dat3m.dartagnan.program.event.arch.*;
+import com.dat3m.dartagnan.program.event.arch.opencl.OpenCLRMWExtremum;
 import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomCAS;
 import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomExch;
 import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomOp;
@@ -54,8 +56,10 @@ public interface EventVisitor<T> {
 
     // ------------------ Common Events ------------------
     default T visitStoreExclusive(StoreExclusive e) { return visitMemEvent(e); }
-    default T visitXchg(Xchg xchg) { return visitMemEvent(xchg); };
-    default T visitCas(CAS cas) { return visitMemEvent(cas); };
+    default T visitXchg(Xchg xchg) { return visitMemEvent(xchg); }
+    default T visitCas(CAS cas) { return visitMemEvent(cas); }
+    default T visitRMWOp(RMWOp rmwOp) { return visitMemEvent(rmwOp); };
+    default T visitRMWFetchOp(RMWFetchOp rmwOp) { return visitMemEvent(rmwOp); };
 
     // ------------------ Linux Events ------------------
     default T visitLKMMAddUnless(LKMMAddUnless e) { return visitMemEvent(e); }
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/RMWFetchOp.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/RMWFetchOp.java
new file mode 100644
index 0000000000..81e1243722
--- /dev/null
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/RMWFetchOp.java
@@ -0,0 +1,33 @@
+package com.dat3m.dartagnan.program.event.arch;
+
+import com.dat3m.dartagnan.expression.Expression;
+import com.dat3m.dartagnan.expression.integers.IntBinaryOp;
+import com.dat3m.dartagnan.program.Register;
+import com.dat3m.dartagnan.program.event.EventVisitor;
+import com.dat3m.dartagnan.program.event.common.RMWOpResultBase;
+
+public class RMWFetchOp extends RMWOpResultBase {
+
+    public RMWFetchOp(Register result, Expression address, IntBinaryOp operator, Expression operand) {
+        super(result, address, operator, operand, "");
+    }
+
+    private RMWFetchOp(RMWFetchOp other) {
+        super(other);
+    }
+
+    @Override
+    public String defaultString() {
+        return String.format("%s = rmw_fetch_%s(%s, %s)", resultRegister, operator.getName().toLowerCase(), operand, address);
+    }
+
+    @Override
+    public RMWFetchOp getCopy(){
+        return new RMWFetchOp(this);
+    }
+
+    @Override
+    public <T> T accept(EventVisitor<T> visitor) {
+        return visitor.visitRMWFetchOp(this);
+    }
+}
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/RMWOp.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/RMWOp.java
new file mode 100644
index 0000000000..74fec42634
--- /dev/null
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/RMWOp.java
@@ -0,0 +1,32 @@
+package com.dat3m.dartagnan.program.event.arch;
+
+import com.dat3m.dartagnan.expression.Expression;
+import com.dat3m.dartagnan.expression.integers.IntBinaryOp;
+import com.dat3m.dartagnan.program.event.EventVisitor;
+import com.dat3m.dartagnan.program.event.common.RMWOpBase;
+
+public class RMWOp extends RMWOpBase {
+
+    public RMWOp(Expression address, IntBinaryOp operator, Expression operand) {
+        super(address, operator, operand, "");
+    }
+
+    private RMWOp(RMWOp other) {
+        super(other);
+    }
+
+    @Override
+    public String defaultString() {
+        return String.format("rmw_%s(%s, %s)", operator.getName(), operand, address);
+    }
+
+    @Override
+    public RMWOp getCopy(){
+        return new RMWOp(this);
+    }
+
+    @Override
+    public <T> T accept(EventVisitor<T> visitor) {
+        return visitor.visitRMWOp(this);
+    }
+}
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java
index b832951328..6d9332618d 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java
@@ -9,13 +9,12 @@
 import com.dat3m.dartagnan.program.event.Tag;
 import com.dat3m.dartagnan.program.event.Tag.ARMv8;
 import com.dat3m.dartagnan.program.event.Tag.C11;
-import com.dat3m.dartagnan.program.event.arch.CAS;
-import com.dat3m.dartagnan.program.event.arch.StoreExclusive;
-import com.dat3m.dartagnan.program.event.arch.Xchg;
+import com.dat3m.dartagnan.program.event.arch.*;
 import com.dat3m.dartagnan.program.event.core.*;
 import com.dat3m.dartagnan.program.event.lang.catomic.*;
 import com.dat3m.dartagnan.program.event.lang.linux.*;
 import com.dat3m.dartagnan.program.event.lang.llvm.*;
+import com.google.common.base.Preconditions;
 
 import java.util.List;
 
@@ -95,8 +94,48 @@ public List<Event> visitCas(CAS cas) {
                 store,
                 casEnd
         );
+    }
+
+    @Override
+    public List<Event> visitRMWOp(RMWOp rmwOp) {
+        Preconditions.checkArgument(!rmwOp.hasTag(ARMv8.MO_ACQ), "Unexpected MO_ACQ tag for RMWOp");
+
+        final Register dummy = rmwOp.getFunction().newRegister(rmwOp.getAccessType());
+        final Expression address = rmwOp.getAddress();
+        final String storeMo = rmwOp.hasTag(ARMv8.MO_REL) ? ARMv8.MO_REL : "";
+
+        final Load load = propagateNoRet(rmwOp, newRMWLoad(dummy, address));
+        final Expression value = expressions.makeBinary(dummy, rmwOp.getOperator(), rmwOp.getOperand());
+
+        return eventSequence(
+                propagateNoRet(rmwOp, load),
+                newRMWStoreWithMo(load, address, value, storeMo)
+        );
+    }
 
+    @Override
+    public List<Event> visitRMWFetchOp(RMWFetchOp rmwOp) {
+        final Register resultRegister = rmwOp.getResultRegister();
+        final Expression address = rmwOp.getAddress();
+        final String loadMo = rmwOp.hasTag(ARMv8.MO_ACQ) ? ARMv8.MO_ACQ : "";
+        final String storeMo = rmwOp.hasTag(ARMv8.MO_REL) ? ARMv8.MO_REL : "";
+
+        Expression operand = rmwOp.getOperand();
+        Local captureOperand = null;
+        if (operand.getRegs().contains(resultRegister)) {
+            final Register tmpReg = rmwOp.getFunction().newRegister(resultRegister.getType());
+            captureOperand = newLocal(tmpReg, operand);
+            operand = tmpReg;
+        }
 
+        final Load load = propagateNoRet(rmwOp, newRMWLoadWithMo(resultRegister, address, loadMo));
+        final Expression value = expressions.makeBinary(resultRegister, rmwOp.getOperator(), operand);
+
+        return eventSequence(
+                captureOperand,
+                propagateNoRet(rmwOp, load),
+                newRMWStoreWithMo(load, address, value, storeMo)
+        );
     }
 
     private <T extends Load> T propagateNoRet(Event orig, T newEv) {
diff --git a/dartagnan/src/test/resources/ARM8-expected.csv b/dartagnan/src/test/resources/ARM8-expected.csv
index 277d70d3b6..042433db31 100644
--- a/dartagnan/src/test/resources/ARM8-expected.csv
+++ b/dartagnan/src/test/resources/ARM8-expected.csv
@@ -7876,7 +7876,5 @@ litmus/AARCH64/NoRet/MP+rel+SWPacq.litmus,0
 litmus/AARCH64/NoRet/MP+rel+SWPacq-noret.litmus,1
 litmus/AARCH64/NoRet/MP+rel+SWP-dmb.ld.litmus,0
 litmus/AARCH64/NoRet/MP+rel+SWPnoret-dmb.ld.litmus,1
-
-// Not yet supported due to grammar/parser limitations
-//litmus/AARCH64/NoRet/MP+rel+LDADD-dmb.ld.litmus,0
-//litmus/AARCH64/NoRet/MP+rel+LDADDnoret-dmb.ld.litmus,1
\ No newline at end of file
+litmus/AARCH64/NoRet/MP+rel+LDADD-dmb.ld.litmus,0
+litmus/AARCH64/NoRet/MP+rel+LDADDnoret-dmb.ld.litmus,1
\ No newline at end of file

From 4aa00620d2b485efb928a82d8a0e6c9713b36bc0 Mon Sep 17 00:00:00 2001
From: Thomas Haas <tomy.haas@t-online.de>
Date: Sun, 15 Feb 2026 12:07:18 +0100
Subject: [PATCH 09/17] Add STADD and variants (except for min/max)

---
 dartagnan/src/main/antlr4/LitmusAArch64.g4    |  70 ++++++++--
 .../visitors/VisitorLitmusAArch64.java        | 123 +++++++++++++-----
 .../processing/compilation/VisitorArm8.java   |   3 +-
 3 files changed, 153 insertions(+), 43 deletions(-)

diff --git a/dartagnan/src/main/antlr4/LitmusAArch64.g4 b/dartagnan/src/main/antlr4/LitmusAArch64.g4
index 796da6474e..8f7f62f67a 100644
--- a/dartagnan/src/main/antlr4/LitmusAArch64.g4
+++ b/dartagnan/src/main/antlr4/LitmusAArch64.g4
@@ -63,9 +63,12 @@ instruction
     |   store
     |   storePair
     |   storeExclusive
+    // AMOs
     |   loadOp
+    |   storeOp
     |   swap
     |   cas
+    // -----
     |   cmp
     |   branch
     |   branchRegister
@@ -125,6 +128,11 @@ loadOp
     |   loadOpInstruction rS64 = register64 Comma rD64 = register64 Comma LBracket address RBracket
     ;
 
+storeOp
+    :   storeOpInstruction rS32 = register32 Comma LBracket address RBracket
+    |   storeOpInstruction rS64 = register64 Comma LBracket address RBracket
+    ;
+
 swap
     :   swapInstruction rS32 = register32 Comma rD32 = register32 Comma LBracket address RBracket
     |   swapInstruction rS64 = register64 Comma rD64 = register64 Comma LBracket address RBracket
@@ -179,25 +187,44 @@ loadExclusiveInstruction locals [boolean acquire, boolean byteSize, boolean half
     |   LDAXRH   {$acquire = true; $halfWordSize = true;}
     ;
 
-loadOpInstruction locals [IntBinaryOp op, boolean acquire, boolean release, boolean byteSize, boolean halfWordSize]
+loadOpInstruction
     // ADD
-    :   LDADD | LDADDA | LDADDL | LDADDAL
+    :   LDADD  | LDADDA  | LDADDL  | LDADDAL
     |   LDADDH | LDADDAH | LDADDLH | LDADDALH
     |   LDADDB | LDADDAB | LDADDLB | LDADDALB
     // EOR
-    |   LDEOR | LDEORA | LDEORL | LDEORAL
+    |   LDEOR  | LDEORA  | LDEORL  | LDEORAL
     |   LDEORH | LDEORAH | LDEORLH | LDEORALH
     |   LDEORB | LDEORAB | LDEORLB | LDEORALB
     // SET
-    |   LDSET | LDSETA | LDSETL | LDSETAL
+    |   LDSET  | LDSETA  | LDSETL  | LDSETAL
     |   LDSETH | LDSETAH | LDSETLH | LDSETALH
     |   LDSETB | LDSETAB | LDSETLB | LDSETALB
     // CLR
-    |   LDCLR | LDCLRA | LDCLRL | LDCLRAL
+    |   LDCLR  | LDCLRA  | LDCLRL  | LDCLRAL
     |   LDCLRH | LDCLRAH | LDCLRLH | LDCLRALH
     |   LDCLRB | LDCLRAB | LDCLRLB | LDCLRALB
     ;
 
+storeOpInstruction
+    // ADD
+    :   STADD  | STADDL
+    |   STADDH | STADDLH
+    |   STADDB | STADDLB
+    // EOR
+    |   STEOR  | STEORL
+    |   STEORH | STEORLH
+    |   STEORB | STEORLB
+    // SET
+    |   STSET  | STSETL
+    |   STSETH | STSETLH
+    |   STSETB | STSETLB
+    // CLR
+    |   STCLR  | STCLRL
+    |   STCLRH | STCLRLH
+    |   STCLRB | STCLRLB
+    ;
+
 storeInstruction locals [boolean release, boolean byteSize, boolean halfWordSize]
     :   STR
     |   STRB    {$byteSize = true;}
@@ -441,7 +468,6 @@ LDADDB       :   'LDADDB'     ;
 LDADDAB      :   'LDADDAB'    ;
 LDADDLB      :   'LDADDLB'    ;
 LDADDALB     :   'LDADDALB'   ;
-
 // EOR (XOR)
 LDEOR        :   'LDEOR'      ;
 LDEORA       :   'LDEORA'     ;
@@ -455,7 +481,6 @@ LDEORB       :   'LDEORB'     ;
 LDEORAB      :   'LDEORAB'    ;
 LDEORLB      :   'LDEORLB'    ;
 LDEORALB     :   'LDEORALB'   ;
-
 // SET (OR)
 LDSET        :   'LDSET'      ;
 LDSETA       :   'LDSETA'     ;
@@ -469,7 +494,6 @@ LDSETB       :   'LDSETB'     ;
 LDSETAB      :   'LDSETAB'    ;
 LDSETLB      :   'LDSETLB'    ;
 LDSETALB     :   'LDSETALB'   ;
-
 // CLR (AND with complement)
 LDCLR        :   'LDCLR'      ;
 LDCLRA       :   'LDCLRA'     ;
@@ -484,6 +508,36 @@ LDCLRAB      :   'LDCLRAB'    ;
 LDCLRLB      :   'LDCLRLB'    ;
 LDCLRALB     :   'LDCLRALB'   ;
 
+// Store Op instructions
+// Add
+STADD        :   'STADD'      ;
+STADDL       :   'STADDL'     ;
+STADDH       :   'STADDH'     ;
+STADDLH      :   'STADDLH'    ;
+STADDB       :   'STADDB'     ;
+STADDLB      :   'STADDLB'    ;
+// EOR (XOR)
+STEOR        :   'STEOR'      ;
+STEORL       :   'STEORL'     ;
+STEORH       :   'STEORH'     ;
+STEORLH      :   'STEORLH'    ;
+STEORB       :   'STEORB'     ;
+STEORLB      :   'STEORLB'    ;
+// SET (OR)
+STSET        :   'STSET'      ;
+STSETL       :   'STSETL'     ;
+STSETH       :   'STSETH'     ;
+STSETLH      :   'STSETLH'    ;
+STSETB       :   'STSETB'     ;
+STSETLB      :   'STSETLB'    ;
+// CLR (AND with complement)
+STCLR        :   'STCLR'      ;
+STCLRL       :   'STCLRL'     ;
+STCLRH       :   'STCLRH'     ;
+STCLRLH      :   'STCLRLH'    ;
+STCLRB       :   'STCLRB'     ;
+STCLRLB      :   'STCLRLB'    ;
+
 
 // Swap word instructions (~ Exchange)
 
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
index 404388ec75..db94053513 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
@@ -4,6 +4,7 @@
 import com.dat3m.dartagnan.exception.ParsingException;
 import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.expression.ExpressionFactory;
+import com.dat3m.dartagnan.expression.Type;
 import com.dat3m.dartagnan.expression.integers.IntBinaryOp;
 import com.dat3m.dartagnan.expression.integers.IntLiteral;
 import com.dat3m.dartagnan.expression.integers.IntUnaryExpr;
@@ -20,6 +21,7 @@
 import com.dat3m.dartagnan.program.event.RegWriter;
 import com.dat3m.dartagnan.program.event.arch.CAS;
 import com.dat3m.dartagnan.program.event.arch.RMWFetchOp;
+import com.dat3m.dartagnan.program.event.arch.RMWOp;
 import com.dat3m.dartagnan.program.event.arch.Xchg;
 import com.dat3m.dartagnan.program.event.core.Label;
 import com.dat3m.dartagnan.program.event.metadata.CustomPrinting;
@@ -351,35 +353,11 @@ public Object visitCas(CasContext ctx) {
         return null;
     }
 
-    private static final CustomPrinting LDOP_PRINTER = e -> {
-        if (!(e instanceof RMWFetchOp ldop)) {
-            return Optional.empty();
-        }
-        final String acq = e.hasTag(MO_ACQ) ? "A" : "";
-        final String rel = e.hasTag(MO_REL) ? "L" : "";
-        final String op = switch (ldop.getOperator()) {
-            case ADD -> "ADD";
-            case XOR -> "EOR";
-            case OR  -> "SET";
-            case AND -> "CLR";
-            default -> throw new RuntimeException("Invalid load op: " + ldop.getOperator());
-        };
-        final String size = switch (((IntegerType)ldop.getResultRegister().getType()).getBitWidth()) {
-            case 16 -> "H";
-            case 8  -> "B";
-            default -> "";
-        };
-        final Expression operand = ldop.getOperand() instanceof IntUnaryExpr expr ?  expr.getOperand() : ldop.getOperand();
-        final Register loadReg = ldop.getResultRegister();
-        final Expression address = ldop.getAddress();
+    record RMWInfo(IntBinaryOp op, boolean isHalfSize, boolean isByteSize, boolean acquire, boolean release) {}
 
-        return Optional.of(String.format("LD%s%s%s%s %s, %s, [%s]", op, acq, rel, size, loadReg, operand, address));
-    };
-
-    @Override
-    public Object visitLoadOp(LoadOpContext ctx) {
-        String instr = ctx.loadOpInstruction().getText();
-        instr = instr.substring(2); // Skip LD
+    // Used for LDXXX and STXXX instructions
+    private RMWInfo getInfoFromInstructionName(String instrName) {
+        String instr = instrName.substring(2); // Skip LD/ST
 
         // TODO: Maybe the following logic can be implemented in the grammar without
         //  an explicit case distinction over all 48 (or more?) variants of LD
@@ -389,8 +367,8 @@ public Object visitLoadOp(LoadOpContext ctx) {
             case "ADD" -> IntBinaryOp.ADD;
             case "EOR" -> IntBinaryOp.XOR;
             case "SET" -> IntBinaryOp.OR;
-            case "CLR" -> IntBinaryOp.AND;
-            default -> throw new ParsingException("Invalid load op: " + instr);
+            case "CLR" -> IntBinaryOp.AND; // Actually & with complement!!!
+            default -> throw new ParsingException("Invalid op " + opCode + " found in " + instrName);
         };
         instr = instr.substring(3);
 
@@ -409,18 +387,41 @@ public Object visitLoadOp(LoadOpContext ctx) {
         final boolean isHalfSize = instr.startsWith("H");
         final boolean isByteSize = instr.startsWith("B");
 
+        return new RMWInfo(op, isHalfSize, isByteSize, acquire, release);
+    }
+
+    private static final CustomPrinting LDOP_PRINTER = e -> {
+        if (!(e instanceof RMWFetchOp ldop)) {
+            return Optional.empty();
+        }
+        final String acq = e.hasTag(MO_ACQ) ? "A" : "";
+        final String rel = e.hasTag(MO_REL) ? "L" : "";
+        final String op = OpToArmOpCode(ldop.getOperator());
+        final String size = getArmSizeSuffix(ldop.getAccessType());
+        final Expression operand = ldop.getOperand() instanceof IntUnaryExpr expr ?  expr.getOperand() : ldop.getOperand();
+        final Register loadReg = ldop.getResultRegister();
+        final Expression address = ldop.getAddress();
+
+        return Optional.of(String.format("LD%s%s%s%s %s, %s, [%s]", op, acq, rel, size, loadReg, operand, address));
+    };
+
+    @Override
+    public Object visitLoadOp(LoadOpContext ctx) {
+        final String instr = ctx.loadOpInstruction().getText();
+        final RMWInfo info = getInfoFromInstructionName(instr);
 
         final Register rs64 = parseRegister64(ctx.rS32, ctx.rS64);
         final Register rt64 = parseRegister64(ctx.rD32, ctx.rD64);
-        final Register rt = shrinkRegister(rt64, ctx.rD32, isHalfSize, isByteSize);
+        final Register rt = shrinkRegister(rt64, ctx.rD32, info.isHalfSize, info.isByteSize);
         Expression operand = expressions.makeCast(rs64, rt.getType(), false);
-        if (opCode.equals("CLR")) {
+        if (info.op == IntBinaryOp.AND) {
+            // This was a CLR instruction
             operand = expressions.makeIntNot(operand);
         }
 
         final Expression address = parseAddress(ctx.address());
-        final RMWFetchOp ldOp = EventFactory.Common.newRmwFetchOp(rt, address, op, operand);
-        ldOp.addTags(release ? MO_REL : null, acquire ? MO_ACQ : null);
+        final RMWFetchOp ldOp = EventFactory.Common.newRmwFetchOp(rt, address, info.op, operand);
+        ldOp.addTags(info.release ? MO_REL : null, info.acquire ? MO_ACQ : null);
         ldOp.setMetadata(LDOP_PRINTER);
 
         add(ldOp);
@@ -428,6 +429,42 @@ public Object visitLoadOp(LoadOpContext ctx) {
         return null;
     }
 
+    private static final CustomPrinting STOP_PRINTER = e -> {
+        if (!(e instanceof RMWOp stop)) {
+            return Optional.empty();
+        }
+        final String rel = e.hasTag(MO_REL) ? "L" : "";
+        final String op = OpToArmOpCode(stop.getOperator());
+        final String size = getArmSizeSuffix(stop.getAccessType());
+        final Expression operand = stop.getOperand() instanceof IntUnaryExpr expr ?  expr.getOperand() : stop.getOperand();
+        final Expression address = stop.getAddress();
+
+        return Optional.of(String.format("ST%s%s%s %s, [%s]", op, rel, size, operand, address));
+    };
+
+    @Override
+    public Object visitStoreOp(StoreOpContext ctx) {
+        final String instr = ctx.storeOpInstruction().getText();
+        final RMWInfo info = getInfoFromInstructionName(instr);
+
+        final Register rs64 = parseRegister64(ctx.rS32, ctx.rS64);
+        // TODO: We don't actually care about the smaller register, but only its type!
+        final Register rs = shrinkRegister(rs64, ctx.rS32, info.isHalfSize, info.isByteSize);
+        Expression operand = expressions.makeCast(rs64, rs.getType(), false);
+        if (info.op == IntBinaryOp.AND) {
+            // This was a CLR instruction
+            operand = expressions.makeIntNot(operand);
+        }
+
+        final Expression address = parseAddress(ctx.address());
+        final RMWOp stOp = EventFactory.Common.newRmwOp(address, info.op, operand);
+        stOp.addTags(info.release ? MO_REL : null);
+        stOp.setMetadata(STOP_PRINTER);
+
+        add(stOp);
+        return null;
+    }
+
     @Override
     public Object visitBranch(BranchContext ctx) {
         Label label = programBuilder.getOrCreateLabel(mainThread, ctx.label().getText());
@@ -587,4 +624,22 @@ private Void add(Event event) {
         programBuilder.addChild(mainThread, event);
         return null;
     }
+
+    private static String OpToArmOpCode(IntBinaryOp op) {
+        return switch (op) {
+            case ADD -> "ADD";
+            case XOR -> "EOR";
+            case OR -> "SET";
+            case AND -> "CLR";
+            default -> throw new RuntimeException("Invalid op: " + op);
+        };
+    }
+
+    private static String getArmSizeSuffix(Type type) {
+        return switch (((IntegerType) type).getBitWidth()) {
+            case 16 -> "H";
+            case 8 -> "B";
+            default -> "";
+        };
+    }
 }
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java
index 6d9332618d..e004cd1652 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java
@@ -105,10 +105,11 @@ public List<Event> visitRMWOp(RMWOp rmwOp) {
         final String storeMo = rmwOp.hasTag(ARMv8.MO_REL) ? ARMv8.MO_REL : "";
 
         final Load load = propagateNoRet(rmwOp, newRMWLoad(dummy, address));
+        load.addTags(Tag.ARMv8.NO_RET);
         final Expression value = expressions.makeBinary(dummy, rmwOp.getOperator(), rmwOp.getOperand());
 
         return eventSequence(
-                propagateNoRet(rmwOp, load),
+                load,
                 newRMWStoreWithMo(load, address, value, storeMo)
         );
     }

From ea3bfa5ff21df20ade14652f207e0cc46da9bb4e Mon Sep 17 00:00:00 2001
From: Thomas Haas <tomy.haas@t-online.de>
Date: Sun, 15 Feb 2026 22:03:07 +0100
Subject: [PATCH 10/17] Fixup after rebase

---
 .../java/com/dat3m/dartagnan/program/event/EventFactory.java  | 4 +---
 .../java/com/dat3m/dartagnan/program/event/EventVisitor.java  | 4 ----
 2 files changed, 1 insertion(+), 7 deletions(-)

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java
index f9597d6523..ba206223e2 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java
@@ -11,9 +11,7 @@
 import com.dat3m.dartagnan.program.Function;
 import com.dat3m.dartagnan.program.Register;
 import com.dat3m.dartagnan.program.Thread;
-import com.dat3m.dartagnan.program.event.arch.CAS;
-import com.dat3m.dartagnan.program.event.arch.StoreExclusive;
-import com.dat3m.dartagnan.program.event.arch.Xchg;
+import com.dat3m.dartagnan.program.event.arch.*;
 import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomCAS;
 import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomExch;
 import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomOp;
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java
index 38a18f0fdb..1017197639 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java
@@ -1,10 +1,6 @@
 package com.dat3m.dartagnan.program.event;
 
-import com.dat3m.dartagnan.program.event.arch.CAS;
-import com.dat3m.dartagnan.program.event.arch.StoreExclusive;
-import com.dat3m.dartagnan.program.event.arch.Xchg;
 import com.dat3m.dartagnan.program.event.arch.*;
-import com.dat3m.dartagnan.program.event.arch.opencl.OpenCLRMWExtremum;
 import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomCAS;
 import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomExch;
 import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomOp;

From 5ca2f9e132af0313eae34cebf7e170c5ba8e855d Mon Sep 17 00:00:00 2001
From: Thomas Haas <tomy.haas@t-online.de>
Date: Sun, 15 Feb 2026 22:28:28 +0100
Subject: [PATCH 11/17] ADD SMIN/SMAX/UMIN/UMAX variants of LDXXX/STXXX

---
 dartagnan/src/main/antlr4/LitmusAArch64.g4    | 116 +++++++++++++++++-
 .../visitors/VisitorLitmusAArch64.java        |  49 +++++---
 2 files changed, 145 insertions(+), 20 deletions(-)

diff --git a/dartagnan/src/main/antlr4/LitmusAArch64.g4 b/dartagnan/src/main/antlr4/LitmusAArch64.g4
index 8f7f62f67a..b3e6dc183a 100644
--- a/dartagnan/src/main/antlr4/LitmusAArch64.g4
+++ b/dartagnan/src/main/antlr4/LitmusAArch64.g4
@@ -204,6 +204,22 @@ loadOpInstruction
     |   LDCLR  | LDCLRA  | LDCLRL  | LDCLRAL
     |   LDCLRH | LDCLRAH | LDCLRLH | LDCLRALH
     |   LDCLRB | LDCLRAB | LDCLRLB | LDCLRALB
+    // SMIN
+    |   LDSMIN  | LDSMINA  | LDSMINL  | LDSMINAL
+    |   LDSMINH | LDSMINAH | LDSMINLH | LDSMINALH
+    |   LDSMINB | LDSMINAB | LDSMINLB | LDSMINALB
+    // UMIN
+    |   LDUMIN  | LDUMINA  | LDUMINL  | LDUMINAL
+    |   LDUMINH | LDUMINAH | LDUMINLH | LDUMINALH
+    |   LDUMINB | LDUMINAB | LDUMINLB | LDUMINALB
+    // SMAX
+    |   LDSMAX  | LDSMAXA  | LDSMAXL  | LDSMAXAL
+    |   LDSMAXH | LDSMAXAH | LDSMAXLH | LDSMAXALH
+    |   LDSMAXB | LDSMAXAB | LDSMAXLB | LDSMAXALB
+    // UMAX
+    |   LDUMAX  | LDUMAXA  | LDUMAXL  | LDUMAXAL
+    |   LDUMAXH | LDUMAXAH | LDUMAXLH | LDUMAXALH
+    |   LDUMAXB | LDUMAXAB | LDUMAXLB | LDUMAXALB
     ;
 
 storeOpInstruction
@@ -223,6 +239,22 @@ storeOpInstruction
     |   STCLR  | STCLRL
     |   STCLRH | STCLRLH
     |   STCLRB | STCLRLB
+    // SMIN
+    |   STSMIN  | STSMINL
+    |   STSMINH | STSMINLH
+    |   STSMINB | STSMINLB
+    // UMIN
+    |   STUMIN  | STUMINL
+    |   STUMINH | STUMINLH
+    |   STUMINB | STUMINLB
+    // SMAX
+    |   STSMAX  | STSMAXL
+    |   STSMAXH | STSMAXLH
+    |   STSMAXB | STSMAXLB
+    // UMAX
+    |   STUMAX  | STUMAXL
+    |   STUMAXH | STUMAXLH
+    |   STUMAXB | STUMAXLB
     ;
 
 storeInstruction locals [boolean release, boolean byteSize, boolean halfWordSize]
@@ -507,6 +539,58 @@ LDCLRB       :   'LDCLRB'     ;
 LDCLRAB      :   'LDCLRAB'    ;
 LDCLRLB      :   'LDCLRLB'    ;
 LDCLRALB     :   'LDCLRALB'   ;
+// SMIN
+LDSMIN        :   'LDSMIN'      ;
+LDSMINA       :   'LDSMINA'     ;
+LDSMINL       :   'LDSMINL'     ;
+LDSMINAL      :   'LDSMINAL'    ;
+LDSMINH       :   'LDSMINH'     ;
+LDSMINAH      :   'LDSMINAH'    ;
+LDSMINLH      :   'LDSMINLH'    ;
+LDSMINALH     :   'LDSMINALH'   ;
+LDSMINB       :   'LDSMINB'     ;
+LDSMINAB      :   'LDSMINAB'    ;
+LDSMINLB      :   'LDSMINLB'    ;
+LDSMINALB     :   'LDSMINALB'   ;
+// UMIN
+LDUMIN        :   'LDUMIN'      ;
+LDUMINA       :   'LDUMINA'     ;
+LDUMINL       :   'LDUMINL'     ;
+LDUMINAL      :   'LDUMINAL'    ;
+LDUMINH       :   'LDUMINH'     ;
+LDUMINAH      :   'LDUMINAH'    ;
+LDUMINLH      :   'LDUMINLH'    ;
+LDUMINALH     :   'LDUMINALH'   ;
+LDUMINB       :   'LDUMINB'     ;
+LDUMINAB      :   'LDUMINAB'    ;
+LDUMINLB      :   'LDUMINLB'    ;
+LDUMINALB     :   'LDUMINALB'   ;
+// SMAX
+LDSMAX        :   'LDSMAX'      ;
+LDSMAXA       :   'LDSMAXA'     ;
+LDSMAXL       :   'LDSMAXL'     ;
+LDSMAXAL      :   'LDSMAXAL'    ;
+LDSMAXH       :   'LDSMAXH'     ;
+LDSMAXAH      :   'LDSMAXAH'    ;
+LDSMAXLH      :   'LDSMAXLH'    ;
+LDSMAXALH     :   'LDSMAXALH'   ;
+LDSMAXB       :   'LDSMAXB'     ;
+LDSMAXAB      :   'LDSMAXAB'    ;
+LDSMAXLB      :   'LDSMAXLB'    ;
+LDSMAXALB     :   'LDSMAXALB'   ;
+// UMAX
+LDUMAX        :   'LDUMAX'      ;
+LDUMAXA       :   'LDUMAXA'     ;
+LDUMAXL       :   'LDUMAXL'     ;
+LDUMAXAL      :   'LDUMAXAL'    ;
+LDUMAXH       :   'LDUMAXH'     ;
+LDUMAXAH      :   'LDUMAXAH'    ;
+LDUMAXLH      :   'LDUMAXLH'    ;
+LDUMAXALH     :   'LDUMAXALH'   ;
+LDUMAXB       :   'LDUMAXB'     ;
+LDUMAXAB      :   'LDUMAXAB'    ;
+LDUMAXLB      :   'LDUMAXLB'    ;
+LDUMAXALB     :   'LDUMAXALB'   ;
 
 // Store Op instructions
 // Add
@@ -537,6 +621,34 @@ STCLRH       :   'STCLRH'     ;
 STCLRLH      :   'STCLRLH'    ;
 STCLRB       :   'STCLRB'     ;
 STCLRLB      :   'STCLRLB'    ;
+// SMIN
+STSMIN        :   'STSMIN'      ;
+STSMINL       :   'STSMINL'     ;
+STSMINH       :   'STSMINH'     ;
+STSMINLH      :   'STSMINLH'    ;
+STSMINB       :   'STSMINB'     ;
+STSMINLB      :   'STSMINLB'    ;
+// UMIN
+STUMIN        :   'STUMIN'      ;
+STUMINL       :   'STUMINL'     ;
+STUMINH       :   'STUMINH'     ;
+STUMINLH      :   'STUMINLH'    ;
+STUMINB       :   'STUMINB'     ;
+STUMINLB      :   'STUMINLB'    ;
+// SMAX
+STSMAX        :   'STSMAX'      ;
+STSMAXL       :   'STSMAXL'     ;
+STSMAXH       :   'STSMAXH'     ;
+STSMAXLH      :   'STSMAXLH'    ;
+STSMAXB       :   'STSMAXB'     ;
+STSMAXLB      :   'STSMAXLB'    ;
+// UMAX
+STUMAX        :   'STUMAX'      ;
+STUMAXL       :   'STUMAXL'     ;
+STUMAXH       :   'STUMAXH'     ;
+STUMAXLH      :   'STUMAXLH'    ;
+STUMAXB       :   'STUMAXB'     ;
+STUMAXLB      :   'STUMAXLB'    ;
 
 
 // Swap word instructions (~ Exchange)
@@ -602,7 +714,7 @@ FenceOpt
     |   'OSH'   |   'osh'       // Outer sharable domain only
     ;
 
-// Bracnch conditions
+// Brancch conditions
 
 EQ  :   'EQ';    // Equal
 NE  :   'NE';    // Not equal
@@ -610,7 +722,7 @@ CS  :   'CS';    // Carry set
 HS  :   'HS';    // Identical to CS
 CC  :   'CC';    // Carry clear
 LO  :   'LO';    // Identical to CC
-MI  :   'MI';	 // Minus or negative result
+MI  :   'MI';    // Minus or negative result
 PL  :   'PL';    // Positive or zero result
 VS  :   'VS';    // Overflow
 VC  :   'VC';    // No overflow
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
index db94053513..f2c5eca349 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
@@ -355,37 +355,46 @@ public Object visitCas(CasContext ctx) {
 
     record RMWInfo(IntBinaryOp op, boolean isHalfSize, boolean isByteSize, boolean acquire, boolean release) {}
 
-    // Used for LDXXX and STXXX instructions
+    // Used for LDXXX and STXXX instructions of shape
+    // ST/LD - XXX/XXXX - {A, L, AL}?  - {H, B}?
+    // Instr - op code  - memory order - access size
     private RMWInfo getInfoFromInstructionName(String instrName) {
         String instr = instrName.substring(2); // Skip LD/ST
 
+        // Access size
+        final boolean isHalfSize = instr.endsWith("H");
+        final boolean isByteSize = instr.endsWith("B");
+        if (isHalfSize || isByteSize) {
+            instr = instr.substring(0, instr.length() - 1);
+        }
+
+        // Memory order
+        final boolean release = instr.endsWith("L");
+        if (release) {
+            instr = instr.substring(0, instr.length() - 1);
+        }
+        final boolean acquire = instr.endsWith("A");
+        if (acquire) {
+            instr = instr.substring(0, instr.length() - 1);
+        }
+
+        // Only OpCode remains
+        assert 3 <= instr.length() && instr.length() <= 4;
         // TODO: Maybe the following logic can be implemented in the grammar without
         //  an explicit case distinction over all 48 (or more?) variants of LD
         // Operation
-        final String opCode = instr.substring(0, 3);
+        final String opCode = instr;
         final IntBinaryOp op = switch (opCode) {
             case "ADD" -> IntBinaryOp.ADD;
             case "EOR" -> IntBinaryOp.XOR;
             case "SET" -> IntBinaryOp.OR;
             case "CLR" -> IntBinaryOp.AND; // Actually & with complement!!!
+            case "SMIN" -> IntBinaryOp.SMIN;
+            case "SMAX" -> IntBinaryOp.SMAX;
+            case "UMIN" -> IntBinaryOp.UMIN;
+            case "UMAX" -> IntBinaryOp.UMAX;
             default -> throw new ParsingException("Invalid op " + opCode + " found in " + instrName);
         };
-        instr = instr.substring(3);
-
-        // Memory order
-        final boolean acquire = instr.startsWith("A");
-        if (acquire) {
-            instr = instr.substring(1);
-        }
-        final boolean release = instr.startsWith("L");
-        if (release) {
-            instr = instr.substring(1);
-        }
-
-        // Access size
-        assert instr.length() <= 1;
-        final boolean isHalfSize = instr.startsWith("H");
-        final boolean isByteSize = instr.startsWith("B");
 
         return new RMWInfo(op, isHalfSize, isByteSize, acquire, release);
     }
@@ -631,6 +640,10 @@ private static String OpToArmOpCode(IntBinaryOp op) {
             case XOR -> "EOR";
             case OR -> "SET";
             case AND -> "CLR";
+            case SMIN -> "SMIN";
+            case SMAX -> "SMAX";
+            case UMIN -> "UMIN";
+            case UMAX -> "UMAX";
             default -> throw new RuntimeException("Invalid op: " + op);
         };
     }

From 363c72bb4fccaad3ffe1d5482685e66e21bddd95 Mon Sep 17 00:00:00 2001
From: Thomas Haas <tomy.haas@t-online.de>
Date: Mon, 16 Feb 2026 10:02:56 +0100
Subject: [PATCH 12/17] Minor renaming

---
 dartagnan/src/main/antlr4/LitmusAArch64.g4     |  2 +-
 .../program/visitors/VisitorLitmusAArch64.java | 18 +++++++++++-------
 .../dartagnan/program/event/arch/CAS.java      |  2 +-
 .../dartagnan/program/event/arch/RMWOp.java    |  2 +-
 4 files changed, 14 insertions(+), 10 deletions(-)

diff --git a/dartagnan/src/main/antlr4/LitmusAArch64.g4 b/dartagnan/src/main/antlr4/LitmusAArch64.g4
index b3e6dc183a..4ec0b70e78 100644
--- a/dartagnan/src/main/antlr4/LitmusAArch64.g4
+++ b/dartagnan/src/main/antlr4/LitmusAArch64.g4
@@ -714,7 +714,7 @@ FenceOpt
     |   'OSH'   |   'osh'       // Outer sharable domain only
     ;
 
-// Brancch conditions
+// Branch conditions
 
 EQ  :   'EQ';    // Equal
 NE  :   'NE';    // Not equal
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
index f2c5eca349..5653d50ed9 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
@@ -25,6 +25,7 @@
 import com.dat3m.dartagnan.program.event.arch.Xchg;
 import com.dat3m.dartagnan.program.event.core.Label;
 import com.dat3m.dartagnan.program.event.metadata.CustomPrinting;
+import com.google.common.base.Preconditions;
 import org.antlr.v4.runtime.tree.TerminalNode;
 
 import java.math.BigInteger;
@@ -353,14 +354,19 @@ public Object visitCas(CasContext ctx) {
         return null;
     }
 
-    record RMWInfo(IntBinaryOp op, boolean isHalfSize, boolean isByteSize, boolean acquire, boolean release) {}
+
+    record LDSTAmoInfo(IntBinaryOp op, boolean isHalfSize, boolean isByteSize, boolean acquire, boolean release) {}
 
     // Used for LDXXX and STXXX instructions of shape
     // ST/LD - XXX/XXXX - {A, L, AL}?  - {H, B}?
     // Instr - op code  - memory order - access size
-    private RMWInfo getInfoFromInstructionName(String instrName) {
+    private LDSTAmoInfo getLDSTInfoFromInstructionName(String instrName) {
+        Preconditions.checkArgument(instrName.startsWith("LD") || instrName.startsWith("ST"));
         String instr = instrName.substring(2); // Skip LD/ST
 
+        // TODO: Maybe the following logic can be implemented in the grammar without
+        //  an explicit case distinction over all 96 (or more?) variants of LD (and ST)
+
         // Access size
         final boolean isHalfSize = instr.endsWith("H");
         final boolean isByteSize = instr.endsWith("B");
@@ -380,8 +386,6 @@ private RMWInfo getInfoFromInstructionName(String instrName) {
 
         // Only OpCode remains
         assert 3 <= instr.length() && instr.length() <= 4;
-        // TODO: Maybe the following logic can be implemented in the grammar without
-        //  an explicit case distinction over all 48 (or more?) variants of LD
         // Operation
         final String opCode = instr;
         final IntBinaryOp op = switch (opCode) {
@@ -396,7 +400,7 @@ private RMWInfo getInfoFromInstructionName(String instrName) {
             default -> throw new ParsingException("Invalid op " + opCode + " found in " + instrName);
         };
 
-        return new RMWInfo(op, isHalfSize, isByteSize, acquire, release);
+        return new LDSTAmoInfo(op, isHalfSize, isByteSize, acquire, release);
     }
 
     private static final CustomPrinting LDOP_PRINTER = e -> {
@@ -417,7 +421,7 @@ private RMWInfo getInfoFromInstructionName(String instrName) {
     @Override
     public Object visitLoadOp(LoadOpContext ctx) {
         final String instr = ctx.loadOpInstruction().getText();
-        final RMWInfo info = getInfoFromInstructionName(instr);
+        final LDSTAmoInfo info = getLDSTInfoFromInstructionName(instr);
 
         final Register rs64 = parseRegister64(ctx.rS32, ctx.rS64);
         final Register rt64 = parseRegister64(ctx.rD32, ctx.rD64);
@@ -454,7 +458,7 @@ public Object visitLoadOp(LoadOpContext ctx) {
     @Override
     public Object visitStoreOp(StoreOpContext ctx) {
         final String instr = ctx.storeOpInstruction().getText();
-        final RMWInfo info = getInfoFromInstructionName(instr);
+        final LDSTAmoInfo info = getLDSTInfoFromInstructionName(instr);
 
         final Register rs64 = parseRegister64(ctx.rS32, ctx.rS64);
         // TODO: We don't actually care about the smaller register, but only its type!
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/CAS.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/CAS.java
index 455f7bd73b..219249196a 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/CAS.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/CAS.java
@@ -17,7 +17,7 @@ private CAS(CAS other){
 
     @Override
     public String defaultString() {
-        return String.format("%s = cas(%s, %s)", resultRegister, address, storeValue);
+        return String.format("%s = cas(%s, %s, %s)", resultRegister, address, expectedValue, storeValue);
     }
 
     @Override
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/RMWOp.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/RMWOp.java
index 74fec42634..9c90da21f6 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/RMWOp.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/RMWOp.java
@@ -17,7 +17,7 @@ private RMWOp(RMWOp other) {
 
     @Override
     public String defaultString() {
-        return String.format("rmw_%s(%s, %s)", operator.getName(), operand, address);
+        return String.format("rmw_%s(%s, %s)", operator.getName().toLowerCase(), operand, address);
     }
 
     @Override

From cc1121e814c80caf7a562d1c4bcf6a8c6e87b889 Mon Sep 17 00:00:00 2001
From: Thomas Haas <tomy.haas@t-online.de>
Date: Mon, 16 Feb 2026 12:40:21 +0100
Subject: [PATCH 13/17] Delete broken assertionValue rule in LitmusAArch64.g4

---
 dartagnan/src/main/antlr4/LitmusAArch64.g4 | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/dartagnan/src/main/antlr4/LitmusAArch64.g4 b/dartagnan/src/main/antlr4/LitmusAArch64.g4
index 4ec0b70e78..6a4d994bbf 100644
--- a/dartagnan/src/main/antlr4/LitmusAArch64.g4
+++ b/dartagnan/src/main/antlr4/LitmusAArch64.g4
@@ -415,12 +415,6 @@ label
     :   Identifier
     ;
 
-assertionValue
-    :   location
-    |   threadId Colon register64
-    |   constant
-    ;
-
 Hexa
     :   '0x'
     ;

From 81527c43e8dcffbe802fd5927fd42701183e0cd0 Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <hernanl.leon@huawei.com>
Date: Mon, 16 Feb 2026 20:07:16 +0800
Subject: [PATCH 14/17] Add more NoRet tests

Signed-off-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
---
 dartagnan/src/test/resources/ARM8-expected.csv       |  6 ++++--
 litmus/AARCH64/NoRet/MP+popl+amo.swpazrp-po.litmus   | 11 +++++++++++
 litmus/AARCH64/NoRet/MP+popl+amo.swpzr-dmb.ld.litmus | 11 +++++++++++
 litmus/AARCH64/NoRet/MP+popl+amo.swpzr-dsb.ld.litmus | 11 +++++++++++
 4 files changed, 37 insertions(+), 2 deletions(-)
 create mode 100644 litmus/AARCH64/NoRet/MP+popl+amo.swpazrp-po.litmus
 create mode 100644 litmus/AARCH64/NoRet/MP+popl+amo.swpzr-dmb.ld.litmus
 create mode 100644 litmus/AARCH64/NoRet/MP+popl+amo.swpzr-dsb.ld.litmus

diff --git a/dartagnan/src/test/resources/ARM8-expected.csv b/dartagnan/src/test/resources/ARM8-expected.csv
index 042433db31..566acb2866 100644
--- a/dartagnan/src/test/resources/ARM8-expected.csv
+++ b/dartagnan/src/test/resources/ARM8-expected.csv
@@ -7867,7 +7867,6 @@ litmus/AARCH64/mixed/WW+RR-variant.litmus,0
 litmus/AARCH64/mixed/WW+RR-variant.litmus,0
 litmus/AARCH64/mixed/CoRR+amo.swph0h0-posh0a.w0+w0.litmus,0
 litmus/AARCH64/mixed/CoRR+rmwh0h0-posh0a.w0+w0.litmus,0
-
 litmus/AARCH64/NoRet/MP+rel+CAS-ok-dmb.ld.litmus,0
 litmus/AARCH64/NoRet/MP+rel+CASnoret-ok-dmb.ld.litmus,1
 litmus/AARCH64/NoRet/MP+rel+CASacq-noret-ok.litmus,1
@@ -7877,4 +7876,7 @@ litmus/AARCH64/NoRet/MP+rel+SWPacq-noret.litmus,1
 litmus/AARCH64/NoRet/MP+rel+SWP-dmb.ld.litmus,0
 litmus/AARCH64/NoRet/MP+rel+SWPnoret-dmb.ld.litmus,1
 litmus/AARCH64/NoRet/MP+rel+LDADD-dmb.ld.litmus,0
-litmus/AARCH64/NoRet/MP+rel+LDADDnoret-dmb.ld.litmus,1
\ No newline at end of file
+litmus/AARCH64/NoRet/MP+rel+LDADDnoret-dmb.ld.litmus,1
+litmus/AARCH64/NoRet/MP+popl+amo.swpazrp-po.litmus,1
+litmus/AARCH64/NoRet/MP+popl+amo.swpzr-dmb.ld.litmus,1
+litmus/AARCH64/NoRet/MP+popl+amo.swpzr-dsb.ld.litmus,1
\ No newline at end of file
diff --git a/litmus/AARCH64/NoRet/MP+popl+amo.swpazrp-po.litmus b/litmus/AARCH64/NoRet/MP+popl+amo.swpazrp-po.litmus
new file mode 100644
index 0000000000..54e0722fd9
--- /dev/null
+++ b/litmus/AARCH64/NoRet/MP+popl+amo.swpazrp-po.litmus
@@ -0,0 +1,11 @@
+AArch64 MP+popl+amo.swpazrp-po
+{
+0:X1=x; 0:X3=y;
+1:X3=y; 1:X1=x;
+}
+ P0           | P1               ;
+ MOV W0,#1    | MOV W2,#2        ;
+ STR W0,[X1]  | SWPA W2,WZR,[X3] ;
+ MOV W2,#1    | LDR W4,[X1]      ;
+ STLR W2,[X3] |                  ;
+exists ([y]=2 /\ 1:X4=0)
\ No newline at end of file
diff --git a/litmus/AARCH64/NoRet/MP+popl+amo.swpzr-dmb.ld.litmus b/litmus/AARCH64/NoRet/MP+popl+amo.swpzr-dmb.ld.litmus
new file mode 100644
index 0000000000..4d8c7ab2b0
--- /dev/null
+++ b/litmus/AARCH64/NoRet/MP+popl+amo.swpzr-dmb.ld.litmus
@@ -0,0 +1,11 @@
+AArch64 MP+popl+amo.swpzr-dmb.ld
+{
+0:X1=x; 0:X3=y;
+1:X3=y; 1:X1=x;
+}
+ P0           | P1             ;
+ MOV W0,#1    | MOV W2,#2      ;
+ STR W0,[X1]  | SWP W2,WZR,[X3] ;
+ MOV W2,#1    | DMB LD         ;
+ STLR W2,[X3] | LDR W0,[X1]    ;
+exists ([y]=2 /\ 1:X0=0)
\ No newline at end of file
diff --git a/litmus/AARCH64/NoRet/MP+popl+amo.swpzr-dsb.ld.litmus b/litmus/AARCH64/NoRet/MP+popl+amo.swpzr-dsb.ld.litmus
new file mode 100644
index 0000000000..54598fad17
--- /dev/null
+++ b/litmus/AARCH64/NoRet/MP+popl+amo.swpzr-dsb.ld.litmus
@@ -0,0 +1,11 @@
+AArch64 MP+popl+amo.swpzr-dsb.ld
+{
+0:X1=x; 0:X3=y;
+1:X3=y; 1:X1=x;
+}
+ P0           | P1             ;
+ MOV W0,#1    | MOV W2,#2      ;
+ STR W0,[X1]  | SWP W2,WZR,[X3] ;
+ MOV W2,#1    | DSB LD         ;
+ STLR W2,[X3] | LDR W0,[X1]    ;
+exists ([y]=2 /\ 1:X0=0)
\ No newline at end of file

From e0c60a68c48621f8a9219c64625bc9206e80810d Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <hernanl.leon@huawei.com>
Date: Mon, 16 Feb 2026 20:56:27 +0800
Subject: [PATCH 15/17] Fix

Signed-off-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
---
 dartagnan/src/main/antlr4/LitmusAArch64.g4 | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/dartagnan/src/main/antlr4/LitmusAArch64.g4 b/dartagnan/src/main/antlr4/LitmusAArch64.g4
index 6a4d994bbf..7dcafec5b3 100644
--- a/dartagnan/src/main/antlr4/LitmusAArch64.g4
+++ b/dartagnan/src/main/antlr4/LitmusAArch64.g4
@@ -405,6 +405,7 @@ register32 returns[String id]
 
 location
     :   Identifier
+    |   LBracket Identifier RBracket
     ;
 
 immediate
@@ -415,6 +416,12 @@ label
     :   Identifier
     ;
 
+assertionValue
+    :   location
+    |   threadId Colon register64
+    |   constant
+    ;
+
 Hexa
     :   '0x'
     ;

From 74374278b6d8e2c11f5da20ab15fae8ab479d9ed Mon Sep 17 00:00:00 2001
From: Thomas Haas <tomy.haas@t-online.de>
Date: Wed, 18 Feb 2026 21:04:19 +0100
Subject: [PATCH 16/17] Feedback

---
 .../visitors/VisitorLitmusAArch64.java        | 105 ++++++++++--------
 .../processing/compilation/VisitorArm8.java   |   2 +-
 .../src/test/resources/ARM8-expected.csv      |   2 -
 3 files changed, 58 insertions(+), 51 deletions(-)

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
index 5653d50ed9..e0562829c7 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java
@@ -409,7 +409,7 @@ private LDSTAmoInfo getLDSTInfoFromInstructionName(String instrName) {
         }
         final String acq = e.hasTag(MO_ACQ) ? "A" : "";
         final String rel = e.hasTag(MO_REL) ? "L" : "";
-        final String op = OpToArmOpCode(ldop.getOperator());
+        final String op = opToArmOpCode(ldop.getOperator());
         final String size = getArmSizeSuffix(ldop.getAccessType());
         final Expression operand = ldop.getOperand() instanceof IntUnaryExpr expr ?  expr.getOperand() : ldop.getOperand();
         final Register loadReg = ldop.getResultRegister();
@@ -417,37 +417,12 @@ private LDSTAmoInfo getLDSTInfoFromInstructionName(String instrName) {
 
         return Optional.of(String.format("LD%s%s%s%s %s, %s, [%s]", op, acq, rel, size, loadReg, operand, address));
     };
-
-    @Override
-    public Object visitLoadOp(LoadOpContext ctx) {
-        final String instr = ctx.loadOpInstruction().getText();
-        final LDSTAmoInfo info = getLDSTInfoFromInstructionName(instr);
-
-        final Register rs64 = parseRegister64(ctx.rS32, ctx.rS64);
-        final Register rt64 = parseRegister64(ctx.rD32, ctx.rD64);
-        final Register rt = shrinkRegister(rt64, ctx.rD32, info.isHalfSize, info.isByteSize);
-        Expression operand = expressions.makeCast(rs64, rt.getType(), false);
-        if (info.op == IntBinaryOp.AND) {
-            // This was a CLR instruction
-            operand = expressions.makeIntNot(operand);
-        }
-
-        final Expression address = parseAddress(ctx.address());
-        final RMWFetchOp ldOp = EventFactory.Common.newRmwFetchOp(rt, address, info.op, operand);
-        ldOp.addTags(info.release ? MO_REL : null, info.acquire ? MO_ACQ : null);
-        ldOp.setMetadata(LDOP_PRINTER);
-
-        add(ldOp);
-        addRegister64Update(rt64, rt);
-        return null;
-    }
-
     private static final CustomPrinting STOP_PRINTER = e -> {
         if (!(e instanceof RMWOp stop)) {
             return Optional.empty();
         }
         final String rel = e.hasTag(MO_REL) ? "L" : "";
-        final String op = OpToArmOpCode(stop.getOperator());
+        final String op = opToArmOpCode(stop.getOperator());
         final String size = getArmSizeSuffix(stop.getAccessType());
         final Expression operand = stop.getOperand() instanceof IntUnaryExpr expr ?  expr.getOperand() : stop.getOperand();
         final Expression address = stop.getAddress();
@@ -455,26 +430,49 @@ public Object visitLoadOp(LoadOpContext ctx) {
         return Optional.of(String.format("ST%s%s%s %s, [%s]", op, rel, size, operand, address));
     };
 
+    private static String opToArmOpCode(IntBinaryOp op) {
+        return switch (op) {
+            case ADD -> "ADD";
+            case XOR -> "EOR";
+            case OR -> "SET";
+            case AND -> "CLR";
+            case SMIN -> "SMIN";
+            case SMAX -> "SMAX";
+            case UMIN -> "UMIN";
+            case UMAX -> "UMAX";
+            default -> throw new RuntimeException("Invalid op: " + op);
+        };
+    }
+
     @Override
-    public Object visitStoreOp(StoreOpContext ctx) {
-        final String instr = ctx.storeOpInstruction().getText();
+    public Object visitLoadOp(LoadOpContext ctx) {
+        final String instr = ctx.loadOpInstruction().getText();
         final LDSTAmoInfo info = getLDSTInfoFromInstructionName(instr);
 
         final Register rs64 = parseRegister64(ctx.rS32, ctx.rS64);
-        // TODO: We don't actually care about the smaller register, but only its type!
-        final Register rs = shrinkRegister(rs64, ctx.rS32, info.isHalfSize, info.isByteSize);
-        Expression operand = expressions.makeCast(rs64, rs.getType(), false);
+        final Register rt64 = parseRegister64(ctx.rD32, ctx.rD64);
+        final Register rt = shrinkRegister(rt64, ctx.rD32, info.isHalfSize, info.isByteSize);
+        Expression operand = expressions.makeCast(rs64, rt.getType(), false);
         if (info.op == IntBinaryOp.AND) {
             // This was a CLR instruction
             operand = expressions.makeIntNot(operand);
         }
 
+        final List<String> mo = new ArrayList<>();
+        if (info.acquire) {
+            mo.add(MO_ACQ);
+        }
+        if (info.release) {
+            mo.add(MO_REL);
+        }
+
         final Expression address = parseAddress(ctx.address());
-        final RMWOp stOp = EventFactory.Common.newRmwOp(address, info.op, operand);
-        stOp.addTags(info.release ? MO_REL : null);
-        stOp.setMetadata(STOP_PRINTER);
+        final RMWFetchOp ldOp = EventFactory.Common.newRmwFetchOp(rt, address, info.op, operand);
+        ldOp.addTags(mo);
+        ldOp.setMetadata(LDOP_PRINTER);
 
-        add(stOp);
+        add(ldOp);
+        addRegister64Update(rt64, rt);
         return null;
     }
 
@@ -638,18 +636,29 @@ private Void add(Event event) {
         return null;
     }
 
-    private static String OpToArmOpCode(IntBinaryOp op) {
-        return switch (op) {
-            case ADD -> "ADD";
-            case XOR -> "EOR";
-            case OR -> "SET";
-            case AND -> "CLR";
-            case SMIN -> "SMIN";
-            case SMAX -> "SMAX";
-            case UMIN -> "UMIN";
-            case UMAX -> "UMAX";
-            default -> throw new RuntimeException("Invalid op: " + op);
-        };
+    @Override
+    public Object visitStoreOp(StoreOpContext ctx) {
+        final String instr = ctx.storeOpInstruction().getText();
+        final LDSTAmoInfo info = getLDSTInfoFromInstructionName(instr);
+
+        final Register rs64 = parseRegister64(ctx.rS32, ctx.rS64);
+        // TODO: We don't actually care about the smaller register, but only its type!
+        final Register rs = shrinkRegister(rs64, ctx.rS32, info.isHalfSize, info.isByteSize);
+        Expression operand = expressions.makeCast(rs64, rs.getType(), false);
+        if (info.op == IntBinaryOp.AND) {
+            // This was a CLR instruction
+            operand = expressions.makeIntNot(operand);
+        }
+
+        final Expression address = parseAddress(ctx.address());
+        final RMWOp stOp = EventFactory.Common.newRmwOp(address, info.op, operand);
+        if (info.release) {
+            stOp.addTags(MO_REL);
+        }
+        stOp.setMetadata(STOP_PRINTER);
+
+        add(stOp);
+        return null;
     }
 
     private static String getArmSizeSuffix(Type type) {
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java
index e004cd1652..49a1306a1c 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java
@@ -104,7 +104,7 @@ public List<Event> visitRMWOp(RMWOp rmwOp) {
         final Expression address = rmwOp.getAddress();
         final String storeMo = rmwOp.hasTag(ARMv8.MO_REL) ? ARMv8.MO_REL : "";
 
-        final Load load = propagateNoRet(rmwOp, newRMWLoad(dummy, address));
+        final Load load = newRMWLoad(dummy, address);
         load.addTags(Tag.ARMv8.NO_RET);
         final Expression value = expressions.makeBinary(dummy, rmwOp.getOperator(), rmwOp.getOperand());
 
diff --git a/dartagnan/src/test/resources/ARM8-expected.csv b/dartagnan/src/test/resources/ARM8-expected.csv
index 566acb2866..23255e1884 100644
--- a/dartagnan/src/test/resources/ARM8-expected.csv
+++ b/dartagnan/src/test/resources/ARM8-expected.csv
@@ -7863,8 +7863,6 @@ litmus/AARCH64/mixed/WW+R+dmb.sysw4w0+q0+BIS.litmus,0
 litmus/AARCH64/mixed/WW+R+dmb.sysw4w0+q0.litmus,0
 litmus/AARCH64/mixed/WW+R+posq0w0+q0+SIMPLE.litmus,0
 litmus/AARCH64/mixed/WW+RR-variant.litmus,0
-litmus/AARCH64/mixed/WW+RR-variant.litmus,0
-litmus/AARCH64/mixed/WW+RR-variant.litmus,0
 litmus/AARCH64/mixed/CoRR+amo.swph0h0-posh0a.w0+w0.litmus,0
 litmus/AARCH64/mixed/CoRR+rmwh0h0-posh0a.w0+w0.litmus,0
 litmus/AARCH64/NoRet/MP+rel+CAS-ok-dmb.ld.litmus,0

From 33f7ef032dffe3122d43915d3aaf96d870f31249 Mon Sep 17 00:00:00 2001
From: Thomas Haas <tomy.haas@t-online.de>
Date: Thu, 19 Feb 2026 12:28:25 +0100
Subject: [PATCH 17/17] Changed compilation scheme of CAS/RMWOp and fixed Xchg
 compilation (Arm8)

---
 .../processing/compilation/VisitorArm8.java   | 68 +++++++------------
 1 file changed, 24 insertions(+), 44 deletions(-)

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java
index 49a1306a1c..294d1ff093 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java
@@ -34,7 +34,7 @@ protected VisitorArm8(boolean useRC11Scheme) {
 
     @Override
     public List<Event> visitStoreExclusive(StoreExclusive e) {
-        RMWStoreExclusive store = newRMWStoreExclusiveWithMo(e.getAddress(), e.getMemValue(), false, e.getMo());
+        final RMWStoreExclusive store = newRMWStoreExclusiveWithMo(e.getAddress(), e.getMemValue(), false, e.getMo());
 
         return eventSequence(
                 store,
@@ -44,14 +44,17 @@ public List<Event> visitStoreExclusive(StoreExclusive e) {
 
     @Override
     public List<Event> visitXchg(Xchg xchg) {
-        Register resultRegister = xchg.getResultRegister();
-        Expression address = xchg.getAddress();
-        String loadMo = xchg.hasTag(ARMv8.MO_ACQ) ? ARMv8.MO_ACQ : "";
-        String storeMo = xchg.hasTag(ARMv8.MO_REL) ? ARMv8.MO_REL : "";
+        final Register resultRegister = xchg.getResultRegister();
+        final Expression address = xchg.getAddress();
+        final String loadMo = xchg.hasTag(ARMv8.MO_ACQ) ? ARMv8.MO_ACQ : "";
+        final String storeMo = xchg.hasTag(ARMv8.MO_REL) ? ARMv8.MO_REL : "";
+
+        final Register dummy = xchg.getFunction().newRegister(resultRegister.getType());
 
         return eventSequence(
-                propagateNoRet(xchg, newRMWLoadExclusiveWithMo(resultRegister, address, loadMo)),
-                newRMWStoreExclusiveWithMo(address, xchg.getValue(), true, storeMo)
+                propagateNoRet(xchg, newRMWLoadExclusiveWithMo(dummy, address, loadMo)),
+                newRMWStoreExclusiveWithMo(address, xchg.getValue(), true, storeMo),
+                newLocal(resultRegister, dummy)
         );
     }
 
@@ -63,36 +66,20 @@ public List<Event> visitCas(CAS cas) {
         final String loadMo = cas.hasTag(ARMv8.MO_ACQ) ? ARMv8.MO_ACQ : "";
         final String storeMo = cas.hasTag(ARMv8.MO_REL) ? ARMv8.MO_REL : "";
 
-        Expression cmpValue = cas.getExpectedValue();
-        Local captureCmpVal = null;
-        if (cmpValue.getRegs().contains(resultRegister)) {
-            Register tmpReg = cas.getFunction().newRegister(resultRegister.getType());
-            captureCmpVal = newLocal(tmpReg, cmpValue);
-            cmpValue = tmpReg;
-        }
 
-        Expression newValue = cas.getStoreValue();
-        Local captureNewVal = null;
-        if (newValue.getRegs().contains(resultRegister)) {
-            Register tmpReg = cas.getFunction().newRegister(resultRegister.getType());
-            captureNewVal = newLocal(tmpReg, newValue);
-            newValue = tmpReg;
-        }
-
-        Label casEnd = newLabel("CAS_end");
-        final Expression cmp = expressions.makeEQ(resultRegister, cmpValue);
-        CondJump branchOnCasCmpResult = newJumpUnless(cmp, casEnd);
-
-        Load load = propagateNoRet(cas, newRMWLoadWithMo(resultRegister, address, loadMo));
-        Store store = newRMWStoreWithMo(load, address, newValue, storeMo);
+        final Register dummy = cas.getFunction().newRegister(resultRegister.getType());
+        final Load load = propagateNoRet(cas, newRMWLoadWithMo(dummy, address, loadMo));
+        final Store store = newRMWStoreWithMo(load, address, cas.getStoreValue(), storeMo);
+        final Expression cmp = expressions.makeEQ(dummy, cas.getExpectedValue());
+        final Label casEnd = newLabel("CAS_end");
+        final CondJump branchOnCasCmpResult = newJumpUnless(cmp, casEnd);
 
         return eventSequence(
-                captureCmpVal,
-                captureNewVal,
                 load,
                 branchOnCasCmpResult,
                 store,
-                casEnd
+                casEnd,
+                newLocal(resultRegister, dummy)
         );
     }
 
@@ -100,10 +87,10 @@ public List<Event> visitCas(CAS cas) {
     public List<Event> visitRMWOp(RMWOp rmwOp) {
         Preconditions.checkArgument(!rmwOp.hasTag(ARMv8.MO_ACQ), "Unexpected MO_ACQ tag for RMWOp");
 
-        final Register dummy = rmwOp.getFunction().newRegister(rmwOp.getAccessType());
         final Expression address = rmwOp.getAddress();
         final String storeMo = rmwOp.hasTag(ARMv8.MO_REL) ? ARMv8.MO_REL : "";
 
+        final Register dummy = rmwOp.getFunction().newRegister(rmwOp.getAccessType());
         final Load load = newRMWLoad(dummy, address);
         load.addTags(Tag.ARMv8.NO_RET);
         final Expression value = expressions.makeBinary(dummy, rmwOp.getOperator(), rmwOp.getOperand());
@@ -121,21 +108,14 @@ public List<Event> visitRMWFetchOp(RMWFetchOp rmwOp) {
         final String loadMo = rmwOp.hasTag(ARMv8.MO_ACQ) ? ARMv8.MO_ACQ : "";
         final String storeMo = rmwOp.hasTag(ARMv8.MO_REL) ? ARMv8.MO_REL : "";
 
-        Expression operand = rmwOp.getOperand();
-        Local captureOperand = null;
-        if (operand.getRegs().contains(resultRegister)) {
-            final Register tmpReg = rmwOp.getFunction().newRegister(resultRegister.getType());
-            captureOperand = newLocal(tmpReg, operand);
-            operand = tmpReg;
-        }
-
-        final Load load = propagateNoRet(rmwOp, newRMWLoadWithMo(resultRegister, address, loadMo));
-        final Expression value = expressions.makeBinary(resultRegister, rmwOp.getOperator(), operand);
+        final Register dummy = rmwOp.getFunction().newRegister(resultRegister.getType());
+        final Load load = propagateNoRet(rmwOp, newRMWLoadWithMo(dummy, address, loadMo));
+        final Expression value = expressions.makeBinary(dummy, rmwOp.getOperator(), rmwOp.getOperand());
 
         return eventSequence(
-                captureOperand,
                 propagateNoRet(rmwOp, load),
-                newRMWStoreWithMo(load, address, value, storeMo)
+                newRMWStoreWithMo(load, address, value, storeMo),
+                newLocal(resultRegister, dummy)
         );
     }