IntersectMBO / IntersectMBO/io-sim

IOSimPOR fails to find a race under specific circumstances

Open
#183 5 comments 2 reactions 0 assignees View on GitHub
bug IOSimPOR
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

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.