MVars implementation is prone to deadlocks

[jasagredo]

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):

• 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.