Add Liveness for PTX and Vulkan

dartagnan/src/main/antlr4/LitmusPTX.g4

@@ -157,6 +157,7 @@ barrier
 atomInstruction
     :   atomOp
     |   atomCAS
+    |   atomExchange
     ;
 
 atomOp
@@ -167,6 +168,10 @@ atomCAS
     :   atom Period mo Period scope Period Cas register Comma location Comma value Comma value
     ;
 
+atomExchange
+    :   atom Period mo Period scope Period Exch register Comma location Comma value
+    ;
+
 redInstruction
     :   red Period mo Period scope Period operation location Comma value
     ;
@@ -317,6 +322,7 @@ Or      :   'or';
 Xor     :   'xor';
 
 Cas     :   'cas';
+Exch    :   'exch';
 
 Proxy       :   'proxy';
 Generic     :   'generic';

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java

@@ -18,6 +18,7 @@
 import com.dat3m.dartagnan.program.event.EventFactory;
 import com.dat3m.dartagnan.program.event.Tag;
 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;
 import com.dat3m.dartagnan.program.event.arch.ptx.PTXRedOp;
 import com.dat3m.dartagnan.program.event.core.*;
@@ -250,6 +251,21 @@ public Object visitAtomCAS(LitmusPTXParser.AtomCASContext ctx) {
         return programBuilder.addChild(mainThread, atom);
     }
 
+    @Override 
+    public Object visitAtomExchange(LitmusPTXParser.AtomExchangeContext ctx) {
+        Register register_destination = programBuilder.getOrNewRegister(mainThread, ctx.register().getText(), archType);
+        MemoryObject object = programBuilder.getOrNewMemoryObject(ctx.location().getText());
+        Expression value = (Expression) ctx.value().accept(this);
+        String mo = ctx.mo().content;
+        String scope = ctx.scope().content;
+        if (!(mo.equals(Tag.PTX.ACQ) || mo.equals(Tag.PTX.REL) || mo.equals(Tag.PTX.ACQ_REL) || mo.equals(Tag.PTX.RLX))) {
+            throw new ParsingException("Atom instruction doesn't support mo: " + mo);
+        }
+        PTXAtomExch atom = EventFactory.PTX.newAtomExch(object, register_destination, value, mo, scope);
+        atom.addTags(ctx.atom().atomProxy);
+        return programBuilder.addChild(mainThread, atom);
+    }
+
     @Override
     public Object visitRedInstruction(LitmusPTXParser.RedInstructionContext ctx) {
         MemoryObject object = programBuilder.getOrNewMemoryObject(ctx.location().getText());

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java

@@ -284,7 +284,6 @@ public Object visitRmwValue(LitmusVulkanParser.RmwValueContext ctx) {
         Register register = (Register) ctx.register().accept(this);
         MemoryObject location = programBuilder.getOrNewMemoryObject(ctx.location().getText());
         Expression value = (Expression) ctx.value().accept(this);
-        Boolean atomic = true; // RMW is always atomic
         String mo = (ctx.mo() != null) ? ctx.mo().content : "";
         String avvis = (ctx.avvis() != null) ? ctx.avvis().content : "";
         String scope = (ctx.scope() != null) ? ctx.scope().content : "";
@@ -295,7 +294,7 @@ public Object visitRmwValue(LitmusVulkanParser.RmwValueContext ctx) {
         if (!avvis.isEmpty()) {
             rmw.addTags(avvis);
         }
-        tagControl(rmw, atomic, mo, avvis, scope, storageClass, storageClassSemantics, avvisSemantics);
+        tagControl(rmw, true, mo, avvis, scope, storageClass, storageClassSemantics, avvisSemantics);
         return programBuilder.addChild(mainThread, rmw);
     }
 
@@ -304,7 +303,6 @@ public Object visitRmwOp(LitmusVulkanParser.RmwOpContext ctx) {
         Register register = (Register) ctx.register().accept(this);
         MemoryObject location = programBuilder.getOrNewMemoryObject(ctx.location().getText());
         Expression value = (Expression) ctx.value().accept(this);
-        Boolean atomic = true; // RMW is always atomic
         String mo = (ctx.mo() != null) ? ctx.mo().content : "";
         String avvis = (ctx.avvis() != null) ? ctx.avvis().content : "";
         String scope = (ctx.scope() != null) ? ctx.scope().content : "";
@@ -316,7 +314,7 @@ public Object visitRmwOp(LitmusVulkanParser.RmwOpContext ctx) {
         if (!avvis.isEmpty()) {
             rmw.addTags(avvis);
         }
-        tagControl(rmw, atomic, mo, avvis, scope, storageClass, storageClassSemantics, avvisSemantics);
+        tagControl(rmw, true, mo, avvis, scope, storageClass, storageClassSemantics, avvisSemantics);
         return programBuilder.addChild(mainThread, rmw);
     }
 

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java

@@ -12,6 +12,7 @@
 import com.dat3m.dartagnan.program.event.arch.StoreExclusive;
 import com.dat3m.dartagnan.program.event.arch.lisa.LISARMW;
 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;
 import com.dat3m.dartagnan.program.event.arch.vulkan.VulkanRMWOp;
 import com.dat3m.dartagnan.program.event.core.FenceWithId;
@@ -707,6 +708,13 @@ public static PTXAtomCAS newAtomCAS(Expression address, Register register, Expre
             return atom;
         }
 
+        public static PTXAtomExch newAtomExch(Expression address, Register register,
+                                            Expression value, String mo, String scope) {
+            PTXAtomExch atom = new PTXAtomExch(register, address, value, mo);
+            atom.addTags(scope);
+            return atom;
+        }
+
         public static PTXRedOp newRedOp(Expression address, Expression value,
                                         IOpBin op, String mo, String scope) {
             // PTX (currently) only generates memory orders ACQ_REL and RLX for red.

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXAtomExch.java

@@ -0,0 +1,33 @@
+package com.dat3m.dartagnan.program.event.arch.ptx;
+
+import com.dat3m.dartagnan.expression.Expression;
+import com.dat3m.dartagnan.program.Register;
+import com.dat3m.dartagnan.program.event.common.RMWXchgBase;
+import com.dat3m.dartagnan.program.event.visitors.EventVisitor;
+
+public class PTXAtomExch extends RMWXchgBase {
+
+    public PTXAtomExch(Register register, Expression address, Expression value, String mo) {
+        super(register, address, value, mo);
+    }
+
+    protected PTXAtomExch(PTXAtomExch other) {
+        super(other);
+    }
+
+    @Override
+    public String defaultString() {
+        return String.format("%s := atom_exch_%s(%s, %s)", resultRegister, mo, storeValue, address);
+    }
+
+    @Override
+    public PTXAtomExch getCopy(){
+        return new PTXAtomExch(this);
+    }
+
+    @Override
+    public <T> T accept(EventVisitor<T> visitor) {
+        return visitor.visitPtxAtomExch(this);
+    }
+
+}

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/visitors/EventVisitor.java

@@ -95,13 +95,14 @@ public interface EventVisitor<T> {
     default T visitEndAtomic(EndAtomic e) { return visitEvent(e); }
 
 	// ------------------ Std events ------------------
-	default T visitAlloc(Alloc e) { return visitEvent(e); }
+    default T visitAlloc(Alloc e) { return visitEvent(e); }
 
     // ------------------ GPU Events ------------------
     default T visitFenceWithId(FenceWithId e) { return visitEvent(e); }
-	default T visitPtxRedOp(PTXRedOp e) { return visitMemEvent(e); }
-	default T visitPtxAtomOp(PTXAtomOp e) { return visitMemEvent(e); }
-	default T visitPtxAtomCAS(PTXAtomCAS e) { return visitMemEvent(e); }
+    default T visitPtxRedOp(PTXRedOp e) { return visitMemEvent(e); }
+    default T visitPtxAtomOp(PTXAtomOp e) { return visitMemEvent(e); }
+    default T visitPtxAtomCAS(PTXAtomCAS e) { return visitMemEvent(e); }
+    default T visitPtxAtomExch(PTXAtomExch e) { return visitMemEvent(e); }
     default T visitVulkanRMW(VulkanRMW e) { return visitMemEvent(e); }
     default T visitVulkanRMWOp(VulkanRMWOp e) { return visitMemEvent(e); }
 }

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPTX.java

@@ -5,6 +5,7 @@
 import com.dat3m.dartagnan.program.Register;
 import com.dat3m.dartagnan.program.event.Tag;
 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;
 import com.dat3m.dartagnan.program.event.arch.ptx.PTXRedOp;
 import com.dat3m.dartagnan.program.event.core.Event;
@@ -59,6 +60,24 @@ public List<Event> visitPtxAtomCAS(PTXAtomCAS e) {
                 store);
     }
 
+    // PTX Exch semantics
+    @Override
+    public List<Event> visitPtxAtomExch(PTXAtomExch e) {
+        Register resultRegister = e.getResultRegister();
+        String mo = e.getMo();
+        Expression address = e.getAddress();
+        Register dummy = e.getFunction().newRegister(resultRegister.getType());
+        Load load = newRMWLoadWithMo(dummy, address, Tag.PTX.loadMO(mo));
+        RMWStore store = newRMWStoreWithMo(load, address, e.getValue(), Tag.PTX.storeMO(mo));
+        this.propagateTags(e, load);
+        this.propagateTags(e, store);
+        return eventSequence(
+                load,
+                store,
+                newLocal(resultRegister, dummy)
+        );
+    }
+
     @Override
     public List<Event> visitPtxRedOp(PTXRedOp e) {
         Expression address = e.getAddress();

dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusPTXv6_0LivenessTest.java

@@ -0,0 +1,41 @@
+package com.dat3m.dartagnan.litmus;
+
+import com.dat3m.dartagnan.configuration.Arch;
+import com.dat3m.dartagnan.configuration.Property;
+import com.dat3m.dartagnan.utils.Result;
+import com.dat3m.dartagnan.utils.rules.Provider;
+import com.dat3m.dartagnan.utils.rules.Providers;
+import com.dat3m.dartagnan.wmm.Wmm;
+import org.junit.runner.RunWith;
+import org.junit.runners.Parameterized;
+
+import java.io.IOException;
+import java.util.EnumSet;
+
+@RunWith(Parameterized.class)
+public class LitmusPTXv6_0LivenessTest extends AbstractLitmusTest {
+
+    public LitmusPTXv6_0LivenessTest(String path, Result expected) {
+        super(path, expected);
+    }
+
+    @Parameterized.Parameters(name = "{index}: {0}, {1}")
+    public static Iterable<Object[]> data() throws IOException {
+        return buildLitmusTests("litmus/PTX/", "PTXv6_0-Liveness");
+    }
+
+    @Override
+    protected Provider<Arch> getTargetProvider() {
+        return () -> Arch.PTX;
+    }
+
+    @Override
+    protected Provider<EnumSet<Property>> getPropertyProvider() {
+        return Provider.fromSupplier(() -> EnumSet.of(Property.LIVENESS));
+    }
+
+    @Override
+    protected Provider<Wmm> getWmmProvider() {
+        return Providers.createWmmFromName(() -> "ptx-v6.0");
+    }
+}

dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusPTXv7_5LivenessTest.java

@@ -0,0 +1,41 @@
+package com.dat3m.dartagnan.litmus;
+
+import com.dat3m.dartagnan.configuration.Arch;
+import com.dat3m.dartagnan.configuration.Property;
+import com.dat3m.dartagnan.utils.Result;
+import com.dat3m.dartagnan.utils.rules.Provider;
+import com.dat3m.dartagnan.utils.rules.Providers;
+import com.dat3m.dartagnan.wmm.Wmm;
+import org.junit.runner.RunWith;
+import org.junit.runners.Parameterized;
+
+import java.io.IOException;
+import java.util.EnumSet;
+
+@RunWith(Parameterized.class)
+public class LitmusPTXv7_5LivenessTest extends AbstractLitmusTest {
+
+    public LitmusPTXv7_5LivenessTest(String path, Result expected) {
+        super(path, expected);
+    }
+
+    @Parameterized.Parameters(name = "{index}: {0}, {1}")
+    public static Iterable<Object[]> data() throws IOException {
+        return buildLitmusTests("litmus/PTX/", "PTXv7_5-Liveness");
+    }
+
+    @Override
+    protected Provider<Arch> getTargetProvider() {
+        return () -> Arch.PTX;
+    }
+
+    @Override
+    protected Provider<EnumSet<Property>> getPropertyProvider() {
+        return Provider.fromSupplier(() -> EnumSet.of(Property.LIVENESS));
+    }
+
+    @Override
+    protected Provider<Wmm> getWmmProvider() {
+        return Providers.createWmmFromName(() -> "ptx-v7.5");
+    }
+}

dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusVulkanLivenessTest.java

@@ -0,0 +1,34 @@
+package com.dat3m.dartagnan.litmus;
+
+import com.dat3m.dartagnan.configuration.Arch;
+import com.dat3m.dartagnan.configuration.Property;
+import com.dat3m.dartagnan.utils.Result;
+import com.dat3m.dartagnan.utils.rules.Provider;
+import org.junit.runner.RunWith;
+import org.junit.runners.Parameterized;
+
+import java.io.IOException;
+import java.util.EnumSet;
+
+@RunWith(Parameterized.class)
+public class LitmusVulkanLivenessTest extends AbstractLitmusTest {
+
+    public LitmusVulkanLivenessTest(String path, Result expected) {
+        super(path, expected);
+    }
+
+    @Parameterized.Parameters(name = "{index}: {0}, {1}")
+    public static Iterable<Object[]> data() throws IOException {
+        return buildLitmusTests("litmus/VULKAN/", "VULKAN-Liveness");
+    }
+
+    @Override
+    protected Provider<Arch> getTargetProvider() {
+        return () -> Arch.VULKAN;
+    }
+
+    @Override
+    protected Provider<EnumSet<Property>> getPropertyProvider() {
+        return Provider.fromSupplier(() -> EnumSet.of(Property.LIVENESS));
+    }
+}

dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusVulkanRacesNochainsTest.java

@@ -17,7 +17,7 @@ public class LitmusVulkanRacesNochainsTest extends AbstractLitmusTest {
 
     @Parameterized.Parameters(name = "{index}: {0}, {1}")
     public static Iterable<Object[]> data() throws IOException {
-        return buildLitmusTests("litmus/VULKAN/DR/", "VULKAN", "-DR-NOCHAINS");
+        return buildLitmusTests("litmus/VULKAN/Data-Race/", "VULKAN", "-DR-NOCHAINS");
     }
 
     @Override

dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusVulkanRacesTest.java

@@ -15,7 +15,7 @@ public class LitmusVulkanRacesTest extends AbstractLitmusTest {
 
     @Parameterized.Parameters(name = "{index}: {0}, {1}")
     public static Iterable<Object[]> data() throws IOException {
-        return buildLitmusTests("litmus/VULKAN/DR/", "VULKAN", "-DR");
+        return buildLitmusTests("litmus/VULKAN/Data-Race/", "VULKAN", "-DR");
     }
 
     @Override