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.
