Open coot opened 7 months ago
Describe the bug The following counterexample is found:
propExploration: FAIL (61.59s) *** Failed! Falsified (after 47 tests and 64 shrinks): AreNotEqual Shrink2 {getShrink2 = Tasks [Task [WhenSet 0 0,ThrowTo 1],Task [],Task [WhenSet 0 0],Task [ThrowTo 1,WhenSet 1 1],Task [ThrowTo 1]]} Schedule control: ControlAwait [ScheduleMod (RacyThreadId [5],2) ControlDefault [(RacyThreadId [4],0),(RacyThreadId [4],1),(RacyThreadId [4],2),(RacyThreadId [3],0),(RacyThreadId [3],1),(RacyThreadId [2],0),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [3],2),(RacyThreadId [3],3),(RacyThreadId [3],4),(RacyThreadId [3],5),(RacyThreadId [1],2),(RacyThreadId [1],3)]] Thread {5} (5) delayed at time Time 0s until after: Thread {1} Thread {1} (1) Thread {2} Thread {3} Thread {3} (3) Thread {4} Thread {4} (4) 0s - Thread [].0 main - SimStart ControlAwait [ScheduleMod (RacyThreadId [5],2) ControlDefault [(RacyThreadId [4],0),(RacyThreadId [4],1),(RacyThreadId [4],2),(RacyThreadId [3],0),(RacyThreadId [3],1),(RacyThreadId [2],0),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [3],2),(RacyThreadId [3],3),(RacyThreadId [3],4),(RacyThreadId [3],5),(RacyThreadId [1],2),(RacyThreadId [1],3)]] 0s - Thread [].0 main - Say Tasks [Task [WhenSet 0 0,ThrowTo 1],Task [],Task [WhenSet 0 0],Task [ThrowTo 1,WhenSet 1 1],Task [ThrowTo 1]] 0s - Thread [].0 main - TxCommitted [] [TVarId 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 [] [TVarId 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 - TxCommitted [] [TVarId 2] Effect { } 0s - Thread [].2 main - Unblocked [] 0s - Thread [].2 main - Deschedule Yield 0s - Thread [].2 main - Effect VectorClock [Thread [].2] Effect { } 0s - Thread [].3 main - Mask MaskedInterruptible 0s - Thread [].3 main - ThreadForked Thread {1} 0s - Thread [].3 main - Deschedule Yield 0s - Thread [].3 main - Effect VectorClock [Thread [].3] Effect { forks = [Thread {1}] } 0s - Thread [].4 main - Mask Unmasked 0s - Thread [].4 main - Deschedule Interruptable 0s - Thread [].4 main - Effect VectorClock [Thread [].4] Effect { } 0s - Thread [].5 main - TxCommitted [] [] 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 - TxCommitted [] [TVarId 3] Effect { } 0s - Thread [].6 main - Unblocked [] 0s - Thread [].6 main - Deschedule Yield 0s - Thread [].6 main - Effect VectorClock [Thread [].6] Effect { } 0s - Thread [].7 main - Mask MaskedInterruptible 0s - Thread [].7 main - ThreadForked Thread {2} 0s - Thread [].7 main - Deschedule Yield 0s - Thread [].7 main - Effect VectorClock [Thread [].7] Effect { forks = [Thread {2}] } 0s - Thread [].8 main - Mask Unmasked 0s - Thread [].8 main - Deschedule Interruptable 0s - Thread [].8 main - Effect VectorClock [Thread [].8] Effect { } 0s - Thread [].9 main - TxCommitted [] [] 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 - TxCommitted [] [TVarId 4] Effect { } 0s - Thread [].10 main - Unblocked [] 0s - Thread [].10 main - Deschedule Yield 0s - Thread [].10 main - Effect VectorClock [Thread [].10] Effect { } 0s - Thread [].11 main - Mask MaskedInterruptible 0s - Thread [].11 main - ThreadForked Thread {3} 0s - Thread [].11 main - Deschedule Yield 0s - Thread [].11 main - Effect VectorClock [Thread [].11] Effect { forks = [Thread {3}] } 0s - Thread [].12 main - Mask Unmasked 0s - Thread [].12 main - Deschedule Interruptable 0s - Thread [].12 main - Effect VectorClock [Thread [].12] Effect { } 0s - Thread [].13 main - TxCommitted [] [] Effect { } 0s - Thread [].13 main - Unblocked [] 0s - Thread [].13 main - Deschedule Yield 0s - Thread [].13 main - Effect VectorClock [Thread [].13] Effect { } 0s - Thread [].14 main - TxCommitted [] [TVarId 5] Effect { } 0s - Thread [].14 main - Unblocked [] 0s - Thread [].14 main - Deschedule Yield 0s - Thread [].14 main - Effect VectorClock [Thread [].14] Effect { } 0s - Thread [].15 main - Mask MaskedInterruptible 0s - Thread [].15 main - ThreadForked Thread {4} 0s - Thread [].15 main - Deschedule Yield 0s - Thread [].15 main - Effect VectorClock [Thread [].15] Effect { forks = [Thread {4}] } 0s - Thread [].16 main - Mask Unmasked 0s - Thread [].16 main - Deschedule Interruptable 0s - Thread [].16 main - Effect VectorClock [Thread [].16] Effect { } 0s - Thread [].17 main - TxCommitted [] [] Effect { } 0s - Thread [].17 main - Unblocked [] 0s - Thread [].17 main - Deschedule Yield 0s - Thread [].17 main - Effect VectorClock [Thread [].17] Effect { } 0s - Thread [].18 main - TxCommitted [] [TVarId 6] Effect { } 0s - Thread [].18 main - Unblocked [] 0s - Thread [].18 main - Deschedule Yield 0s - Thread [].18 main - Effect VectorClock [Thread [].18] Effect { } 0s - Thread [].19 main - Mask MaskedInterruptible 0s - Thread [].19 main - ThreadForked Thread {5} 0s - Thread [].19 main - Deschedule Yield 0s - Thread [].19 main - Effect VectorClock [Thread [].19] Effect { forks = [Thread {5}] } 0s - Thread [].20 main - Mask Unmasked 0s - Thread [].20 main - Deschedule Interruptable 0s - Thread [].20 main - Effect VectorClock [Thread [].20] Effect { } 0s - Thread [].21 main - TxCommitted [] [] Effect { } 0s - Thread [].21 main - Unblocked [] 0s - Thread [].21 main - Deschedule Yield 0s - Thread [].21 main - Effect VectorClock [Thread [].21] Effect { } 0s - Thread [].22 main - TxCommitted [TVarId 1] [] Effect { writes = fromList [TVarId 1] } 0s - Thread [].22 main - Unblocked [] 0s - Thread [].22 main - Deschedule Yield 0s - Thread [].22 main - Effect VectorClock [Thread [].22] Effect { writes = fromList [TVarId 1] } 0s - Thread [].23 main - TxBlocked [Labelled TVarId 2 async-RacyThreadId [1]] Effect { reads = fromList [TVarId 2] } 0s - Thread [].23 main - Deschedule Blocked BlockedOnSTM 0s - Thread [].23 main - Effect VectorClock [Thread [].23] Effect { reads = fromList [TVarId 2] } 0s - Thread {5}.0 - Mask Unmasked 0s - Thread {5}.0 - Deschedule Interruptable 0s - Thread {5}.0 - Effect VectorClock [Thread {5}.0, Thread [].19] Effect { } 0s - Thread {5}.1 5 - TxCommitted [] [TVarId 7] Effect { reads = fromList [TVarId 1] } 0s - Thread {5}.1 5 - Unblocked [] 0s - Thread {5}.1 5 - Deschedule Yield 0s - Thread {5}.1 5 - Effect VectorClock [Thread {5}.1, Thread [].22] Effect { reads = fromList [TVarId 1] } 0s - Thread {5}.2 5 - FollowControl ControlAwait [ScheduleMod (RacyThreadId [5],2) ControlDefault [(RacyThreadId [4],0),(RacyThreadId [4],1),(RacyThreadId [4],2),(RacyThreadId [3],0),(RacyThreadId [3],1),(RacyThreadId [2],0),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [3],2),(RacyThreadId [3],3),(RacyThreadId [3],4),(RacyThreadId [3],5),(RacyThreadId [1],2),(RacyThreadId [1],3)]] 0s - Thread {5}.2 5 - AwaitControl Thread {5}.2 ControlFollow [(RacyThreadId [4],0),(RacyThreadId [4],1),(RacyThreadId [4],2),(RacyThreadId [3],0),(RacyThreadId [3],1),(RacyThreadId [2],0),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [3],2),(RacyThreadId [3],3),(RacyThreadId [3],4),(RacyThreadId [3],5),(RacyThreadId [1],2),(RacyThreadId [1],3)] [] 0s - Thread {5}.2 5 - Deschedule Sleep 0s - Thread {5}.2 5 - ThreadSleep 0s - Thread {4}.0 - Reschedule ControlFollow [(RacyThreadId [4],0),(RacyThreadId [4],1),(RacyThreadId [4],2),(RacyThreadId [3],0),(RacyThreadId [3],1),(RacyThreadId [2],0),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [3],2),(RacyThreadId [3],3),(RacyThreadId [3],4),(RacyThreadId [3],5),(RacyThreadId [1],2),(RacyThreadId [1],3)] [] 0s - Thread {4}.0 - PerformAction Thread {4}.0 0s - Thread {4}.0 - PerformAction Thread {4}.0 0s - Thread {4}.0 - Mask Unmasked 0s - Thread {4}.0 - Deschedule Interruptable 0s - Thread {4}.0 - Effect VectorClock [Thread {4}.0, Thread [].15] Effect { } 0s - Thread {4}.1 - PerformAction Thread {4}.1 0s - Thread {4}.1 - PerformAction Thread {4}.1 0s - Thread {4}.1 4 - PerformAction Thread {4}.1 0s - Thread {4}.1 4 - TxCommitted [] [TVarId 8] Effect { reads = fromList [TVarId 1] } 0s - Thread {4}.1 4 - Unblocked [] 0s - Thread {4}.1 4 - Deschedule Yield 0s - Thread {4}.1 4 - Effect VectorClock [Thread {4}.1, Thread [].22] Effect { reads = fromList [TVarId 1] } 0s - Thread {4}.2 - Reschedule ControlFollow [(RacyThreadId [4],2),(RacyThreadId [3],0),(RacyThreadId [3],1),(RacyThreadId [2],0),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [3],2),(RacyThreadId [3],3),(RacyThreadId [3],4),(RacyThreadId [3],5),(RacyThreadId [1],2),(RacyThreadId [1],3)] [] 0s - Thread {4}.2 4 - PerformAction Thread {4}.2 0s - Thread {4}.2 4 - ThrowTo (ExitFailure 0) Thread {2} 0s - Thread {4}.2 4 - ThrowToBlocked 0s - Thread {4}.2 4 - Deschedule Blocked BlockedOnThrowTo 0s - Thread {4}.2 4 - Effect VectorClock [Thread {2}.0, Thread {4}.2, Thread [].22] Effect { throws = [Thread {2}] } 0s - Thread {3}.0 - Reschedule ControlFollow [(RacyThreadId [3],0),(RacyThreadId [3],1),(RacyThreadId [2],0),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [3],2),(RacyThreadId [3],3),(RacyThreadId [3],4),(RacyThreadId [3],5),(RacyThreadId [1],2),(RacyThreadId [1],3)] [] 0s - Thread {3}.0 - PerformAction Thread {3}.0 0s - Thread {3}.0 - PerformAction Thread {3}.0 0s - Thread {3}.0 - Mask Unmasked 0s - Thread {3}.0 - Deschedule Interruptable 0s - Thread {3}.0 - Effect VectorClock [Thread {3}.0, Thread [].11] Effect { } 0s - Thread {3}.1 - PerformAction Thread {3}.1 0s - Thread {3}.1 - PerformAction Thread {3}.1 0s - Thread {3}.1 3 - PerformAction Thread {3}.1 0s - Thread {3}.1 3 - TxCommitted [] [TVarId 9] Effect { reads = fromList [TVarId 1] } 0s - Thread {3}.1 3 - Unblocked [] 0s - Thread {3}.1 3 - Deschedule Yield 0s - Thread {3}.1 3 - Effect VectorClock [Thread {3}.1, Thread [].22] Effect { reads = fromList [TVarId 1] } 0s - Thread {2}.0 - Reschedule ControlFollow [(RacyThreadId [2],0),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [3],2),(RacyThreadId [3],3),(RacyThreadId [3],4),(RacyThreadId [3],5),(RacyThreadId [1],2),(RacyThreadId [1],3)] [] 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 - ThrowToUnmasked Labelled Thread {4} 4 0s - Thread {2}.0 - Effect VectorClock [Thread {2}.0, Thread [].7] Effect { wakeup = [Thread {4}] } 0s - Thread {4}.- 4 - ThrowToWakeup 0s - Thread {2}.0 - Deschedule Yield 0s - Thread {2}.0 - Effect VectorClock [Thread {2}.0, Thread {4}.2, Thread [].22] Effect { wakeup = [Thread {4}] } 0s - Thread {1}.0 - Reschedule ControlFollow [(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [3],2),(RacyThreadId [3],3),(RacyThreadId [3],4),(RacyThreadId [3],5),(RacyThreadId [1],2),(RacyThreadId [1],3)] [] 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 [].3] Effect { } 0s - Thread {1}.1 - PerformAction Thread {1}.1 0s - Thread {1}.1 - PerformAction Thread {1}.1 0s - Thread {1}.1 1 - PerformAction Thread {1}.1 0s - Thread {1}.1 1 - TxCommitted [] [TVarId 10] Effect { reads = fromList [TVarId 1] } 0s - Thread {1}.1 1 - Unblocked [] 0s - Thread {1}.1 1 - Deschedule Yield 0s - Thread {1}.1 1 - Effect VectorClock [Thread {1}.1, Thread [].22] Effect { reads = fromList [TVarId 1] } 0s - Thread {3}.2 - Reschedule ControlFollow [(RacyThreadId [3],2),(RacyThreadId [3],3),(RacyThreadId [3],4),(RacyThreadId [3],5),(RacyThreadId [1],2),(RacyThreadId [1],3)] [] 0s - Thread {3}.2 3 - PerformAction Thread {3}.2 0s - Thread {3}.2 3 - TxCommitted [TVarId 0] [] Effect { reads = fromList [TVarId 0], writes = fromList [TVarId 0] } 0s - Thread {3}.2 3 - Say 0 0s - Thread {3}.2 3 - Unblocked [] 0s - Thread {3}.2 3 - Deschedule Yield 0s - Thread {3}.2 3 - Effect VectorClock [Thread {3}.2, Thread [].22] Effect { reads = fromList [TVarId 0], writes = fromList [TVarId 0] } 0s - Thread {3}.3 - Reschedule ControlFollow [(RacyThreadId [3],3),(RacyThreadId [3],4),(RacyThreadId [3],5),(RacyThreadId [1],2),(RacyThreadId [1],3)] [] 0s - Thread {3}.3 3 - PerformAction Thread {3}.3 0s - Thread {3}.3 3 - Mask MaskedInterruptible 0s - Thread {3}.3 3 - Deschedule Interruptable 0s - Thread {3}.3 3 - Effect VectorClock [Thread {3}.3, Thread [].22] Effect { } 0s - Thread {3}.4 3 - PerformAction Thread {3}.4 0s - Thread {3}.4 3 - PerformAction Thread {3}.4 0s - Thread {3}.4 3 - TxCommitted [Labelled TVarId 4 async-RacyThreadId [3]] [] Effect { reads = fromList [TVarId 4], writes = fromList [TVarId 4] } 0s - Thread {3}.4 3 - Unblocked [] 0s - Thread {3}.4 3 - Deschedule Yield 0s - Thread {3}.4 3 - Effect VectorClock [Thread {3}.4, Thread [].22] Effect { reads = fromList [TVarId 4], writes = fromList [TVarId 4] } 0s - Thread {3}.5 - Reschedule ControlFollow [(RacyThreadId [3],5),(RacyThreadId [1],2),(RacyThreadId [1],3)] [] 0s - Thread {3}.5 3 - PerformAction Thread {3}.5 0s - Thread {3}.5 3 - ThreadFinished 0s - Thread {3}.5 3 - Deschedule Terminated 0s - Thread {3}.5 3 - Effect VectorClock [Thread {3}.5, Thread [].22] Effect { } 0s - Thread {1}.2 - Reschedule ControlFollow [(RacyThreadId [1],2),(RacyThreadId [1],3)] [] 0s - Thread {1}.2 1 - PerformAction Thread {1}.2 0s - Thread {1}.2 1 - TxBlocked [TVarId 0] Effect { reads = fromList [TVarId 0] } 0s - Thread {1}.2 1 - Deschedule Blocked BlockedOnSTM 0s - Thread {1}.2 1 - Effect VectorClock [Thread {1}.2, Thread {3}.2, Thread [].22] Effect { reads = fromList [TVarId 0] } InternalError "assertion failure: Thread {1} not runnable" assertion failure: Thread {1} not runnable Use --quickcheck-replay=901028 to reproduce. Use -p '/propExploration/' to rerun this test only.
Ref. I also reproduced it on Linux.
Describe the bug The following counterexample is found:
Ref. I also reproduced it on Linux.