diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,5 @@ +# Revision history for reference-counting + +## 0.1.0.0 -- YYYY-mm-dd + +* First version. Released on an unsuspecting world. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2023, Rodrigo Mesquita + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Rodrigo Mesquita nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,174 @@ +# General idea + +You can create an alias to a resource, and then `share` that alias +multiple times. You can `forget` aliases of resources. When the last alias is +forgotten, the resource is freed with the given finaliser. + +Linearity in the reference counting API guarantees that an aliased resource will +be freed exactly once because, in turn, all aliases of a resource need to be +forgotten exactly once. Moreover, linearity exacts an explicit operation to +share aliases which means we can trivially increment the reference count when +`share` is called. + +# Usage + +The only application to date using `reference-counting` (this package) is +`ghengin`. Ghengin is a (very) experimental engine where both CPU and GPU +resources required to render games are tracked linearly throughout the engine +(using linear IO). + +When developing such a large program using linear types, a way to share +linear resources and interleave their usage in non-trivial ways throughout the +renderer turned out to be critical. That's where `reference-counting` comes in. +At that point in time, I was fortunately reading TAPL2 which has a chapter on +reference counting with linear types which also inspired me to write a draft +version of this library. + +Note that the package is still in an experimental/candidate state where +there are potential unsoundness bugs in the API design. +The point of this candidate release is to receive feedback on the design and its +flaws -- I'm very interested if you discover it is unsound -- it has been a +while since I wrote this first, and some things look suspicious to me now. OTOH +the paged-in-me was mostly sure of them at the time. + +Despite my uneasiness, I have to say, as a pratical statement of reliability, +that it has been working wonderfully as a central point in resource management +within the engine[1]. + +If you are looking for a considerably complex application using +`reference-counting`, you can try to take a look at the engine source code and +hope that your eyes don't bleed out. + +If you are looking for a more palpable example, there are two trivial ones in `test/`. + +[1] Seriously, after having fully rewritten the Core of the renderer in the +linear IO monad with reference counting I haven't yet encountered resource bugs, +whereas previously there were so many that I decided to rewrite the engine with +linear types... + +# Design + +The key datatype is `Alias` (opaque, tracks references dynamically under the +hood). +```haskell +newAlias :: (a ⊸ μ ()) ⊸ a ⊸ m (Alias μ a) +``` +The first argument is a function to free the resource when the last reference to +it is freed, and the second argument is the resource you're creating an alias +for. + +When you have an alias of a resource (`Alias m a`, where the `m` is the context +in which the resource can be freed), you can `share` the alias. Sharing an alias +to a resource means there are now more aliases to the resource: +```haskell +share :: Alias μ a %1 -> m (Alias μ a, Alias μ a) +``` +In fact, you can `share` anything which is `Shareable`. `Alias`es are trivially +shareable, but other types can be as well via generic deriving, or a little bit +of effort. For example, we can `share` a list of aliases `[Alias Renderer +Vk.Buffer]` to get two lists with the same aliases (`([Alias Renderer +Vk.Buffer], [Alias Renderer Vk.Buffer])`), and all nested aliases will also get +shared in order to return the two lists. + +When you no longer need an alias you can `forget` it. If this is the last alias +to the resource, the finalizer action (the first argument to `newAlias`) will be +called on the aliased value `a`. +```haskell +forget :: Alias μ a %1 -> μ () +``` +Similarly to `share` and `Shareable`, `forget` also works for any `Forgettable` type. +Note that for `Alias`, the context in which `forget` is called has to be the +same where the finalizer action is defined (the `μ` parameter to `Alias`), since +the finalizer will be called if this was the last alias. + +## The tricky bits + +This becomes way less simple when we allow aliased values to be actually used. +That is, we only care about aliases if we can refer to the original values using +them. Here be dragons. + +The two key ways of using the stored value are `get` and `use/useM`. +`useM` follows a more common Haskell pattern: +```haskell +useM :: Alias μ a %1 -> (a %1 -> IO (a, b)) %1 -> IO (Alias μ a, b) +``` +Operate on the aliased `a` and keep it aliased plus return the `b` byproduct. +There is also a misnamed `modifyM` function which is `useM` without the `b`... + +Then, there's the arguably most difficult to reason about primitive, `get`: +```haskell +get :: Alias μ a %1 -> μ (a, a %1 -> μ ()) +``` +The `get` primitive will un-alias a resource and get its value. +By case analysis, either this was the last alias to this resource, or it was +not. If it was the last alias, we need to make sure the resource is linearly +freed. If it was not, we need to make sure it *isn't* freed since there are +still aliases to it. + +How do we ensure that the resource is freed if this was the last alias, and that +it is not if it wasn't? The trick is to return both the resource and a finalizer +function linearly -- where the finalizer is actually a no-op if there are more +aliases to that same resource. + +The returned function needs to be called exactly once on the resource since it +is returned in a linear tuple -- it will either make sure the resource isn't +consumed (because it is fake-consumed by the finaliser), or make sure it is +consumed (because the finaliser will really consume the resource if this was the +last alias). + +This sounds like an awful idea. Maybe we could even just get by with `useM` +which seems less troublesome? One thing that worries me is to what extent could +you call the weird-finaliser on something which wasn't related to the resource +returned alongside it? ... + +# Notes + +> [!CAUTION] +> It seems that Haddock is rendering incorrectly the lollipop symbol (`⊸`) which +> stands for linear arrow (`%1 ->`) in some places. This is quite unfortunate. +> You may have to double check the source to see if an argument is in fact +> linear... + +### type alias for alias + +Typically you'll want to export a type synonym for `Alias` over the monad you +can free resources in, import `Data.Linear.Alias` qualified (most functions, +such as `share` and `get` are short and are arguably better to be qualified in +general), such that there are no conflicts between the type synonym `Alias` and the +library defined `Alias.Alias` name +```haskell +import qualified Data.Linear.Alias as Alias +type Alias = Alias.Alias Linear.IO -- Choose the monad you can allocate and free this + -- reference counted resource in +``` +### opaqueness for soundness? + +Perhaps this is very important to explain somehow earlier on or enforce: The +*aliased* things should be opaque. That is, you should not be able to easily +modify the value which is aliased into something else. So, good aliasable values +would be e.g. pointers, handles, buffers, devices, GPU textures, `IORef`s, +etc... + +The problem here is the underlying representation of `Alias m a` which will not use +a mutable reference like `IORef` for the `a` across the aliases (I've wondered +before if it should, but it never made sense for my case where the things I was +aliasing were already mutable like `Vk.Buffer`; leaving it as `a` doesn't +preclude the user from stuffing an `IORef` to alias). + +So, if the `a` value is changeable, you could end up in a situation where you +have two aliases that should hold the same value, but are different. In effect, +whichever of the two aliases is forgotten last will call the finalizer action on +the `a` value. If these values are different, the finalizer action will depend +on the last forgotten resource... which is very unsound. + +### thread safety + +We are using `atomic-counter` for counting, but what happens if there two +actions on the same alias at the same time? It may just be that the +responsibility of thread safety when two aliased resources are used at the same +time is of the resource type (it seems that way). + +For example, if the aliased resource was an `IORef`, it'd be the caller's +responsibility to use `atomicModifyIORef` if a multi-threaded program were using +multiple aliases to that same ref at once. + diff --git a/reference-counting.cabal b/reference-counting.cabal new file mode 100644 --- /dev/null +++ b/reference-counting.cabal @@ -0,0 +1,98 @@ +cabal-version: 3.4 +-- The cabal-version field refers to the version of the .cabal specification, +-- and can be different from the cabal-install (the tool) version and the +-- Cabal (the library) version you are using. As such, the Cabal (the library) +-- version used must be equal or greater than the version stated in this field. +-- Starting from the specification version 2.2, the cabal-version field must be +-- the first thing in the cabal file. + +-- Initial package description 'reference-counting' generated by +-- 'cabal init'. For further documentation, see: +-- http://haskell.org/cabal/users-guide/ +-- +-- The name of the package. +name: reference-counting + +-- The package version. +-- See the Haskell package versioning policy (PVP) for standards +-- guiding when and how versions should be incremented. +-- https://pvp.haskell.org +-- PVP summary: +-+------- breaking API changes +-- | | +----- non-breaking API additions +-- | | | +--- code changes with no API change +version: 0.1.0.0 + +-- A short (one-line) description of the package. +synopsis: A reference counting library to alias linear resources + +-- A longer description of the package. +description: A reference counting library to alias linear resources. + Get started by importing @'Data.Linear.Alias'@! + +-- The license under which the package is released. +license: BSD-3-Clause + +-- The file containing the license text. +license-file: LICENSE + +-- The package author(s) and maintainer(s). +author: Rodrigo Mesquita +maintainer: rodrigo.m.mesquita@gmail.com + +-- A copyright notice. +-- copyright: + +category: Data +build-type: Simple +tested-with: GHC ==9.8.2 + +extra-doc-files: CHANGELOG.md + README.md + +source-repository head + type: git + location: https://github.com/alt-romes/reference-counting + +common warnings + ghc-options: -Wall + -- -dlint -dcore-lint -dasm-lint -dcmm-lint -dstg-lint + +library + import: warnings + + exposed-modules: Data.Linear.Alias + Data.Linear.Alias.Unsafe + Data.Linear.Alias.Internal + + build-depends: base >= 4.17.0 && < 4.22, + linear-base >= 0.3 && < 0.5, + atomic-counter >= 0.1.2 && < 0.2, + + -- only for instances of Aliasable + containers >= 0.6 && < 0.7, + + hs-source-dirs: src + default-language: GHC2021 + +test-suite reference-counting-test + import: warnings + + default-language: GHC2021 + + -- Modules included in this executable, other than Main. + -- other-modules: + + -- The interface type and version of the test suite. + type: exitcode-stdio-1.0 + + -- Directories containing source files. + hs-source-dirs: test + + -- The entrypoint to the test suite. + main-is: Main.hs + + -- Test dependencies. + build-depends: + base, + reference-counting, + linear-base diff --git a/src/Data/Linear/Alias.hs b/src/Data/Linear/Alias.hs new file mode 100644 --- /dev/null +++ b/src/Data/Linear/Alias.hs @@ -0,0 +1,243 @@ +{-# LANGUAGE UnicodeSyntax, LinearTypes, QualifiedDo, NoImplicitPrelude, BlockArguments, ImpredicativeTypes, DefaultSignatures #-} +{-# LANGUAGE UndecidableInstances #-} -- Rep a in the Generically instance +-- | Simple reference counting with linear types inspired by Advanced Topics in +-- Types and Programming Languages Chapter 1 +module Data.Linear.Alias + ( + -- * The heart of aliasing + Alias + , Shareable(..) + , Forgettable(..) + , get + + -- * Using and modifying aliased resources + , use + , useM + , modify + , modifyM + , hoist + + -- * Creating aliases + , newAlias + ) where + +import GHC.Generics +import Control.Functor.Linear as Linear hiding (get, modify) +import Control.Monad.IO.Class.Linear +import Prelude.Linear hiding (forget) +import qualified Control.Concurrent.Counter as Counter +import qualified Unsafe.Linear as Unsafe +import qualified Data.IntMap as IM +import qualified Data.Bifunctor.Linear as B + +import Data.Linear.Alias.Internal +import qualified Data.Linear.Alias.Unsafe as Unsafe.Alias + +-- TODO: This is already using atomic-counter, but this is not good enough (it would be cool to use the unlifted one). +-- Check out the TODO file. + +----- Signature functions ----- + +-- | Create an alias for a resource. +newAlias :: MonadIO m + => (a ⊸ μ ()) -- ^ Function to free resource when the last alias is released + ⊸ a -- ^ The resource to alias + ⊸ m (Alias μ a) +newAlias freeC x = Linear.do + Ur c <- liftSystemIOU $ Counter.new 1 + pure $ Alias freeC c x + + +-- | This function returns a value that is aliased in a linear pair with a +-- function to free the linear value. Since both the value and freeing function +-- must be consumed linearly, it is guaranteed that the returned function is +-- the one used to free the resource. +-- +-- The cleanup function can be one of two things: +-- +-- * If the returned value was the last reference, the function is the one +-- passed as an argument to 'new' +-- +-- * Otherwise, if this isn't the last reference to the value, the freeing +-- function will be a no-op, but still must be called on the value. +-- +-- Usage: +-- +-- @ +-- (x, cleanup) <- Alias.get ref +-- x' <- useSomehow x +-- cleanup x' +-- @ +get :: MonadIO μ => Alias μ a ⊸ μ (a, a ⊸ μ ()) +-- Note on unsafety: If some (sub-)resource is unsafely duplicated from the +-- returned @a@, it's crucial that if @a@ is freed manually, it cannot be +-- passed on to the resource-freeing-function! If you don't mess with unsafety +-- this shouldn't be possible. (This is kind of a moot comment since it must be +-- considered in each case carefully). +get (Alias freeC counter x) = Linear.do + -- The freeing function, in consuming @x@ linearly, is guaranteed to also + -- free/forget recursively nested reference-counted resources (guaranteed in + -- its implementation by linearity @freeC@). + Ur oldCount <- liftSystemIOU (Counter.sub counter 1) + if oldCount == 1 + then Linear.do + -- This is the last reference to the resource, free it. + pure (x, freeC) + else + -- This is not the last reference, do nothing else. + pure (x, Unsafe.toLinear (\_ -> pure ())) + +-- | Like 'modifyM' +modify :: (a ⊸ a) ⊸ Alias μ a ⊸ Alias μ a +modify f (Alias freeC counter x) = Alias freeC counter (f x) + +-- | Run a monadic function that modifies a reference counted resource. +modifyM :: MonadIO m => (a ⊸ m a) ⊸ Alias μ a ⊸ m (Alias μ a) +modifyM f (Alias freeC counter x) = Alias freeC counter <$> f x + +-- | Like 'useM' +use :: Alias μ a ⊸ (a ⊸ (a, b)) ⊸ (Alias μ a, b) +use (Alias freeC counter x) f = case f x of (a,b) -> (Alias freeC counter a, b) + +-- | Use a reference value in an action that uses that value linearly +-- without destroying it. +-- +-- The value with the same reference count will be returned together with a +-- byproduct of the linear computation. +useM :: MonadIO m + => Alias μ a ⊸ (a ⊸ m (a, b)) ⊸ m (Alias μ a, b) +useM (Alias freeC counter x) f = f x >>= \(a,b) -> pure (Alias freeC counter a, b) + + +hoist :: MonadIO m => ((a ⊸ m ()) ⊸ b ⊸ μ ()) ⊸ (a ⊸ b) ⊸ Alias m a ⊸ Alias μ b +hoist freeAB f (Alias freeA counter x) = Alias (freeAB freeA) counter (f x) + + +----- Signature classes ----- + +class Forgettable m a where + -- | Forget the existence of a linear resource + forget :: MonadIO m => a ⊸ m () + -- romes: I had never thought about it, but it's a bit weird for the method + -- to have constraints over the @m@, where the instances don't have to + -- require that instance? + +instance Forgettable μ (Alias μ a) where + -- | Forget the existence of a linearly aliased resource, freeing it if necessary + forget :: MonadIO μ => Alias μ a ⊸ μ () + forget (Alias freeC counter x) = Linear.do + -- Read comment regarding the freeing function and recursively nested aliases in @'get'@. + Ur oldCount <- liftSystemIOU (Counter.sub counter 1) + if oldCount == 1 + then Linear.do + -- This is the last reference to the resource, free it. + freeC x + else + -- No-op + pure (Unsafe.toLinear (\_ -> ()) x) + +class Shareable m a where + -- | Share a linear resource + -- + -- Careful! You must make sure that all aliases recursively nested within + -- this structure @a@ are properly shared/incremented. + -- + -- If you fail to implement this correctly, reference counting won't be sound. + -- Good thing is we can do this automatically! It's much less bug-prone, + -- especially if you update the definition of a datatype. Your @a@ just needs + -- to instance 'Generic'. + share :: MonadIO m => a ⊸ m (a, a) + + default share :: (Generic a, Fields (Rep a)) => MonadIO m => a ⊸ m (a, a) + share = Unsafe.toLinear $ \x -> Linear.do + + -- We can forget the counted fields after incrementing them all + consume <$> + traverse' (\(SomeAlias alias) -> Linear.do + a' <- Unsafe.Alias.inc alias -- increment reference count + Unsafe.toLinear const (pure ()) a') (countedFields x) + + -- It's safe to return two references to the pointer because we've + -- incremented the reference count of all nested aliases. Both references must be used + -- linearly *and* we decrement the reference count with every use except + -- for the last through @free@, ensuring the resource is freed exactly one. + return (x,x) + +instance Shareable m (Alias μ a) where + -- | Share a linearly aliased resource, the heart of reference counting aliases. + share :: MonadIO m => Alias μ a ⊸ m (Alias μ a, Alias μ a) + share alias'' = Linear.do + -- Implement manually since there is no Generic instance for Alias + alias' <- Unsafe.Alias.inc alias'' + pure $ Unsafe.toLinear (\alias -> (alias, alias)) alias' + +instance (Generic a, Fields (Rep a)) => Shareable m (Generically a) where + share = Unsafe.toLinear $ \(Generically x) -> Linear.do + -- Same implementation as the default instance of `share` + consume <$> + traverse' (\(SomeAlias alias) -> Linear.do + a' <- Unsafe.Alias.inc alias -- increment reference count + Unsafe.toLinear const (pure ()) a') (countedFields x) + return (Generically x, Generically x) + +-- Just like 'share', but doesn't require the action to be performed whithin +-- a MonadIO. Is there a situation where one might want to use 'share' +-- explicitly rather than dup? At least while let bindings are not working for linear types. +-- +-- I suppose we also require that this function is bound strictly, as otherwise the value might not be incremented when expected +-- In that sense I suppose it is unsafe? If we call unsafeDup, then forget, but don't force the result of unsafeDup, forget will actually forget the result instead of having been incremented? +-- Have I taken precautions enough to ensure things happen as expected or does unsafePerformIO still not give me that? +-- +-- Still seems unwieldly... the side effects are too observable +-- unsafeDup :: Alias x a ⊸ (Alias x a, Alias x a) +-- unsafeDup s = let !(a1,a2) = Unsafe.toLinear unsafePerformIO (share s) in (a1,a2) +-- {-# NOINLINE unsafeDup #-} + +----- Other instances ----- + +-- The Consumable => Forgettable and Dupable => Shareable instances end up being a nuisance, despite being useful to have forgettable instances of things like Ints for free. + +-- instance {-# OVERLAPPABLE #-} Consumable a => Forgettable m a where +-- forget a = pure (consume a) +-- {-# INLINE forget #-} +-- instance {-# OVERLAPPABLE #-} Dupable a => Shareable m a where +-- share a = pure (dup2 a) +-- {-# INLINE share #-} + +instance (Forgettable m a, Forgettable m b) => Forgettable m (a,b) where + forget (a,b) = forget a >> forget b + {-# INLINE forget #-} + +instance (Forgettable m a, Forgettable m b, Forgettable m c) => Forgettable m (a,b,c) where + forget (a,b,c) = forget a >> forget b >> forget c + {-# INLINE forget #-} + +instance Forgettable m a => Forgettable m (IM.IntMap a) where + forget im = consume <$> traverse' forget (IM.elems im) + {-# INLINE forget #-} + +instance Forgettable m a => Forgettable m [a] where + forget l = consume <$> traverse' forget l + {-# INLINE forget #-} + +instance (Shareable m a, Shareable m b) => Shareable m (a,b) where + share (a0,b0) = Linear.do + (a1,a2) <- share a0 + (b1,b2) <- share b0 + pure ((a1,b1),(a2,b2)) + {-# INLINE share #-} + +instance Shareable m a => Shareable m (IM.IntMap a) where + share im = B.bimap (Unsafe.toLinear IM.fromList) (Unsafe.toLinear IM.fromList) . unzip <$> + traverse' share (IM.toList im) + {-# INLINE share #-} + +instance Shareable m a => Shareable m [a] where + share l = unzip <$> traverse' share l + {-# INLINE share #-} + +instance Forgettable m Int where + forget = pure . consume +instance Shareable m Int where + share = pure . dup2 + diff --git a/src/Data/Linear/Alias/Internal.hs b/src/Data/Linear/Alias/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Data/Linear/Alias/Internal.hs @@ -0,0 +1,61 @@ +{-# OPTIONS_HADDOCK not-home #-} +{-# LANGUAGE ImpredicativeTypes, UnicodeSyntax, LinearTypes, QualifiedDo, + NoImplicitPrelude, BlockArguments, DefaultSignatures, QuantifiedConstraints, + UndecidableInstances, AllowAmbiguousTypes #-} +module Data.Linear.Alias.Internal where + +import GHC.Generics + +import Prelude.Linear +import qualified Control.Concurrent.Counter as Counter + +-- Usage: type RefC = RefC' MonadYou'reUsing + +-- | A reference counted alias +data Alias m a where + Alias :: (a ⊸ m ()) -- ^ Function to free resource when the last alias is forgotten + -> !Counter.Counter -- ^ The counter associated to this reference counted alias + -> a -- ^ The aliased resource + ⊸ Alias m a + +-- I don't see a way to instance Functor if the free resource function is kept +-- in the body of the reference (it shows up in both the co- and contra-variant +-- position) + +-- Generic utilities + +-- | Return all reference counted (recursively nested) fields of @a@. +-- These are not only @'Alias'es@ directly, but all the recursively nested +-- @'Alias'es@ in @a@. +countedFields :: (Generic a, Fields (Rep a)) => a -> [SomeAlias] +-- The alternative of using the 'Data' constraint instead of Generic isn't +-- good, since it would require making @Alias m a@ instance Data, which is +-- hard. +countedFields x = fields (from x) +{-# INLINE countedFields #-} + +data SomeAlias = ∀ m b. SomeAlias (Alias m b) + +class Fields rep where + fields :: rep a -> [SomeAlias] + +instance Fields V1 where + fields _ = [] + +instance Fields U1 where + fields _ = [] + +instance Fields f => Fields (M1 i c f) where + fields (M1 x) = fields x + +instance (Fields a, Fields b) => Fields (a :+: b) where + fields (L1 x) = fields x + fields (R1 x) = fields x + +instance (Fields a, Fields b) => Fields (a :*: b) where + fields (a :*: b) = fields a ++ fields b + +-- In the case of an alias, we add it the list of aliased values. +instance Fields (K1 i (Alias m a)) where + fields (K1 r) = [SomeAlias r] + diff --git a/src/Data/Linear/Alias/Unsafe.hs b/src/Data/Linear/Alias/Unsafe.hs new file mode 100644 --- /dev/null +++ b/src/Data/Linear/Alias/Unsafe.hs @@ -0,0 +1,44 @@ +-- | This module is designed to be imported qualified. It provides unsafe +-- operations over the reference counted structures in order to build new +-- primitives wrt linearity. +-- +-- @ +-- import qualified Data.Counted.Unsafe as Unsafe +-- @ +{-# LANGUAGE LinearTypes, NoImplicitPrelude, QualifiedDo, UnicodeSyntax, + BlockArguments #-} +module Data.Linear.Alias.Unsafe where + +import Prelude.Linear +import Control.Functor.Linear as Linear +import Control.Monad.IO.Class.Linear + +import qualified Control.Concurrent.Counter as Counter + +import Data.Linear.Alias.Internal + +import qualified Unsafe.Linear as Unsafe + +-- | Unsafely increment the counter of some reference counted resource +inc :: MonadIO m => Alias m' a ⊸ m (Alias m' a) +inc = Unsafe.toLinear \(Alias f counter a) -> Linear.do + Ur _ <- incCounter counter -- increment reference count + pure (Alias f counter a) + where + incCounter c = liftSystemIOU (Counter.add c 1) + +-- | Unsafely decrement the counter of some reference counted resource and get +-- the reference counted value (it's really, really quite unsafe). +-- +-- This doesn't free the resource if the reference count reaches 0. +dec :: MonadIO m => Alias μ a ⊸ m (Ur a) +dec = Unsafe.toLinear \(Alias _ counter a) -> Linear.do + Ur _ <- decCounter counter -- decrement reference count + pure (Ur a) + where + decCounter c = liftSystemIOU (Counter.sub c 1) + +-- | Unsafely get an aliased value. All counters are kept unchanged. +get :: Alias m' a -> a +get (Alias _ _ a) = a + diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,74 @@ +{-# LANGUAGE NoImplicitPrelude, LinearTypes, QualifiedDo, DerivingStrategies, DeriveAnyClass, BlockArguments #-} +module Main (main) where + +import GHC.Generics +import qualified Prelude +import System.IO.Linear as Linear (withLinearIO, IO, fromSystemIO, fromSystemIOU) +import Prelude.Linear hiding (IO) +import Control.Functor.Linear as Linear +import qualified Data.Functor.Linear as DL +import qualified Unsafe.Linear as Unsafe + +-- reference-counting +import qualified Data.Linear.Alias as A + +-------------------------------------------------------------------------------- +-- Test 1 +-------------------------------------------------------------------------------- + +data SomeResource where + UnsafeCreateResource :: Int -> SomeResource + +newResource :: Int %1 -> IO SomeResource +freeResource :: SomeResource %1 -> IO () + +test1 :: IO () +test1 = Linear.do + res <- newResource 0 + ref <- A.newAlias freeResource res + (ref1, ref2) <- A.share ref + A.forget ref1 + A.forget ref2 + +-------------------------------------------------------------------------------- +-- Test 2 +-------------------------------------------------------------------------------- + +test2 :: IO () +test2 = Linear.do + let list = [1..200] + refs <- DL.forM list \i -> Linear.do + newResource i >>= A.newAlias freeResource + case refs of + [] -> ok + (x:xs) -> Linear.do + (x1, x2) <- A.share x + A.forget x1 + A.forget (x2:xs) + -- sort | uniq -c of the stdin should have 1 entry for i=1 to i=200 freed + where + ok = fromSystemIO $ putStrLn "ok" + +-------------------------------------------------------------------------------- +-- Main +-------------------------------------------------------------------------------- + +main :: Prelude.IO () +main = withLinearIO $ Linear.do + () <- test1 + () <- test2 + pure (Ur ()) + + +-------------------------------------------------------------------------------- +-- Internal +-------------------------------------------------------------------------------- + +{-# OPAQUE newResource #-} +{-# OPAQUE freeResource #-} +newResource = Unsafe.toLinear \i -> Linear.do + () <- fromSystemIO $ Prelude.putStrLn $ "initialising linear resource " ++ Prelude.show i + return $ UnsafeCreateResource i +freeResource (UnsafeCreateResource i) = Linear.do + () <- fromSystemIO $ Prelude.putStrLn $ "freeing linear resource " ++ Prelude.show i + return ()