There should be a patch release of dejafu after this, since the
doctest examples changed.
Also, need to bump to a nightly snapshot in `stack.yaml` for
stylish-haskell, which looks to have skipped GHC 9.0 support.
In principle, we could now drop support for GHC 8.0, 8.2, and 8.4, but
supporting those isn't causing any problems yet.
With the ParMonad / "testing exposes a deadlock" / randomly test,
simplification threw an error:
Exception: (dejafu) Got a different result after simplifying:
'True' /= 'Abort'
This is failing even with previously supported versions of GHC, so I
think it's a new library version (probably random, giving an original
trace which exposes the bug).
Disabling "safe IO" for this test fixes it, which means that either
the IO is not safe after all, or that there's another bug elsewhere
which is being hidden now that simplification is more
restricted... however, none of the other tests are failing, so I hope
it's just the IO.
This adds the overhead of constructing the effect to every STM
transaction, which I worried would be a large cost; but it turns out
that the overhead is negligible.
This is for transactions which throw an exception, rather than
stuffing that information into the `STM` action. This makes the
traces a bit clearer (eg, you can now tell without needing to inspect
the STM trace if an exception was thrown by a transaction).
I've called this "ThrownSTM" rather than "ThrowSTM" because it's like
"BlockedSTM" (just another failure case), and that's also past tense.
In this excerpt:
uninterruptibleMask $ \restore -> fork $ do
result <- try (restore (throw ThreadKilled))
...
The `throw` jumps to an exception handler registered outside the
`restore`, which means there is a masking state change. Previously,
dejafu handled this by inserting an `AResetMask` action as the first
action of the handler; but this is incorrect, as it opens a potential
race condition with another thread calling `throwTo`. As `throw` (and
`throwTo`, and an uncaught `throwSTM`) "use up" the exception handler,
this is not a benign race: the thread will be killed!
The solution is to atomically restore the masking state.
This commit implements that, and changes `Throw`, `ThrowTo`, and `STM`
to include the new masking state (if it changed). I think this is a
bit confusing, so I'll make a follow-up commit to split out a new
`ThrownSTM` action.
It's wrong to use initialDepState when there is a setup action, as the
action could end with a DepState which is not the same as the initial
one. Here's an example of it going wrong:
> :{
resultsSet defaultWay defaultMemType $ do
v <- newMVar ()
fork (takeMVar v)
readMVar v
:}
fromList [Left Deadlock,Right ()]
> :{
resultsSet defaultWay defaultMemType $
withSetup (newMVar ()) $ \v -> do
fork (takeMVar v)
readMVar v
:}
fromList [Right ()]
This PR pushes responsibility for the DepState into the Context, and
the DepState is passed to all schedulers. That means it's been
promoted from an internal type to a user-facing one, so I gave it the
more generic name "ConcurrencyState". Furthermore, the snapshotted
DepState is passed to all the DPOR functions, and the trace
simplification functions.
initialDepState is now only used:
- in Conc.Internal to initialise a new context
- in SCT.Internal when there is no snapshot
With careful application of typeclass instances to this GADT, and by
redefining 'ConcT' in terms of it, this solves the type inference
problem and removes the need for the 'basic' function. This approach
also has less newtype wrapping/unwrapping, and so is probably a step
in the right direction even without the type inference advantages.
The diff is quite big because things have needed to migrate between
modules to avoid the import graph getting even worse.
This works by pulling the LengthBound out of the Bounds. A logical
extension of this would be to do away with Bounds entirely, and make
PreemptionBound and FairBound settings in their own right, but as they
only apply to DPOR, keeping them coupled to it feels less misleading.
The 'Program' is the new formulation of dejafu unit tests. A
'Program' is one of three types:
- A 'ConcT', which is as before.
- A 'WithSetup', which corresponds to 'dontCheck'.
- A 'WithSetupAndTeardown', which corresponds to 'subconcurrency'.
This more new formulation makes it impossible to nest 'withSetup' (the
replacement for 'dontCheck') or 'withSetupAndTeardown' (the
half-replacement for 'subconcurrency'), by as these functions take a
'ConcT' as their argument and produce a 'Program WithSetup' or
'Program WithSetupAndTeardown'.
The testing functions have all been generalised to work with this
'Program' type.
