Closed btwilk closed 1 year ago
@btwilk Unfortunetely, we do not support multiple suspensions at the moment, but we are considering imrpoving this part later.
@btwilk Suprisingly, we did not have applications with multiple suspension points per operation. Coroutine-based data structures (like queues or channels) mostly have only one natural suspension point. I opened a more general issue, so I am closing this one
Version: 2.15 I'm model checking some code that uses Mutex. I ran into a case where lincheck incorrectly considers a coroutine that should still be running to have finished. Here is a minimal example:
Here is the assertion error: coroutine-assertion-error.txt
In contrast, the equivalent code with thread synchronization model checks as expected (no counterexamples found):