From 1b4552f7da9375bf7bfbf8c1b9bc8f82a80d3efd Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Mon, 2 Sep 2024 16:11:26 +0200 Subject: [PATCH 1/2] Add support to CAAT for SyncBar and SyncFence relations (by cutting them). --- .../verification/solving/RefinementSolver.java | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 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 index bebb12fd78..24cebd241a 100644 --- 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; // 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,7 +523,8 @@ private static void addBiases(Wmm memoryModel, EnumSet biases) { memoryModel.getOrCreatePredefinedRelation(POLOC), rf, memoryModel.getOrCreatePredefinedRelation(CO), - memoryModel.getOrCreatePredefinedRelation(FR))))); + memoryModel.getOrCreatePredefinedRelation(FR) + )))); } if (biases.contains(Baseline.NO_OOTA)) { // ---- acyclic (dep | rf) ---- @@ -524,7 +532,8 @@ private static void addBiases(Wmm memoryModel, EnumSet biases) { memoryModel.getOrCreatePredefinedRelation(CTRL), memoryModel.getOrCreatePredefinedRelation(DATA), memoryModel.getOrCreatePredefinedRelation(ADDR), - rf)))); + rf) + ))); } if (biases.contains(Baseline.ATOMIC_RMW)) { // ---- empty (rmw & fre;coe) ---- From 8680657df2b8cb7f561144488321d03cf93f8f90 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Mon, 2 Sep 2024 17:27:27 +0200 Subject: [PATCH 2/2] - Added cutting of vloc relation (Refinement still fails to understand virtual memory properly) - Enabled Spirv tests --- .../dartagnan/verification/solving/RefinementSolver.java | 2 +- .../com/dat3m/dartagnan/spirv/basic/SpirvAssertionsTest.java | 4 ++-- .../dat3m/dartagnan/spirv/benchmarks/SpirvAssertionsTest.java | 4 ++-- .../com/dat3m/dartagnan/spirv/benchmarks/SpirvChecksTest.java | 4 ++-- .../com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java | 4 ++-- .../com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java | 4 ++-- .../com/dat3m/dartagnan/spirv/gpuverify/SpirvRacesTest.java | 4 ++-- 7 files changed, 13 insertions(+), 13 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 index 24cebd241a..f432c68d0f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java @@ -473,7 +473,7 @@ 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; // GPUs + || def instanceof SyncFence || def instanceof SyncBar || def instanceof SameVirtualLocation; // GPUs } private static RefinementModel generateRefinementModel(Wmm original) { 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 index 18878d7f92..9c2f3fa06c 100644 --- 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 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 index 96acad8bbc..9006c1b99f 100644 --- 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 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 index 6043e53303..c217abd6f7 100644 --- 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 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 index 5f4ac94440..a5c88e5f77 100644 --- 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 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 index 6124efb5b0..b682b3505e 100644 --- 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 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 index 29b7ad7990..da21d9fb30 100644 --- 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 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()); }