Add options to detect brittleness across multiple runs and portfolio results.

[zafer-esen]

(Detailed description to be added.)

Adds two main options:

/portfolioVcIterations:<n>
              Enables /randomizeVcIterations and returns the first successful
              proof result (if any) out of n randomized VCs.
/portfolioVcBatchSize:<m>
              Splits n in /portfolioVcIterations:<n> into n/m batches (or
              n/m+1 batches if n is not divisible by m). 
              Defaults to 1.

              Iterations in a batch can be executed concurrently, but each
              batch is executed sequentially to completion. A batch execution
              is considered complete when all iterations in that batch
              complete execution. If any of the iterations in a batch returns
              a valid verification outcome, remaining batches are cancelled.
              Since the iterations and batches are created deterministically,
              this implies determinism when using /portfolioVcIterations.

Also adds an analysis to detect brittleness among iterations in executed batches, and reports these as warnings.

[shazqadeer]

What is the motivation for /portfolioVcBatchSize?

[zafer-esen]

With /portfolioVcBatchSize:1 each (randomized) iteration is run sequentially, and verification of a split stops as soon as one of the iterations of that split is verified. If it is the first iteration that gets verified, brittleness cannot be detected. Specifying a batch size greater than 1 enforces more iterations for the same split to run to completion, which increases the chance of detecting brittleness in that split.

Batches run sequentially in order to have determinism. Iterations in a batch can run concurrently.

I am planning to extend the PR description, and the PR itself still needs some work (brittleness analysis parameters are currently hard-coded). Any feedback would be very welcome!

The current implemented definition of brittle is:

• All iterations are verified, but there are significant differences between the randomized iterations of some split in run times or resource counts,
• For the same split, there is at least one iteration that is verified, and there is at least one iteration that is not.

In both cases the split is still verified, but a brittleness warning is printed.

[zafer-esen]

Use-case examples:

• I don't want to increase verification times, and I don't care much about brittleness, but I want Boogie to re-attempt verification of (only) failed VCs up to n times using randomized iterations of that VC (randomized as in /randomizeVcIterations:n). It should return as soon as a VC is verified, but keep going up to n iterations if not.

  • Pass /portfolioVcIterations:n. This will default the batch size to 1. This will still report brittleness if a split is not verified in the first iteration, but not in other cases.

• I want to run a small brittleness analysis.

  • Pass /portfolioVcIterations:n and /portfolioVcBatchSize:m. Values for m and n depend on the amount of desired concurrency and the minimum number of iterations that should be compared. When n > m, the verification of each split will be attempted at least m times, which will likely multiply verification time by the batch size m. This will further increase if none of the iterations in the first batch of some split is verified, in which case the next batch will be attempted.

It should be noted that iterations from different splits can still run concurrently in either case.

[shazqadeer]

I thought brittleness analysis is already implemented via /randomizedVcIterations:n which tries the VCs for n times and allows the user to examine the result for each time. I didn't understand why you want to implement brittleness analysis again with these new options. On the other hand, the motivation for /portfolioVcIterations:n is clear to me; this option stops generating randomized versions as soon as success is achieved.

[zafer-esen]

I understand now what you mean, and I agree that batching is perhaps unnecessary. My initial motivation was that batching would make it possible to execute iterations inside a batch concurrently, but iterations from different splits can already be interleaved.

For brittleness analysis, I think one extra capability /portfolioVcIterations:n and /portfolioVcBatchSize:m have over /randomizedVcIterations:m is that, /randomizedVcIterations:m would not detect pass/fail brittleness (i.e., iterations with at least one verified and one failing) if the first m iterations all fail.

When using /portfolioVcBatchSize:m, n (the number of iterations) could be set greater than m (the batch size). This ensures that at least m iterations for each VC will be executed. If all m iterations fail for some VC, at least one other batch will be executed for that VC, increasing the chances of detecting a passing iteration. In any case, this is probably not a very important feature and one I didn't really think of when working on this PR.

This PR also adds some code for doing a brittleness analysis within Boogie (i.e., not just outputting results from every iteration). Currently this is only done when using /portfolioVcIterations:n with a batch size greater than 1.

Maybe it is cleaner to remove batching altogether and to only keep the portfolio code. The analysis from the previous paragraph could be done when using /randomizeVcIterations:n in that case, or removed as well. I think doing such an analysis at Boogie level has its benefits though. I can update this PR based on what you think.

[shazqadeer]

It would be better to remove batching and add the brittleness analysis to /randomizeVcIterations:n.