Failing to remove dependent transitions from the sleep set, somewhere

[barrucadu]

This is now half-done: #185 implements enforcing the correctness invariants.

However, the sleep set invariant does not hold, so there's a problem somewhere. Fortunately I am pretty sure that we're just forgetting to remove a dependent transition from the set somewhere, so it's no great concern. But it would be good to fix that to close off this issue.

---

dejafu/dejafu/Test/DejaFu/SCT/Internal/DPOR.hs

Lines 37 to 59 in 5237eff

	-- | DPOR execution is represented as a tree of states, characterised
	-- by the decisions that lead to that state.
	data DPOR = DPOR
	{ dporRunnable :: Set ThreadId
	-- ^ What threads are runnable at this step.
	, dporTodo :: Map ThreadId Bool
	-- ^ Follow-on decisions still to make, and whether that decision
	-- was added conservatively due to the bound.
	, dporNext :: Maybe (ThreadId, DPOR)
	-- ^ The next decision made. Executions are explored in a
	-- depth-first fashion, so this changes as old subtrees are
	-- exhausted and new ones explored.
	, dporDone :: Set ThreadId
	-- ^ All transitions which have been taken from this point,
	-- including conservatively-added ones.
	, dporSleep :: Map ThreadId ThreadAction
	-- ^ Transitions to ignore (in this node and children) until a
	-- dependent transition happens.
	, dporTaken :: Map ThreadId ThreadAction
	-- ^ Transitions which have been taken, excluding
	-- conservatively-added ones. This is used in implementing sleep
	-- sets.
	} deriving (Eq, Show)

There are some data invariants associated with DPOR values:

1. dporTodo is a subset of dporRunnable
2. dporDone is a subset of dporRunnable
3. dporTaken is a subset of dporDone
4. dporTodo and dporDone are disjoint
5. The dporNext thread (if there is one) is in dporDone
6. These properties hold recursively

There's also this one, which is more of a performance issue than a correctness issue:

1. dporSleep and dporDone are disjoint

It would be good to check these invariants everywhere they could in principle be broken (all functions which produce a DPOR):

dejafu/dejafu/Test/DejaFu/SCT/Internal/DPOR.hs

Lines 158 to 164 in 5237eff

	let taken = M.insert tid' a (dporTaken dpor)
	sleep = dporSleep dpor `M.union` dporTaken dpor
	in dpor { dporTaken = if conservative then dporTaken dpor else taken
	, dporTodo = M.delete tid' (dporTodo dpor)
	, dporNext = Just (tid', subtree state' tid' sleep trc)
	, dporDone = S.insert tid' (dporDone dpor)
	}

dejafu/dejafu/Test/DejaFu/SCT/Internal/DPOR.hs

Lines 174 to 191 in 5237eff

	in DPOR
	{ dporRunnable = S.fromList $ case rest of
	((_, runnable, _):_) -> map fst runnable
	[] -> []
	, dporTodo = M.empty
	, dporNext = case rest of
	((d', _, _):_) ->
	let tid' = tidOf tid d'
	in Just (tid', subtree state' tid' sleep' rest)
	[] -> Nothing
	, dporDone = case rest of
	((d', _, _):_) -> S.singleton (tidOf tid d')
	[] -> S.empty
	, dporSleep = sleep'
	, dporTaken = case rest of
	((d', _, a'):_) -> M.singleton (tidOf tid d') a'
	[] -> M.empty
	}

dejafu/dejafu/Test/DejaFu/SCT/Internal/DPOR.hs

Lines 290 to 293 in 5237eff

	dpor' = dpor
	{ dporTodo = dporTodo dpor `M.union` M.fromList todo
	, dporNext = Just (tid, child)
	}

I think the way to do this would be a function like:

verifyDPOR :: String -> DPOR -> DPOR
verifyDPOR src dpor
  | {- if invariant 1 fails -} = fatal src "thread exists in todo set but not in runnable set"
  | {- ... -}
  | otherwise = dpor

There's no need to check the recursive case, as if a DPOR value is recursively valid, then it remains valid even if we attach it to an invalid DPOR value via dporNext. So as long as verifyDPOR gets called everywhere a DPOR value is created or updated, we ensure correctness.