From 995eb74176b50ccf4cd06458d1f47f00f023b597 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 13 Feb 2024 13:24:35 -0800 Subject: [PATCH 1/6] Concurrent data structure for per-split coverage MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Normally, Boogie generates only one task per split, so per-split data structures won’t be accessed concurrently. However, when using /randomizeVcIterations together with /trackVerificationCoverage, multiple tasks may concurrently update the `CoveredElements` property. This change will result in tracking the union of covered elements across all VC generation iterations, but that seems like reasonable behavior for a very rare use case. --- Source/Houdini/HoudiniSession.cs | 3 ++- Source/VCGeneration/ProofRun.cs | 3 ++- Source/VCGeneration/Split.cs | 3 ++- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/Source/Houdini/HoudiniSession.cs b/Source/Houdini/HoudiniSession.cs index 5c1032115..48c1ef648 100644 --- a/Source/Houdini/HoudiniSession.cs +++ b/Source/Houdini/HoudiniSession.cs @@ -1,4 +1,5 @@ using System; +using System.Collections.Concurrent; using System.Diagnostics.Contracts; using System.Collections.Generic; using System.IO; @@ -126,7 +127,7 @@ public class HoudiniStatistics private readonly Houdini houdini; public HoudiniStatistics stats; public List Counterexamples { get; } = new(); - public HashSet CoveredElements { get; } = new(); + public ConcurrentBag CoveredElements { get; } = new(); private VCExpr conjecture; private ProverInterface.ErrorHandler handler; VerificationResultCollector collector; diff --git a/Source/VCGeneration/ProofRun.cs b/Source/VCGeneration/ProofRun.cs index f1f38e9af..7972a4c45 100644 --- a/Source/VCGeneration/ProofRun.cs +++ b/Source/VCGeneration/ProofRun.cs @@ -1,3 +1,4 @@ +using System.Collections.Concurrent; using System.Collections.Generic; using Microsoft.Boogie; @@ -8,5 +9,5 @@ public interface ProofRun { List Counterexamples { get; } - HashSet CoveredElements { get; } + ConcurrentBag CoveredElements { get; } } \ No newline at end of file diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 4ccd1cc09..70af021c1 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -1,4 +1,5 @@ using System; +using System.Collections.Concurrent; using System.Collections.Generic; using System.Diagnostics; using System.Linq; @@ -912,7 +913,7 @@ public VerificationRunResult ReadOutcome(int iteration, Checker checker, Verifie public List Counterexamples { get; } = new(); - public HashSet CoveredElements { get; } = new(); + public ConcurrentBag CoveredElements { get; } = new(); /// /// As a side effect, updates "this.parent.CumulativeAssertionCount". From f1e5a59e97c955b4033ab8e4af435d7b8e3f4cb6 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 13 Feb 2024 13:28:53 -0800 Subject: [PATCH 2/6] Add test --- .../verificationCoverageConcurrent.bpl | 106 ++++++++++++++++++ 1 file changed, 106 insertions(+) create mode 100644 Test/coverage/verificationCoverageConcurrent.bpl diff --git a/Test/coverage/verificationCoverageConcurrent.bpl b/Test/coverage/verificationCoverageConcurrent.bpl new file mode 100644 index 000000000..ea5532c44 --- /dev/null +++ b/Test/coverage/verificationCoverageConcurrent.bpl @@ -0,0 +1,106 @@ +// Use many cores to be more likely to trigger concurrent access. +// Success is simply that it doesn't crash. +// RUN: %boogie -vcsCores:8 -trackVerificationCoverage -randomizeVcIterations:10 "%s" + +procedure testRequiresAssign(n: int) + requires {:id "r0"} n > 0; // covered + requires {:id "r_not_1"} n < 10; // not covered +{ + var x: int; + x := {:id "a0"} n + 1; // covered + assert {:id "assert_a0"} x == n + 1; // covered + x := {:id "a_not_1"} 0; // not covered + assert {:id "assert_r0"} n > 0; // covered +} + +procedure sum(n: int) returns (s: int) + requires {:id "spre1"} n >= 0; // covered + ensures {:id "spost"} s == (n * (n + 1)) div 2; // covered +{ + var i: int; + var foo: int; + + i := 0; + s := 0; + foo := 27; + while (i < n) + invariant {:id "sinv1"} 0 <= i && i <= n; // covered: established, maintained, assumed + invariant {:id "sinv2"} s == (i * (i + 1)) div 2; // covered: established, maintained, assumed + invariant {:id "sinv_not_1"} n >= 0; // covered: established, maintained, NOT assumed + { + i := i + 1; + s := s + i; + foo := {:id "update_foo"} foo * 2; // not covered + } +} + +procedure contradictoryAssume(n: int) +{ + assume {:id "cont_assume_1"} n > 0; // covered + assume {:id "cont_assume_2"} n < 0; // covered + assume {:id "unreach_assume_1"} n == 5; // not covered + assert {:id "unreach_assert_1"} n < 10; // not covered +} + +// NB: an explicit `requires false` leads to _nothing_ being covered +procedure falseRequires(n: int) + requires {:id "false_req"} n != n; // covered +{ + assert {:id "false_assert"} false; // not covered +} + +procedure contradictoryRequires(n: int) + requires {:id "cont_req_1"} n > 0; // covered + requires {:id "cont_req_2"} n < 0; // covered +{ + assume {:id "n_eq_5"} n == 5; // not covered + assert {:id "n_lt_10"} n > 10; // not covered +} + +procedure assumeFalse() { + assume {:id "assumeFalse"} false; // covered + assert {:id "assertSimple"} 1 + 1 == 2; // not covered +} + +procedure testEnsuresCallee(n: int) returns (r: int) + requires {:id "ter0"} n > 0; // covered + ensures {:id "tee0"} r > n; // covered by this procedure and caller + ensures {:id "tee1"} r > 0; // covered when proving this procedure, not from caller +{ + r := n + 1; +} + +procedure testEnsuresCaller(n: int) returns (r: int) + requires {:id "ter1"} n > 0; // covered + ensures {:id "tee_not_1"} r > n; // covered +{ + var x: int; + var y: int; + call {:id "call1"} x := testEnsuresCallee(n+1); // requires and ensures covered + call {:id "call2"} y := testEnsuresCallee(n+1); // requires and ensures covered + assert {:id "call2_tee1"} y > 0; + r := {:id "xy_sum"} x + y; // covered +} + +procedure obviouslyUnconstrainedCode(x: int) returns (a: int, b: int) + requires {:id "x_gt_10"} x > 10; // covered + requires {:id "x_lt_100"} x < 100; // not covered + ensures {:id "a_gt_10"} a > 10; // covered +{ + a := {:id "constrained"} x + 1; // covered: constrained by ensures clause + b := {:id "not_constrained"} x - 1; // not covered: not constrained by ensures clause +} + + +procedure contradictoryEnsuresClause(x: int) returns (r: int); + requires {:id "xpos_abs"} x > 1; // covered (established by caller) + ensures {:id "cont_ens_abs"} r > x && r < 0; // covered (used by caller proof) + +// Call function that has contradictory ensures clauses. +procedure callContradictoryFunction(x: int) returns (r: int) + requires {:id "xpos_caller"} x > 1; // covered + ensures {:id "caller_ensures"} r < 0; // not covered +{ + call {:id "call_cont"} r := contradictoryEnsuresClause(x); // requires and ensures covered + r := {:id "unreachable_assignment"} r - 1; // not covered +} From 5de1b5fc1e30a5d67ad6c3b8e72fdd2fb3b771e5 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 15 Feb 2024 15:31:19 -0800 Subject: [PATCH 3/6] Clone Split instead of using ConcurrentBag --- Source/Houdini/HoudiniSession.cs | 2 +- Source/VCGeneration/ProofRun.cs | 2 +- Source/VCGeneration/Split.cs | 35 ++++++++++++++++++++- Source/VCGeneration/SplitAndVerifyWorker.cs | 3 +- 4 files changed, 38 insertions(+), 4 deletions(-) diff --git a/Source/Houdini/HoudiniSession.cs b/Source/Houdini/HoudiniSession.cs index 48c1ef648..d5c5aba1a 100644 --- a/Source/Houdini/HoudiniSession.cs +++ b/Source/Houdini/HoudiniSession.cs @@ -127,7 +127,7 @@ public class HoudiniStatistics private readonly Houdini houdini; public HoudiniStatistics stats; public List Counterexamples { get; } = new(); - public ConcurrentBag CoveredElements { get; } = new(); + public HashSet CoveredElements { get; } = new(); private VCExpr conjecture; private ProverInterface.ErrorHandler handler; VerificationResultCollector collector; diff --git a/Source/VCGeneration/ProofRun.cs b/Source/VCGeneration/ProofRun.cs index 7972a4c45..3c59f865c 100644 --- a/Source/VCGeneration/ProofRun.cs +++ b/Source/VCGeneration/ProofRun.cs @@ -9,5 +9,5 @@ public interface ProofRun { List Counterexamples { get; } - ConcurrentBag CoveredElements { get; } + HashSet CoveredElements { get; } } \ No newline at end of file diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 70af021c1..cd93fe7f0 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -89,6 +89,39 @@ public Split(VCGenOptions options, List /*!*/ blocks, randomGen = new Random(RandomSeed ?? 0); } + public Split(Split oldSplit) + { + Options = oldSplit.Options; + randomGen = oldSplit.randomGen; + Run = oldSplit.Run; + Blocks = oldSplit.Blocks; // Could be deep, but doesn't need to be here. + bigBlocks = oldSplit.bigBlocks; // Could be deep, but doesn't need to be here. + TopLevelDeclarations = oldSplit.TopLevelDeclarations; // Could be deep, but doesn't need to be here. + stats = oldSplit.stats; // Could be deep, but doesn't need to be here. + splitBlock = oldSplit.splitBlock; + assertToAssume = oldSplit.assertToAssume; + assumizedBranches = oldSplit.assumizedBranches; // Could be deep, but doesn't need to be here. + score = oldSplit.score; + scoreComputed = oldSplit.scoreComputed; + totalCost = oldSplit.totalCost; + assertionCount = oldSplit.assertionCount; + assertionCost = oldSplit.assertionCost; + GotoCmdOrigins = oldSplit.GotoCmdOrigins; // Could be deep, but doesn't need to be here. + parent = oldSplit.parent; // Could be deep, but doesn't need to be here. + copies = oldSplit.copies; // Could be deep, but doesn't need to be here. + doingSlice = oldSplit.doingSlice; + sliceInitialLimit = oldSplit.sliceInitialLimit; + sliceLimit = oldSplit.sliceLimit; + slicePos = oldSplit.slicePos; + protectedFromAssertToAssume = oldSplit.protectedFromAssertToAssume; // Could be deep, but doesn't need to be here. + keepAtAll = oldSplit.keepAtAll; // Could be deep, but doesn't need to be here. + SplitIndex = oldSplit.SplitIndex; + reporter = oldSplit.reporter; + bsid = oldSplit.bsid; + Counterexamples = new(); // Create fresh, so it can be updated. + CoveredElements = new(); // Create fresh, so it can be updated. + } + private void PrintTopLevelDeclarationsForPruning(Program program, Implementation implementation, string suffix) { if (!Options.Prune || Options.PrintPrunedFile == null) @@ -913,7 +946,7 @@ public VerificationRunResult ReadOutcome(int iteration, Checker checker, Verifie public List Counterexamples { get; } = new(); - public ConcurrentBag CoveredElements { get; } = new(); + public HashSet CoveredElements { get; } = new(); /// /// As a side effect, updates "this.parent.CumulativeAssertionCount". diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index 63b763de0..27e911613 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/SplitAndVerifyWorker.cs @@ -110,7 +110,8 @@ async Task DoWorkForMultipleIterations(Split split, CancellationToken cancellati int currentSplitNumber = DoSplitting ? Interlocked.Increment(ref splitNumber) - 1 : -1; split.SplitIndex = currentSplitNumber; var tasks = Enumerable.Range(0, options.RandomizeVcIterations).Select(iteration => - DoWork(iteration, split, cancellationToken)); + // Clone the split so it can be safely updated in each parallel task. + DoWork(iteration, new Split(split), cancellationToken)); await Task.WhenAll(tasks); } From fe61fb96ad3cf4784e1f4121dddafde8cac9295f Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 15 Feb 2024 15:32:43 -0800 Subject: [PATCH 4/6] Undo obsolete imports --- Source/Houdini/HoudiniSession.cs | 1 - Source/VCGeneration/ProofRun.cs | 1 - Source/VCGeneration/Split.cs | 1 - 3 files changed, 3 deletions(-) diff --git a/Source/Houdini/HoudiniSession.cs b/Source/Houdini/HoudiniSession.cs index d5c5aba1a..5c1032115 100644 --- a/Source/Houdini/HoudiniSession.cs +++ b/Source/Houdini/HoudiniSession.cs @@ -1,5 +1,4 @@ using System; -using System.Collections.Concurrent; using System.Diagnostics.Contracts; using System.Collections.Generic; using System.IO; diff --git a/Source/VCGeneration/ProofRun.cs b/Source/VCGeneration/ProofRun.cs index 3c59f865c..f1f38e9af 100644 --- a/Source/VCGeneration/ProofRun.cs +++ b/Source/VCGeneration/ProofRun.cs @@ -1,4 +1,3 @@ -using System.Collections.Concurrent; using System.Collections.Generic; using Microsoft.Boogie; diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index cd93fe7f0..bff7b06c9 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -1,5 +1,4 @@ using System; -using System.Collections.Concurrent; using System.Collections.Generic; using System.Diagnostics; using System.Linq; From ce2ff9dacea0c843849705b761eaf19f52d2c576 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 19 Feb 2024 08:46:35 -0800 Subject: [PATCH 5/6] Revert "Clone Split instead of using ConcurrentBag" This reverts commit 5de1b5fc1e30a5d67ad6c3b8e72fdd2fb3b771e5. --- Source/Houdini/HoudiniSession.cs | 2 +- Source/VCGeneration/ProofRun.cs | 2 +- Source/VCGeneration/Split.cs | 35 +-------------------- Source/VCGeneration/SplitAndVerifyWorker.cs | 3 +- 4 files changed, 4 insertions(+), 38 deletions(-) diff --git a/Source/Houdini/HoudiniSession.cs b/Source/Houdini/HoudiniSession.cs index 5c1032115..48cc14d50 100644 --- a/Source/Houdini/HoudiniSession.cs +++ b/Source/Houdini/HoudiniSession.cs @@ -126,7 +126,7 @@ public class HoudiniStatistics private readonly Houdini houdini; public HoudiniStatistics stats; public List Counterexamples { get; } = new(); - public HashSet CoveredElements { get; } = new(); + public ConcurrentBag CoveredElements { get; } = new(); private VCExpr conjecture; private ProverInterface.ErrorHandler handler; VerificationResultCollector collector; diff --git a/Source/VCGeneration/ProofRun.cs b/Source/VCGeneration/ProofRun.cs index f1f38e9af..7ba21cec3 100644 --- a/Source/VCGeneration/ProofRun.cs +++ b/Source/VCGeneration/ProofRun.cs @@ -8,5 +8,5 @@ public interface ProofRun { List Counterexamples { get; } - HashSet CoveredElements { get; } + ConcurrentBag CoveredElements { get; } } \ No newline at end of file diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index bff7b06c9..c802a85a5 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -88,39 +88,6 @@ public Split(VCGenOptions options, List /*!*/ blocks, randomGen = new Random(RandomSeed ?? 0); } - public Split(Split oldSplit) - { - Options = oldSplit.Options; - randomGen = oldSplit.randomGen; - Run = oldSplit.Run; - Blocks = oldSplit.Blocks; // Could be deep, but doesn't need to be here. - bigBlocks = oldSplit.bigBlocks; // Could be deep, but doesn't need to be here. - TopLevelDeclarations = oldSplit.TopLevelDeclarations; // Could be deep, but doesn't need to be here. - stats = oldSplit.stats; // Could be deep, but doesn't need to be here. - splitBlock = oldSplit.splitBlock; - assertToAssume = oldSplit.assertToAssume; - assumizedBranches = oldSplit.assumizedBranches; // Could be deep, but doesn't need to be here. - score = oldSplit.score; - scoreComputed = oldSplit.scoreComputed; - totalCost = oldSplit.totalCost; - assertionCount = oldSplit.assertionCount; - assertionCost = oldSplit.assertionCost; - GotoCmdOrigins = oldSplit.GotoCmdOrigins; // Could be deep, but doesn't need to be here. - parent = oldSplit.parent; // Could be deep, but doesn't need to be here. - copies = oldSplit.copies; // Could be deep, but doesn't need to be here. - doingSlice = oldSplit.doingSlice; - sliceInitialLimit = oldSplit.sliceInitialLimit; - sliceLimit = oldSplit.sliceLimit; - slicePos = oldSplit.slicePos; - protectedFromAssertToAssume = oldSplit.protectedFromAssertToAssume; // Could be deep, but doesn't need to be here. - keepAtAll = oldSplit.keepAtAll; // Could be deep, but doesn't need to be here. - SplitIndex = oldSplit.SplitIndex; - reporter = oldSplit.reporter; - bsid = oldSplit.bsid; - Counterexamples = new(); // Create fresh, so it can be updated. - CoveredElements = new(); // Create fresh, so it can be updated. - } - private void PrintTopLevelDeclarationsForPruning(Program program, Implementation implementation, string suffix) { if (!Options.Prune || Options.PrintPrunedFile == null) @@ -945,7 +912,7 @@ public VerificationRunResult ReadOutcome(int iteration, Checker checker, Verifie public List Counterexamples { get; } = new(); - public HashSet CoveredElements { get; } = new(); + public ConcurrentBag CoveredElements { get; } = new(); /// /// As a side effect, updates "this.parent.CumulativeAssertionCount". diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index 27e911613..63b763de0 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/SplitAndVerifyWorker.cs @@ -110,8 +110,7 @@ async Task DoWorkForMultipleIterations(Split split, CancellationToken cancellati int currentSplitNumber = DoSplitting ? Interlocked.Increment(ref splitNumber) - 1 : -1; split.SplitIndex = currentSplitNumber; var tasks = Enumerable.Range(0, options.RandomizeVcIterations).Select(iteration => - // Clone the split so it can be safely updated in each parallel task. - DoWork(iteration, new Split(split), cancellationToken)); + DoWork(iteration, split, cancellationToken)); await Task.WhenAll(tasks); } From 0bbb1e7992bfba01c115636f4805661b2b28f96e Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 19 Feb 2024 08:49:20 -0800 Subject: [PATCH 6/6] Revert "Undo obsolete imports" This reverts commit fe61fb96ad3cf4784e1f4121dddafde8cac9295f. --- Source/Houdini/HoudiniSession.cs | 1 + Source/VCGeneration/ProofRun.cs | 1 + Source/VCGeneration/Split.cs | 1 + 3 files changed, 3 insertions(+) diff --git a/Source/Houdini/HoudiniSession.cs b/Source/Houdini/HoudiniSession.cs index 48cc14d50..48c1ef648 100644 --- a/Source/Houdini/HoudiniSession.cs +++ b/Source/Houdini/HoudiniSession.cs @@ -1,4 +1,5 @@ using System; +using System.Collections.Concurrent; using System.Diagnostics.Contracts; using System.Collections.Generic; using System.IO; diff --git a/Source/VCGeneration/ProofRun.cs b/Source/VCGeneration/ProofRun.cs index 7ba21cec3..7972a4c45 100644 --- a/Source/VCGeneration/ProofRun.cs +++ b/Source/VCGeneration/ProofRun.cs @@ -1,3 +1,4 @@ +using System.Collections.Concurrent; using System.Collections.Generic; using Microsoft.Boogie; diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index c802a85a5..70af021c1 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -1,4 +1,5 @@ using System; +using System.Collections.Concurrent; using System.Collections.Generic; using System.Diagnostics; using System.Linq;