Commit 160c64f7 authored by tharris's avatar tharris
Browse files

STM invariants

parent 47ca77ea
......@@ -145,3 +145,7 @@ test('conc059', compose(only_compiler_types(['ghc']),
compile_and_run, ['conc059_c.c'])
clean(['conc059_c.o'])
test('conc060', normal, compile_and_run, ['-package stm'])
test('conc061', normal, compile_and_run, ['-package stm'])
test('conc062', normal, compile_and_run, ['-package stm'])
test('conc063', exit_code(1), compile_and_run, ['-package stm'])
module Main where
import GHC.Conc
import Control.Exception
-- Create trivial invariants using a single TVar
main = do
putStr "\nStarting\n"
x <- atomically ( newTVar 42 )
putStr "\nAdding trivially true invariant (no TVar access)\n"
atomically ( alwaysSucceeds ( return 1 ) )
putStr "\nAdding trivially true invariant (no TVar access)\n"
atomically ( always ( return True ) )
putStr "\nAdding a trivially true invariant (TVar access)\n"
atomically ( alwaysSucceeds ( readTVar x ) )
putStr "\nAdding an invraiant that's false when attemted to be added\n"
Control.Exception.catch (atomically ( do writeTVar x 100
alwaysSucceeds ( do v <- readTVar x
if (v == 100) then throwDyn "URK" else return () )
writeTVar x 0 ) )
(\e -> putStr ("Caught: " ++ (show e) ++ "\n"))
putStr "\nWriting to a TVar watched by a trivially true invariant\n"
atomically ( writeTVar x 17 )
putStr "\nAdding a second trivially true invariant (same TVar access)\n"
atomically ( alwaysSucceeds ( readTVar x ) )
putStr "\nWriting to a TVar watched by both trivially true invariants\n"
atomically ( writeTVar x 18 )
putStr "\nAdding a trivially false invariant (no TVar access)\n"
Control.Exception.catch (atomically ( alwaysSucceeds ( throwDyn "Exn raised in invariant" ) ) )
(\e -> putStr ("Caught: " ++ (show e) ++ "\n"))
putStr "\nAdding a trivially false invariant (no TVar access)\n"
Control.Exception.catch (atomically ( always ( throwDyn "Exn raised in invariant" ) ) )
(\e -> putStr ("Caught: " ++ (show e) ++ "\n"))
putStr "\nAdding a trivially false invariant (no TVar access)\n"
Control.Exception.catch (atomically ( always ( return False ) ) )
(\e -> putStr ("Caught: " ++ (show e) ++ "\n"))
putStr "\nAdding a trivially false invariant (with TVar access)\n"
Control.Exception.catch (atomically (
alwaysSucceeds ( do t <- readTVar x
throwDyn "Exn raised in invariant" ) ) )
(\e -> putStr ("Caught: " ++ (show e) ++ "\n"))
putStr "\nAdding a third invariant true if TVar != 42\n"
atomically ( alwaysSucceeds ( do t <- readTVar x
if (t == 42) then throwDyn "Exn raised in invariant" else return () ) )
putStr "\nViolating third invariant by setting TVar to 42\n"
Control.Exception.catch (atomically ( writeTVar x 42 ) )
(\e -> putStr ("Caught: " ++ (show e) ++ "\n"))
putStr "\nChecking final TVar contents\n"
t <- atomically ( readTVar x )
putStr ("Final value = " ++ (show t) ++ "\n")
putStr "\nDone\n"
Starting
Adding trivially true invariant (no TVar access)
Adding trivially true invariant (no TVar access)
Adding a trivially true invariant (TVar access)
Adding an invraiant that's false when attemted to be added
Caught: exception :: [Char]
Writing to a TVar watched by a trivially true invariant
Adding a second trivially true invariant (same TVar access)
Writing to a TVar watched by both trivially true invariants
Adding a trivially false invariant (no TVar access)
Caught: exception :: [Char]
Adding a trivially false invariant (no TVar access)
Caught: exception :: [Char]
Adding a trivially false invariant (no TVar access)
Caught: Transacional invariant violation
Adding a trivially false invariant (with TVar access)
Caught: exception :: [Char]
Adding a third invariant true if TVar != 42
Violating third invariant by setting TVar to 42
Caught: exception :: [Char]
Checking final TVar contents
Final value = 18
Done
module Main where
import GHC.Conc
import Control.Concurrent
import Control.Exception
main = do putStr "Starting\n";
t <- atomically (newTVar 42)
v <- atomically (readTVar t)
putStr ("TVar contains " ++ (show v) ++ "\n")
-- ......................................................................
-- Check that we roll back when an exception leaves an atomic block
putStr ("Raising uncaught exn in atomic block\n");
Control.Exception.catch (atomically (
do writeTVar t 17
throwDyn "Exn raised in a tx" ) )
(\e -> putStr ("Caught: " ++ (show e) ++ "\n"))
v <- atomically (readTVar t)
putStr ("TVar contains " ++ (show v) ++ "\n")
-- ......................................................................
-- Check that we commit a catchSTM nested tx
putStr ("Trying a catchSTM without raising an exception\n");
Control.Exception.catch (atomically (
catchSTM ( do writeTVar t 17 )
( \e -> throw e ) ) )
(\e -> putStr ("Caught: " ++ (show e) ++ "\n"))
v <- atomically (readTVar t)
putStr ("TVar contains " ++ (show v) ++ "\n")
-- ......................................................................
-- Check that we roll back when an exception is caught and rethrown in
-- an atomic block
putStr ("Raising caught and rethrown exn in atomic block\n");
Control.Exception.catch (atomically (
catchSTM ( do writeTVar t 42
throwDyn "Exn raised in a tx" )
( \e -> throw e ) ) )
(\e -> putStr ("Caught: " ++ (show e) ++ "\n"))
v <- atomically (readTVar t)
putStr ("TVar contains " ++ (show v) ++ "\n")
-- ......................................................................
-- Check that we roll back just the "catchSTM" block when an exception is
-- raised in it (but caught later in the same atomic block)
putStr ("Raising caught and rethrown exn in atomic block\n");
v <- atomically (
do writeTVar t 0
catchSTM ( do writeTVar t 1
throwDyn "Exn raised in a tx" )
( \_ -> return () )
readTVar t )
putStr ("TVar contained " ++ (show v) ++ " at end of atomic block\n")
v <- atomically (readTVar t)
putStr ("TVar contains " ++ (show v) ++ "\n")
-- ......................................................................
-- Check that 'retry' can propagate through a catchSTM
putStr ("Testing retry inside catchSTM\n");
Control.Exception.catch (atomically (
( catchSTM ( retry )
( \e -> throw e ) )
`orElse` ( return () ) ) )
(\e -> putStr ("Caught: " ++ (show e) ++ "\n"))
v <- atomically (readTVar t)
putStr ("TVar contains " ++ (show v) ++ "\n")
Starting
TVar contains 42
Raising uncaught exn in atomic block
Caught: exception :: [Char]
TVar contains 42
Trying a catchSTM without raising an exception
TVar contains 17
Raising caught and rethrown exn in atomic block
Caught: exception :: [Char]
TVar contains 17
Raising caught and rethrown exn in atomic block
TVar contained 0 at end of atomic block
TVar contains 0
Testing retry inside catchSTM
TVar contains 0
module Main where
import GHC.Conc
import Control.Exception
-- Test invariants using multiple TVars
main = do
putStr "\nStarting\n"
(x1, x2, x3) <- atomically ( do x1 <- newTVar 0
x2 <- newTVar 0
x3 <- newTVar 0
return (x1, x2, x3))
putStr "\nAttaching invariant\n";
atomically ( alwaysSucceeds ( do v1 <- readTVar x1
v23 <- readTVar (if (v1 >= 0) then x2 else x3)
if (v23 > v1) then throwDyn "Exn" else return () ) )
putStr "\nTouching invariant (should keep on same TVars)\n"
atomically ( do writeTVar x1 1
writeTVar x2 1 )
putStr "\nTouching invariant (should move it to other TVars)\n"
atomically ( do writeTVar x1 (-1)
writeTVar x3 (-1) )
putStr "\nTouching invariant (should keep on same TVars)\n"
atomically ( do writeTVar x1 (-2)
writeTVar x3 (-3) )
putStr "\nChecking TVar contents\n"
(t1, t2, t3) <- atomically ( do t1 <- readTVar x1
t2 <- readTVar x2
t3 <- readTVar x3
return (t1, t2, t3))
putStr ("Contents = (" ++ (show t1) ++ "," ++ (show t2) ++ "," ++ (show t3) ++ ")\n")
putStr "\nDone\n"
Starting
Attaching invariant
Touching invariant (should keep on same TVars)
Touching invariant (should move it to other TVars)
Touching invariant (should keep on same TVars)
Checking TVar contents
Contents = (-2,1,-3)
Done
module Main where
import GHC.Conc
import Control.Exception
-- Test invariants using updates & blocking in invariants
main = do
putStr "\nStarting\n"
(x1, x2, x3) <- atomically ( do x1 <- newTVar 0
x2 <- newTVar 0
x3 <- newTVar 0
return (x1, x2, x3))
putStr "\nAttaching successful invariant that makes an update\n";
atomically ( alwaysSucceeds ( writeTVar x1 42 ) )
putStr "\nAttaching successful invariant that uses retry&orelse internally\n";
atomically ( alwaysSucceeds ( retry `orElse` return () ) )
putStr "\nAttaching a failed invariant that makes an update\n";
Control.Exception.catch (atomically ( do writeTVar x1 17
alwaysSucceeds ( throwDyn "Exn raised in invariant" ) ) )
(\e -> putStr ("Caught: " ++ (show e) ++ "\n"))
putStr "\nAttaching an invariant that blocks\n";
forkIO ( do threadDelay 1000000
atomically ( writeTVar x1 10 )
return ())
atomically ( do alwaysSucceeds ( do v1 <- readTVar x1
if (v1 == 0) then retry else return () )
)
putStr "\nAnother update to the TVar with the blocking invariant\n"
atomically ( writeTVar x1 20 )
putStr "\nUpdate the TVar to cause the invariant to block again (expect thread blocked indef)\n"
atomically ( writeTVar x1 0 )
Starting
Attaching successful invariant that makes an update
Attaching successful invariant that uses retry&orelse internally
Attaching a failed invariant that makes an update
Caught: exception :: [Char]
Attaching an invariant that blocks
Another update to the TVar with the blocking invariant
Update the TVar to cause the invariant to block again (expect thread blocked indef)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment