From 5de1b5fc1e30a5d67ad6c3b8e72fdd2fb3b771e5 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 15 Feb 2024 15:31:19 -0800 Subject: [PATCH] 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); }