Software Transactional Memory on Free Monads
Realizing that I hadn’t written anything useful about HF and Haskell for Habr, and that there is quite a good reason for a technical article, I decided to shake the old days. The article focuses 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, compared to the “real” STM. Let's discuss this.
STM is an approach for programming a competitive data model. Competitiveness here is that different parts of the model can be updated in different flows independently of each other, and conflicts on shared resources are resolved with the help of 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. Did not change? Well, the new values will be fixed. Did someone have time before you? This is a conflict, if you please, restart your calculations on the new data. Schematically it can be represented as follows:
Here, atomic operations are performed by threads in parallel, but committed only within transactions that block access to the variable parts of the model.
')
There are different variations of STM, but we will talk specifically about the one proposed in the famous work “Composable Memory Transactions” , since it is distinguished by a number of remarkable properties:
A model can be any kind of data structure. You can convert any of your regular model into a transactional one, for this STM-libraries provide various primitives: variables ( TVar ), queues ( TQueue ), arrays ( TArray ) and many others. One can guess that the transaction variables - TVars ("creatures") - are already minimally sufficient for a full-fledged STM, and everything else is expressed through them.
Consider, for example, the problem of the 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. In the end, only one philosopher would dine, and four others would reflect, and the next time he would have dined another, but also one, although theoretically, with five forks, two could have dinner in parallel. Therefore, you need to make a competitive model that will give the most expected behavior. Here is how the calculation in the STM monad could look like for a model with separate forks-creatures:
The function returns True if the plug was free, and it was successfully “taken”, that is, overwritten by tFork . False will be if the plug is already in business and cannot 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 fork (for example, the left one), but do not take another one (for example, the right fork, which was occupied by the neighbor). The takeForks function, of course, returns False in this case, but what about the fact that one fork did end up in the hands of our philosopher? He will not be able to eat alone, so it must be put back, and continue to think for some 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 somewhat differently than in terms of other competitive structures. We can assume that both the variables tLeftFork and tRightFork are local copies that are not associated with the same resource from other philosophers. Therefore, you can not "put" the plug back, and tell the calculation that it failed. Then our one taken fork will not be written into shared resources - it’s all the same that there was no successful takeFork call. This is very convenient, and it is the “undo” operation of the current monadic calculation that distinguishes the implementation of the haskel STM from the others. To cancel, there is a special retry method, let's rewrite takeForks using it:
The calculation will be successful when both forks were taken at once by our philosopher. Otherwise, it will restart over and over at some intervals. In this version, we do not return Bool , because we do not need to know whether both resources have been successfully captured. If the function is executed and the calculation is not filled, then it is successful.
After taking forks, we will probably need to do something else, for example, to transfer the philosopher to the “Eating” state. We simply do this after calling takeForks , and the STM monad will take care of the “creature” states to be consistent:
We will leave the full implementation of this method as an exercise, and now consider the last missing link. So far we only described the logic of the transactional model, but we have not yet created any specific TVar , and have not run anything. Let's do it:
The atomically :: STM a -> IO a combinator performs the calculation in the STM monad atomically. From the type it can be seen that the pure part - working with a competitive model - is separated from impure calculations in the IO monad. STM-code should not have effects. It’s better - none at all, otherwise you will get some strange results when you restart, for example, if you wrote to a file, in some situations you may get spurious records, 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 you from creating new TVars inside the STM using a clean combinator newTVar :: a -> STM (TVar a) . We just did not need it. Attentive ones will notice that only forks are a shared resource here, and the condition of the philosophers themselves is wrapped in TVar for convenience only.
Summarize. The minimum STM implementation should contain the following functions for working with TVar :
Perform 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 constructions, for example, an instance of the class of types Alternative for STM , but let's leave it to self-study.
Implementing a correctly 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 by far the best, and in other languages STM is not quite real. It can be assumed that monadic STM with the possibility of restarting calculations and controlling effects is not in any imperative language. But this is all idle reasoning, and I may be wrong. Unfortunately, I don’t understand the insides of even the stm hasksel library, not to mention other ecosystems. However, 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 (domain-specific language) and the expected behavior, this is 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 to 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 covers many issues of design and software architecture in functional programming, I will leave other details behind the brackets. Curious people can refer to numerous sources on the Internet or to my half-book “Functional Design and Architecture” , where Free monads are given special attention.
And now let's look at the code of my library stm-free .
Since STM is a domain-specific language for creating transactional models, it is pure and monadic, we can assume that for a minimal STM, Free DSL should contain the same methods for working with TVar, and they will be automatically compiled and clean in this very Free-monad. First, we define what TVar is.
We will need to distinguish between our "beasts", 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 TVar a type. Working 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 a Free-Monad should be built on top of some kind of eDSL. The easiest way to set it up 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 the methods with some effect. Obviously, the NewTVar method should be interpreted with the result “a new TVar is created and returned as a result”. But you can make an interpreter that will do something else, for example, write to the database, log, or even make calls to a real STM.
These constructors contain all the necessary information to be interpreted. The NewTVar constructor contains some user-defined value a , and when interpreted we will put this value in the new TVar. But the problem is that a must be different for each NewTVar call. If we just wrote STMF next a , a would already be common to the whole code, where several NewTVar calls are tied :
But it is meaningless, because we still want to use NewTVar for our arbitrary types, and so that they do not push. Therefore, we remove a in the local visibility of only a specific method.
The more interesting question is, where is our custom monad for STM? Here she is:
We wrapped the STMF type into the Free type, and with it came all the monadic properties we needed. 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 an example with the dining philosophers and simply replace STM with STML :
Easy win! But there are things that we have missed. For example, the method for terminating computation retry . It is easy to add:
There are some minor differences in my library from the older sister; in particular, the method of retry here returns Unit , although it must return an arbitrary type a . This is not a fundamental limitation, but an artifact of rapid development of PoC, and in the future I will fix it. Nevertheless, even this code will remain without alterations except for replacing the monad itself:
Monadic eDSL is most similar to the basic implementation, but the launch of STML scripts is different. My atomically atomizer , unlike the base implementation, takes an additional argument — the context in which the calculation will run.
In context, user data is stored in the form of TVar, so you can have several different contexts. This can be useful, for example, to separate transactional models — so that they do not affect each other. For example, in one model, a huge amount of user data is created, while in another model, the TVar set does not change at all. Then it makes sense to separate contexts so that the second model does not have any problems due to the “swelling” neighbor when performing. In the base implementation, the context is global, and I don’t really know how to get around this.
The philosophers launch code now looks like this:
What happens when we run the script atomically ? The interpretation of the scenario relative to the real environment begins. It is at this point that TVars begin to form and change, interrupt conditions are checked, and it is inside the atomically that the transaction will either be fixed in the passed context, or be rolled out and restarted. The algorithm is as follows:
The context may change as long as the given calculation does something with its local copy. Conflict arises when at least one TVar changed, involved in this calculation. This will be seen by a unique identifier stored in each instance. But if the calculation did not use TVar, 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. The status is a local copy of all TVar:
Inside this monad we will unwind and interpret two mutually nested structures: the STML type, which, as we remember, is built using the Free type, and the STMF type. The Free type is a little brainwave, since it is recursive. He has two options:
Interpretation is done by 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 the transaction variables, and can change them freely. The runSTML call is made from another function, runSTM , which checks for locally modified TVars for conflicts with the global copy from the context, and decides whether to restart the transaction.
I will leave this function without explanation, and I will not dive into the details of 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 adequacy of behavior”, but it’s not clear what is considered adequate STM behavior. But at least, I didn’t reveal any external differences on the task of the dining philosophers, which means that the idea works, and it can be brought to mind. In particular, you can greatly optimize runtime, make smarter conflict resolution and make a local copy more intelligent. The approach with interpretation and Free-monad is quite flexible, and the code, as you can see, is much smaller, and in general it is very straightforward. And this is good, because it opens another way for the implementation of STM in other languages.
For example, now I port Free-monad STM in C ++, which is associated with my own unique difficulties for this language. As a result of the work, I will give a talk 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. Competitiveness here is that different parts of the model can be updated in different flows independently of each other, and conflicts on shared resources are resolved with the help of 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. Did not change? Well, the new values will be fixed. Did someone have time before you? This is a conflict, if you please, restart your calculations on the new data. Schematically it can be represented as follows:
Here, atomic operations are performed by threads in parallel, but committed only within transactions that block access to the variable parts of the model.
')
There are different variations of STM, but we will talk specifically about the one proposed in the famous work “Composable Memory Transactions” , since it is distinguished by a number of remarkable properties:
- the concepts of data model and calculations above it are separated;
- computations are the STM monad, and they are composable in full accordance with the AF paradigm;
- there is the notion of manually restarting the calculation (retry);
- Finally, there is an excellent implementation for Haskell, which, however, I will not consider, but I will focus on my own, interface-like.
A model can be any kind of data structure. You can convert any of your regular model into a transactional one, for this STM-libraries provide various primitives: variables ( TVar ), queues ( TQueue ), arrays ( TArray ) and many others. One can guess that the transaction variables - TVars ("creatures") - are already minimally sufficient for a full-fledged STM, and everything else is expressed through them.
Consider, for example, the problem of the 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. In the end, only one philosopher would dine, and four others would reflect, and the next time he would have dined another, but also one, although theoretically, with five forks, two could have dinner in parallel. Therefore, you need to make a competitive model that will give the most expected behavior. Here is how the calculation in the STM monad could look like for a model with separate forks-creatures:
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 by tFork . False will be if the plug is already in business and cannot be touched. Now consider a couple of forks. There can be five situations:
- Both are free
- Left is busy (left neighbor), right is free
- Left is free, right is busy (right neighbor)
- Both are busy (neighbors)
- Both are busy (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 fork (for example, the left one), but do not take another one (for example, the right fork, which was occupied by the neighbor). The takeForks function, of course, returns False in this case, but what about the fact that one fork did end up in the hands of our philosopher? He will not be able to eat alone, so it must be put back, and continue to think for some 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 somewhat differently than in terms of other competitive structures. We can assume that both the variables tLeftFork and tRightFork are local copies that are not associated with the same resource from other philosophers. Therefore, you can not "put" the plug back, and tell the calculation that it failed. Then our one taken fork will not be written into shared resources - it’s all the same that there was no successful takeFork call. This is very convenient, and it is the “undo” operation of the current monadic calculation that distinguishes the implementation of the haskel STM from the others. To cancel, there is a special retry method, 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) retry The calculation will be successful when both forks were taken at once by our philosopher. Otherwise, it will restart over and over at some intervals. In this version, we do not return Bool , because we do not need to know whether both resources have been successfully captured. If the function is executed and the calculation is not filled, then it is successful.
After taking forks, we will probably need to do something else, for example, to transfer the philosopher to the “Eating” state. We simply do this after calling takeForks , and the STM monad will take care of the “creature” states to be 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. So far we only described the logic of the transactional model, but we have not yet created any specific TVar , and have not run 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 100000 The atomically :: STM a -> IO a combinator performs the calculation in the STM monad atomically. From the type it can be seen that the pure part - working with a competitive model - is separated from impure calculations in the IO monad. STM-code should not have effects. It’s better - none at all, otherwise you will get some strange results when you restart, for example, if you wrote to a file, in some situations you may get spurious records, 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 you from creating new TVars inside the STM using a clean combinator newTVar :: a -> STM (TVar a) . We just did not need it. Attentive ones will notice that only forks are a shared resource here, and the condition of the philosophers themselves is wrapped in TVar for convenience only.
Summarize. The minimum STM implementation should contain the following functions for working with TVar :
newTVar :: a -> STM (TVar a) readTVar :: TVar a -> STM a writeTVar :: TVar a -> a -> STM () Perform calculations:
atomically :: STM a -> IO a Finally, the ability to restart the calculation will be a huge plus:
retry :: STM a Of course, in libraries there are a huge number of other useful constructions, for example, an instance of the class of types Alternative for STM , but let's leave it to self-study.
STM on Free Monads
Implementing a correctly 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 by far the best, and in other languages STM is not quite real. It can be assumed that monadic STM with the possibility of restarting calculations and controlling effects is not in any imperative language. But this is all idle reasoning, and I may be wrong. Unfortunately, I don’t understand the insides of even the stm hasksel library, not to mention other ecosystems. However, 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 (domain-specific language) and the expected behavior, this is 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, compiled monadically, that is, truly functional;
- The code on this DSL will not contain anything extra, besides the subject area, which means that 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 to 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 covers many issues of design and software architecture in functional programming, I will leave other details behind the brackets. Curious people can refer to numerous sources on the Internet or to my half-book “Functional Design and Architecture” , where Free monads are given special attention.
And now let's look at the code of my library stm-free .
Since STM is a domain-specific language for creating transactional models, it is pure and monadic, we can assume that for a minimal STM, Free DSL should contain the same methods for working with TVar, and they will be automatically compiled and clean in this very Free-monad. First, we define what TVar is.
type UStamp = Unique newtype TVarId = TVarId UStamp data TVar a = TVar TVarId We will need to distinguish between our "beasts", 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 TVar a type. Working 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 next And here you need to stay in more detail.
Why should we do this? The bottom line is that a Free-Monad should be built on top of some kind of eDSL. The easiest way to set it up 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 the methods with some effect. Obviously, the NewTVar method should be interpreted with the result “a new TVar is created and returned as a result”. But you can make an interpreter that will do something else, for example, write to the database, log, or even make calls to a real STM.
These constructors contain all the necessary information to be interpreted. The NewTVar constructor contains some user-defined value a , and when interpreted we will put this value in the new TVar. But the problem is that a must be different for each NewTVar call. If we just wrote STMF next a , a would already be common to the whole code, where several NewTVar calls are tied :
data STMF next a where NewTVar :: a -> (TVar a -> next) -> STMF next But it is meaningless, because we still want to use NewTVar for our arbitrary types, and so that they do not push. Therefore, we remove a in the local visibility of only a specific method.
Note In fact, to speed up the work on Proof of Concept, I have a restriction on type a so that it can be serialized (an instance of the ToJSON / FromJSON class from the aeson library). The fact is that I will need to keep these different types of TVars in a map, but I do not want to bother with Typeable / Dynamic or, especially, with HLists . In real STM type a can be absolutely any, even functions. I will also deal with this issue sometime later.And what is this next field? Here we step on the demand from the Free-monad. She needs to store somewhere the continuation of the current method, and just the next field does not suit her, - ADT should be a functor on 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 a type STMF 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) The more interesting question is, where is our custom monad for STM? Here she is:
type STML next = Free STMF next We wrapped the STMF type into the Free type, and with it came all the monadic properties we needed. 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 an example with the dining philosophers and simply 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, the method for terminating computation retry . It is easy to add:
data STMF next where Retry :: STMF next instance Functor STMF where fmap g Retry = Retry retry :: STML () retry = liftF Retry There are some minor differences in my library from the older sister; in particular, the method of retry here returns Unit , although it must return an arbitrary type a . This is not a fundamental limitation, but an artifact of rapid development of PoC, and in the future I will fix it. Nevertheless, even this code will remain without alterations except for replacing the monad itself:
takeForks :: (TFork, TFork) -> STML () takeForks (tLeftFork, tRightFork) = do leftTaken <- takeFork tLeftFork rightTaken <- takeFork tRightFork when (not leftTaken || not rightTaken) retry Monadic eDSL is most similar to the basic implementation, but the launch of STML scripts is different. My atomically atomizer , unlike the base implementation, takes an additional argument — the context in which the calculation will run.
atomically :: Context -> STML a -> IO a In context, user data is stored in the form of TVar, so you can have several different contexts. This can be useful, for example, to separate transactional models — so that they do not affect each other. For example, in one model, a huge amount of user data is created, while in another model, the TVar set does not change at all. Then it makes sense to separate contexts so that the second model does not have any problems due to the “swelling” neighbor when performing. In the base implementation, the context is global, and I don’t really know how to get around this.
The philosophers 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 100000 Little about interpretation
What happens when we run the script atomically ? The interpretation of the scenario relative to the real environment begins. It is at this point that TVars begin to form and change, interrupt conditions are checked, and it is inside the atomically that the transaction will either be fixed in the passed context, or be rolled out and restarted. The algorithm is as follows:
- Get a unique transaction ID.
- Atomic remove a local copy from the current context. This is where a short context lock occurs; 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 for conflicts between the local copy and the context.
- If conflicts are found, put the stream to sleep for a while and go to step 1.
- If there is no conflict, everything will also atomically hold the local copy into context.
- The end.
The context may change as long as the given calculation does something with its local copy. Conflict arises when at least one TVar changed, involved in this calculation. This will be seen by a unique identifier stored in each instance. But if the calculation did not use TVar, 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. The status is a local copy of all TVar:
data AtomicRuntime = AtomicRuntime { ustamp :: UStamp , localTVars :: TVars } type Atomic a = StateT AtomicRuntime IO a Inside this monad we will unwind and interpret two mutually nested structures: the STML type, which, as we remember, is built using the Free type, and the STMF type. The Free type is a little brainwave, since it is recursive. He has two options:
data Free fa = Pure a | Free (f (Free fa)) Interpretation is done by 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 the transaction variables, and can change them freely. The runSTML call is made from another function, runSTM , which checks for locally modified TVars for conflicts with the global copy from the context, and decides 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 stml I will leave this function without explanation, and I will not dive into the details of 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 adequacy of behavior”, but it’s not clear what is considered adequate STM behavior. But at least, I didn’t reveal any external differences on the task of the dining philosophers, which means that the idea works, and it can be brought to mind. In particular, you can greatly optimize runtime, make smarter conflict resolution and make a local copy more intelligent. The approach with interpretation and Free-monad is quite flexible, and the code, as you can see, is much smaller, and in general it is very straightforward. And this is good, because it opens another way for the implementation of STM in other languages.
For example, now I port Free-monad STM in C ++, which is associated with my own unique difficulties for this language. As a result of the work, I will give a talk at the April C ++ Russia 2018 conference, and if anyone is going to visit it, then we can discuss this topic in more detail.
Source: https://habr.com/ru/post/350628/
All Articles