[Civl] Improvements to pool-based quantifier instantiation #862
Conversation
This file contains 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
shazqadeer
force-pushed
the
treiber-alloc-linear
branch
from
be6bbf7
to
5a05558
Compare
added 4 commits
April 4, 2024 21:32
shazqadeer
changed the title
keyboardDrummer
added a commit
that referenced
this pull request
Aug 13, 2024
### Changes - Made a change to the Dispose method of `CustomStackSizePoolTaskScheduler.cs`, so it now interrupts all its thread instead of joining them. I think this was causing the entire Boogie process to hang after it was finished, causing tests to deadlock. - Add `blame-hang-timeout` to the `dotnet test` invocation that runs the NUnit tests, which allows identifying which test fails when the unit tests timeout. - Add an undocumented option `/processTimeLimit` that can be used by tests to let Boogie stop itself after a certain timespan, allowing developers to get a stacktrace of where Boogie was at the point of timeout. - Remove APIs for cancelling requests, which were only available programmatically and not used by Dafny. - Fix a bug that could cause a concurrency related exception in `QuantifierInstantiationInfo`, which was introduced by #862. - Use an invariant culture somewhere in printing debug output, so the Boogie tests locally pass on my machine, despite my European culture. - Some renaming of variations of VerifyImplementation, to make the differences more clear. - Configure a 30 seconds timelimit per VC for all Boogie tests by default. Added an exception for a few slow tests - Let Boogie cancel checking of a VC after its timelimit has passed, regardless of what the solver is doing ### Testing - Did not add any additional tests - Let the test-suite succeed without retries 4 times, in an attempt to determine that it resolves the test instabilities we've had.
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.
Added a pool hint to nondeterministic output parameter of One_New. Since this procedure is polymorphic, the pool name "One_New" may correspond to many types. Therefore, pool-based quantifier instantiation is updated so that it can handle the same pool name attached to bound variables of several types. The main idea is to be permissive in the construction of instantiations but prune out illegal instances just before the instantiation.
Changed AtomicAllocNode in treiber-stack.bpl so that the output variable
successis explicitly initialized. This prevents quantification over the initial (nondeterministic) value ofsuccessin the construction of the gate of AtomicAllocNode. Ultimately, this results in better behaved VCs.Together the two changes above reduce flakiness in the proof of treiber-stack.bpl.