Verified Commit cc365f16 authored by Sven Keidel's avatar Sven Keidel
Browse files

add cache for garbage collection

parent 877be70d
Pipeline #68288 passed with stages
in 43 minutes and 29 seconds
......@@ -23,21 +23,28 @@ class (Arrow c, Profunctor c) => ArrowCache a b c | c -> a, c -> b where
type Widening c
-- | Initializes a cache entry with 'bottom'.
initialize :: c a b
--
-- The operation satisfies the following laws:
-- * 'initialize' is an update with bottom: @(_,_,b)<-update-<(Unstable,a,⊥) ⊑ b'<-initialize-<a@
initialize :: (?cacheWidening :: Widening c) => c a b
-- | Looks up if there is an entry in the cache.
lookup :: c a (Maybe (Stable,b))
-- | Write a new entry to the cache.
write :: c (a,b,Stable) ()
-- | Update an existing entry in the cache.
--
-- The operation satisfies the following laws:
-- * 'update' increases the entry: if @(s',a',b') <- update -< (s,a,b)@ then @a ⊑ a'@, and @b ⊑ b'@
-- * 'update' does not forget: if @(s',a',b') <- update -< (s,a,b); m <- lookup -< a@ then @Just (s ⊔ s',b') ⊑ m@
update :: (?cacheWidening :: Widening c) => c (Stable,a,b) (Stable,a,b)
-- | Write a new entry to the cache.
write :: c (a,b,Stable) ()
-- | Set a given entry to stable or unstable.
setStable :: c (Stable,a) ()
default initialize :: (c ~ t c', ArrowTrans t, ArrowCache a b c') => c a b
default initialize :: (c ~ t c', ArrowTrans t, ArrowCache a b c', ?cacheWidening :: Widening c') => c a b
default lookup :: (c ~ t c', ArrowTrans t, ArrowCache a b c') => c a (Maybe (Stable,b))
default write :: (c ~ t c', ArrowTrans t, ArrowCache a b c') => c (a,b,Stable) ()
default update :: (c ~ t c', ArrowTrans t, ArrowCache a b c', ?cacheWidening :: Widening c') => c (Stable,a,b) (Stable,a,b)
......@@ -56,12 +63,12 @@ class (Arrow c, Profunctor c) => ArrowCache a b c | c -> a, c -> b where
{-# INLINE setStable #-}
class (ArrowIterateCache a b c) => ArrowParallelCache a b c where
lookupOldCache :: c a b
lookupOldCache :: (?cacheWidening :: Widening c) => c a b
lookupNewCache :: c a (Maybe b)
updateNewCache :: (?cacheWidening :: Widening c) => c (a,b) b
isStable :: c () Stable
default lookupOldCache :: (c ~ t c', ArrowTrans t, ArrowParallelCache a b c') => c a b
default lookupOldCache :: (c ~ t c', ArrowTrans t, ArrowParallelCache a b c', ?cacheWidening :: Widening c') => c a b
default lookupNewCache :: (c ~ t c', ArrowTrans t, ArrowParallelCache a b c') => c a (Maybe b)
default updateNewCache :: (c ~ t c', ArrowTrans t, ArrowParallelCache a b c', ?cacheWidening :: Widening c') => c (a,b) b
default isStable :: (c ~ t c', ArrowTrans t, ArrowParallelCache a b c') => c () Stable
......
......@@ -333,6 +333,69 @@ instance (Arrow c, Profunctor c) => ArrowIterateCache (s,a) (s,b) (CacheT Monoto
returnA -< ((sNew,a),(sNew,b))
{-# INLINE nextIteration #-}
-- | Cache for an analysis with abstract garbage collection. The type variable
-- @s@ stands for the store.
data GarbageCollect a b where
GarbageCollect :: HashMap a (Stable,s,s,b) -> GarbageCollect (s,a) (s,b)
instance IsEmpty (GarbageCollect (s,a) (s,b)) where
empty = GarbageCollect empty
instance (Show s, Show a, Show b) => Show (GarbageCollect (s,a) (s,b)) where
show (GarbageCollect m) = show m
instance (Pretty s, Pretty a, Pretty b) => Pretty (GarbageCollect (s,a) (s,b)) where
pretty (GarbageCollect m) =
align (list [ pretty s1 <+> "×" <+> pretty a <+> showArrow st <+> pretty s2 <+> "×" <+> pretty b | (a,(st,s1,s2,b)) <- M.toList m])
instance (Identifiable a, PreOrd s, LowerBounded b, ArrowChoice c, Profunctor c)
=> ArrowCache (s,a) (s,b) (CacheT GarbageCollect (s,a) (s,b) c) where
type Widening (CacheT GarbageCollect (s,a) (s,b) c) = (W.Widening s,W.Widening b)
initialize = CacheT $ modify' $ \((sNew1,a),GarbageCollect cache) ->
let (widenS,_) = ?cacheWidening
in case M.lookup a cache of
Just (_,sOld1,sOld2,b)
| sNew1 sOld1 -> ((sOld2,b), GarbageCollect cache)
| otherwise -> let (_,sWiden1) = widenS sOld1 sNew1
(_,sWiden2) = widenS sOld2 sNew1
in ((sWiden2,b), GarbageCollect (M.insert a (Unstable,sWiden1,sOld2,b) cache))
Nothing -> ((sNew1,bottom), GarbageCollect (M.insert a (Unstable,sNew1,sNew1,bottom) cache))
lookup = CacheT $ modify' $ \((sNew1,a),m@(GarbageCollect cache)) ->
case M.lookup a cache of
Just (st,sOld1,sOld2,b)
| sNew1 sOld1 -> (Just (st,(sOld2,b)), m)
| otherwise -> (Just (Unstable,(sOld2,b)), m)
_ -> (Nothing, m)
update = CacheT $ modify' $ \((stable0,(sNew1,a),(sNew2,bNew)),GarbageCollect cache) ->
let (widenS,widenB) = ?cacheWidening
in case M.lookup a cache of
Just (_,sOld1,sOld2,bOld) ->
let (stable1,sWiden1) = widenS sOld1 sNew1
(stable2,sWiden2) = widenS sOld2 sNew2
(stable3,bWiden) = widenB bOld bNew
in ((stable1 stable2 stable3, (sWiden1,a), (sWiden2,bWiden)),
GarbageCollect (M.insert a (stable0 stable1 stable2 stable3, sWiden1, sWiden2, bWiden) cache))
Nothing -> ((Unstable,(sNew1,a),(sNew2,bNew)), GarbageCollect (M.insert a (Unstable,sNew1,sNew2,bNew) cache))
write = CacheT $ modify' $ \(((sNew1, a), (sNew2,b), st), GarbageCollect cache) ->
((), GarbageCollect (M.insert a (st, sNew1, sNew2, b) cache))
setStable = CacheT $ proc _ -> returnA -< ()
{-# INLINE initialize #-}
{-# INLINE lookup #-}
{-# INLINE write #-}
{-# INLINE update #-}
{-# INLINE setStable #-}
{-# SCC initialize #-}
{-# SCC lookup #-}
{-# SCC write #-}
{-# SCC update #-}
{-# SCC setStable #-}
instance (Arrow c, Profunctor c) => ArrowIterateCache (s,a) (s,b) (CacheT GarbageCollect (s,a) (s,b) c) where
nextIteration = CacheT $ proc ((_,a),(sNew2,b)) -> do
put -< GarbageCollect empty
returnA -< ((sNew2,a),(sNew2,b))
{-# INLINE nextIteration #-}
------ Monotone Cache that factors out the monotone element ------
data MonotoneFactor a b where
MonotoneFactor :: s -> HashMap a b -> MonotoneFactor (s,a) (s,b)
......
flags: {}
extra-package-dbs: []
resolver: lts-15.3
resolver: lts-16.5
packages:
- 'arrows'
- 'lib'
......
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