boogie-org / boogie

Boogie
http://research.microsoft.com/en-us/projects/boogie/
MIT License
506 stars 111 forks source link

Resolve Boogie test deadlocks #932

Closed keyboardDrummer closed 1 month ago

keyboardDrummer commented 1 month ago

Changes

Testing

shazqadeer commented 1 month ago

@keyboardDrummer : Thanks for digging into the flaky CI issues. I had also noticed these small tests failing in CI with a timeout and had no idea what was going on.

Fix a bug that could cause a concurrency related exception in QuantifierInstantiationInfo, which was introduced by https://github.com/boogie-org/boogie/pull/862.

To improve my understanding, could you say a bit more about the bug introduced by my aforementioned PR?

keyboardDrummer commented 1 month ago

To improve my understanding, could you say a bit more about the bug introduced by my aforementioned PR?

The fix is in this commit: https://github.com/boogie-org/boogie/pull/932/commits/c79011bbe26af6ebf7055ef44d0b96901b4f13e3 While running tests, I saw a concurrent modification exception during a call to HashSet.Add done from FindInstantiationHints. Looking at the git history, FindInstantiationHints was originally designed to be able to be called concurrently, but since the introduction of the HashSet it no longer supported this. I replaced the use of HashSet with a ConcurrentBag so it can handle concurrent Add calls.