[Haskell-cafe] Combining ST with STM

[Thomas Koster]

Jonas,

Thank you for your swift response.

On 9 February 2016 at 14:43, Thomas Koster <tkoster at gmail.com> wrote:
> I have an STM transaction that needs some private, temporary state.
> The most obvious way is to simply pass pure state as arguments, but
> for efficiency, I would like this state to be some kind of mutable
> array, like STArray.
>
> The private state is, by definition, not shared, so
> including it in the STM log and commit process is, as far as I can
> tell, pointless.
>
> ST and STArray still appear to be the most appropriate tools for the
> private state, because STRefs and STArrays really, really are private.
>
> So this basically means I want to interleave ST and STM in a "safe"
> way. That is, if the STM transaction retries, I want the ST state to
> be vaporised as well.
>
> Ideally, I would love to be able to say something like this:
>
> -- | Copy the value from the shared TVar into the private STRef.
> load :: TVar a -> STRef a -> STSTM s ()
> load shared private = do
>   value <- liftSTM (readTVar shared)
>   liftST (writeSTRef private value)
>
> Naturally, that STRef must originate from a call to newSTRef earlier
> in the same transaction and is private to it, just like the real ST
> monad. As far as I can tell, I am not trying to weaken either ST or
> STM in any way here.

On 9 February 2016 at 23:46, Thomas Koster <tkoster at gmail.com> wrote:
> Please forgive the typo in the type signature of "load", which should
> have been:
>
> load :: TVar a -> STRef s a -> STSTM s ()
>
> Let me elaborate on STSTM, a monad I made up for this example that
> combines the characteristics of ST and STM in the way that I want.
> If my requirements were unclear from my prose, perhaps the code below
> will illuminate them better.
>
> An STSTM transaction is intended to be an STM transaction imbued with a
> state token that encapsulates additional, transaction-local state in the
> spirit of ST.
>
> It is not intended to secretly perform IO inside STM, a la
> GHC.Conc.unsafeIOToSTM.
>
> It is not intended to facilitate the leaking of state into or out of an
> STM transaction through STRefs, nor to communicate state between
> successive retries of an STM transaction.

On 10 February 2016 at 01:12, Jonas Scholl <anselm.scholl at tu-harburg.de> wrote:
> I understand that, you just said, you wanted to sprinkle some runST
> calls with unsafeThawArray and unsafeFreezeArray into your STM code. So
> I assumed you wanted to share an (ST)Array between these STM actions.

Sorry for the confusion. unsafeThawArray and unsafeFreezeArray were an
alternative solution for modifying the transaction-local Array in place,
directly in an STM action.

Rather than use unsafeThawArray, STSTM is intended to allow the safe
interleaving of safe STM actions with safe ST actions, where the ST
state is local and private to the STM transaction. I don't plan on using
any unsafe ST functions with STSTM at all. Naturally, the STSTM
implementation itself must use some kind of unsafe function, but
hopefully only in a safe way.

On 9 February 2016 at 23:46, Thomas Koster <tkoster at gmail.com> wrote:
> Thanks to hints from Ryan and Jonas, I made an attempt at implementing
> it myself.
>
> Below is my implementation of STSTM and associated operations. You will
> need to link with the "primitive" and "stm" packages. I used versions
> 0.6 and 2.4.4, resp., and GHC 7.10.2.
>
>
> {-# LANGUAGE GeneralizedNewtypeDeriving, Rank2Types #-}
>
> module Control.Monad.STSTM
>   (
>     STSTM,
>     liftST,
>     liftSTM,
>     atomicallyRunST,
>     module Control.Monad.STM
>   )
> where
>
> import Control.Monad.Primitive
> import Control.Monad.ST
> import Control.Monad.STM
>
> -- | A computation of type @STSTM s a@ is an 'STM' computation that
> -- also transforms a transaction-local internal state indexed by @s@, as
> -- in the 'ST' monad, and returns a value of type @a at .
> newtype STSTM s a = STSTM { unSTSTM :: STM a }
>   deriving (Functor, Applicative, Monad)
>
> -- | Lift an 'ST' computation into the 'STSTM' transaction.
> liftST :: ST s a -> STSTM s a
> {-# INLINE liftST #-}
> liftST x = STSTM $
>   let y = unsafeInlineST x
>   in  y `seq` return y

On 10 February 2016 at 01:12, Jonas Scholl <anselm.scholl at tu-harburg.de> wrote:
> This is highly unsafe and will not do what you think it does!
> unsafeInlineST provides an ST action with a realWorld# token out of thin
> air and thus can float outside liftST, especially because you inline it.
> This produces exactly the bug I reported against STMonadTrans.

Thank you for checking it out. I am not surprised that it does not do
what I think, because I don't even know what to think: unsafeInlineST
had no documentation. I wonder what its purpose is then.

So you are saying that because there is no data dependency on the *true*
state token (it evaluates the fake token instead), GHC is free to
rearrange, duplicate or elide the effects on the state with regard to
the other calls to liftST (and the STM actions too), causing those
effects on the state to be unpredictable?

Is this also why I thought I needed seq, when in fact what I needed to
do was thread the correct state token?

> A safe version could take the state token from the STM action, pass it
> into the ST action and carry on with the returned state token (look at
> GHC.Conc.Sync). Or convert the ST action to IO and then just run the IO
> action in STM.

This makes much more sense. I will look into these alternatives.

> This should be fine if you do not use unsafeThaw - any
> garbage written to some STRef/STArray will be thrown away after the
> runtime sees the STM action will fail and restarts it.

That's what I want.

On 9 February 2016 at 23:46, Thomas Koster <tkoster at gmail.com> wrote:
> -- | Lift an 'STM' computation into the 'STSTM' transaction.
> liftSTM :: STM a -> STSTM s a
> {-# INLINE liftSTM #-}
> liftSTM = STSTM
>
> -- | Perform a series of 'STSTM' actions atomically.
> --
> -- The 'ST' state is discarded when the 'STM' transaction commits or
> -- retries.
> atomicallyRunST :: (forall s. STSTM s a) -> IO a
> {-# INLINE atomicallyRunST #-}
> atomicallyRunST x = atomically (unSTSTM x)
>
>
> Some commentary follows:
>
> Some initial sanity testing with the GHC threaded runtime shows that it
> does what I want, but I am not familiar enough with Core or the RTS to
> predict whether or not it will launch nuclear missiles at the next
> transit of Venus. I would be grateful for any feedback.
>
> The use of rank-2 polymorphism in the type of atomicallyRunST is
> intended to encapsulate the ST state exactly like it does for runST,
> and that the ST state cannot leak into or out of the transaction.

On 10 February 2016 at 01:12, Jonas Scholl <anselm.scholl at tu-harburg.de> wrote:
> What you still can not use is unsafeThaw. Consider this:
>
> foo :: Array Int Val -> TVar Int -> IO someResult
> foo arr var = atomicallyRunST $ do
>     marr <- liftST $ unsafeThaw arr
>     val <- liftSTM $ readTVar var
>     liftST $ writeArray marr val someOtherVal
>     ... do something more...
>
> What happens if the transaction is restarted after the write? You've
> written into arr (unsafeThaw did not copy it), but have no log to revert
> the write. Now you see a different immutable array. This is bad.
>
> So you can not use unsafeThaw. Even if only one transaction gets a hold
> on this array and it would be safe to use unsafeThaw with plain ST (as
> this can not retry), because the transaction has to depend on other
> TVars etc, otherwise there would be no need for STM.
>
> And now I am wondering what happens if a thread evaluates something like
> runST ... unsafeThawArray ... unsafeFreezeArray ... and is hit by an
> asynchronous exception... The computation is restated the next time the
> thunk is demanded, but this could have already changed the array, right?
> So can runST ... unsafeThawArray ... be used in a safe way or is this
> combination inherently broken?

Agreed. This is a problem wherever unsafeThawArray is used. I understand
that nothing I do can make unsafeThawArray safer. Using unsafe functions
here would be at least as unsafe as using them in ST. But if the idea of
STSTM works and is safe, I will not be using any unsafe ST functions in
the ST actions at all.

> Anyway, I think the following holds true:
>  - using STRefs: These must have been created in the transaction, so it
> works.
>  - using STArrays: unsafeThawing an incoming Array will break
> referential transparency sooner or later. Thawing (and thus copying) the
> incoming array or creating a fresh one should work.
>  - using TArrays: You can return these from the STM action and start
> another one later with them without breaking referential transparency as
> always. If you have to modify incoming arguments, even if only one STM
> action has a reference to them at a time, these can be faster as you do
> not have to copy everything - instead they will have a log of the
> writes, so you would have to benchmark copying against transaction logs.

On 9 February 2016 at 23:46, Thomas Koster <tkoster at gmail.com> wrote:
> STSTM is not a monad transformer (visibly or internally). I hope that
> any potential problems that might afflict the STMonadTrans package are
> irrelevant here.

On 10 February 2016 at 01:12, Jonas Scholl <anselm.scholl at tu-harburg.de> wrote:
> You won't have problems with lists as underlying monad, yes.

On 9 February 2016 at 23:46, Thomas Koster <tkoster at gmail.com> wrote:
> I use seq in liftST to force the unsafe inline ST computation to occur
> before bind proceeds to the next computation. Without seq, ST
> computations returning () (or anything else that is not evaluated)
> appear to stay as thunks and never transform any state. I suspect this
> may cause problems with bottoms, but I am not sure if that is any
> different from real ST/runST.

On 10 February 2016 at 01:12, Jonas Scholl <anselm.scholl at tu-harburg.de> wrote:
> Keep in mind that a `seq` b does not guarantee that a is evaluated
> before b. I think this is not a problem here, as there are more severe
> problems anyway (see above), but this is generally good to have in mind
> when writing such code.

I hope that if I can fix the unsafety by threading the true state token
through, as per your suggestion above, seq will no longer be necessary.

--
Thomas Koster