module Data.LVar.Internal.Pure
( PureLVar(..),
newPureLVar, putPureLVar,
waitPureLVar, freezePureLVar,
getPureLVar, unsafeGetPureLVar,
verifyFiniteJoin, verifyFiniteGet
) where
import Control.LVish
import Control.LVish.DeepFrz.Internal
import Control.LVish.Internal
import Data.IORef
import qualified Control.LVish.SchedIdempotent as LI
import Algebra.Lattice
import GHC.Prim (unsafeCoerce#)
import System.IO.Unsafe (unsafePerformIO)
newtype PureLVar s t = PureLVar (LVar s (IORef t) t)
instance Show a => Show (PureLVar Frzn a) where
show (PureLVar lv) = show$ unsafePerformIO$ readIORef$ state lv
verifyFiniteJoin :: (Eq a, Show a) => [a] -> (a -> a -> a) -> Maybe String
verifyFiniteJoin allStates join =
case (isCommutative, isAssociative, isIdempotent) of
(hd : _ , _, _) -> Just $ "commutativity violated!: " ++ show hd
(_ , hd : _, _) -> Just $ "associativity violated!: " ++ show hd
(_ , _, hd : _) -> Just $ "idempotency violated!: " ++ show hd
([], [], []) -> Nothing
where
isCommutative = [(a, b) | a <- allStates, b <- allStates, a `join` b /= b `join` a]
isAssociative = [(a, b, c) |
a <- allStates,
b <- allStates,
c <- allStates,
a `join` (b `join` c) /= (a `join` b) `join` c]
isIdempotent = [a | a <- allStates, a `join` a /= a]
verifyFiniteGet :: (Eq a, Show a, JoinSemiLattice a,
Eq b, Show b) =>
[a] -> (b,b) -> (a -> b) -> Maybe String
verifyFiniteGet allStates (bot,top) getter =
case (botBefore, constAfter) of
((a,b):_, _) -> Just$ "violation! input "++ show a
++" unblocked get, but larger input"++show b++" did not."
(_, (a,b):_) -> Just$ "violation! value at "++ show a
++" was non-bottom ("++show (getter a)
++"), but then changed at "++show b++" ("++ show (getter b)++")"
([],[]) -> Nothing
where
botBefore = [ (a,b)
| a <- allStates, b <- allStates
, a `joinLeq` b, getter b == bot
, not (getter a == bot) ]
constAfter = [ (a,b)
| a <- allStates, b <- allStates
, a `joinLeq` b
, getter a /= bot
, getter a /= getter b
, getter b /= top
]
newPureLVar :: JoinSemiLattice t =>
t -> Par d s (PureLVar s t)
newPureLVar st = WrapPar$ fmap (PureLVar . WrapLVar) $
LI.newLV $ newIORef st
getPureLVar :: (JoinSemiLattice t, Eq t) => PureLVar s t -> [t] -> Par d s t
getPureLVar (PureLVar (WrapLVar lv)) thrshSet =
WrapPar$ LI.getLV lv globalThresh deltaThresh
where globalThresh ref _ = do
x <- readIORef ref
logDbgLn_ 5 " [Pure] Getting from a Pure LVar.. read ref."
deltaThresh x
deltaThresh x =
return $ checkThresholds x thrshSet
checkThresholds :: (JoinSemiLattice t, Eq t) => t -> [t] -> Maybe t
checkThresholds currentState thrshSet = case thrshSet of
[] -> Nothing
(thrsh : thrshs) -> if thrsh `joinLeq` currentState
then Just thrsh
else checkThresholds currentState thrshs
unsafeGetPureLVar :: (JoinSemiLattice t, Eq t) => PureLVar s t -> (t -> Bool) -> Par d s t
unsafeGetPureLVar (PureLVar (WrapLVar lv)) thrsh =
WrapPar$ LI.getLV lv globalThresh deltaThresh
where globalThresh ref _ = do
x <- readIORef ref
logDbgLn_ 5 " [Pure] unsafeGetPureLVar: read the ref."
deltaThresh x
deltaThresh x =
return $! if thrsh x
then Just x
else Nothing
waitPureLVar :: (JoinSemiLattice t, Eq t) =>
PureLVar s t -> t -> Par d s ()
waitPureLVar (PureLVar (WrapLVar iv)) thrsh =
WrapPar$ LI.getLV iv globalThresh deltaThresh
where globalThresh ref _ = do
x <- readIORef ref
logDbgLn_ 5 " [Pure] checking global thresh..."
deltaThresh x
deltaThresh x | thrsh `joinLeq` x = do logDbgLn_ 5 " [Pure] Delta thresh met!"
return $ Just ()
| otherwise = do logDbgLn_ 5 " [Pure] Check Delta thresh.. Not yet."
return Nothing
putPureLVar :: JoinSemiLattice t =>
PureLVar s t -> t -> Par d s ()
putPureLVar (PureLVar (WrapLVar iv)) !new =
WrapPar $ LI.putLV iv putter
where
putter !ref = do
logDbgLn_ 5 " [Pure] Putting to pure LVar.."
atomicModifyIORef' ref $ \ oldval -> (join oldval new, ())
return $! Just $! new
freezePureLVar :: PureLVar s t -> Par QuasiDet s t
freezePureLVar (PureLVar (WrapLVar lv)) = WrapPar$
do LI.freezeLV lv
LI.getLV lv globalThresh deltaThresh
where
globalThresh ref True = fmap Just $ readIORef ref
globalThresh _ False = return Nothing
deltaThresh _ = return Nothing
instance Eq (PureLVar s v) where
PureLVar lv1 == PureLVar lv2 = state lv1 == state lv2
instance DeepFrz a => DeepFrz (PureLVar s a) where
type FrzType (PureLVar s a) = PureLVar Frzn (FrzType a)
frz = unsafeCoerce#
logDbgLn_ _ _ = return ()