March 27, 2018 at 15:53Software Transactional Memory on Free Monads
Having realized that for a long time I did not write anything useful on Habr about FP and Haskell, and that there is a completely excellent reason for a technical article, I decided to shake the old days. The article will focus on Software Trasactional Memory (STM) , which I managed to implement on Free monads with the participation of ADTs (Algebraic Data Types) and MVars (competitive mutable variables). And, in general, the Proof of Concept turned out to be extremely simple, in comparison with the "real" STM. Let's discuss it.
STM is an approach for programming a competitive data model. The competition here is that different parts of the model can be updated in different threads independently of each other, and conflicts on shared resources are resolved using transactions. Transaction is similar to that in the database, but there are a number of differences. Suppose you want to change some of the data in your code. Conceptually, we can assume that your code does not write directly to the model, but works with a copy of the part that it needs. At the end, the STM engine opens the transaction and first checks that the part of the model you are interested in has not changed by anyone. Didn't change? Well, the new values will be fixed. Someone managed before you? This is a conflict, kindly restart your calculations on new data. Schematically, this can be represented as follows:
Here atomic operations are performed by threads in parallel, but are committed only within transactions that block access to mutable parts of the model.
There are different variations of STM, but we will talk specifically about what was proposed in the famous work “Composable Memory Transactions” , because it has a number of remarkable properties:
A model can be any data structure. You can convert any of your regular models into transactional ones. For this, STM libraries provide various primitives: variables ( TVar ), queues ( TQueue ), arrays ( TArray ) and many others. You can guess that the transactional variables - TVar'i ("critters") - are already minimally sufficient for a full-fledged STM, and everything else is expressed through them.
Consider, for example, the problem of dining philosophers . We can imagine forks as a common resource to which we need to build competitive access:
This model is the simplest: each fork is stored in its own transaction variable, and you need to work with them in pairs: (fork1, fork2), (fork2, fork3), ... (fork5, fork1) . But such a structure would work worse:
Because there is only one shared resource, and if we had five philosophizing streams, they would receive the right to commit in turn. As a result, only one philosopher would dine, and four others would think, and the next time another would dine, but also one, although theoretically with five forks, two can dine in parallel. Therefore, you need to create a competitive model that will give the most expected behavior. Here's what the calculation in the STM monad might look like for a model with separate creature forks:
The function returns True if the plug was free, and it was successfully “taken”, that is, overwritten tFork . False will be if the plug is already in operation, and it can not be touched. Now consider a couple of forks. There can be five situations:
We now write the taking of both forks by our philosopher:
You may notice that the code allows you to take one plug (for example, the left one), but not take another (for example, the right one, which turned out to be occupied by a neighbor). The takeForks function , of course, will return False in this case, but what about the fact that one fork is still in the hands of our philosopher? He will not be able to eat alone, therefore, it must be put back, and continue to think for some more time. After that, you can try again in the hope that both forks will be free.
But "put back" in terms of STM is implemented in a slightly different way than in terms of other competitive structures. We can assume that both variables are tLeftFork and tRightFork- These are local copies that are not connected with the same resource by other philosophers. Therefore, you can not "put" the plug back, but tell the calculation that it failed. Then our one fork will not be written to the shared resources - anyway, there was no successful call to takeFork . This is very convenient, and it is the “cancellation” operation of the current monadic calculation that distinguishes the Haskelian STM implementation from others. There is a special retry method for canceling , let's rewrite takeForks using it:
The calculation will be successful when both forks were taken by our philosopher at once. Otherwise, it will restart again and again at some intervals. In this version, we do not return Bool , because we do not need to know whether both resources were successfully captured. If the function is executed and does not file the calculation, it means successfully.
After taking the forks, we probably need to do something else, for example, put the philosopher in the “Eating” state. We just do this after calling takeForks , and the STM monad will make sure the conditions of the "creatures" are consistent:
We will leave the full implementation of this method as an exercise, and now consider the last missing link. For the time being, we only described the logic of the transactional model, but we have not yet created any specific TVar , and did not start anything. Let's do it:
The atomically :: STM a -> IO a combinator performs calculations in the STM monad atomically. It can be seen from the type that the pure part - working with a competitive model - is separated from unclean computing in the IO monad . The STM code should not have effects. Better - none at all, otherwise when restarting you will get some strange results, for example, if you wrote to a file, then in some situations you can get spurious entries, and this error is very difficult to catch. Therefore, we can assume that in the STM monad there are only pure calculations, and their execution is an atomic operation, which, however, does not block other calculations. The functions for creating TVar newTVarIO :: a -> IO (TVar a) are also unclean.but nothing prevents creating new TVar inside STM using the pure combinator newTVar :: a -> STM (TVar a) . We just didn't need it. Attentive people will notice that only forks are a shared resource, and the condition of the philosophers themselves is wrapped in TVar only for convenience.
Summarize. The minimum implementation of STM should contain the following functions for working with TVar :
Performing calculations:
Finally, the ability to restart the calculation will be a huge plus:
Of course, in libraries there are a huge number of other useful constructs, for example, an instance of the Alternative type class for STM , but let's leave it for independent study.
Implementing a properly working STM is considered difficult, and it is better if there is support from the compiler. I have heard that the implementations in Haskell and Clojure are the best at the moment, and in other languages the STM is not quite real. It can be assumed that there are no monadic STMs with the ability to restart calculations and control effects in any imperative language. But this is all idle reasoning, and I may be wrong. Unfortunately, I do not understand the insides of even the Haskel library stm, not to mention other ecosystems. Nevertheless, from the point of view of the interface, it is quite clear how the code should behave in a multi-threaded environment. And if there is a specification of the interface (subject-oriented language) and the expected behavior, this is already enough to try to create your own STM using Free-monads.
So, Free Monads . Any DSL built on Free monads will have the following characteristics:
Free monads are a very powerful tool, and they can be considered the “right”, purely functional approach for implementing Inversion of Control . According to my feelings, any problem in the subject area can also be solved with the help of Free-monadic DSL. Since this topic is very extensive and touches on many issues of software design and architecture in functional programming, I will leave the other details out of the picture. Curious people can turn to numerous sources on the Internet or to my semi- book Functional Design and Architecture , where Free Monads are given special attention.
Now let's take a look at the code of my stm-free library .
Since STM is a subject-oriented language for creating transactional models, it is clean and monadic, we can assume that for a minimum STM, Free DSL should contain the same methods for working with TVar, and they will be automatically composable and clean in this very Free monad. First, determine what TVar is.
We will need to distinguish between our "creatures", so each instance will be identified by a unique value. The library user does not need to know this, he is expected to use the type TVar a . Dealing with values of this type is half the behavior of our little STM. Therefore, we define ADT with the appropriate methods:
And here you need to stay in more detail.
Why should we do this? The bottom line is that the Free Monad must be built on top of some kind of eDSL. The easiest way to set it is to define possible methods in the form of ADT constructors. The end user will not work with this type, but we will use it to interpret methods with some effect. Obviously, the NewTVar method should be interpreted with the result "a new TVar was created and returned as a result." But you can make such an interpreter that will do something else, for example - write to the database, to the log, or even make calls to the real STM.
These constructors contain all the necessary information to be interpreted. The NewTVar constructor contains some custom value a, and in the interpretation we will put this value in the new TVar. But the problem is that a must be its own for every call to NewTVar . If we just wrote STMF next a , a would already be common to all the code where several NewTVar calls are tied :
But this is pointless, because we still want to use NewTVar for our arbitrary types, and so that they do not jostle with it. Therefore, we remove a in the local visibility of only a particular method.
A more interesting question is where is finally our custom monad for STM. Here she is:
We wrapped the STMF type in the Free type , and with it came all the monadic properties we need. It remains only to create a series of convenient monadic functions on top of our bare STMF methods :
As a result, we can already operate with a transactional model in the form of TVars. In fact, you can take the example of dining philosophers and easily replace STM with STML :
Easy win! But there are things that we have missed. For example, a method for breaking retry calculations . It is easy to add:
There are slight differences in my library from my older sister; in particular, the retry method here returns Unit , although it must return an arbitrary type a . This is not a fundamental limitation, but an artifact of the rapid development of PoC, and in the future I will fix it. Nevertheless, even this code will remain without alterations except to replace the monad itself:
Monadic eDSL is as similar as possible to the base implementation, but the launch of STML scripts is different. My atomically combinator , unlike the base implementation, takes an additional argument - the context in which the calculation will spin.
The context stores user data in the form of TVar, so you can have several different contexts. This can be useful, for example, for separating transactional models - so that they do not affect each other. Say, in one model a huge amount of user data is created, and in another model, the TVar set does not change at all. Then it makes sense to separate the contexts so that the second model doesn’t experience problems due to the “swelling” neighbor. In the basic implementation, the context is global, and I have no idea how this can be circumvented.
The philosopher launch code now looks like this:
What happens when we run a script using atomically ? The interpretation of the scenario relative to the real environment begins. It is at this moment that TVars begin to be created and changed, interrupt conditions are checked, and it is inside atomically that the transaction will either be committed in the transferred context, or will be rolled back and restarted. The algorithm is as follows:
The context may change while this calculation does something with its local copy. The conflict arises when at least one TVar involved in this calculation has changed. This will be seen by the unique identifier stored in each instance. But if the calculation did not use TVar in any way, there will be no conflict.
Let our real environment be expressed by a certain Atomic monad , which is a stack of State and IO monads. As a state - a local copy of all TVar:
Inside this monad, we will unwind and interpret two mutually nested structures: the STML type , which, as we recall, is built using the Free type , and the STMF type . The type of Free is a little brain-stemming, as it is recursive. He has two options:
The interpretation is made simple pattern-matching. The interpreter returns either the value of the entire transaction, or a command to restart it.
The functions newTVar ', readTVar', writeTvar ' work with a local copy of transaction variables, and can freely change them. The runSTML call is made from another function, runSTM , which will check the locally modified TVars for conflicts with the global copy from the context, and decide whether to restart the transaction.
I’ll leave this function without explanation, and I won’t go into details about how the tryCommit function is implemented . Not very optimal, to be honest, but this is a topic for a separate article.
In my implementation, there are a number of subtle points that I still need to realize. There may still be unobvious bugs, and more cases need to be checked “for adequate behavior”, but it’s not clear what is considered adequate STM behavior. But at least, I did not reveal any external differences in the problem of dining philosophers, which means that the idea works, and it can be brought to mind. In particular, you can greatly optimize the runtime, make it more intelligent to resolve conflicts and remove a local copy. The approach with interpretation and the Free Monad turns out to be very flexible, and the code, as you can see for yourself, is much smaller, and it is generally very straightforward. And this is good, because it still opens the way for the implementation of STM in other languages.
For example, now I am porting Free-monadic STM in C ++, which entails my own difficulties unique to this language. Based on the results of the work, I will make a report at the April C ++ Russia 2018 conference , and if anyone is going to visit it, then we can discuss this topic in more detail.
Software transactional memory
STM is an approach for programming a competitive data model. The competition here is that different parts of the model can be updated in different threads independently of each other, and conflicts on shared resources are resolved using transactions. Transaction is similar to that in the database, but there are a number of differences. Suppose you want to change some of the data in your code. Conceptually, we can assume that your code does not write directly to the model, but works with a copy of the part that it needs. At the end, the STM engine opens the transaction and first checks that the part of the model you are interested in has not changed by anyone. Didn't change? Well, the new values will be fixed. Someone managed before you? This is a conflict, kindly restart your calculations on new data. Schematically, this can be represented as follows:
Here atomic operations are performed by threads in parallel, but are committed only within transactions that block access to mutable parts of the model.
There are different variations of STM, but we will talk specifically about what was proposed in the famous work “Composable Memory Transactions” , because it has a number of remarkable properties:
- The concepts of a data model and computations above it are separated;
- computing is the STM monad, and they are composable in full accordance with the FP paradigm;
- there is the concept of manually restarting the calculation (retry);
- finally, there is an excellent implementation for Haskell, which, however, I will not consider, but will focus on my own, interface-like.
A model can be any data structure. You can convert any of your regular models into transactional ones. For this, STM libraries provide various primitives: variables ( TVar ), queues ( TQueue ), arrays ( TArray ) and many others. You can guess that the transactional variables - TVar'i ("critters") - are already minimally sufficient for a full-fledged STM, and everything else is expressed through them.
Consider, for example, the problem of dining philosophers . We can imagine forks as a common resource to which we need to build competitive access:
data ForkState = Free | Taken
type TFork = TVar ForkState
data Forks = Forks
{ fork1 :: TFork
, fork2 :: TFork
, fork3 :: TFork
, fork4 :: TFork
, fork5 :: TFork
}This model is the simplest: each fork is stored in its own transaction variable, and you need to work with them in pairs: (fork1, fork2), (fork2, fork3), ... (fork5, fork1) . But such a structure would work worse:
type Forks = TVar [ForkState]Because there is only one shared resource, and if we had five philosophizing streams, they would receive the right to commit in turn. As a result, only one philosopher would dine, and four others would think, and the next time another would dine, but also one, although theoretically with five forks, two can dine in parallel. Therefore, you need to create a competitive model that will give the most expected behavior. Here's what the calculation in the STM monad might look like for a model with separate creature forks:
data ForkState = Free | Taken
type TFork = TVar ForkState
takeFork :: TFork -> STM Bool
takeFork tFork = do
forkState <- readTVar tFork
when (forkState == Free) (writeTVar tFork Taken)
pure (forkState == Free)The function returns True if the plug was free, and it was successfully “taken”, that is, overwritten tFork . False will be if the plug is already in operation, and it can not be touched. Now consider a couple of forks. There can be five situations:
- Both are free
- Left busy (left neighbor), right free
- Left is free, right is busy (right neighbor)
- Both are busy (neighbors)
- Both are busy (by our philosopher)
We now write the taking of both forks by our philosopher:
takeForks :: (TFork, TFork) -> STM Bool
takeForks (tLeftFork, tRightFork) = do
leftTaken <- takeFork tLeftFork
rightTaken <- takeFork tRightFork
pure (leftTaken && rightTaken)You may notice that the code allows you to take one plug (for example, the left one), but not take another (for example, the right one, which turned out to be occupied by a neighbor). The takeForks function , of course, will return False in this case, but what about the fact that one fork is still in the hands of our philosopher? He will not be able to eat alone, therefore, it must be put back, and continue to think for some more time. After that, you can try again in the hope that both forks will be free.
But "put back" in terms of STM is implemented in a slightly different way than in terms of other competitive structures. We can assume that both variables are tLeftFork and tRightFork- These are local copies that are not connected with the same resource by other philosophers. Therefore, you can not "put" the plug back, but tell the calculation that it failed. Then our one fork will not be written to the shared resources - anyway, there was no successful call to takeFork . This is very convenient, and it is the “cancellation” operation of the current monadic calculation that distinguishes the Haskelian STM implementation from others. There is a special retry method for canceling , let's rewrite takeForks using it:
takeForks :: (TFork, TFork) -> STM ()
takeForks (tLeftFork, tRightFork) = do
leftTaken <- takeFork tLeftFork
rightTaken <- takeFork tRightFork
when (not leftTaken || not rightTaken) retryThe calculation will be successful when both forks were taken by our philosopher at once. Otherwise, it will restart again and again at some intervals. In this version, we do not return Bool , because we do not need to know whether both resources were successfully captured. If the function is executed and does not file the calculation, it means successfully.
After taking the forks, we probably need to do something else, for example, put the philosopher in the “Eating” state. We just do this after calling takeForks , and the STM monad will make sure the conditions of the "creatures" are consistent:
data PhilosopherState = Thinking | Eating
data Philosopher = Philosopher
{ pState :: TVar PhilosopherState
, pLeftFork :: TFork
, pRrightFork :: TFork
}
changePhilosopherActivity :: Philosopher -> STM ()
changePhilosopherActivity (Philosopher tState tLeftFork tRightFork) = do
state <- readTVar tState
case state of
Thinking -> do
taken <- takeForks tFs
unless taken retry -- Do not need to put forks if any was taken!
writeTVar tAct Eating
pure Eating
Eating -> error "Changing state from Eating not implemented."We will leave the full implementation of this method as an exercise, and now consider the last missing link. For the time being, we only described the logic of the transactional model, but we have not yet created any specific TVar , and did not start anything. Let's do it:
philosoperWorker :: Philosopher -> IO ()
philosoperWorker philosopher = do
atomically (changePhilosopherActivity philosopher)
threadDelay 5000
philosoperWorker philosopher
runPhilosophers :: IO ()
runPhilosophers = do
tState1 <- newTVarIO Thinking
tState2 <- newTVarIO Thinking
tFork1 <- newTVarIO Free
tFork2 <- newTVarIO Free
forkIO (philosoperWorker (Philosopher tState1 tFork1 tFork2))
forkIO (philosoperWorker (Philosopher tState2 tFork2 tFork1))
threadDelay 100000The atomically :: STM a -> IO a combinator performs calculations in the STM monad atomically. It can be seen from the type that the pure part - working with a competitive model - is separated from unclean computing in the IO monad . The STM code should not have effects. Better - none at all, otherwise when restarting you will get some strange results, for example, if you wrote to a file, then in some situations you can get spurious entries, and this error is very difficult to catch. Therefore, we can assume that in the STM monad there are only pure calculations, and their execution is an atomic operation, which, however, does not block other calculations. The functions for creating TVar newTVarIO :: a -> IO (TVar a) are also unclean.but nothing prevents creating new TVar inside STM using the pure combinator newTVar :: a -> STM (TVar a) . We just didn't need it. Attentive people will notice that only forks are a shared resource, and the condition of the philosophers themselves is wrapped in TVar only for convenience.
Summarize. The minimum implementation of STM should contain the following functions for working with TVar :
newTVar :: a -> STM (TVar a)
readTVar :: TVar a -> STM a
writeTVar :: TVar a -> a -> STM ()Performing calculations:
atomically :: STM a -> IO aFinally, the ability to restart the calculation will be a huge plus:
retry :: STM aOf course, in libraries there are a huge number of other useful constructs, for example, an instance of the Alternative type class for STM , but let's leave it for independent study.
STM on Free Monads
Implementing a properly working STM is considered difficult, and it is better if there is support from the compiler. I have heard that the implementations in Haskell and Clojure are the best at the moment, and in other languages the STM is not quite real. It can be assumed that there are no monadic STMs with the ability to restart calculations and control effects in any imperative language. But this is all idle reasoning, and I may be wrong. Unfortunately, I do not understand the insides of even the Haskel library stm, not to mention other ecosystems. Nevertheless, from the point of view of the interface, it is quite clear how the code should behave in a multi-threaded environment. And if there is a specification of the interface (subject-oriented language) and the expected behavior, this is already enough to try to create your own STM using Free-monads.
So, Free Monads . Any DSL built on Free monads will have the following characteristics:
- Pure DSL, monadically composable, that is, truly functional;
- The code on such a DSL will not contain anything superfluous, in addition to the subject area, which means it is easier to read and understand;
- Interface and implementation are effectively separated;
- There can be several implementations, and they can be replaced in runtime.
Free monads are a very powerful tool, and they can be considered the “right”, purely functional approach for implementing Inversion of Control . According to my feelings, any problem in the subject area can also be solved with the help of Free-monadic DSL. Since this topic is very extensive and touches on many issues of software design and architecture in functional programming, I will leave the other details out of the picture. Curious people can turn to numerous sources on the Internet or to my semi- book Functional Design and Architecture , where Free Monads are given special attention.
Now let's take a look at the code of my stm-free library .
Since STM is a subject-oriented language for creating transactional models, it is clean and monadic, we can assume that for a minimum STM, Free DSL should contain the same methods for working with TVar, and they will be automatically composable and clean in this very Free monad. First, determine what TVar is.
type UStamp = Unique
newtype TVarId = TVarId UStamp
data TVar a = TVar TVarIdWe will need to distinguish between our "creatures", so each instance will be identified by a unique value. The library user does not need to know this, he is expected to use the type TVar a . Dealing with values of this type is half the behavior of our little STM. Therefore, we define ADT with the appropriate methods:
data STMF next where
NewTVar :: a -> (TVar a -> next) -> STMF next
WriteTVar :: TVar a -> a -> next -> STMF next
ReadTVar :: TVar a -> (a -> next) -> STMF nextAnd here you need to stay in more detail.
Why should we do this? The bottom line is that the Free Monad must be built on top of some kind of eDSL. The easiest way to set it is to define possible methods in the form of ADT constructors. The end user will not work with this type, but we will use it to interpret methods with some effect. Obviously, the NewTVar method should be interpreted with the result "a new TVar was created and returned as a result." But you can make such an interpreter that will do something else, for example - write to the database, to the log, or even make calls to the real STM.
These constructors contain all the necessary information to be interpreted. The NewTVar constructor contains some custom value a, and in the interpretation we will put this value in the new TVar. But the problem is that a must be its own for every call to NewTVar . If we just wrote STMF next a , a would already be common to all the code where several NewTVar calls are tied :
data STMF next a where
NewTVar :: a -> (TVar a -> next) -> STMF nextBut this is pointless, because we still want to use NewTVar for our arbitrary types, and so that they do not jostle with it. Therefore, we remove a in the local visibility of only a particular method.
Note . In fact, to speed up work on the Proof of Concept, I have been limited to type a so that it is serializable (an instance of the ToJSON / FromJSON class from the aeson library ). The fact is that I will need to store these different types of TVar in the map, but I do not want to mess with Typeable / Dynamic or, especially, with HLists . In real STM, type a can be absolutely anything, even a function. I will also deal with this issue sometime later.What is this next field like? Here we step on the demand from the Free Monad. She needs somewhere to store the continuation of the current method, and just the next field does not suit her - ADT should be a functor for this field. So, the NewTVar method should return TVar a , and we see that the continuation (TVar a -> next) is just waiting for our new input variable. On the other hand, WriteTVar does not return anything useful, so the continuation is of type next , that is, it does not expect anything to enter. Making an STMF type functor is easy:
instance Functor STMF where
fmap g (NewTVar a nextF) = NewTVar a (g . nextF)
fmap g (WriteTVar tvar a next ) = WriteTVar tvar a (g next)
fmap g (ReadTVar tvar nextF) = ReadTVar tvar (g . nextF)A more interesting question is where is finally our custom monad for STM. Here she is:
type STML next = Free STMF nextWe wrapped the STMF type in the Free type , and with it came all the monadic properties we need. It remains only to create a series of convenient monadic functions on top of our bare STMF methods :
newTVar :: ToJSON a => a -> STML (TVar a)
newTVar a = liftF (NewTVar a id)
writeTVar :: ToJSON a => TVar a -> a -> STML ()
writeTVar tvar a = liftF (WriteTVar tvar a ())
readTVar :: FromJSON a => TVar a -> STML a
readTVar tvar = liftF (ReadTVar tvar id)As a result, we can already operate with a transactional model in the form of TVars. In fact, you can take the example of dining philosophers and easily replace STM with STML :
data ForkState = Free | Taken
type TFork = TVar ForkState
takeFork :: TFork -> STML Bool
takeFork tFork = do
forkState <- readTVar tFork
when (forkState == Free) (writeTVar tFork Taken)
pure (forkState == Free)Easy win! But there are things that we have missed. For example, a method for breaking retry calculations . It is easy to add:
data STMF next where
Retry :: STMF next
instance Functor STMF where
fmap g Retry = Retry
retry :: STML ()
retry = liftF RetryThere are slight differences in my library from my older sister; in particular, the retry method here returns Unit , although it must return an arbitrary type a . This is not a fundamental limitation, but an artifact of the rapid development of PoC, and in the future I will fix it. Nevertheless, even this code will remain without alterations except to replace the monad itself:
takeForks :: (TFork, TFork) -> STML ()
takeForks (tLeftFork, tRightFork) = do
leftTaken <- takeFork tLeftFork
rightTaken <- takeFork tRightFork
when (not leftTaken || not rightTaken) retryMonadic eDSL is as similar as possible to the base implementation, but the launch of STML scripts is different. My atomically combinator , unlike the base implementation, takes an additional argument - the context in which the calculation will spin.
atomically :: Context -> STML a -> IO aThe context stores user data in the form of TVar, so you can have several different contexts. This can be useful, for example, for separating transactional models - so that they do not affect each other. Say, in one model a huge amount of user data is created, and in another model, the TVar set does not change at all. Then it makes sense to separate the contexts so that the second model doesn’t experience problems due to the “swelling” neighbor. In the basic implementation, the context is global, and I have no idea how this can be circumvented.
The philosopher launch code now looks like this:
philosoperWorker :: Context -> Philosopher -> IO ()
philosoperWorker ctx philosopher = do
atomically ctx (changePhilosopherActivity philosopher)
threadDelay 5000
philosoperWorker ctx philosopher
runPhilosophers :: IO ()
runPhilosophers = do
ctx <- newContext -- Создание контекста.
tState1 <- newTVarIO ctx Thinking
tState2 <- newTVarIO ctx Thinking
tFork1 <- newTVarIO ctx Free
tFork2 <- newTVarIO ctx Free
forkIO (philosoperWorker ctx (Philosopher tState1 tFork1 tFork2))
forkIO (philosoperWorker ctx (Philosopher tState2 tFork2 tFork1))
threadDelay 100000A little bit about interpretation
What happens when we run a script using atomically ? The interpretation of the scenario relative to the real environment begins. It is at this moment that TVars begin to be created and changed, interrupt conditions are checked, and it is inside atomically that the transaction will either be committed in the transferred context, or will be rolled back and restarted. The algorithm is as follows:
- Get a unique transaction identifier.
- Atomically remove a local copy from the current context. A brief context lock occurs here, this is done using MVar, which acts like a normal mutex.
- Run the interpretation of the script with a local copy, wait for the result.
- If the command to restart the calculation is received, put the stream to sleep for a while and go to step 1.
- If the result is obtained, atomically check the conflicts of the local copy and context.
- If conflicts are found, euthanize the flow for a while and go to step 1.
- If there are no conflicts, everything will also atomically freeze the local copy into context.
- The end.
The context may change while this calculation does something with its local copy. The conflict arises when at least one TVar involved in this calculation has changed. This will be seen by the unique identifier stored in each instance. But if the calculation did not use TVar in any way, there will be no conflict.
Let our real environment be expressed by a certain Atomic monad , which is a stack of State and IO monads. As a state - a local copy of all TVar:
data AtomicRuntime = AtomicRuntime
{ ustamp :: UStamp
, localTVars :: TVars
}
type Atomic a = StateT AtomicRuntime IO aInside this monad, we will unwind and interpret two mutually nested structures: the STML type , which, as we recall, is built using the Free type , and the STMF type . The type of Free is a little brain-stemming, as it is recursive. He has two options:
data Free f a
= Pure a
| Free (f (Free f a))The interpretation is made simple pattern-matching. The interpreter returns either the value of the entire transaction, or a command to restart it.
interpretStmf :: STMF a -> Atomic (Either RetryCmd a)
interpretStmf (NewTVar a nextF) = Right . nextF <$> newTVar' a
interpretStmf (ReadTVar tvar nextF) = Right . nextF <$> readTVar' tvar
interpretStmf (WriteTVar tvar a next) = const (Right next) <$> writeTVar' tvar a
interpretStmf Retry = pure $ Left RetryCmd
interpretStml :: STML a -> Atomic (Either RetryCmd a)
interpretStml (Pure a) = pure $ Right a
interpretStml (Free f) = do
eRes <- interpretStmf f
case eRes of
Left RetryCmd -> pure $ Left RetryCmd
Right res -> interpretStml res
runSTML :: STML a -> Atomic (Either RetryCmd a)
runSTML = interpretStml
The functions newTVar ', readTVar', writeTvar ' work with a local copy of transaction variables, and can freely change them. The runSTML call is made from another function, runSTM , which will check the locally modified TVars for conflicts with the global copy from the context, and decide whether to restart the transaction.
runSTM :: Int -> Context -> STML a -> IO a
runSTM delay ctx stml = do
(ustamp, snapshot) <- takeSnapshot ctx
(eRes, AtomicRuntime _ stagedTVars) <- runStateT (runSTML stml) (AtomicRuntime ustamp snapshot)
case eRes of
Left RetryCmd -> runSTM (delay * 2) ctx stml
Right res -> do
success <- tryCommit ctx ustamp stagedTVars
if success
then return res
else runSTM (delay * 2) ctx stmlI’ll leave this function without explanation, and I won’t go into details about how the tryCommit function is implemented . Not very optimal, to be honest, but this is a topic for a separate article.
Conclusion
In my implementation, there are a number of subtle points that I still need to realize. There may still be unobvious bugs, and more cases need to be checked “for adequate behavior”, but it’s not clear what is considered adequate STM behavior. But at least, I did not reveal any external differences in the problem of dining philosophers, which means that the idea works, and it can be brought to mind. In particular, you can greatly optimize the runtime, make it more intelligent to resolve conflicts and remove a local copy. The approach with interpretation and the Free Monad turns out to be very flexible, and the code, as you can see for yourself, is much smaller, and it is generally very straightforward. And this is good, because it still opens the way for the implementation of STM in other languages.
For example, now I am porting Free-monadic STM in C ++, which entails my own difficulties unique to this language. Based on the results of the work, I will make a report at the April C ++ Russia 2018 conference , and if anyone is going to visit it, then we can discuss this topic in more detail.
