dejafu 0.9.0.2 → 0.9.0.3

raw patch · 4 files changed

+52/−36 lines, 4 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.markdown +17/−0
• Test/DejaFu/SCT.hs +3/−6
• Test/DejaFu/SCT/Internal.hs +30/−28
• dejafu.cabal +2/−2

@@ -7,6 +7,23 @@ *de facto* standard Haskell versioning scheme.  +0.9.0.3+-------++- **Date**    2017-11-06+- **Git tag** [dejafu-0.9.0.3][]+- **Hackage** https://hackage.haskell.org/package/dejafu-0.9.0.3++### Miscellaneous++- Impose a dependency between commits and memory barriers, to make barriers sound (#138).++[dejafu-0.9.0.3]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.9.0.3+++---------------------------------------------------------------------------------------------------++ 0.9.0.2 ------- 

@@ -512,7 +512,7 @@                                        conc        let bpoints = findBacktracks (schedBoundKill s) (schedBPoints s) trace-      let newDPOR = addTrace conservative trace dp+      let newDPOR = incorporateTrace conservative trace dp        if schedIgnore s         then go (force newDPOR)@@ -521,13 +521,10 @@     Nothing -> pure []    -- The DPOR scheduler.-  scheduler = dporSched memtype (cBound cb)+  scheduler = dporSched (cBound cb)    -- Find the new backtracking steps.-  findBacktracks = findBacktrackSteps memtype (cBacktrack cb)--  -- Incorporate a trace into the DPOR tree.-  addTrace = incorporateTrace memtype+  findBacktracks = findBacktrackSteps (cBacktrack cb)  -- | SCT via uniform random scheduling. --

@@ -140,9 +140,7 @@  -- | Add a new trace to the stack.  This won't work if to-dos aren't explored depth-first. incorporateTrace-  :: MemType-  -- ^ Memory model-  -> Bool+  :: Bool   -- ^ Whether the \"to-do\" point which was used to create this new   -- execution was conservative or not.   -> Trace@@ -150,7 +148,7 @@   -- and the action performed.   -> DPOR   -> DPOR-incorporateTrace memtype conservative trace dpor0 = grow initialDepState (initialDPORThread dpor0) trace dpor0 where+incorporateTrace conservative trace dpor0 = grow initialDepState (initialDPORThread dpor0) trace dpor0 where   grow state tid trc@((d, _, a):rest) dpor =     let tid'   = tidOf tid d         state' = updateDepState state tid' a@@ -174,7 +172,7 @@   -- Construct a new subtree corresponding to a trace suffix.   subtree state tid sleep ((_, _, a):rest) =     let state' = updateDepState state tid a-        sleep' = M.filterWithKey (\t a' -> not $ dependent memtype state' tid a t a') sleep+        sleep' = M.filterWithKey (\t a' -> not $ dependent state' tid a t a') sleep     in DPOR         { dporRunnable = S.fromList $ case rest of             ((_, runnable, _):_) -> map fst runnable@@ -207,9 +205,7 @@ -- runnable, a dependency is imposed between this final action and -- everything else. findBacktrackSteps-  :: MemType-  -- ^ Memory model.-  -> BacktrackFunc+  :: BacktrackFunc   -- ^ Backtracking function. Given a list of backtracking points, and   -- a thread to backtrack to at a specific point in that list, add   -- the new backtracking points. There will be at least one: this@@ -226,7 +222,7 @@   -> Trace   -- ^ The execution trace.   -> [BacktrackStep]-findBacktrackSteps memtype backtrack boundKill = go initialDepState S.empty initialThread [] . F.toList where+findBacktrackSteps backtrack boundKill = go initialDepState S.empty initialThread [] . F.toList where   -- Walk through the traces one step at a time, building up a list of   -- new backtracking points.   go state allThreads tid bs ((e,i):is) ((d,_,a):ts) =@@ -284,7 +280,7 @@             -- pre-empting the action UNLESS the pre-emption would             -- possibly allow for a different relaxed memory stage.             | isBlock (bcktAction b) && isBarrier (simplifyLookahead n) = False-            | otherwise = dependent' memtype (bcktState b) (bcktThreadid b) (bcktAction b) u n+            | otherwise = dependent' (bcktState b) (bcktThreadid b) (bcktAction b) u n     in backtrack bs idxs  -- | Add new backtracking points, if they have not already been@@ -440,13 +436,11 @@ -- yielded. Furthermore, threads which /will/ yield are ignored in -- preference of those which will not. dporSched-  :: MemType-  -- ^ Memory model.-  -> IncrementalBoundFunc k+  :: IncrementalBoundFunc k   -- ^ Bound function: returns true if that schedule prefix terminated   -- with the lookahead decision fits within the bound.   -> Scheduler (DPORSchedState k)-dporSched memtype boundf = Scheduler $ \prior threads s ->+dporSched boundf = Scheduler $ \prior threads s ->   let     -- The next scheduler state     nextState rest = s@@ -521,7 +515,7 @@     [] ->       let choices  = restrictToBound id initialise           checkDep t a = case prior of-            Just (tid, act) -> dependent memtype (schedDepState s) tid act t a+            Just (tid, act) -> dependent (schedDepState s) tid act t a             Nothing -> False           ssleep'  = M.filterWithKey (\t a -> not $ checkDep t a) $ schedSleep s           choices' = filter (`notElem` M.keys ssleep') choices@@ -586,8 +580,8 @@ -- This is basically the same as 'dependent'', but can make use of the -- additional information in a 'ThreadAction' to make better decisions -- in a few cases.-dependent :: MemType -> DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool-dependent memtype ds t1 a1 t2 a2 = case (a1, a2) of+dependent :: DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool+dependent ds t1 a1 t2 a2 = case (a1, a2) of   -- @SetNumCapabilities@ and @GetNumCapabilities@ are NOT dependent   -- IF the value read is the same as the value written. 'dependent''   -- can not see the value read (as it hasn't happened yet!), and so@@ -611,8 +605,8 @@   (BlockedSTM _, BlockedSTM _) -> checkSTM    _ -> case (,) <$> rewind a1 <*> rewind a2 of-    Just (l1, l2) -> dependent' memtype ds t1 a1 t2 l2 && dependent' memtype ds t2 a2 t1 l1-    _ -> dependentActions memtype ds (simplifyAction a1) (simplifyAction a2)+    Just (l1, l2) -> dependent' ds t1 a1 t2 l2 && dependent' ds t2 a2 t1 l1+    _ -> dependentActions ds (simplifyAction a1) (simplifyAction a2)    where     -- STM actions A and B are dependent if A wrote to anything B@@ -624,8 +618,8 @@ -- -- Termination of the initial thread is handled specially in the DPOR -- implementation.-dependent' :: MemType -> DepState -> ThreadId -> ThreadAction -> ThreadId -> Lookahead -> Bool-dependent' memtype ds t1 a1 t2 l2 = case (a1, l2) of+dependent' :: DepState -> ThreadId -> ThreadAction -> ThreadId -> Lookahead -> Bool+dependent' ds t1 a1 t2 l2 = case (a1, l2) of   -- Worst-case assumption: all IO is dependent.   (LiftIO, WillLiftIO) -> True @@ -648,13 +642,13 @@   (SetNumCapabilities _, WillGetNumCapabilities)   -> True   (SetNumCapabilities a, WillSetNumCapabilities b) -> a /= b -  _ -> dependentActions memtype ds (simplifyAction a1) (simplifyLookahead l2)+  _ -> dependentActions ds (simplifyAction a1) (simplifyLookahead l2)  -- | Check if two 'ActionType's are dependent. Note that this is not -- sufficient to know if two 'ThreadAction's are dependent, without -- being so great an over-approximation as to be useless!-dependentActions :: MemType -> DepState -> ActionType -> ActionType -> Bool-dependentActions memtype ds a1 a2 = case (a1, a2) of+dependentActions :: DepState -> ActionType -> ActionType -> Bool+dependentActions ds a1 a2 = case (a1, a2) of   -- Unsynchronised reads and writes are always dependent, even under   -- a relaxed memory model, as an unsynchronised write gives rise to   -- a commit, which synchronises.@@ -668,13 +662,21 @@   -- empty.   --   -- See [RMMVerification], lemma 5.25.-  (UnsynchronisedWrite r1, _) | same crefOf && isCommit a2 r1 && isBuffered ds r1 -> False-  (_, UnsynchronisedWrite r2) | same crefOf && isCommit a1 r2 && isBuffered ds r2 -> False+  (UnsynchronisedWrite r1, PartiallySynchronisedCommit _) | same crefOf && isBuffered ds r1 -> False+  (PartiallySynchronisedCommit _, UnsynchronisedWrite r2) | same crefOf && isBuffered ds r2 -> False    -- Unsynchronised reads where a memory barrier would flush a   -- buffered write-  (UnsynchronisedRead r1, _) | isBarrier a2 -> isBuffered ds r1 && memtype /= SequentialConsistency-  (_, UnsynchronisedRead r2) | isBarrier a1 -> isBuffered ds r2 && memtype /= SequentialConsistency+  (UnsynchronisedRead r1, _) | isBarrier a2 -> isBuffered ds r1+  (_, UnsynchronisedRead r2) | isBarrier a1 -> isBuffered ds r2++  -- Commits and memory barriers must be dependent, as memory barriers+  -- (currently) flush in a consistent order.  Alternative orders need+  -- to be explored as well.  Perhaps a better implementation of+  -- memory barriers would just block every non-commit thread while+  -- any buffer is nonempty.+  (PartiallySynchronisedCommit _, _) | isBarrier a2 -> True+  (_, PartiallySynchronisedCommit _) | isBarrier a1 -> True    (_, _) -> case getSame crefOf of     -- Two actions on the same CRef where at least one is synchronised

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                dejafu-version:             0.9.0.2+version:             0.9.0.3 synopsis:            Systematic testing for Haskell concurrency.  description:@@ -37,7 +37,7 @@ source-repository this   type:     git   location: https://github.com/barrucadu/dejafu.git-  tag:      dejafu-0.9.0.2+  tag:      dejafu-0.9.0.3  library   exposed-modules:     Test.DejaFu