From 7887589f634344384acfa274a4f0d5ebc745d896 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Thu, 5 Sep 2024 10:46:00 +0200 Subject: [PATCH 1/2] Add support to CAAT for SyncBar, SyncFence and Vloc relations (#724) --- .../verification/solving/RefinementSolver.java | 15 ++++++++++++--- .../spirv/basic/SpirvAssertionsTest.java | 4 ++-- .../spirv/benchmarks/SpirvAssertionsTest.java | 4 ++-- .../spirv/benchmarks/SpirvChecksTest.java | 4 ++-- .../spirv/benchmarks/SpirvRacesTest.java | 4 ++-- .../spirv/gpuverify/SpirvChecksTest.java | 4 ++-- .../dartagnan/spirv/gpuverify/SpirvRacesTest.java | 4 ++-- 7 files changed, 24 insertions(+), 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 index bebb12fd78..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 @@ -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,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) ---- 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()); } From 1bd4bd02171badff84a45d9789afe058e9621266 Mon Sep 17 00:00:00 2001 From: natgavrilenko Date: Thu, 5 Sep 2024 16:17:29 +0200 Subject: [PATCH 2/2] Add unrolling bound to program spec encoding (#727) --- .../dartagnan/encoding/PropertyEncoder.java | 6 +++-- .../spirv/basic/SpirvAssertionsTest.java | 24 +++++++------------ 2 files changed, 12 insertions(+), 18 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java index 36427a5adf..994f9da6bd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java @@ -36,6 +36,7 @@ import static com.dat3m.dartagnan.configuration.Property.*; import static com.dat3m.dartagnan.program.Program.SourceLanguage.LLVM; +import static com.dat3m.dartagnan.program.Program.SpecificationType.ASSERT; import static com.dat3m.dartagnan.wmm.RelationNameRepository.CO; public class PropertyEncoder implements Encoder { @@ -275,7 +276,7 @@ private TrackableFormula encodeProgramSpecification() { case FORALL, NOT_EXISTS, ASSERT -> bmgr.not(PROGRAM_SPEC.getSMTVariable(context)); case EXISTS -> PROGRAM_SPEC.getSMTVariable(context); }; - if (!program.getFormat().equals(LLVM)) { + if (!ASSERT.equals(program.getSpecificationType())) { encoding = bmgr.and(encoding, encodeProgramTermination()); } return new TrackableFormula(trackingLiteral, encoding); @@ -283,9 +284,10 @@ private TrackableFormula encodeProgramSpecification() { private BooleanFormula encodeProgramTermination() { final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); - return bmgr.and(program.getThreads().stream() + BooleanFormula exitReached = bmgr.and(program.getThreads().stream() .map(t -> bmgr.equivalence(context.execution(t.getEntry()), context.execution(t.getExit()))) .toList()); + return bmgr.and(exitReached, bmgr.not(encodeBoundEventExec())); } // ====================================================================== 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 9c2f3fa06c..e86077b009 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 @@ -28,8 +28,7 @@ import static com.dat3m.dartagnan.configuration.Property.PROGRAM_SPEC; import static com.dat3m.dartagnan.utils.ResourceHelper.getRootPath; import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath; -import static com.dat3m.dartagnan.utils.Result.FAIL; -import static com.dat3m.dartagnan.utils.Result.PASS; +import static com.dat3m.dartagnan.utils.Result.*; import static org.junit.Assert.assertEquals; @RunWith(Parameterized.class) @@ -79,30 +78,23 @@ public static Iterable data() throws IOException { {"builtin-all-321.spv.dis", 1, PASS}, {"branch-cond-ff.spv.dis", 1, PASS}, {"branch-cond-ff-inverted.spv.dis", 1, PASS}, - {"branch-cond-bf.spv.dis", 1, FAIL}, + {"branch-cond-bf.spv.dis", 1, UNKNOWN}, {"branch-cond-bf.spv.dis", 2, PASS}, - {"branch-cond-bf.spv.dis", 3, PASS}, - {"branch-cond-fb.spv.dis", 1, FAIL}, + {"branch-cond-fb.spv.dis", 1, UNKNOWN}, {"branch-cond-fb.spv.dis", 2, PASS}, - {"branch-cond-fb.spv.dis", 3, PASS}, {"branch-cond-struct.spv.dis", 1, PASS}, {"branch-cond-struct-read-write.spv.dis", 1, PASS}, {"branch-race.spv.dis", 1, PASS}, - {"branch-loop.spv.dis", 2, FAIL}, + {"branch-loop.spv.dis", 2, UNKNOWN}, {"branch-loop.spv.dis", 3, PASS}, - {"branch-loop.spv.dis", 4, PASS}, - {"loop-struct-cond.spv.dis", 1, FAIL}, + {"loop-struct-cond.spv.dis", 1, UNKNOWN}, {"loop-struct-cond.spv.dis", 2, PASS}, - {"loop-struct-cond.spv.dis", 3, PASS}, - {"loop-struct-cond-suffix.spv.dis", 1, FAIL}, + {"loop-struct-cond-suffix.spv.dis", 1, UNKNOWN}, {"loop-struct-cond-suffix.spv.dis", 2, PASS}, - {"loop-struct-cond-suffix.spv.dis", 3, PASS}, - {"loop-struct-cond-sequence.spv.dis", 2, FAIL}, + {"loop-struct-cond-sequence.spv.dis", 2, UNKNOWN}, {"loop-struct-cond-sequence.spv.dis", 3, PASS}, - {"loop-struct-cond-sequence.spv.dis", 4, PASS}, - {"loop-struct-cond-nested.spv.dis", 2, FAIL}, + {"loop-struct-cond-nested.spv.dis", 2, UNKNOWN}, {"loop-struct-cond-nested.spv.dis", 3, PASS}, - {"loop-struct-cond-nested.spv.dis", 4, PASS}, {"phi.spv.dis", 1, PASS}, {"phi-unstruct-true.spv.dis", 1, PASS}, {"phi-unstruct-false.spv.dis", 1, PASS},