IOSimPOR propExploration failure

[coot]

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.