Avoid concurrency errors when combining /randomizeVcIterations and /trackVerificationCoverage

[atomb]

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 PR makes the set of covered elements be a ConcurrentBag to allow updates.

I think a more significant refactoring of this code makes sense, but is not as straightforward as it initially seemed. For the moment, this simple change allows a rarely but occasionally useful mode of operation to succeed with correct results and without crashing, so it's strictly better than what's there at the moment.

[keyboardDrummer]

multiple tasks may concurrently update the CoveredElements property.

Shouldn't we make it so that only one task does those updates?

[atomb]

multiple tasks may concurrently update the CoveredElements property.

Shouldn't we make it so that only one task does those updates?

Then we either lose the performance benefit of running all iterations in parallel, or have complex logic for deciding which task does it, which could easily lead to a different concurrency bug.

[keyboardDrummer]

Wouldn't it be safer, and more performant, to create separate Split instances for the different random iterations? I don't think CoveredElements is the only field of Split that is modified while verifying the split.

[atomb]

Wouldn't it be safer, and more performant, to create separate Split instances for the different random iterations? I don't think CoveredElements is the only field of Split that is modified while verifying the split.

The only other fields that seem to be updated in the process are Counterexamples and provenCost.

It would arguably be safer to do each iteration on a different Split instance, which we could do by making it possible to clone a Split. It wouldn't be faster (because each Split would need to be cloned, adding a little extra computation), but it would eliminate the need for concurrent data structures.

[atomb]

Wouldn't it be safer, and more performant, to create separate Split instances for the different random iterations? I don't think CoveredElements is the only field of Split that is modified while verifying the split.

The only other fields that seem to be updated in the process are Counterexamples and provenCost.

It would arguably be safer to do each iteration on a different Split instance, which we could do by making it possible to clone a Split. It wouldn't be faster (because each Split would need to be cloned, adding a little extra computation), but it would eliminate the need for concurrent data structures.

Doing this turns out to be more complex than I'd thought. I'm inclined to merge the simpler change to a ConcurrentBag to avoid crashes while preserving reasonable semantics while we work out a better refactoring.

[keyboardDrummer]

Doing this turns out to be more complex than I'd thought.

What's complex about it?

I think it would be nice if a split can assume it's state doesn't get modified concurrently. In particular, making some of the state thread-safe and the rest not, seems like it would be laying a trap for future developers.

[keyboardDrummer]

Btw, does this line not also introduce suffer from not being thread-safe?

boogie/Source/VCGeneration/Checker.cs

Line 161 in baf6dbc

SolverOptions.RandomSeed = 1 < Options.RandomizeVcIterations ? split.NextRandom() : split.RandomSeed;

[keyboardDrummer]

dafny measure-complexity recently switched over to using the new verification pipeline, and I don't see code where that does anything with the --iterations argument. I'm not sure how the tests still pass, apparently they do not test sufficiently. I'll create a release-blocking issue: dafny-lang/dafny#5134

A fix is to update VerificationTask so that it is clone-able. Dafny can then clone VerificationTasks when it sees --iterations is used, and run each clone. These clones can also create copies of Split, so that there are no concurrency issues.

[atomb]

Doing this turns out to be more complex than I'd thought.

What's complex about it?

Only that the first thing I tried led to a deadlock that I couldn't reproduce locally but that consistently showed up in one of the CI jobs. I'm sure it's resolvable, it'll just take more time than I originally thought.

I think it would be nice if a split can assume it's state doesn't get modified concurrently. In particular, making some of the state thread-safe and the rest not, seems like it would be laying a trap for future developers.

I do think that's the better approach.

[atomb]

dafny measure-complexity recently switched over to using the new verification pipeline, and I don't see code where that does anything with the --iterations argument. I'm not sure how the tests still pass, apparently they do not test sufficiently. I'll create a release-blocking issue: dafny-lang/dafny#5134

I think updating here to check for multiple instances of the pattern it's currently looking for should catch the problem. I can confirm that the updated test fails for me right now.

A fix is to update VerificationTask so that it is clone-able. Dafny can then clone VerificationTasks when it sees --iterations is used, and run each clone. These clones can also create copies of Split, so that there are no concurrency issues.

Yeah, I agree. And the refactoring you've recently done should make this more straightforward than it would have been in the past.

[atomb]

This issue has a better solution now, so I'm going to close this PR.