input-output-hk / io-sim

Haskell's IO simulator which closely follows core packages (base, async, stm).
https://hackage.haskell.org/package/io-sim
Apache License 2.0
37 stars 15 forks source link

IOSimPOR failure #113

Closed coot closed 1 year ago

coot commented 1 year ago

Steps to reproduce

Steps to reproduce the behaviour:

prop = propExploration (Tasks [Task [ThrowTo 1, WhenSet 0 0],
                               Task [Delay 1],
                               Task [WhenSet 0 0],
                               Task [WhenSet 1 0, ThrowTo 1]])

but requires a modified Task interpreter which is using aysnc & wait, instead of forkIO and threadDelay as a synchronisation primitive.

assert, called at src/Control/Monad/IOSimPOR/Internal.hs:956:71 in io-sim-1.2.0.0-inplace:Control.Monad.IOSimPOR.Internal

Trace

Time 0s - (RacyThreadId [1],2)  - EventEffect Effect { throws = [RacyThreadId [2]], }
-- ^ last scheduled step, `(RacyThreadId [1], 3)`, which does `WhenSet 0 0` would be blocked.
Time 0s - (RacyThreadId [4],4)  - EventThreadWake
Time 0s - (RacyThreadId [4],4)  - EventThrowTo (ExitFailure 0) (RacyThreadId [2])
-- ^ executes: ThrowTo 1 
Time 0s - (RacyThreadId [4],4)  - EventThrowToBlocked
Time 0s - (RacyThreadId [4],4)  - EventDeschedule (Blocked BlockedOnThrowTo)
Time 0s - (RacyThreadId [4],4)  - EventEffect Effect { throws = [RacyThreadId [2]], }
Time 0s - (RacyThreadId [2],0)  - EventMask Unmasked
Time 0s - (RacyThreadId [2],0)  - EventDeschedule Interruptable
Time 0s - (RacyThreadId [2],0)  - EventDeschedule Yield
Time 0s - (RacyThreadId [2],0)  - EventThrowToUnmasked (Labelled (RacyThreadId [4]) Nothing)
Time 0s - (RacyThreadId [4],-1)  - EventThrowToWakeup
-- ^ receives the exception, which interrupts the step before `Delay 1`
Time 0s - (RacyThreadId [2],0)  - EventEffect Effect { }
Time 0s - (RacyThreadId [4],5)  - EventMask MaskedInterruptible
Time 0s - (RacyThreadId [4],5)  - EventDeschedule Interruptable
Time 0s - (RacyThreadId [4],5)  - EventEffect Effect { }
Time 0s - (RacyThreadId [4],6)  - EventTxCommitted [Labelled (TVarId 5) (Just "async-RacyThreadId [4]")] [] (Just Effect { reads = fromList [TVarId 5], writes = fromList [TVarId 5], })
-- ^ task commits results to its `Async`
Time 0s - (RacyThreadId [4],6)  - EventUnblocked []
Time 0s - (RacyThreadId [4],6)  - EventDeschedule Yield
Time 0s - (RacyThreadId [4],6)  - EventEffect Effect { reads = fromList [TVarId 5], writes = fromList [TVarId 5], }
Time 0s - (RacyThreadId [4],7)  - EventThreadFinished
-- ^ task terminates
Time 0s - (RacyThreadId [4],7)  - EventDeschedule Terminated
Time 0s - (RacyThreadId [4],7)  - EventEffect Effect { }
Time 0s - (RacyThreadId [2],1)  - EventThrow (ExitFailure 0)
-- exception is thrown
Time 0s - (RacyThreadId [2],1)  - EventMask MaskedInterruptible
Time 0s - (RacyThreadId [2],1)  - EventEffect Effect { }
Time 0s - (RacyThreadId [2],2)  - EventMask MaskedInterruptible
Time 0s - (RacyThreadId [2],2)  - EventDeschedule Interruptable
Time 0s - (RacyThreadId [2],2)  - EventEffect Effect { }
Time 0s - (RacyThreadId [2],3)  - EventTxCommitted [Labelled (TVarId 3) (Just "async-RacyThreadId [2]")] [] (Just Effect { reads = fromList [TVarId 3], writes = fromList [TVarId 3], })
Time 0s - (RacyThreadId [2],3)  - EventUnblocked []
Time 0s - (RacyThreadId [2],3)  - EventDeschedule Yield
Time 0s - (RacyThreadId [2],3)  - EventEffect Effect { reads = fromList [TVarId 3], writes = fromList [TVarId 3], }
Time 0s - (RacyThreadId [2],4)  - EventThreadFinished
Time 0s - (RacyThreadId [2],4)  - EventDeschedule Terminated
Time 0s - (RacyThreadId [1],-1)  - EventThrowToWakeup
Time 0s - (RacyThreadId [2],4)  - EventEffect Effect { }
Time 0s - (RacyThreadId [1],3)  - EventTxBlocked [Labelled (TVarId 0) Nothing] (Just Effect { reads = fromList [TVarId 0], })
Time 0s - (RacyThreadId [1],3)  - EventDeschedule (Blocked BlockedOnSTM)
Time 0s - (RacyThreadId [1],3)  - EventEffect Effect { reads = fromList [TVarId 0], }
  , completeRaces = []})
-- ^ deadlock discovered
Deadlock (Time 0s) [Labelled (RacyThreadId [1]) Nothing,Labelled (RacyThreadId [2]) Nothing,Labelled (RacyThreadId [3]) Nothing,Labelled (RacyThreadId [4]) Nothing,Labelled (ThreadId []) (Just "main")]
coot commented 1 year ago

Fixed in #114.