IntersectMBO / IntersectMBO/io-sim
IOSimPOR fails to find a race under specific circumstances
- Dominant language
- Haskell
- Stars
- 54
- Forks
- 25
- Avg merge
- 3h 9m
- Merged PRs (30d)
- 1
Description
**Describe the bug**
This test case:
```haskell
prop_race :: Property
prop_race = exploreSimTrace id action $ \_ trace ->
case traceResult False trace of
Left (FailureDeadlock err) -> counterexample (ppTrace trace) $ property False
_ -> property True
where
action :: IOSim s ()
action = do
exploreRaces
ref <- newMVar 0
tq <- atomically newTQueue
let f = do
atomically $ writeTQueue tq ()
bracketOnError
(takeMVar ref)
(tryPutMVar ref)
(putMVar ref . (+1))
t1 <- async f
t2 <- async f
async (cancel t1) >>= wait
wait t2
wait t1
```
will succeed. However removing the `atomically $ writeTQueue tq ()` will make it fail because of a Deadlock. The deadlock is indeed present in the implementation: t1 takes, t1 puts, t1 receives exception, t2 takes, t1 tryPut succesfully, t2 blocks on put.
Writing to that tqueue before running the `bracketOnError` results in the race not being found by IOSimPOR. This looks like a direct bug.
**Desktop (please complete the following information):**
- `GHC` version: 9.6.6
- `io-sim` version: 1.6.0.0
- `io-classes` version: 1.7.0.0
**Additional context**
Add any other context about the problem here. Attach `io-sim` or `io-sim-por` trace if possible.
A trace with the deadlock if removing the mentioned line:
[fail.txt](https://github.com/user-attachments/files/17330656/fail.txt)
Contributor guide
Assessment
This issue has not been assessed yet.