MVars implementation is prone to deadlocks #181
Description
Describe the bug
The following property:
action = do
exploreRaces
mv <- newMVar 0
t1 <- async $ withMVar mv (\v -> pure (v + 1, ()))
t2 <- async $ do
withMVar mv (\v -> pure (v + 1, ()))
withMVar mv (\v -> pure (v + 1, ()))
t3 <- async $ cancel t1
wait t3
wait t2
wait t1
prop = quickCheck $ exploreSimTrace id action $ \_ trace ->
case traceResult False trace of
Left (FailureDeadlock err) -> counterexample (ppTrace trace) $ property False
_ -> property True)Results in a deadlock. The trace is (omitting the Races traces):
Schedule control: ControlAwait [ScheduleMod (Thread {3}.1) ControlDefault [Thread {2}.0,Thread {2}.1,Thread {2}.2,Thread {2}.3,Thread {1}.0,Thread {1}.1],ScheduleMod (Thread {2}.4) ControlDefault [Thread {1}.2]]
Thread {2} delayed at time Time 0s
until after:
Thread {1}
Thread {3}
0s - Thread [].0 main - SimStart ControlAwait [ScheduleMod (Thread {3}.1) ControlDefault [Thread {2}.0,Thread {2}.1,Thread {2}.2,Thread {2}.3,Thread {1}.0,Thread {1}.1],ScheduleMod (Thread {2}.4) ControlDefault [Thread {1}.2]]
0s - Thread [].0 main - TxCommitted [] [MVarId 0] Effect { }
0s - Thread [].0 main - Unblocked []
0s - Thread [].0 main - Deschedule Yield
0s - Thread [].0 main - Effect VectorClock [Thread [].0] Effect { }
0s - Thread [].1 main - TxCommitted [] [TMVarId 1] Effect { }
0s - Thread [].1 main - Unblocked []
0s - Thread [].1 main - Deschedule Yield
0s - Thread [].1 main - Effect VectorClock [Thread [].1] Effect { }
0s - Thread [].2 main - Mask MaskedInterruptible
0s - Thread [].2 main - ThreadForked Thread {1}
0s - Thread [].2 main - Deschedule Yield
0s - Thread [].2 main - Effect VectorClock [Thread [].2] Effect { forks = [Thread {1}] }
0s - Thread [].3 main - Mask Unmasked
0s - Thread [].3 main - Deschedule Interruptable
0s - Thread [].3 main - Effect VectorClock [Thread [].3] Effect { }
0s - Thread [].4 main - TxCommitted [] [] Effect { }
0s - Thread [].4 main - Unblocked []
0s - Thread [].4 main - Deschedule Yield
0s - Thread [].4 main - Effect VectorClock [Thread [].4] Effect { }
0s - Thread [].5 main - TxCommitted [] [TMVarId 2] Effect { }
0s - Thread [].5 main - Unblocked []
0s - Thread [].5 main - Deschedule Yield
0s - Thread [].5 main - Effect VectorClock [Thread [].5] Effect { }
0s - Thread [].6 main - Mask MaskedInterruptible
0s - Thread [].6 main - ThreadForked Thread {2}
0s - Thread [].6 main - Deschedule Yield
0s - Thread [].6 main - Effect VectorClock [Thread [].6] Effect { forks = [Thread {2}] }
0s - Thread [].7 main - Mask Unmasked
0s - Thread [].7 main - Deschedule Interruptable
0s - Thread [].7 main - Effect VectorClock [Thread [].7] Effect { }
0s - Thread [].8 main - TxCommitted [] [] Effect { }
0s - Thread [].8 main - Unblocked []
0s - Thread [].8 main - Deschedule Yield
0s - Thread [].8 main - Effect VectorClock [Thread [].8] Effect { }
0s - Thread [].9 main - TxCommitted [] [TMVarId 3] Effect { }
0s - Thread [].9 main - Unblocked []
0s - Thread [].9 main - Deschedule Yield
0s - Thread [].9 main - Effect VectorClock [Thread [].9] Effect { }
0s - Thread [].10 main - Mask MaskedInterruptible
0s - Thread [].10 main - ThreadForked Thread {3}
0s - Thread [].10 main - Deschedule Yield
0s - Thread [].10 main - Effect VectorClock [Thread [].10] Effect { forks = [Thread {3}] }
0s - Thread [].11 main - Mask Unmasked
0s - Thread [].11 main - Deschedule Interruptable
0s - Thread [].11 main - Effect VectorClock [Thread [].11] Effect { }
0s - Thread [].12 main - TxCommitted [] [] Effect { }
0s - Thread [].12 main - Unblocked []
0s - Thread [].12 main - Deschedule Yield
0s - Thread [].12 main - Effect VectorClock [Thread [].12] Effect { }
0s - Thread [].13 main - TxBlocked [Labelled TMVarId 3 async-RacyThreadId [3]] Effect { reads = [Labelled TMVarId 3 async-RacyThreadId [3]] }
0s - Thread [].13 main - Deschedule Blocked BlockedOnSTM
0s - Thread [].13 main - Effect VectorClock [Thread [].13] Effect { reads = [Labelled TMVarId 3 async-RacyThreadId [3]] }
0s - Thread {3}.0 - Mask Unmasked
0s - Thread {3}.0 - Deschedule Interruptable
0s - Thread {3}.0 - Effect VectorClock [Thread {3}.0, Thread [].10] Effect { }
0s - Thread {3}.1 - FollowControl ControlAwait [ScheduleMod (Thread {3}.1) ControlDefault [Thread {2}.0,Thread {2}.1,Thread {2}.2,Thread {2}.3,Thread {1}.0,Thread {1}.1],ScheduleMod (Thread {2}.4) ControlDefault [Thread {1}.2]]
0s - Thread {3}.1 - AwaitControl Thread {3}.1 ControlFollow [(RacyThreadId [2],0),(RacyThreadId [2],1),(RacyThreadId [2],2),(RacyThreadId [2],3),(RacyThreadId [1],0),(RacyThreadId [1],1)] [ScheduleMod (Thread {2}.4) ControlDefault [Thread {1}.2]]
0s - Thread {3}.1 - Deschedule Sleep
0s - Thread {2}.0 - Reschedule ControlFollow [(RacyThreadId [2],0),(RacyThreadId [2],1),(RacyThreadId [2],2),(RacyThreadId [2],3),(RacyThreadId [1],0),(RacyThreadId [1],1)] [ScheduleMod (Thread {2}.4) ControlDefault [Thread {1}.2]]
0s - Thread {2}.0 - PerformAction Thread {2}.0
0s - Thread {2}.0 - PerformAction Thread {2}.0
0s - Thread {2}.0 - Mask Unmasked
0s - Thread {2}.0 - Deschedule Interruptable
0s - Thread {2}.0 - Effect VectorClock [Thread {2}.0, Thread [].6] Effect { }
0s - Thread {2}.1 - PerformAction Thread {2}.1
0s - Thread {2}.1 - PerformAction Thread {2}.1
0s - Thread {2}.1 - Mask MaskedInterruptible
0s - Thread {2}.1 - PerformAction Thread {2}.1
0s - Thread {2}.1 - PerformAction Thread {2}.1
0s - Thread {2}.1 - TxCommitted [MVarId 0] [] Effect { reads = [MVarId 0], writes = [MVarId 0] }
0s - Thread {2}.1 - Unblocked []
0s - Thread {2}.1 - Deschedule Yield
0s - Thread {2}.1 - Effect VectorClock [Thread {2}.1, Thread [].6] Effect { reads = [MVarId 0], writes = [MVarId 0] }
0s - Thread {2}.2 - Reschedule ControlFollow [(RacyThreadId [2],2),(RacyThreadId [2],3),(RacyThreadId [1],0),(RacyThreadId [1],1)] [ScheduleMod (Thread {2}.4) ControlDefault [Thread {1}.2]]
0s - Thread {2}.2 - PerformAction Thread {2}.2
0s - Thread {2}.2 - PerformAction Thread {2}.2
0s - Thread {2}.2 - Mask Unmasked
0s - Thread {2}.2 - Deschedule Interruptable
0s - Thread {2}.2 - Effect VectorClock [Thread {2}.2, Thread [].6] Effect { }
0s - Thread {2}.3 - PerformAction Thread {2}.3
0s - Thread {2}.3 - Mask MaskedInterruptible
0s - Thread {2}.3 - Deschedule Interruptable
0s - Thread {2}.3 - Effect VectorClock [Thread {2}.3, Thread [].6] Effect { }
0s - Thread {2}.4 - AwaitControl Thread {2}.4 ControlFollow [(RacyThreadId [1],0),(RacyThreadId [1],1)] [ScheduleMod (Thread {2}.4) ControlDefault [Thread {1}.2]]
0s - Thread {2}.4 - Deschedule Sleep
0s - Thread {1}.0 - Reschedule ControlFollow [(RacyThreadId [1],0),(RacyThreadId [1],1)] [ScheduleMod (Thread {2}.4) ControlDefault [Thread {1}.2]]
0s - Thread {1}.0 - PerformAction Thread {1}.0
0s - Thread {1}.0 - PerformAction Thread {1}.0
0s - Thread {1}.0 - Mask Unmasked
0s - Thread {1}.0 - Deschedule Interruptable
0s - Thread {1}.0 - Effect VectorClock [Thread {1}.0, Thread [].2] Effect { }
0s - Thread {1}.1 - PerformAction Thread {1}.1
0s - Thread {1}.1 - PerformAction Thread {1}.1
0s - Thread {1}.1 - Mask MaskedInterruptible
0s - Thread {1}.1 - PerformAction Thread {1}.1
0s - Thread {1}.1 - PerformAction Thread {1}.1
0s - Thread {1}.1 - TxCommitted [MVarId 0] [Labelled TVarId 4 internal-takevar] Effect { reads = [MVarId 0], writes = [MVarId 0] }
0s - Thread {1}.1 - Unblocked []
0s - Thread {1}.1 - Deschedule Yield
0s - Thread {1}.1 - Effect VectorClock [Thread {1}.1, Thread {2}.1, Thread [].6] Effect { reads = [MVarId 0], writes = [MVarId 0] }
0s - Thread {3}.1 - ThrowTo (AsyncCancelled) Thread {1}
0s - Thread {3}.1 - ThrowToBlocked
0s - Thread {3}.1 - Deschedule Blocked BlockedOnThrowTo
0s - Thread {3}.1 - Effect VectorClock [Thread {1}.2, Thread {2}.1, Thread {3}.1, Thread [].10] Effect { throws = [Thread {1}] }
0s - Thread {2}.4 - FollowControl ControlAwait [ScheduleMod (Thread {2}.4) ControlDefault [Thread {1}.2]]
0s - Thread {2}.4 - AwaitControl Thread {2}.4 ControlFollow [(RacyThreadId [1],2)] []
0s - Thread {2}.4 - Deschedule Sleep
0s - Thread {2}.4 - ThreadSleep
0s - Thread {1}.2 - Reschedule ControlFollow [(RacyThreadId [1],2)] []
0s - Thread {1}.2 - PerformAction Thread {1}.2
0s - Thread {1}.2 - PerformAction Thread {1}.2
0s - Thread {1}.2 - TxBlocked [Labelled TVarId 4 internal-takevar] Effect { reads = [Labelled TVarId 4 internal-takevar] }
0s - Thread {1}.2 - Deschedule Blocked BlockedOnSTM
0s - Thread {1}.2 - Deschedule Interruptable
0s - Thread {1}.2 - ThrowToUnmasked Thread {3}
0s - Thread {1}.2 - Effect VectorClock [Thread {1}.2, Thread {2}.1, Thread [].6] Effect { reads = [Labelled TVarId 4 internal-takevar], wakeup = [Thread {3}] }
0s - Thread {3}.- - ThrowToWakeup
0s - Thread {1}.2 - Deschedule Yield
0s - Thread {1}.2 - Effect VectorClock [Thread {1}.2, Thread {2}.1, Thread {3}.1, Thread [].10] Effect { reads = [Labelled TVarId 4 internal-takevar], wakeup = [Thread {3}] }
0s - Thread {3}.2 - TxBlocked [Labelled TMVarId 1 async-RacyThreadId [1]] Effect { reads = [Labelled TMVarId 1 async-RacyThreadId [1]] }
0s - Thread {3}.2 - Deschedule Blocked BlockedOnSTM
0s - Thread {3}.2 - Effect VectorClock [Thread {1}.2, Thread {2}.1, Thread {3}.2, Thread [].10] Effect { reads = [Labelled TMVarId 1 async-RacyThreadId [1]] }
0s - Thread {2}.4 - ThreadWake
0s - Thread {2}.4 - TxCommitted [Labelled TVarId 4 internal-takevar, MVarId 0] [] Effect { reads = [MVarId 0], writes = [Labelled TVarId 4 internal-takevar, MVarId 0] }
0s - Thread {2}.4 - Unblocked []
0s - Thread {2}.4 - Deschedule Yield
0s - Thread {2}.4 - Effect VectorClock [Thread {1}.1, Thread {2}.4, Thread [].6] Effect { reads = [MVarId 0], writes = [Labelled TVarId 4 internal-takevar, MVarId 0] }
0s - Thread {2}.5 - Mask Unmasked
0s - Thread {2}.5 - Deschedule Interruptable
0s - Thread {2}.5 - Effect VectorClock [Thread {1}.1, Thread {2}.5, Thread [].6] Effect { }
0s - Thread {2}.6 - Mask MaskedInterruptible
0s - Thread {2}.6 - TxCommitted [MVarId 0] [Labelled TVarId 5 internal-takevar] Effect { reads = [MVarId 0], writes = [MVarId 0] }
0s - Thread {2}.6 - Unblocked []
0s - Thread {2}.6 - Deschedule Yield
0s - Thread {2}.6 - Effect VectorClock [Thread {1}.1, Thread {2}.6, Thread [].6] Effect { reads = [MVarId 0], writes = [MVarId 0] }
0s - Thread {2}.7 - TxBlocked [Labelled TVarId 5 internal-takevar] Effect { reads = [Labelled TVarId 5 internal-takevar] }
0s - Thread {2}.7 - Deschedule Blocked BlockedOnSTM
0s - Thread {2}.7 - Effect VectorClock [Thread {1}.1, Thread {2}.7, Thread [].6] Effect { reads = [Labelled TVarId 5 internal-takevar] }
0s - Thread {1}.3 - Throw AsyncCancelled
0s - Thread {1}.3 - Mask MaskedInterruptible
0s - Thread {1}.3 - Effect VectorClock [Thread {1}.3, Thread {2}.1, Thread {3}.1, Thread [].10] Effect { }
0s - Thread {1}.4 - TxCommitted [MVarId 0] [] Effect { reads = [MVarId 0], writes = [MVarId 0] }
0s - Thread {1}.4 - Unblocked []
0s - Thread {1}.4 - Deschedule Yield
0s - Thread {1}.4 - Effect VectorClock [Thread {1}.4, Thread {2}.6, Thread {3}.1, Thread [].10] Effect { reads = [MVarId 0], writes = [MVarId 0] }
0s - Thread {1}.5 - Throw AsyncCancelled
0s - Thread {1}.5 - Mask MaskedInterruptible
0s - Thread {1}.5 - Effect VectorClock [Thread {1}.5, Thread {2}.6, Thread {3}.1, Thread [].10] Effect { }
0s - Thread {1}.6 - Mask MaskedInterruptible
0s - Thread {1}.6 - Deschedule Interruptable
0s - Thread {1}.6 - Effect VectorClock [Thread {1}.6, Thread {2}.6, Thread {3}.1, Thread [].10] Effect { }
0s - Thread {1}.7 - TxCommitted [Labelled TMVarId 1 async-RacyThreadId [1]] [] Effect { reads = [Labelled TMVarId 1 async-RacyThreadId [1]], writes = [Labelled TMVarId 1 async-RacyThreadId [1]], wakeup = [Thread {3}] }
0s - Thread {3}.- - TxWakeup [Labelled TMVarId 1 async-RacyThreadId [1]]
0s - Thread {1}.7 - Unblocked [Thread {3}]
0s - Thread {1}.7 - Deschedule Yield
0s - Thread {1}.7 - Effect VectorClock [Thread {1}.7, Thread {2}.6, Thread {3}.1, Thread [].10] Effect { reads = [Labelled TMVarId 1 async-RacyThreadId [1]], writes = [Labelled TMVarId 1 async-RacyThreadId [1]], wakeup = [Thread {3}] }
0s - Thread {3}.3 - TxCommitted [] [] Effect { reads = [Labelled TMVarId 1 async-RacyThreadId [1]] }
0s - Thread {3}.3 - Unblocked []
0s - Thread {3}.3 - Deschedule Yield
0s - Thread {3}.3 - Effect VectorClock [Thread {1}.7, Thread {2}.6, Thread {3}.3, Thread [].10] Effect { reads = [Labelled TMVarId 1 async-RacyThreadId [1]] }
0s - Thread {3}.4 - Mask MaskedInterruptible
0s - Thread {3}.4 - Deschedule Interruptable
0s - Thread {3}.4 - Effect VectorClock [Thread {1}.7, Thread {2}.6, Thread {3}.4, Thread [].10] Effect { }
0s - Thread {3}.5 - TxCommitted [Labelled TMVarId 3 async-RacyThreadId [3]] [] Effect { reads = [Labelled TMVarId 3 async-RacyThreadId [3]], writes = [Labelled TMVarId 3 async-RacyThreadId [3]], wakeup = [Thread []] }
0s - Thread [].- main - TxWakeup [Labelled TMVarId 3 async-RacyThreadId [3]]
0s - Thread {3}.5 - Unblocked [Thread []]
0s - Thread {3}.5 - Deschedule Yield
0s - Thread {3}.5 - Effect VectorClock [Thread {1}.7, Thread {2}.6, Thread {3}.5, Thread [].10] Effect { reads = [Labelled TMVarId 3 async-RacyThreadId [3]], writes = [Labelled TMVarId 3 async-RacyThreadId [3]], wakeup = [Thread []] }
0s - Thread [].14 main - TxCommitted [] [] Effect { reads = [Labelled TMVarId 3 async-RacyThreadId [3]] }
0s - Thread [].14 main - Unblocked []
0s - Thread [].14 main - Deschedule Yield
0s - Thread [].14 main - Effect VectorClock [Thread {1}.7, Thread {2}.6, Thread {3}.5, Thread [].14] Effect { reads = [Labelled TMVarId 3 async-RacyThreadId [3]] }
0s - Thread [].15 main - TxBlocked [Labelled TMVarId 2 async-RacyThreadId [2]] Effect { reads = [Labelled TMVarId 2 async-RacyThreadId [2]] }
0s - Thread [].15 main - Deschedule Blocked BlockedOnSTM
0s - Thread [].15 main - Effect VectorClock [Thread {1}.7, Thread {2}.6, Thread {3}.5, Thread [].15] Effect { reads = [Labelled TMVarId 2 async-RacyThreadId [2]] }
0s - Thread {3}.6 - ThreadFinished
0s - Thread {3}.6 - Deschedule Terminated
0s - Thread {3}.6 - Effect VectorClock [Thread {1}.7, Thread {2}.6, Thread {3}.6, Thread [].10] Effect { }
0s - Thread {1}.8 - ThreadFinished
0s - Thread {1}.8 - Deschedule Terminated
0s - Thread {1}.8 - Effect VectorClock [Thread {1}.8, Thread {2}.6, Thread {3}.1, Thread [].10] Effect { }
0s - - Deadlock [Thread {1},Thread {2},Thread {3},Labelled Thread [] main]
The problem is that the value that the second thread puts in the MVar is given to thread 1 via the internal-takevar and not put in the MVar. Cancelling the thread instantly results in the value disappearing with the forgotten internal-takevar.
This is because on presence of an AsyncException during a blocked take, we remove the takevar from the queue but we lose the value with it. See https://github.com/input-output-hk/io-sim/blob/main/io-sim/src/Control/Monad/IOSim/STM.hs#L400-L401
Expected behaviour
The value should be given to the next one in queue, if any, or written to the MVar.
Desktop (please complete the following information):
GHCversion: 9.6.6io-simversion: 1.6.0.0io-classesversion: 1.7.0.0
Additional context
Add any other context about the problem here. Attach io-sim or io-sim-por trace if possible.