Enable InferAndVerify to schedule tasks on the scheduler of the caller, enabling verifying different Boogie programs in parallel using one ThreadPool #1
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
keyboardDrummer
force-pushed
the
removeAllCommandLineOptionsClo
branch
from
2e4a622 to
3479f7f
Compare
- CheckerPool is now a field of ExecutionEngine and ExecutionEngine inherits from `IDisposable`, to give more control over the lifetime of the `CheckerPool` to Boogie consumers and to ensure `CheckerPool` does not hold a different `ExecutionEngineOptions` object then is used by the rest of the code. - Snapshots turn out not to work well when reusing the checkerPool, so when snapshots are used the checker pool is not reused for each snapshot. - Introduce interfaces `ExecutionEngineOptions`, `HoudiniOptions`, `VCGenOptions` and `ConcurrencyOptions` for holding options related to their respective assemblies. - Reduce the references to `CoreOptions.Clo` from 204 to 92.
- Add a fix to `Source/VCGeneration/Checker.GoBackToIdle` for when a model view file is used. - ExecutionEngine takes a `VerificationResultCache` as an argument instead of storing it in a static variable, so consumers have control over the lifetime of the cache. Consumers who want to migrate cheaply should create their own static `VerificationResultCache`. - Remove all references to `CoreOptions.Clo`
It's a minor part of Boogie's full memory footprint, but it adds up over many calls to Boogie. On Test/havoc0 I observe a 4-5% reduction of the footprint of the whole program.
keyboardDrummer
force-pushed
the
returnVerificationResultTasks
branch
from
520ee90 to
834af51
Compare
Updates the process of collecting verification results and generating XML from them so that it should be safe to use `/xml` and `/vcsCores` together without getting mangled, interleaved output. In the process, make the results of checking individual splits more readily available at the higher levels of the verification call tree. This should be a step toward allowing clients such as Dafny to access fine-grained verification results without needing to read the XML output. The `VerificationResult` type now includes a list of `SplitResult` objects. If there's any more information a client is likely to need from verification, it should probably wind up in either `VerificationResult` or `SplitResult`.
keyboardDrummer
force-pushed
the
returnVerificationResultTasks
branch
from
77e382c to
1e2738e
Compare
…org#498) This is for Dafny: it makes it easier to keep the few "general" settings at the top while putting the rest of the help after Dafny's settings, like this: Usage: … General settings Boogie general settings Dafny settings Boogie settings
…e-org#512) This PR moves portions of the SMTLibProcessTheoremProver class into a subclass called SMTLibInteractiveTheoremProver. The goal is that everything in SMTLibProcessTheoremProver should be useful for either interactive or batch mode solvers. It then adds another subclass, SMTLibBatchTheoremProver, to address issue boogie-org#511.
This includes a location in addition to an outcome for each split entry in the XML result report.
Ensures that Boogie's solver interface, including batch mode, work smoothly with all supported solvers.
keyboardDrummer
force-pushed
the
returnVerificationResultTasks
branch
from
d0dffab to
7e7c37e
Compare
* added code to StandardVisitor so that it visits attributes for all commands and expressions consequently, inlining and monomorphization will get simpler additionally, any pass that depends on inlining will also not have to worry about attribute processing * added comment * removed whitespace
* Move VerificationResult and CommandLineParseState to separate files * Extract methods in InferAndVerify * Remove region directive
…rg#528) * Extract methods * Rename Process to Emit
Adds a structured type for describing proof obligations with potentially different text for success and failure forms. As a result, describing successful proofs becomes less awkward. This is more valuable for Boogie clients (such as Dafny) than it is for Boogie itself, though it has the benefit of grouping error messages in one place. At the moment, Boogie only uses the failure text, but I could imagine it using the success text at some point. Dafny plans to use the success text right away, and to provide a large number of additional subclasses to attach to the instances of AssertCmd it generates. I also hope that it could serve as a more general replacement for ErrorData, though I don't have a very thorough idea of how the various Boogie clients currently use that property.
keyboardDrummer
force-pushed
the
returnVerificationResultTasks
branch
from
a1cea2d to
55d7633
Compare
keyboardDrummer
force-pushed
the
returnVerificationResultTasks
branch
from
55d7633 to
4811d87
Compare
…ion when using parallel Boogie (boogie-org#531) ### Changes - Maintain order of logging that results from use the `-traceCaching` option when using parallel Boogie - Replace `OutputCollector` with `ConcurrentToSequentialWriteManager` that allows writing to the final TextWriter immediately when child TextWriters are written to, instead of only after calls to `WriteMoreOutput`. ### Testing - Use `%parallel-boogie` in `runtest.snapshot` which already uses `-traceCaching` - Add a test for `ConcurrentToSequentialWriteManager` - Tweak `test0/SplitOnEveryAssert.bpl` and `commandline/SplitOnEveryAssert.bpl` because the output order has improved slightly
keyboardDrummer
force-pushed
the
returnVerificationResultTasks
branch
from
da8a119 to
53c9b29
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.