Add support to CAAT for SyncBar, SyncFence and Vloc relations (#724)

hernanponcedeleon · Sep 5, 2024 · 7887589 · 7887589
1 parent 5e10cda
commit 7887589
Show file tree

Hide file tree

Showing 7 changed files with 24 additions and 15 deletions.
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java
@@ -469,6 +469,13 @@ private RefinementIteration doRefinementIteration(ProverEnvironment prover, WMMS
     // ================================================================================================================
     // Special memory model processing
 
+    private static boolean isUnknownDefinitionForCAAT(Definition def) {
+        // TODO: We should probably automatically cut all "unknown relation",
+        //  i.e., use a white-list of known relations instead of a blacklist of unknown one's.
+        return def instanceof LinuxCriticalSections // LKMM
+                || def instanceof SyncFence || def instanceof SyncBar || def instanceof SameVirtualLocation; // GPUs
+    }
+
     private static RefinementModel generateRefinementModel(Wmm original) {
         // We cut (i) negated axioms, (ii) negated relations (if derived),
         // and (iii) some special relations because they are derived from internal relations (like data/addr/ctrl)
@@ -492,7 +499,7 @@ private static RefinementModel generateRefinementModel(Wmm original) {
             } else if (c instanceof Definition def && def.getDefinedRelation().hasName()) {
                 // (iii) Special relations
                 final String name = def.getDefinedRelation().getName().get();
-                if (name.equals(DATA) || name.equals(CTRL) || name.equals(ADDR) || name.equals(CRIT)) {
+                if (name.equals(DATA) || name.equals(CTRL) || name.equals(ADDR) || isUnknownDefinitionForCAAT(def)) {
                     constraintsToCut.add(c);
                 }
             } else if (c instanceof Definition def && def instanceof Fences) {
@@ -516,15 +523,17 @@ private static void addBiases(Wmm memoryModel, EnumSet<Baseline> biases) {
                     memoryModel.getOrCreatePredefinedRelation(POLOC),
                     rf,
                     memoryModel.getOrCreatePredefinedRelation(CO),
-                    memoryModel.getOrCreatePredefinedRelation(FR)))));
+                    memoryModel.getOrCreatePredefinedRelation(FR)
+            ))));
         }
         if (biases.contains(Baseline.NO_OOTA)) {
             // ---- acyclic (dep | rf) ----
             memoryModel.addConstraint(new Acyclicity(memoryModel.addDefinition(new Union(memoryModel.newRelation(),
                     memoryModel.getOrCreatePredefinedRelation(CTRL),
                     memoryModel.getOrCreatePredefinedRelation(DATA),
                     memoryModel.getOrCreatePredefinedRelation(ADDR),
-                    rf))));
+                    rf)
+            )));
         }
         if (biases.contains(Baseline.ATOMIC_RMW)) {
             // ---- empty (rmw & fre;coe) ----

diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java
@@ -7,6 +7,7 @@
 import com.dat3m.dartagnan.utils.Result;
 import com.dat3m.dartagnan.verification.VerificationTask;
 import com.dat3m.dartagnan.verification.solving.AssumeSolver;
+import com.dat3m.dartagnan.verification.solving.RefinementSolver;
 import com.dat3m.dartagnan.wmm.Wmm;
 import org.junit.Test;
 import org.junit.runner.RunWith;
@@ -120,10 +121,9 @@ public static Iterable<Object[]> data() throws IOException {
 
     @Test
     public void testAllSolvers() throws Exception {
-        /* TODO: Implementation
         try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
             assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult());
-        }*/
+        }
         try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
             assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult());
         }

diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java
@@ -7,6 +7,7 @@
 import com.dat3m.dartagnan.utils.Result;
 import com.dat3m.dartagnan.verification.VerificationTask;
 import com.dat3m.dartagnan.verification.solving.AssumeSolver;
+import com.dat3m.dartagnan.verification.solving.RefinementSolver;
 import com.dat3m.dartagnan.wmm.Wmm;
 import org.junit.Test;
 import org.junit.runner.RunWith;
@@ -113,10 +114,9 @@ public static Iterable<Object[]> data() throws IOException {
 
     @Test
     public void testAllSolvers() throws Exception {
-        /* TODO: Implementation
         try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
              assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult());
-        }*/
+        }
         try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
             assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult());
         }

diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java
@@ -7,6 +7,7 @@
 import com.dat3m.dartagnan.utils.Result;
 import com.dat3m.dartagnan.verification.VerificationTask;
 import com.dat3m.dartagnan.verification.solving.AssumeSolver;
+import com.dat3m.dartagnan.verification.solving.RefinementSolver;
 import com.dat3m.dartagnan.wmm.Wmm;
 import org.junit.Test;
 import org.junit.runner.RunWith;
@@ -117,10 +118,9 @@ public static Iterable<Object[]> data() throws IOException {
 
     @Test
     public void testAllSolvers() throws Exception {
-        /* TODO: Implementation
         try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
             assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult());
-        }*/
+        }
         try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
             assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult());
         }

diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java
@@ -7,6 +7,7 @@
 import com.dat3m.dartagnan.utils.Result;
 import com.dat3m.dartagnan.verification.VerificationTask;
 import com.dat3m.dartagnan.verification.solving.AssumeSolver;
+import com.dat3m.dartagnan.verification.solving.RefinementSolver;
 import com.dat3m.dartagnan.wmm.Wmm;
 import org.junit.Test;
 import org.junit.runner.RunWith;
@@ -118,10 +119,9 @@ public static Iterable<Object[]> data() throws IOException {
 
     @Test
     public void testAllSolvers() throws Exception {
-        /* TODO: Implementation
         try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
             assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult());
-        }*/
+        }
         try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
             assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult());
         }

diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java
@@ -7,6 +7,7 @@
 import com.dat3m.dartagnan.utils.Result;
 import com.dat3m.dartagnan.verification.VerificationTask;
 import com.dat3m.dartagnan.verification.solving.AssumeSolver;
+import com.dat3m.dartagnan.verification.solving.RefinementSolver;
 import com.dat3m.dartagnan.wmm.Wmm;
 import org.junit.Test;
 import org.junit.runner.RunWith;
@@ -345,10 +346,9 @@ public static Iterable<Object[]> data() throws IOException {
 
     @Test
     public void testAllSolvers() throws Exception {
-        /* TODO: Implementation
         try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
             assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult());
-        }*/
+        }
         try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
             assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult());
         }

diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java
@@ -7,6 +7,7 @@
 import com.dat3m.dartagnan.utils.Result;
 import com.dat3m.dartagnan.verification.VerificationTask;
 import com.dat3m.dartagnan.verification.solving.AssumeSolver;
+import com.dat3m.dartagnan.verification.solving.RefinementSolver;
 import com.dat3m.dartagnan.wmm.Wmm;
 import org.junit.Test;
 import org.junit.runner.RunWith;
@@ -345,10 +346,9 @@ public static Iterable<Object[]> data() throws IOException {
 
     @Test
     public void testAllSolvers() throws Exception {
-        /* TODO: Implementation
         try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
             assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult());
-        }*/
+        }
         try (SolverContext ctx = mkCtx(); ProverEnvironment prover = mkProver(ctx)) {
             assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult());
         }