mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-12-19 03:21:49 +03:00
cea4d59b3c
Conceptually, commits are happening truly in parallel
nondeterministically, and the commit threads are introduced to unify
this source of nondeterminism with the scheduling decisions. Commit
threads are not real threads, and switching to one is not a real context
switch, it therefore doesn't count as a preemption.
For example, this execution clearly has no preemptions in:
S1---C-S1---
It would be absurd to say it has 1 preemption. But what about this?
S1---C-S2---
This clearly DOES have a preemption. S1 was preempted by C (but we don't
count that), and then S2 started to execute! Control should have been
returned to S1.
Prior to now, this case was not considered specially. So every commit
effectively gives rise to a free preemption! This is bad for two
reasons:
- More schedules get executed, so testing takes longer.
- This is actually, in a sense, unsound! Results are potentially being
reported which could NEVER arise under ANY real-world execution
subject to those bounds!
It is because of this latter point that some of the expected results in
test litmusWP27 have been removed. They require more than the standard
two preemptions to observe.
Closes #39.
170 lines
6.7 KiB
Haskell
Executable File
170 lines
6.7 KiB
Haskell
Executable File
{-# LANGUAGE RankNTypes #-}
|
|
|
|
module Cases.Litmus where
|
|
|
|
import Control.Monad (replicateM)
|
|
import Data.List (nub, sort)
|
|
import Test.DejaFu (MemType(..), defaultBounds, gives')
|
|
import Test.DejaFu.Deterministic (ConcST)
|
|
import Test.DejaFu.SCT (sctPreBound, defaultPreemptionBound)
|
|
import Test.Framework (Test, testGroup)
|
|
import Test.Framework.Providers.HUnit (hUnitTestToTests)
|
|
import Test.HUnit (test)
|
|
import Test.HUnit.DejaFu (testDejafu')
|
|
|
|
import Control.Monad.Conc.Class
|
|
|
|
tests :: [Test]
|
|
tests =
|
|
[ litmusTest "intelWP21" intelWP21
|
|
[(0,0),(0,1),(1,1)]
|
|
[(0,0),(0,1),(1,1)]
|
|
[(0,0),(0,1),(1,1)]
|
|
|
|
, litmusTest "intelWP22" intelWP22
|
|
[(0,0),(0,1),(1,0)]
|
|
[(0,0),(0,1),(1,0)]
|
|
[(0,0),(0,1),(1,0)]
|
|
|
|
, litmusTest "intelWP23" intelWP23
|
|
[(0,1),(1,0),(1,1)]
|
|
[(0,0),(0,1),(1,0),(1,1)]
|
|
[(0,0),(0,1),(1,0),(1,1)]
|
|
|
|
, litmusTest "intelWP24" intelWP24
|
|
[(1,1)]
|
|
[(1,1)]
|
|
[(1,1)]
|
|
|
|
, litmusTest "intelWP25" intelWP25
|
|
[((1,0),(1,1)),((1,1),(1,0)),((1,1),(1,1))]
|
|
[((1,0),(1,0)),((1,0),(1,1)),((1,1),(1,0)),((1,1),(1,1))]
|
|
[((1,0),(1,0)),((1,0),(1,1)),((1,1),(1,0)),((1,1),(1,1))]
|
|
|
|
, litmusTest "intelWP26" intelWP26
|
|
[(0,0,0),(0,0,1),(1,0,1)]
|
|
[(0,0,0),(0,0,1),(1,0,0),(1,0,1)]
|
|
[(0,0,0),(0,0,1),(1,0,0),(1,0,1)]
|
|
|
|
, litmusTest "intelWP27" intelWP27
|
|
[((0,0),(0,0)),((0,0),(1,1)),((0,0),(2,2)),((1,1),(1,1)),((1,1),(1,2)),((1,1),(2,1)),((1,1),(2,2)),((1,2),(1,1)),((1,2),(2,2)),((2,1),(1,1)),((2,1),(2,2)),((2,2),(1,1)),((2,2),(2,1)),((2,2),(2,2))]
|
|
[((0,0),(0,0)),((0,0),(1,1)),((0,0),(2,2)),((1,1),(1,1)),((1,1),(1,2)),((1,1),(2,1)),((1,1),(2,2)),((1,2),(1,1)),((1,2),(2,2)),((2,1),(1,1)),((2,1),(2,2)),((2,2),(1,1)),((2,2),(2,1)),((2,2),(2,2))]
|
|
[((0,0),(0,0)),((0,0),(1,1)),((0,0),(2,2)),((1,1),(1,1)),((1,1),(1,2)),((1,1),(2,1)),((1,1),(2,2)),((1,2),(1,1)),((1,2),(2,2)),((2,1),(1,1)),((2,1),(2,2)),((2,2),(1,1)),((2,2),(2,1)),((2,2),(2,2))]
|
|
|
|
, litmusTest "intelWP28" intelWP28
|
|
[((0,0),(0,0)),((0,0),(0,1)),((0,0),(1,0)),((0,0),(1,1)),((0,1),(1,0)),((0,1),(1,1)),((1,0),(0,1)),((1,0),(1,1)),((1,1),(1,1))]
|
|
[((0,0),(0,0)),((0,0),(0,1)),((0,0),(1,0)),((0,0),(1,1)),((0,1),(1,0)),((0,1),(1,1)),((1,0),(0,1)),((1,0),(1,1)),((1,1),(0,1)),((1,1),(1,0)),((1,1),(1,1))]
|
|
[((0,0),(0,0)),((0,0),(0,1)),((0,0),(1,0)),((0,0),(1,1)),((0,1),(1,0)),((0,1),(1,1)),((1,0),(0,1)),((1,0),(1,1)),((1,1),(0,1)),((1,1),(1,0)),((1,1),(1,1))]
|
|
]
|
|
|
|
litmusTest :: (Eq a, Show a) => String -> (forall t. ConcST t a) -> [a] -> [a] -> [a] -> Test
|
|
litmusTest name act sq tso pso = testGroup name . hUnitTestToTests $ test
|
|
[ testDejafu' SequentialConsistency defaultBounds act "SQ" (gives' sq)
|
|
, testDejafu' TotalStoreOrder defaultBounds act "TSO" (gives' tso)
|
|
, testDejafu' PartialStoreOrder defaultBounds act "PSO" (gives' pso)
|
|
]
|
|
|
|
-- | Run a litmus test against the three different memory models, and
|
|
-- real IO, and print the results.
|
|
--
|
|
-- Make sure before doing this that you have more than 1 capability,
|
|
-- or the @IO@ behaviour will be severely constrained! The @IO@ test
|
|
-- is run 99,999 times, but is still not guaranteed to see all the
|
|
-- possible results. This is why dejafu is good!
|
|
compareTest :: (Ord a, Show a) => (forall m. MonadConc m => m a) -> IO ()
|
|
compareTest act = do
|
|
putStrLn $ "DejaFu-SQ: " ++ results SequentialConsistency
|
|
putStrLn $ "DejaFu-TSO: " ++ results TotalStoreOrder
|
|
putStrLn $ "DejaFu-PSO: " ++ results PartialStoreOrder
|
|
putStr "IO: " >> ioResults >>= putStrLn
|
|
|
|
where
|
|
results memtype = show . nub . sort . map (\(Right a,_) -> a) $
|
|
sctPreBound memtype defaultPreemptionBound act
|
|
|
|
ioResults = show . nub . sort <$> replicateM 99999 act
|
|
|
|
-------------------------------------------------------------------------------
|
|
|
|
-- The following collection of litmus tests are all from
|
|
-- <https://orbi.ulg.ac.be/bitstream/2268/158670/1/thesis.pdf>
|
|
|
|
-- | Loads are not reordered with other loads and stores are not
|
|
-- reordered with other stores.
|
|
intelWP21 :: MonadConc m => m (Int, Int)
|
|
intelWP21 = snd <$> litmus2
|
|
(\x y -> writeCRef x 1 >> writeCRef y 1)
|
|
(\x y -> (,) <$> readCRef y <*> readCRef x)
|
|
|
|
-- | Stores are not reordered with older loads.
|
|
intelWP22 :: MonadConc m => m (Int, Int)
|
|
intelWP22 = litmus2
|
|
(\x y -> do r1 <- readCRef x; writeCRef y 1; pure r1)
|
|
(\x y -> do r2 <- readCRef y; writeCRef x 1; pure r2)
|
|
|
|
-- | Loads may be reordered with older stores to different locations.
|
|
intelWP23 :: MonadConc m => m (Int, Int)
|
|
intelWP23 = litmus2
|
|
(\x y -> writeCRef x 1 >> readCRef y)
|
|
(\x y -> writeCRef y 1 >> readCRef x)
|
|
|
|
-- | Loads are not reordered with older stores to the same location.
|
|
intelWP24 :: MonadConc m => m (Int, Int)
|
|
intelWP24 = litmus2
|
|
(\x _ -> writeCRef x 1 >> readCRef x)
|
|
(\_ y -> writeCRef y 1 >> readCRef y)
|
|
|
|
-- | Intra-processor forwarding is allowed
|
|
intelWP25 :: MonadConc m => m ((Int, Int), (Int, Int))
|
|
intelWP25 = litmus2
|
|
(\x y -> do writeCRef x 1; r1 <- readCRef x; r2 <- readCRef y; pure (r1, r2))
|
|
(\x y -> do writeCRef y 1; r3 <- readCRef y; r4 <- readCRef x; pure (r3, r4))
|
|
|
|
-- | Stores are transitively visible.
|
|
intelWP26 :: MonadConc m => m (Int, Int, Int)
|
|
intelWP26 = do
|
|
x <- newCRef 0
|
|
y <- newCRef 0
|
|
j1 <- spawn (writeCRef x 1)
|
|
j2 <- spawn (do r1 <- readCRef x; writeCRef x 1; pure r1)
|
|
j3 <- spawn (do r2 <- readCRef y; r3 <- readCRef x; pure (r2,r3))
|
|
(\() r1 (r2,r3) -> (r1,r2,r3)) <$> readMVar j1 <*> readMVar j2 <*> readMVar j3
|
|
|
|
-- | Total order on stores to the same location.
|
|
intelWP27 :: MonadConc m => m ((Int, Int), (Int, Int))
|
|
intelWP27 = do
|
|
x <- newCRef 0
|
|
j1 <- spawn (writeCRef x 1)
|
|
j2 <- spawn (writeCRef x 2)
|
|
j3 <- spawn (do r1 <- readCRef x; r2 <- readCRef x; pure (r1, r2))
|
|
j4 <- spawn (do r3 <- readCRef x; r4 <- readCRef x; pure (r3, r4))
|
|
(\() () r12 r23 -> (r12, r23)) <$> readMVar j1 <*> readMVar j2 <*> readMVar j3 <*> readMVar j4
|
|
|
|
-- | Independent Read Independent Write.
|
|
--
|
|
-- IRIW is a standard litmus test which allows in some architectures
|
|
-- ((1,0),(1,0)). Intel (and TSO/PSO) forbid it.
|
|
intelWP28 :: MonadConc m => m ((Int, Int), (Int, Int))
|
|
intelWP28 = do
|
|
x <- newCRef 0
|
|
y <- newCRef 0
|
|
j1 <- spawn (writeCRef x 1)
|
|
j2 <- spawn (writeCRef y 1)
|
|
j3 <- spawn (do r1 <- readCRef x; r2 <- readCRef y; pure (r1, r2))
|
|
j4 <- spawn (do r3 <- readCRef y; r4 <- readCRef x; pure (r3, r4))
|
|
(\() () r12 r23 -> (r12, r23)) <$> readMVar j1 <*> readMVar j2 <*> readMVar j3 <*> readMVar j4
|
|
|
|
-------------------------------------------------------------------------------
|
|
|
|
-- | Create two @CRef@s, fork the two threads, and return the result.
|
|
litmus2 :: MonadConc m
|
|
=> (CRef m Int -> CRef m Int -> m b)
|
|
-> (CRef m Int -> CRef m Int -> m c)
|
|
-> m (b, c)
|
|
litmus2 thread1 thread2 = do
|
|
x <- newCRef 0
|
|
y <- newCRef 0
|
|
j1 <- spawn (thread1 x y)
|
|
j2 <- spawn (thread2 x y)
|
|
(,) <$> readMVar j1 <*> readMVar j2
|