A paper in the works for quite some time. You can download the latest version here.
Here's what the abstract says:
Join patterns are a powerful concurrency abstraction to coordinate multiple events. We propose an extension with guards and propagation and argue that both features are essential in many programming situations. We develop a parallel execution scheme which we have fully implemented as a library in Haskell. Our results provide new insights how to write parallel programs on multi-core architectures.
Interested? You can get the implementation via the Haskell platform hackage. Download the join package which in turn relies on the multisetrewrite package. The multisetrewrite package provides the basic functionality to execute join patterns (with guards and propagation) in parallel. The join package adds synchronous and asynchronous arguments and join method calls. The user interface is still a bit clumsy to use but this will hopefully be improved over time.
Showing posts with label concurrency. Show all posts
Showing posts with label concurrency. Show all posts
Saturday, 6 December 2008
Friday, 5 December 2008
Concurrent Goal-Based Execution of Constraint Handling Rules
We (my PhD student Edmund and me) have just submitted a paper with this title to Theory and Practice of Logic Programming. The paper complements our PPDP'08 paper on parallel Constraint Handling Rules execution. You can get the paper here.
Here's what the abstract says:
We introduce a systematic, concurrent execution scheme for Constraint Handling Rules (CHR) based on a previously proposed goal-based CHR semantics. We establish strong correspondence results to the abstract CHR semantics, thus guaranteeing that any answer in the concurrent, goal-based CHR semantics is reproducible in the abstract CHR semantics. Our work provides the foundation to obtain efficient, parallel CHR execution schemes.
Here's what the abstract says:
We introduce a systematic, concurrent execution scheme for Constraint Handling Rules (CHR) based on a previously proposed goal-based CHR semantics. We establish strong correspondence results to the abstract CHR semantics, thus guaranteeing that any answer in the concurrent, goal-based CHR semantics is reproducible in the abstract CHR semantics. Our work provides the foundation to obtain efficient, parallel CHR execution schemes.
Thursday, 4 December 2008
STM with control: Communication for retrying transactions
While working on the join pattern with guards and propagation implementation, we (my PhD student Edmund and me) came across an interesting problem which points out the current limited control/communication capabilities of retrying STM transactions (in Haskell). More on join patterns later. Here's the gist of the problem and a solution in form of a new Haskell library.
We're given a list of switches, they can either be on or off
If all switches are on, we switch them all off and report True If one switch is off, we do nothing and report False.
In a sequential setting, this task is straightforward. But what if the switches are shared among concurrent threads performing the above task?
In a concurrent setting, the task must be formulated as follows.
Atomically (
If all switches are on, we switch them all off and report True
If one switch is off, we do nothing and report False. )
Sounds like an application of STM. Indeed, here's a solution.
We first check that all switches are on. Only then we switch all of them off. Isolation and atomicity of STM are important here.
Isolation guarantees that no intermediate step is visible to any other thread. After checking that all switches are on, we have the guarantee that they are still on, once we switch them off. Atomicity guarantees that all operations are executed all at once or not all which implies that some of the initially read switch values has changed. In this case, we abort the transaction and discard all changes so far and start over again.
It's tempting to immediately turn a switch off once we've read that the switch is on. But what if we read that a switch is still on? We need some additionally functionality to explicitly abort the transactions. That's what the retry and orElse combinators are for.
The loop reads the status of each switch and turns the switch off if the switch is on. Otherwise, we 'abort' by returning False. For example, in case of the initial list [On, On, Off, On] we reach the third switch and the intermediate result [Off, Off, Off, On]. We can't just naively exit at this stage because the tasks demands that all changes are done atomically, ie to its full extent or not at all.
Here comes the rescue. The retry combinator allows the programmer to explicitly abort a transaction. That is, we discard all changes (which is important) here. The orElse combinator allows the programmer to compose two transaction. The second transaction will be executed if the first transaction retries. Exactly what we require.
Suppose each switch is attached to an action, sort of a continuation. Let's say an IO action.
We want to return the continuation of the switch which first 'failed'. Here's the updated task description.
Atomically (
If all switches are on, we switch them all off and report True
Otherwise, return the continuation of the first turned on switch.)
The signature of the function we need to implement
What are our options how to implement the above?
We could adapt our first solution verifyAndSwitchOff. This is pretty straightforward. What about verifyAndSwitchOff2? Previously, we simply return False in the second orElse branch. For the more interesting task, we need to iterate over the list of pairs of switches and continuation and select the continuation of the first switch which is still on. This means that in both case we possibly need to iterate over the list twice. This is inefficient and leads to clumsy code.
Below we make use of an extension of STM where a retrying transaction can pass some information to the second transaction composed with orElse.
The extension is implemented as the STMControl.STMC library. The new primitives are:
STMC stands for STM with more control. The first parameter refers to the type of the value transmited in case of a retryC. The parameter in the orElseC combinator is now a function which accepts the result transmitted of the retrying transaction.
The implementation is fairly simple and uses an (abused) reader monad on top of STM. Here's finally an application of the new functionality.
The loop checks and resets all switches. In case a switch is turned off we return the attached continuation. We use the Maybe type to indicate failure (Just c) or success (Nothing). In case of success, we return the donothing continuation. Otherwise, we retryC to discard all changes made so far and pass the continuation to the second transaction which then returns this continuation.
I'd say compared to the other options, the STMC solution looks pretty clean and easy to understand.
That's the final extension, I promise. Suppose that to each switch there's also an attached STM Bool transaction. In addition to testing that the switch is off, we also test that the STM Bool transaction evaluates to True. Otherwise, we discard our changes and return the attached continuation.
The required changes to our previous solution are minor. In fact, I can't see how to implement the even more interesting task with STM alone. I believe that this task strictly requires STMC or something similar.
The complete source code of this example is available as part of the stmcontrol package on the Haskell platform hackage.
What if the transaction is aborted just after execution of L1? Is our use of unsafeIOToSTM (un)safe? It's safe. It's okay to discard the IO action in case the transaction is rolled back. The important point is that if the transaction is explicitly retried, the IO action has been executed (which is the case as far as I understand the interplay of STM and unsafeIOToSTM).
The task
We're given a list of switches, they can either be on or off
> data Switch = On | Off
If all switches are on, we switch them all off and report True If one switch is off, we do nothing and report False.
In a sequential setting, this task is straightforward. But what if the switches are shared among concurrent threads performing the above task?
In a concurrent setting, the task must be formulated as follows.
Atomically (
If all switches are on, we switch them all off and report True
If one switch is off, we do nothing and report False. )
Sounds like an application of STM. Indeed, here's a solution.
> verifyAndSwitchOff :: [TVar Switch] -> IO Bool
> verifyAndSwitchOff ts =
> atomically $ do
> bs <- mapM (\s -> do v <- readTVar s
> case v of
> On -> return True
> Off -> return False)
> ts
>
> if (and bs)
> then do mapM (\s -> do writeTVar s Off) ts
> return True
> else return False
We first check that all switches are on. Only then we switch all of them off. Isolation and atomicity of STM are important here.
Isolation guarantees that no intermediate step is visible to any other thread. After checking that all switches are on, we have the guarantee that they are still on, once we switch them off. Atomicity guarantees that all operations are executed all at once or not all which implies that some of the initially read switch values has changed. In this case, we abort the transaction and discard all changes so far and start over again.
It's tempting to immediately turn a switch off once we've read that the switch is on. But what if we read that a switch is still on? We need some additionally functionality to explicitly abort the transactions. That's what the retry and orElse combinators are for.
> verifyAndSwitchOff2 :: [TVar Switch] -> IO Bool
> verifyAndSwitchOff2 ts =
> let loop [] = return True
> loop (s:xs) = do v <- readTVar s
> case v of
> On -> do writeTVar s Off
> loop xs
> Off -> return False
> in atomically $
> (do b <- loop ts
> if b then return True
> else retry)
>
> `orElse`
>
> return False
The loop reads the status of each switch and turns the switch off if the switch is on. Otherwise, we 'abort' by returning False. For example, in case of the initial list [On, On, Off, On] we reach the third switch and the intermediate result [Off, Off, Off, On]. We can't just naively exit at this stage because the tasks demands that all changes are done atomically, ie to its full extent or not at all.
Here comes the rescue. The retry combinator allows the programmer to explicitly abort a transaction. That is, we discard all changes (which is important) here. The orElse combinator allows the programmer to compose two transaction. The second transaction will be executed if the first transaction retries. Exactly what we require.
Making the task more interesting
Suppose each switch is attached to an action, sort of a continuation. Let's say an IO action.
> type Cnt = IO ()
We want to return the continuation of the switch which first 'failed'. Here's the updated task description.
Atomically (
If all switches are on, we switch them all off and report True
Otherwise, return the continuation of the first turned on switch.)
The signature of the function we need to implement
verifyAndSwitchOffCnt :: [(TVar Switch, Cnt)] -> IO Cnt
What are our options how to implement the above?
We could adapt our first solution verifyAndSwitchOff. This is pretty straightforward. What about verifyAndSwitchOff2? Previously, we simply return False in the second orElse branch. For the more interesting task, we need to iterate over the list of pairs of switches and continuation and select the continuation of the first switch which is still on. This means that in both case we possibly need to iterate over the list twice. This is inefficient and leads to clumsy code.
Below we make use of an extension of STM where a retrying transaction can pass some information to the second transaction composed with orElse.
The extension is implemented as the STMControl.STMC library. The new primitives are:
newTVarC :: b -> STMC a (TVar b)
readTVarC :: TVar b -> STMC a b
writeTVarC :: TVar b -> b -> STMC a ()
atomicallyC :: STMC a b -> IO b
retryC :: a -> STMC a b
orElseC :: STMC a b -> (a -> STMC a b) -> STMC a b
STMC stands for STM with more control. The first parameter refers to the type of the value transmited in case of a retryC. The parameter in the orElseC combinator is now a function which accepts the result transmitted of the retrying transaction.
The implementation is fairly simple and uses an (abused) reader monad on top of STM. Here's finally an application of the new functionality.
> verifyAndSwitchOffCnt :: [(TVar Switch, Cnt)] -> IO Cnt
> verifyAndSwitchOffCnt tcs =
> let loop [] = return Nothing
> loop ((s,c):xs) = do v <- readTVarC s
> case v of
> On -> do writeTVarC s Off
> loop xs
> Off -> return (Just c)
> in atomicallyC $
> (do r <- loop tcs
> case r of
> Nothing -> return (return ()) -- default (donothing) continuation
> Just c -> retryC c)
>
> `orElseC`
>
> (\c -> return c)
The loop checks and resets all switches. In case a switch is turned off we return the attached continuation. We use the Maybe type to indicate failure (Just c) or success (Nothing). In case of success, we return the donothing continuation. Otherwise, we retryC to discard all changes made so far and pass the continuation to the second transaction which then returns this continuation.
I'd say compared to the other options, the STMC solution looks pretty clean and easy to understand.
Making the task even more interesting
That's the final extension, I promise. Suppose that to each switch there's also an attached STM Bool transaction. In addition to testing that the switch is off, we also test that the STM Bool transaction evaluates to True. Otherwise, we discard our changes and return the attached continuation.
> verifyAndSwitchOffCnt2 :: [(TVar Switch, STM Bool, Cnt)] -> IO Cnt
> verifyAndSwitchOffCnt2 tcs =
> let loop [] = return Nothing
> loop ((s,stm,c):xs) =
> do v <- readTVarC s
> case v of
> On -> do writeTVarC s Off
> b <- lift $ stm
STMC are (reader monad) lifted STM operations
> if b then loop xs
> else return (Just c)
> Off -> return (Just c)
> in atomicallyC $
> (do r <- loop tcs
> case r of
> Nothing -> return (return ()) -- default (donothing) continuation
> Just c -> retryC c)
>
> `orElseC`
>
> (\c -> return c)
The required changes to our previous solution are minor. In fact, I can't see how to implement the even more interesting task with STM alone. I believe that this task strictly requires STMC or something similar.
The complete source code of this example is available as part of the stmcontrol package on the Haskell platform hackage.
Implementation details
type STMC a b = ReaderT (IORef a) STM b
retryC :: a -> STMC a b
retryC x = do msgChan <- ask
lift $ unsafeIOToSTM (writeIORef msgChan x) -- L1
lift $ retry
What if the transaction is aborted just after execution of L1? Is our use of unsafeIOToSTM (un)safe? It's safe. It's okay to discard the IO action in case the transaction is rolled back. The important point is that if the transaction is explicitly retried, the IO action has been executed (which is the case as far as I understand the interplay of STM and unsafeIOToSTM).
Saturday, 29 November 2008
Transactions in Constraint Handling Rules
A paper to be presented at ICLP'08, Udine, Italy, December'08. My co-author Tom Schrijvers will give the presentation but here's already a draft of the talk.
If you've followed my previous posts on (software) transactions (in memory aka STM), this paper is more on the theoretical (greek symbol) side, but still worth a read if you seek for a systematic method to improve the efficiency of your STM code.
In the paper, we enrich the Constraint Handling Rules (CHR) calculus with transactions. If you've never heard the name CHR before, think of multi-set rewriting, bounded transactions, or a form of join pattern with guards and propagation. The paper develops a theory of how to (possibly) transform unbounded transactions to bounded transactions. Under optimistic concurrency control, unbounded transactions (e.g. transactions traversing a dynamic data structure such as a linked list) often yield "false" conflicts which means that transactions are executed sequentially instead of in parallel. Bounded transactions (e.g. dining philosphers which grap a bounded, two, number of forks) are generally free of such (in)efficiency problems. Details are in the paper.
If you've followed my previous posts on (software) transactions (in memory aka STM), this paper is more on the theoretical (greek symbol) side, but still worth a read if you seek for a systematic method to improve the efficiency of your STM code.
In the paper, we enrich the Constraint Handling Rules (CHR) calculus with transactions. If you've never heard the name CHR before, think of multi-set rewriting, bounded transactions, or a form of join pattern with guards and propagation. The paper develops a theory of how to (possibly) transform unbounded transactions to bounded transactions. Under optimistic concurrency control, unbounded transactions (e.g. transactions traversing a dynamic data structure such as a linked list) often yield "false" conflicts which means that transactions are executed sequentially instead of in parallel. Bounded transactions (e.g. dining philosphers which grap a bounded, two, number of forks) are generally free of such (in)efficiency problems. Details are in the paper.
Tuesday, 18 November 2008
High-level Software Transaction Protocols
The topic is how to built high-level (composable) software transaction protocols on top of highly-concurrent, low-level data structures which are not composable. Yes, this is sort of a continuation of my previous 'Transactional Boosting' post. What I'm looking for is a systematic method to built boosted protocols. I believe that a promising formalism are join patterns (aka multi-set rewrite rules).
Here's my attempt to recast the transactional boosting approach in terms of the join pattern language extension I'm currently working on. Join patterns can now have guards and propagation. For example, the following join patterns says
if we find method calls foo(x,y) and bar(y,z) where the condition x > z holds (notice the implicit constraint imposed via the shared variable z), then we remove (simplify) bar(y,z) from the method store but we keep (propagate) foo(x,y).
Okay, so let's make use of such join patterns to specify the boosted transactional protocol. For simplicity, let's consider a very simple to be boosted object. A set with one 'add' operation.
The interface:
From the environment, we get the current transaction identifier (kind of ThreadId). We create a synchronization variable on which we will block. But first we call the method
addI(t,x,r) whose interaction with other method calls is specified below
(In a Join setting, method calls are recorded in a store).
The protocol to check for conflicts:
The first join pattern checks for non-commuting method calls (subtle point: we assume that the propagated head will NOT be executed as a goal). Join patterns are tried from top to bottom (in our implementation). Hence, if the first join pattern can't fire we try the second one which applies if all calls to add commute and there exist at least two add calls (we assume multi-set semantics, one call can't match two occurrences). In the 'commute' case, we call the primitive add (relying on the highly-concurrent, low-level data structure) and unblock the original add call. Registering of the inverse operation is necessary in case we abort the transaction. The last join pattern applies if we're the first to call add. Adding add calls to the store guarantees that
all calls are made visible to each other.
A transaction can only commit (reach the end) if it doesn't encounter conflicts. Otherwise, the transaction will be suspended.
The commit protocol has two stages. We first unblock one suspended add call (if exists). Otherwise, we do nothing. The assumption is that the committing transaction calls 'commit(t)'.
Actually, we could be more optimistic and unblock all commuting add calls. I can't see how to nicely formulate this with join pattern alone (we'd need to traverse all suspended calls and select all commuting ones).
We yet to release all 'locks' (the stored add calls) held by transaction t. Once more, we call 'commit(t)'.
The propagated goal 'commit(t)' guarantees that we exhaustively release all locks (a for loop join pattern style).
In the last commit step, we erase all registered inverse operations.
As said above, in the current formulation, a transaction can only reach the end (and thus commit) if it doesn't encounter conflicts. The transaction won't fail or retry. It can only happen that the transaction is suspended, possibly indefinitely.
To avoid 'cyclic suspension' deadlocks, the 'transactional boosting' approach uses a time-out to actually fail a transaction. In case of failure, we need to remove the transaction's method calls
and we execute the registered inverse operations. Then, the transaction is started from scratch.
The above description is not necessarily meant to be used in an efficient implementation. However, I believe that the use of join patterns allows us to to give a nice declarative specification of 'transactional boosting' and its underlying protocols. I will be interesting to consider alternative 'boosting' protocols. It appears that in general the 'boosting' approach can only support pessimistic concurrency. Optimistic concurrency requires that a transaction only commits its updates only after no conflicts have been detected.
In my experience, transactional boosting and optimistic concurrency only works out for some specific cases, eg the multi-set rewrite stuff I mentioned in my earlier 'Transactional Boosting' post.
Anyway, there's still lots to discover. Guess that's something for a future post.
Transactional boosting revisited
Here's my attempt to recast the transactional boosting approach in terms of the join pattern language extension I'm currently working on. Join patterns can now have guards and propagation. For example, the following join patterns says
foo(x,y) \ bar(y,z) when x > z = ...
if we find method calls foo(x,y) and bar(y,z) where the condition x > z holds (notice the implicit constraint imposed via the shared variable z), then we remove (simplify) bar(y,z) from the method store but we keep (propagate) foo(x,y).
Okay, so let's make use of such join patterns to specify the boosted transactional protocol. For simplicity, let's consider a very simple to be boosted object. A set with one 'add' operation.
The interface:
add x = do t <- readEnv
r <- newSync
addI(t,x,r)
v <- readSync r
From the environment, we get the current transaction identifier (kind of ThreadId). We create a synchronization variable on which we will block. But first we call the method
addI(t,x,r) whose interaction with other method calls is specified below
(In a Join setting, method calls are recorded in a store).
The protocol to check for conflicts:
-- conflict --> suspend
addI(t1,x,_) \ addI(t2,x,r) = addS(t2,x,r)
-- commute
addI(t1,x,_) \ addI(t2,y,r) when x \= y = do primAdd y
register t2 'remove y'
r:= ()
addToStore 'addI(t,x,r)'
-- first call
addI(t,x,r) = do primAdd x
register t 'remove x'
r:= ()
addToStore 'addI(t,x,r)'
The first join pattern checks for non-commuting method calls (subtle point: we assume that the propagated head will NOT be executed as a goal). Join patterns are tried from top to bottom (in our implementation). Hence, if the first join pattern can't fire we try the second one which applies if all calls to add commute and there exist at least two add calls (we assume multi-set semantics, one call can't match two occurrences). In the 'commute' case, we call the primitive add (relying on the highly-concurrent, low-level data structure) and unblock the original add call. Registering of the inverse operation is necessary in case we abort the transaction. The last join pattern applies if we're the first to call add. Adding add calls to the store guarantees that
all calls are made visible to each other.
A transaction can only commit (reach the end) if it doesn't encounter conflicts. Otherwise, the transaction will be suspended.
The commit protocol has two stages. We first unblock one suspended add call (if exists). Otherwise, we do nothing. The assumption is that the committing transaction calls 'commit(t)'.
commit(t), addI(t,x,_), addS(t2,x,r) = addI(t2,x,r)
commit(t) = return ()
Actually, we could be more optimistic and unblock all commuting add calls. I can't see how to nicely formulate this with join pattern alone (we'd need to traverse all suspended calls and select all commuting ones).
We yet to release all 'locks' (the stored add calls) held by transaction t. Once more, we call 'commit(t)'.
commit(t) \ addI(t,x,_) = return ()
commit(t) = return ()
The propagated goal 'commit(t)' guarantees that we exhaustively release all locks (a for loop join pattern style).
In the last commit step, we erase all registered inverse operations.
As said above, in the current formulation, a transaction can only reach the end (and thus commit) if it doesn't encounter conflicts. The transaction won't fail or retry. It can only happen that the transaction is suspended, possibly indefinitely.
To avoid 'cyclic suspension' deadlocks, the 'transactional boosting' approach uses a time-out to actually fail a transaction. In case of failure, we need to remove the transaction's method calls
fail(t) \ addI(t,_,_) = return ()
fail(t) \ addS(t,_,_) = return ()
fail(t) = return ()
and we execute the registered inverse operations. Then, the transaction is started from scratch.
Where to go next
The above description is not necessarily meant to be used in an efficient implementation. However, I believe that the use of join patterns allows us to to give a nice declarative specification of 'transactional boosting' and its underlying protocols. I will be interesting to consider alternative 'boosting' protocols. It appears that in general the 'boosting' approach can only support pessimistic concurrency. Optimistic concurrency requires that a transaction only commits its updates only after no conflicts have been detected.
In my experience, transactional boosting and optimistic concurrency only works out for some specific cases, eg the multi-set rewrite stuff I mentioned in my earlier 'Transactional Boosting' post.
Anyway, there's still lots to discover. Guess that's something for a future post.
Sunday, 16 November 2008
Transactional boosting
This post is about software transactional memory (STM) and how to retain its benefits (composability) while trying to minimize its drawbacks (poor performance due to false conflicts).
Software transactional memory (STM) is a concurrency control mechanism analogous to database transactions for controlling access to shared memory in concurrent computing (wikipedia). Below is a simple example of a concurrent, unordered singly-linked list using STM as supported by GHC Haskell.
The straightforward definitions of the linked list operations are left out. They are all executed within the STM monad which will guarantee that the operation is executed atomically, i.e. to its full extent or not at all which means in the programm language setting that we re-run (aka rollback/retry) the operation.
In Haskell, we can easily build 'bigger' STM operations by gluing together 'smaller' STM operations. For example, the transaction checks if elements 3 and 4 are present in the list and then will delete both elements. The entire transaction is executed atomically which guarantees that in case we return True, elements 3 and 4 were present but have now been deleted. Neat!
The benefits of STM over say locks are well documented. However, STM has (often) a significant performance disadvantage. Our (naive) STM implementation will protect the entire list. Suppose that elements 3 and 4 are stored towards the tail of the list. Hence, we (almost) need to traverse the entire list which then potentially leads to false conflicts with other concurrent STM operations. The effect is that many concurrent STM operations will be serialized (i.e.~sequential instead of parallel execution).
I recently wrote a paper with the above title to be presented at DAMP'09, in collaboration with Simon Marlow and Edmund Lam. Our results show that the naive STM implementation is no match against more fine-tuned implementations which
Please check the paper for the details.
The (well-known) downside of this more efficient singly-linked operations (efficient in the sense they enjoy a higher degree of concurrency) is that they are not composable anymore. That is, it is non-trivial to implement the above transaction (atomically find and delete 3 and 4) using the more efficient implementations.
Maurice Herlihy and Eric Koskinen wrote two recent papers on a topic they refer to as transactional boosting: How to recover the 'high-level' benefits of STM while relying on 'low-level', highly concurrent data-structures.
The papers are (see Eric's website):
My understanding of how the transactional boosting approach meant to work is that
It seems that the transactional boosting approach assumes pessimistic concurrency. I'm still not clear about the exact details of the approach but it looks definitely very promising.
Incidentally, I ran across the issue of transactional boosting in my own work on concurrent execution of multi-set rewrite rules.
Below are simple examples of (monomorphic for simplicity) multi-set rewrite rules.
Right-hand sides are omitted because they don't matter here.
Multi-set rewrite rules operate on a store, a multi-set of elements. We can concurrently apply multi-set rewrite rules if they operate on non-conflict parts of the store. Suppose, we have the store
Then, the first rule can be applied on (the first) A and B and the second rule can be
applied on (the second A) and C. There's no conflict. Hence, both rules can be applied concurrently.
The point is that the store is implemented as a concurrent data-structure and execution of a rewrite rule can be viewed as an STM transaction. For example, the operational interpretation of the first rule is
The first implementation of concurrent multi-set rewrite rules, in collaboration with Edmund Lam (my PhD student btw), presented here
used a (naive) STM list to implement the store. Our experiments confirm that such an approach won't scale. Due to a high(ly likely) number of false conflicts, multi-set rewrite rules are executed sequentially, though, we ought to execute them in parallel.
Our latest implementation, presented here
uses a more low-level, 'more concurrent' data-structure which is *not* composable. Hence, we had to implement our own STM protocol on top of the low-level data-structure (The PPDP paper is a bit unclear about this but we'll present what we've achieved in its full glory in a forth-coming journal submission soon).
STM is great but it often has poor performance. There are many applications where we wish to have a 'transactional boosting' approach. As far as I can tell, the approach laid out by Maurice Herlihy and Eric Koskinen is fairly different from the approach we used for concurrent execution of multi-set rewrite rules. Possibly, there's some unifying theory but I have the feeling that transactional boosting relies on some domain-specific assumption. Anyway, interesting times with many interesting topics. I'm sure there' more to say about transactional boosting.
Software transactional memory: Composability and false conflicts
Software transactional memory (STM) is a concurrency control mechanism analogous to database transactions for controlling access to shared memory in concurrent computing (wikipedia). Below is a simple example of a concurrent, unordered singly-linked list using STM as supported by GHC Haskell.
date List a = Node {val :: a, next :: TVar a}
| Nil
insert :: TVar a -> a -> STM ()
find :: TVar a -> a -> STM Bool
-- True = present, False = absent
delete :: TVar a -> a -> STM Bool
-- True = present and deleted, False = absent
-- atomically delete 3 and 4 if present
transaction :: TVar a -> IO Bool
transaction root = atomically $ do
b1 <- find root 3
b2 <- find root 4
if b1 && b2 then do
delete root 3
delete root 4
else return False
The straightforward definitions of the linked list operations are left out. They are all executed within the STM monad which will guarantee that the operation is executed atomically, i.e. to its full extent or not at all which means in the programm language setting that we re-run (aka rollback/retry) the operation.
In Haskell, we can easily build 'bigger' STM operations by gluing together 'smaller' STM operations. For example, the transaction checks if elements 3 and 4 are present in the list and then will delete both elements. The entire transaction is executed atomically which guarantees that in case we return True, elements 3 and 4 were present but have now been deleted. Neat!
The benefits of STM over say locks are well documented. However, STM has (often) a significant performance disadvantage. Our (naive) STM implementation will protect the entire list. Suppose that elements 3 and 4 are stored towards the tail of the list. Hence, we (almost) need to traverse the entire list which then potentially leads to false conflicts with other concurrent STM operations. The effect is that many concurrent STM operations will be serialized (i.e.~sequential instead of parallel execution).
Comparing concurrent linked-list implementations in Haskell
I recently wrote a paper with the above title to be presented at DAMP'09, in collaboration with Simon Marlow and Edmund Lam. Our results show that the naive STM implementation is no match against more fine-tuned implementations which
- either side-step the STM protocol (only each node operation is performed within the STM)
- employ lock-coupling via Haskell's MVars, or
- rely on atomic compare-and-swap.
Please check the paper for the details.
The (well-known) downside of this more efficient singly-linked operations (efficient in the sense they enjoy a higher degree of concurrency) is that they are not composable anymore. That is, it is non-trivial to implement the above transaction (atomically find and delete 3 and 4) using the more efficient implementations.
Transactional boosting
Maurice Herlihy and Eric Koskinen wrote two recent papers on a topic they refer to as transactional boosting: How to recover the 'high-level' benefits of STM while relying on 'low-level', highly concurrent data-structures.
The papers are (see Eric's website):
- Transactional Boosting: A Methodology for Highly-Concurrent Transactional Objects
M. Herlihy, E. Koskinen. PPoPP 2008
- Aggressive Transactional Boosting
E. Koskinen, M. Herlihy.
Under submission. August 2008.
My understanding of how the transactional boosting approach meant to work is that
- the user needs to verify if primitive operations 'commute', otherwise
- the operands of (non-commuting) operations will be protected by an abstract lock,
- each operations requires an inverse which will be executed if the transaction fails to commit.
It seems that the transactional boosting approach assumes pessimistic concurrency. I'm still not clear about the exact details of the approach but it looks definitely very promising.
Incidentally, I ran across the issue of transactional boosting in my own work on concurrent execution of multi-set rewrite rules.
Multi-set rewriting and transactional boosting
Below are simple examples of (monomorphic for simplicity) multi-set rewrite rules.
Right-hand sides are omitted because they don't matter here.
A, B <==> ...
A, C <==> ...
Multi-set rewrite rules operate on a store, a multi-set of elements. We can concurrently apply multi-set rewrite rules if they operate on non-conflict parts of the store. Suppose, we have the store
{A, A, B, C}
Then, the first rule can be applied on (the first) A and B and the second rule can be
applied on (the second A) and C. There's no conflict. Hence, both rules can be applied concurrently.
The point is that the store is implemented as a concurrent data-structure and execution of a rewrite rule can be viewed as an STM transaction. For example, the operational interpretation of the first rule is
atomically $ do
find A
find B
if both present
then do delete A
delete B
else return ()
The first implementation of concurrent multi-set rewrite rules, in collaboration with Edmund Lam (my PhD student btw), presented here
Edmund S. L. Lam, Martin Sulzmann:
A concurrent constraint handling rules implementation
in Haskell with software transactional memory. DAMP 2007:
used a (naive) STM list to implement the store. Our experiments confirm that such an approach won't scale. Due to a high(ly likely) number of false conflicts, multi-set rewrite rules are executed sequentially, though, we ought to execute them in parallel.
Our latest implementation, presented here
Martin Sulzmann, Edmund S. L. Lam:
Parallel execution of multi-set constraint rewrite
rules. PPDP 2008
uses a more low-level, 'more concurrent' data-structure which is *not* composable. Hence, we had to implement our own STM protocol on top of the low-level data-structure (The PPDP paper is a bit unclear about this but we'll present what we've achieved in its full glory in a forth-coming journal submission soon).
Summary
STM is great but it often has poor performance. There are many applications where we wish to have a 'transactional boosting' approach. As far as I can tell, the approach laid out by Maurice Herlihy and Eric Koskinen is fairly different from the approach we used for concurrent execution of multi-set rewrite rules. Possibly, there's some unifying theory but I have the feeling that transactional boosting relies on some domain-specific assumption. Anyway, interesting times with many interesting topics. I'm sure there' more to say about transactional boosting.
Wednesday, 12 November 2008
Actor versus Join Concurrency
This post tries to shed some light on the differences and commonalities between actor and join style concurrency and explains its connection to multi-set rewrite rules.
Recently, I've published two libraries supporting
Both libraries support similar forms of coordination primitives in terms of multi-set rewrite rules with guards. For example, consider
which says that if there's a seller and a buyer where both agree on the object x to be sold, then we execute the right-hand side "do something".
What's the connection to rewrite rules? Well, in case there's "Seller Obj" and "Buyer Obj", both will be rewritten to "do something". It's natural to view sellers and buyers as resources. To rewrite multiple resources, we simply use multi-set rewrite rules. For example,
will remove two occurences of "A" by "blah".
Lesson learned so far. The basic coordination primitives behind actor and join style concurrency are expressed in terms of multi-set rewrite rules. In the join setting, these multi-set rewrite rules are commonly referred to as join-patterns. However, please take note that Erlang-style actors only support single-headed rewrite rules and join-style concurrency as found in JoCaml, Polyphonic C or Claudio Russo's Joins librariy does not support guards (both features are supported by the above mentioned libaries).
Assuming we agree on a common set of multi-set rewrite rules (possibly with guards), what's the difference then between actor and join concurrency?
In the actor setting, we commonly assume that multi-set rewrite are applied sequentially. In the special case of Erlang's single-headed rewrite rules, we start scanning the mailbox (that's the place where sellers, buyers etc are stored) from left to right. For each mailbox element (often referred to as message aka method or even constraint in the rewrite setting), we then try the single-headed rewrite rules from top to bottom, until a match is found. In the general case of multi-set (headed) rewrite rules, we can assume that things can get a bit more tricky. Check out the paper below for a formal sequential execution semantics
But if rewrite rules are executed sequentially where does concurrency come in? Well, we can have concurrent actors which communicate by sending each other messages (aka methods or constraints). The messages itself are processed and executed sequentially by each actor. You may therefore argue that the behavior of each actor is completely deterministic.
In the join setting, the place where methods (aka messages or constraints) are kept is commonly referred to as a "store". Any multi-set rewrite rule can fire as soon as we find a match for its left-hand side among the st of stored methods. The only condition is that if two rewrite rules fire concurrently, they must operate on non-overlapping parts.
Both styles of concurrency use the same coordination primitive, i.e. multi-set rewrite rules. I'd argue that actor and join concurrency serve different purposes (hence, are equally useful). One can emulate the other but I prefer to have efficient support for both of them (not via emulation).
NOTE: I wrote this post are seeing these comments on reddit.com:
So, having a blog is possibly useful after all :)
Recently, I've published two libraries supporting
Coordination via multi-set rewrite rules with guards
Both libraries support similar forms of coordination primitives in terms of multi-set rewrite rules with guards. For example, consider
Seller x, Buyer x --> "do something"
which says that if there's a seller and a buyer where both agree on the object x to be sold, then we execute the right-hand side "do something".
What's the connection to rewrite rules? Well, in case there's "Seller Obj" and "Buyer Obj", both will be rewritten to "do something". It's natural to view sellers and buyers as resources. To rewrite multiple resources, we simply use multi-set rewrite rules. For example,
A, A --> "blah"
will remove two occurences of "A" by "blah".
Lesson learned so far. The basic coordination primitives behind actor and join style concurrency are expressed in terms of multi-set rewrite rules. In the join setting, these multi-set rewrite rules are commonly referred to as join-patterns. However, please take note that Erlang-style actors only support single-headed rewrite rules and join-style concurrency as found in JoCaml, Polyphonic C or Claudio Russo's Joins librariy does not support guards (both features are supported by the above mentioned libaries).
Assuming we agree on a common set of multi-set rewrite rules (possibly with guards), what's the difference then between actor and join concurrency?
Actor concurrency
In the actor setting, we commonly assume that multi-set rewrite are applied sequentially. In the special case of Erlang's single-headed rewrite rules, we start scanning the mailbox (that's the place where sellers, buyers etc are stored) from left to right. For each mailbox element (often referred to as message aka method or even constraint in the rewrite setting), we then try the single-headed rewrite rules from top to bottom, until a match is found. In the general case of multi-set (headed) rewrite rules, we can assume that things can get a bit more tricky. Check out the paper below for a formal sequential execution semantics
Martin Sulzmann, Edmund S. L. Lam, Peter Van Weert,
Actors with Multi-headed Message Receive Patterns.
COORDINATION 2008
But if rewrite rules are executed sequentially where does concurrency come in? Well, we can have concurrent actors which communicate by sending each other messages (aka methods or constraints). The messages itself are processed and executed sequentially by each actor. You may therefore argue that the behavior of each actor is completely deterministic.
Join concurrency
In the join setting, the place where methods (aka messages or constraints) are kept is commonly referred to as a "store". Any multi-set rewrite rule can fire as soon as we find a match for its left-hand side among the st of stored methods. The only condition is that if two rewrite rules fire concurrently, they must operate on non-overlapping parts.
Summary
Both styles of concurrency use the same coordination primitive, i.e. multi-set rewrite rules. I'd argue that actor and join concurrency serve different purposes (hence, are equally useful). One can emulate the other but I prefer to have efficient support for both of them (not via emulation).
NOTE: I wrote this post are seeing these comments on reddit.com:
- Actor model concurrency for Haskell
- Multi-set rewrite rules with guards and a parallel execution scheme
So, having a blog is possibly useful after all :)
The BaggerProblem
Description
There are n number of bags which can be filled up with either large, medium or small items. The weight of items of a specific kind is fixed. The maximum weight carried by a bag is fixed.
Bags are filled up with items in a fixed order:
- 1. In sequential order from lowest to highest bag number
- 2. Exhaustively fill up the bag first with
- (a) large items, then
- (b) medium items, then
- (c) small items.
- (a) large items, then
The straightforward solution is to
- 1. Fill up bags with large items, then
- 2. with medium items, and then finally with
- 3. small items.
However, once a bag has been exhaustively filled up with large items (we either stop because the bag reached its maximum capacity of large items, or we're simply running out of large items), we can start filling up this bag with medium items. The point is that we don't have to wait until all bags are exhaustively filled up with large items.
This form of concurrency has clear connection to instruction pipelining. What we want to show here is how to come up with a concurrent solution to the bagger problem
We'll give two solutions:
- a solution using join-patterns extended with guards,
- from which we can easily derive a more 'elementary' solution using standard synchronization primitives such as Software Transactional Memory (STM).
Solution using Join extended with guards
The join-calculus (and languages implementing join-patterns) doesn't support guards. Hence, we make use of our join extension which supports guards. The guards we use here are in fact implicit (shared variables). Here we go:
The methods we introduce are:
Bag(kind,no,content) denotes a bag which
- currently expects to be filled with items of kind 'kind'
- no is the bags number
- content refers to the current content
Initially, all bags are of the form
Bag(Large,i,Empty)
Item(k) denotes an item of kind 'kind'
The above methods are all asynchronous.
We introduce two synchronous methods.
Iterator(kind,no) fills up bag number no with items of kind 'kind'.
Initially, there are three 'iterators':
- Iterator(Large,1)
- Iterator(Medium,1)
- Iterator(Small,1)
Each will run in its own thread. Each starts in 'Large' mode.
That is, only the large iterator can fill up the bags (sequentially).
Once the large iterator is done with bag number i, the bag is
'unlocked' by moving from 'Large' to 'Medium' mode and so on.
GetItem(kind,r) looks for an item of kind 'kind', the outcome
is reported in r of type Maybe Weight.
Here are the join patterns and their bodies.
(We assume that join patterns are executed from top to bottom,
for convenience only)
Bag(kind,no,content) & Iterator(kind,no) =
if (weight content) + (weight kind) >= maxBagWeight
then do bag (next kind) no content
if no < MaxBagNo
then iterator kind (no+1)
else return ()
else do
r <- getItem k
case r of
Nothing -> do
bag (next kind) no content
if no < MaxBagNo -- (***)
then iterator kind (no+1)
else return ()
Just itemWeight -> do
bag kind no (add content itemWeight)
iterator kind no
Item(k) & GetItem(k,x) = case k of
Large -> x := Just Large
...
GetItem(k,x) = x:= Nothing
NOTE:
First, I thought we could replace (***) by the 'default' rule
Iterator(kind, no) = return ()
which we put *after* the first rule.
However, this won't work because the 'small' iterator waiting for
the medium and large iterator may terminate prematurely.
A concrete implementation of the above can be found
here as part of the multisetrewrite library.
Elementary solution in Haskell using STM
> import IO
> import Data.IORef
> import Control.Concurrent
> import Control.Concurrent.STM
> import Control.Concurrent.Chan
We set up the item space by storing large, medium and small
items into their respective list. For each kind of items,
there's at most one thread trying to access the items.
Hence, using IORefs is fine.
> data ItemSpace = IS { large :: IORef [()]
> , medium :: IORef [()]
> , small :: IORef [()] }
We only store () values, the weights are fixed.
> largeWeight = 6
> mediumWeight = 4
> smallWeight = 2
The kind of items we support are either large, medium or small.
Done is a "dummy" item. We'll move from large to medium to small items.
Done simply indicates that we are done.
> data Item = Large | Medium | Small | Done deriving (Eq, Show)
> next :: Item -> Item
> next Large = Medium
> next Medium = Small
> next Small = Done
> itemWeight :: Item -> Int
> itemWeight Large = largeWeight
> itemWeight Medium = mediumWeight
> itemWeight Small = smallWeight
The procedure to fetch items. There may be concurrent threads
accessing either large, medium or small items. But there's
at most one thread for each kind.
> fetch :: ItemSpace -> Item -> IO (Maybe ())
> fetch is kind =
> let get m = do
> l <- readIORef m
> case l of
> (x:xs) -> do writeIORef m xs
> return (Just x)
> [] -> return Nothing
> in case kind of
> Large -> get (large is)
> Medium -> get (medium is)
> Small -> get (small is)
Each bag records its current weight and content.
The mode tells us which kind of items are currently allowed to
be put into the bag. The mode is protected by a TVar which allows us
to suspend until the large items are exhaustively put into the bag.
> data Bag = Bag { mode :: TVar Item
> , curWeight :: IORef Int
> , content :: IORef [Item] }
> printBag :: Bag -> IO ()
> printBag bag = do
> w <- readIORef (curWeight bag)
> c <- readIORef (content bag)
> putStrLn $ (show (w,c))
The maximum weight held by each bag is fixed.
> maxBagWeight = 16
We add an item to a bag by incrementing the bags weight
plus updating the content.
> add :: Bag -> Item -> IO ()
> add bag kind = do
> w <- readIORef (curWeight bag)
> c <- readIORef (content bag)
> writeIORef (curWeight bag) (w + itemWeight kind)
> writeIORef (content bag) (kind : c)
We check if a bag becomes full (over-weight) if we would add
another item.
> bagIsFull :: Bag -> Item -> IO (Bool)
> bagIsFull bag kind = do
> w <- readIORef (curWeight bag)
> return ((w + itemWeight kind) > maxBagWeight)
fillBag fills up (exhaustively) a bag with items of a given kind.
We 'unlock' the bag by 'incrementing' the mode if
- the bag is full
- no more items of this kind are left
> incrementMode :: Bag -> IO ()
> incrementMode bag =
> atomically $ do status <- readTVar (mode bag)
> writeTVar (mode bag) (next status)
> fillBag :: ItemSpace -> Bag -> Item -> IO ()
> fillBag is bag Done = error "not happening here"
> fillBag is bag kind =
> let loop = do
> b <- bagIsFull bag kind
> if b then incrementMode bag
> else do
> r <- fetch is kind
> case r of
> Nothing -> incrementMode bag
> Just _ -> do add bag kind
> loop
> in loop
We process (ie fill up) the list of bags sequentially.
For each bag we must wait untill its our turn.
The priorities are
large > medium > small
> waitMode :: Bag -> Item -> IO ()
> waitMode bag kind =
> atomically $ do status <- readTVar (mode bag)
> if status == kind then return ()
> else retry
> processBags :: ItemSpace -> Item -> [Bag] -> IO ()
> processBags is kind bs =
> mapM_ (\b -> do waitMode b kind
> fillBag is b kind) bs
For each kind we spawn a thread to fill up the list of bags.
> start :: ItemSpace -> [Bag] -> IO ()
> start is bs = do
> cnt <- atomically $ newTVar 0
> let spawn = \kind -> forkIO (do processBags is kind bs
> atomically $ do v <- readTVar cnt
> writeTVar cnt (v+1))
> spawn Large
> spawn Medium
> spawn Small
> atomically $ do v <- readTVar cnt
> if v == 3 then return ()
> else retry
testing
> createIS ln mn sn = do
> l <- newIORef [ () | x <- [1..ln]]
> m <- newIORef [ () | x <- [1..mn]]
> s <- newIORef [ () | x <- [1..sn]]
> return (IS {large = l, medium = m, small = s})
> emptyBag = do
> m <- atomically $ newTVar Large
> w <- newIORef 0
> c <- newIORef []
> return Bag {mode = m, curWeight = w, content = c}
> test largeNo medNo smallNo bagNo = do
> is <- createIS largeNo medNo smallNo
> bs <- mapM (\_ -> emptyBag) [1..bagNo]
> mapM_ (\b -> printBag b) bs
> putStrLn "Start"
> start is bs
> putStrLn "Done"
> mapM_ (\b -> printBag b) bs
Some observations
The STM solution can be improved. The thread filling up bags with large items doesn't need to check the status of the bag and the thread filling up small items only needs to be waken up once the 'medium' thread is done. We could achieve this behavior by replacing
mode :: TVar Item
with
mode1 :: TVar Item
mode2 :: TVar Item
That is, the 'medium' thread retries on mode1 and the 'small' thread retries on mode2.
In the join solution none of these optimizations are necessary, they are dealt with implicitly. For example, if Iterator(Small,someNo) is unable to fire a join-pattern, this method will be suspended (i.e. the method is put into the store). If the mode of a bag finally switches to small, this active bag will then in combination with the inactive (ie suspended) Iterator(Small,someNo) trigger the join-pattern.
Wednesday, 5 November 2008
From Join to UPPAAL and back
I'm currently teaching a course using UPPAAL for modelling and anlysis of communicating FAs (finite automatas). In this post, I will show some interesting connections between communicating FAs and coordination patters as found in the Join calculus (referred to as Join for brevity).
For concreteness, let's consider a (classic) coordination example: The 'bridge' problem. We have four soldiers on the left (unsafe) side of the bridge. They'd like to cross the bridge to get to the right (safe) side. The problem is it's at night and they need a torch to cross the bridge. The torch can carry a maximum of two soliders. We assume that the torch always carries two soliders from right to left and only solider goes back (left to right).
In Join, we can specify/model this problem as follows. We introduce synchronous methods 'take', 'release' and 'takeBack' to model the actions. We introduce asynchronous methods 'free', 'one', 'two', 'oneLeft', 'rightSide' and 'oneFrom' to represent the states of the torch and 'unsafe(i)', 'towards(i)', 'safe(i)' and 'back(i)' to represent the states of soldier i. Their meaning will become clear once see the join-patterns describing the interaction between torch and soldiers.
The behavior of the torch is specified via the following join-patterns (using Haskell-style syntax).
Of course, we could have unfolded the above definitions into the following (and thus omitting the intermediate states)
This makes it even clearer that the torch waits for two soldiers to grab the torch. Then, the torch (with the soldiers) crosses the bridge (this is implicit). The torch releases both soliders and the torch will take back a soldier and release this soldier on the unsafe side again. The more verbose representation (using the intermediate states) will be useful later when discussing the connection to communicating FAs.
We yet need to model the behavior of solider(i). We finally make use of some multi-headed join-patterns.
For example, the first join-pattern above says that if solider i is in the unsafe state and we can take the torch, then we unblock the caller of take (remember that take is synchronous) and we issue a new asynchronous method call towards(i). The semantics of join-pattern is actually fairly simply. In essence, multi-set rewriting where the methods are treated as resources. The multisetrewrite library introduced in a previous post, can easily encode join-patterns (and even more, eg guards etc).
I will release some runnable code at some later stage.
The point of this exercise is not to show what can be done with Join, rather, we want to establish some connections to communicating FAs. So, what's the connection? In Join, a join-pattern is triggered (aka executed) if we can match the pattern head with the specified method calls. In communicating FAs, two automatas 'communicate' if we find matching send (!) and receive (?) transitions.
Each component of the tuple corresponds to the states of a communicating FA (CFA). If one CFA has a send edge (a!) which matches the receiving edge (a?) of another CFA, then we make a transition along those edges as shown in the above diagram. This smells similar to Join, right? Indeed, in Join we can represent
by
and
by
The states are turned into asynchronous method calls and the actions 'a' are turned into synchronous method calls.
In fact, the Join program shown above was derived from the following CFAs
using this translation scheme.
The torch CFA:
Torch
The soldier CFA:
Soldier 3
It's also possible to systematically translate Join programs to CFAs but it's getting more tedious to work out the details. Both languages are equally expressive. However, (I claim) Join allows us to specify more complex coordination patterns more easily than CFAs (therefore the transformation to CFAs gets quite involved). The advantages of having a Join representation of CFAs is that we know how to efficiently execute Join programs (eg see the multisetrewrite library which exploits join-style concurrency by executing non-overlapping join-patterns in parallel). On the other hand, a CFA representation of Join allows to make use of UPPAAL's expressive query language and its model checking facilities. For example, via the query
we can check if (assuming we have four soldiers) it's possible for all four soldiers to reach the safe side. E says there exists a trace and <> says there exists a state.
We can also check if the system does not deadlock
This property is not satisfied for the following reason. In case all four soldiers are on the safe side and one solider makes its way back to the unsafe side, the soldier gets to the unsafe side but won't be able to get back to the safe side. Remember that in our torch model, we require two soldiers per torch. For this example at least, the deadlock property doesn't say much. We only know that the program will terminate (possibly in some undesired state).
UPPAAL's query language is a subset of CTL btw. This implies that we canNOT verify (very compliated) queries such as "are the join-patterns confluent". Confluence requires to quantify over traces, then over states and then again over traces which is beyond CTL (for good reasons because it gets way too complex to check such properties).
Anyway, the connection between Join and CFAs is quite useful. This way I became a much better UPPAAL user. First write your program in Join and then convert to CFAs. I will write more about this connection at some later stage.
For concreteness, let's consider a (classic) coordination example: The 'bridge' problem. We have four soldiers on the left (unsafe) side of the bridge. They'd like to cross the bridge to get to the right (safe) side. The problem is it's at night and they need a torch to cross the bridge. The torch can carry a maximum of two soliders. We assume that the torch always carries two soliders from right to left and only solider goes back (left to right).
In Join, we can specify/model this problem as follows. We introduce synchronous methods 'take', 'release' and 'takeBack' to model the actions. We introduce asynchronous methods 'free', 'one', 'two', 'oneLeft', 'rightSide' and 'oneFrom' to represent the states of the torch and 'unsafe(i)', 'towards(i)', 'safe(i)' and 'back(i)' to represent the states of soldier i. Their meaning will become clear once see the join-patterns describing the interaction between torch and soldiers.
The behavior of the torch is specified via the following join-patterns (using Haskell-style syntax).
free = do take
one
one = do take
two
two = do release
oneLeft
oneLeft = do release
rightSide
rightSide = do takeBack
oneFrom
oneFrom = do release
free
Of course, we could have unfolded the above definitions into the following (and thus omitting the intermediate states)
free = do take
take
release
release
takeBack
release
free
This makes it even clearer that the torch waits for two soldiers to grab the torch. Then, the torch (with the soldiers) crosses the bridge (this is implicit). The torch releases both soliders and the torch will take back a soldier and release this soldier on the unsafe side again. The more verbose representation (using the intermediate states) will be useful later when discussing the connection to communicating FAs.
We yet need to model the behavior of solider(i). We finally make use of some multi-headed join-patterns.
unsafe(i) & take = towards(i)
towards(i) & release = safe(i)
safe(i) & takeBack = back(i)
back(i) & release = unsafe(i)
For example, the first join-pattern above says that if solider i is in the unsafe state and we can take the torch, then we unblock the caller of take (remember that take is synchronous) and we issue a new asynchronous method call towards(i). The semantics of join-pattern is actually fairly simply. In essence, multi-set rewriting where the methods are treated as resources. The multisetrewrite library introduced in a previous post, can easily encode join-patterns (and even more, eg guards etc).
I will release some runnable code at some later stage.
The point of this exercise is not to show what can be done with Join, rather, we want to establish some connections to communicating FAs. So, what's the connection? In Join, a join-pattern is triggered (aka executed) if we can match the pattern head with the specified method calls. In communicating FAs, two automatas 'communicate' if we find matching send (!) and receive (?) transitions.
p --- a! --> q r --- a? --> t
-----------------------------------------
(p,r) --- a --> (q,t)
Each component of the tuple corresponds to the states of a communicating FA (CFA). If one CFA has a send edge (a!) which matches the receiving edge (a?) of another CFA, then we make a transition along those edges as shown in the above diagram. This smells similar to Join, right? Indeed, in Join we can represent
p --- a! --> q
by
p = do a
q
and
p --- a? --> q
by
p & a = q
The states are turned into asynchronous method calls and the actions 'a' are turned into synchronous method calls.
In fact, the Join program shown above was derived from the following CFAs
using this translation scheme.
The torch CFA:
Torch
Get your own at Scribd or explore others:
The soldier CFA:
Soldier 3
Get your own at Scribd or explore others:
It's also possible to systematically translate Join programs to CFAs but it's getting more tedious to work out the details. Both languages are equally expressive. However, (I claim) Join allows us to specify more complex coordination patterns more easily than CFAs (therefore the transformation to CFAs gets quite involved). The advantages of having a Join representation of CFAs is that we know how to efficiently execute Join programs (eg see the multisetrewrite library which exploits join-style concurrency by executing non-overlapping join-patterns in parallel). On the other hand, a CFA representation of Join allows to make use of UPPAAL's expressive query language and its model checking facilities. For example, via the query
E<> safe(1) and safe(2) and safe(3) and safe(4)
we can check if (assuming we have four soldiers) it's possible for all four soldiers to reach the safe side. E says there exists a trace and <> says there exists a state.
We can also check if the system does not deadlock
A[] not deadlock
This property is not satisfied for the following reason. In case all four soldiers are on the safe side and one solider makes its way back to the unsafe side, the soldier gets to the unsafe side but won't be able to get back to the safe side. Remember that in our torch model, we require two soldiers per torch. For this example at least, the deadlock property doesn't say much. We only know that the program will terminate (possibly in some undesired state).
UPPAAL's query language is a subset of CTL btw. This implies that we canNOT verify (very compliated) queries such as "are the join-patterns confluent". Confluence requires to quantify over traces, then over states and then again over traces which is beyond CTL (for good reasons because it gets way too complex to check such properties).
Anyway, the connection between Join and CFAs is quite useful. This way I became a much better UPPAAL user. First write your program in Join and then convert to CFAs. I will write more about this connection at some later stage.
Tuesday, 28 October 2008
Multi-set rewrite rules with guards and a parallel execution scheme
Latest news/updates
- Sat Dec 6 18:34:20 CET 2008:
- Parallel join pattern with guards and propagation extension built on top of multisetrewrite.
- Check here here for more information.
- Parallel join pattern with guards and propagation extension built on top of multisetrewrite.
- Wed Nov 12 11:08:47 CET 2008:
New multisetrewrite-0.1.1 version uploaded to hackage
- Includes more examples, a CHRSolver.hs and Join.hs abstraction
built on top of multi-set rewrite
- Some fun examples using these abstractions: GossipingGirls and BaggerProblem.
Brief description
We provide a library for multi-set rewrite rules with guards. Rewrite rules are executed concurrently as long as they operate on non-overlapping left-hand sides. We make use of highly-concurrent, non-blocking data structures based on CAS lists. Thus, we can parallelize concurrent rule executions on a multi-core architecture.
The library is similar in style to the below described actor library. The difference is that while actors run concurrently, their receive clauses (sort of multi-set rewrite rules) are only executed sequentially.
Download
The multisetrewrite library is implemented in Haskell and available
via
http://hackage.haskell.org
(look for the multisetrewrite library among the Concurrency packages)
Examples
The library comes with two examples (will hopefully increase over time).
Concurrent stack
The gist of the multi-set rewrite rules describing a concurrent stack (the actual example in Stack.hs is more verbose, after all it's 'only' a library and not
a new compiler).
[push x, pop y] .->. y := x
[push x, stack s] .->. stack (x:s)
[pop y, stack s] `when` (isNotEmptyStack s) .->. let (x:xs) = s
y := x
stack xs
push is synchronous whereas pop and stack are asynchronous. The above shows how to encode join-patterns via multisetrewrite. We are more expressive than join-patterns because we also support guards, non-linear (aka shared) variables (doesn't show up in the above).
CHR solver
On top of multisetrewrite we implement a CHR solver. See CHR.hs in the distribution.
To illustrate the expressive power, we implement the mergesort algorithm
via multi-set rewrite rules.
Here's the gist of the rules (as said above already, the actual implementation is more verbose).
Leq(x,a) \ Leq(x,b) when a < b <==> Leq(a,b)
Merge(n,a), Merge(n,b) when a < b <==> \Leq(a,b),\Merge(n+1,a)
Points to note:
- The right-hand side of the first rule uses a mix of propagation and simplification. Leq(x,a) is propagated (ie not removed) whereas Leq(x,b) is simplified.
- We make use of non-linear variables and guards in both rules.
Monday, 20 October 2008
Actors with Multi-Headed Receive Clauses
The actor model provides high-level concurrency abstractions to coordinate simultaneous computations by message passing. Languages implementing the actor model such as Erlang commonly only support single-headed pattern matching over received messages.
In
we propose an extension of the Actor model with receive clauses supporting multi-headed message patterns.
Here's a simple example of a market-place actor
We employ the combination of multiple messages in a receive pattern and non-linear patterns to test for a matching seller and a buyer. Non-linear patterns are in fact a short-hand for guards. That is, the above is equivalent to
The formal details of a such an enriched actor model are described in the above mentioned paper. We have also implemented the system as a library extension in Haskell. More on this below.
Available via
http://hackage.haskell.org
(look for the actor library among the Concurrency packages)
The Haskell-Actor implementation makes use of
Haskell channels provide the basic abstraction to write (send) and read (receive) from a channel (mailbox). Thus, we can straightforwardly model actors with *single-headed* receive clauses. That is, we read messages one at a time and check for the occurrence of a specific message. The novelty of Haskell-Actor mailboxes is that we can test for the ocurrence of multiple messages via *multi-headed* receive clauses (see the above market-place example).
Messages are user-definable via Haskell data types. The user needs to provide some boiler-plate code (type class instances) to define message pattern matching.
To use Haskell-Actor library you'll need
to understand the following combinators.
We'll discuss each of the above in turn.
receive is similar to case statements in Haskell. One difference is that we can match against multiple messages (see the above market-place actor).
Haskell doesn't allow us to overload the pattern matching syntax (it's a library extension). We solve this by providing (generic) primitives to implement multi-headed message pattern matching in receive clauses by providing a (generic) set of primitives which need to be extended by the user for the specific message type (described as a data type).
For example, consider the following simple message type found in the Chain.hs example
There are two things, the user needs to provide.
By providing the hash-map and the message-specific matcher, we can define an actor which waits for the 'Blah' message to arrive and then sends the same message to its neighbor.
NOTE: The receive statement is similar to case statements in Haskell. That is, we make explicit the actor/mailbox to which we apply a list of receive clauses. In Erlang, the actor/mailbox is implicit.
Given the pid (process identification number, similar to Erlang) we can send a message to an actor. For example,
toPID is a primitive which extracts the pid from the neighbor actor
creates a new actor for a specific message type, given
a hash-map. For example,
We spawn a new (Haskell) thread in which we apply the first argument (the actor) to the second argument (the behavior). For example,
where curr refers to the current actor and prev to the previous actor.
simply kills the thread (we don't kill any sub-actor threads, must be taken care of by the user).
The below examples are part of the distribution.
Creates some n number of actors which pass around some message.
The standard ping-pong actor example. Simply call the main function and see what's happening.
A market-place using server and client actors. Call the main function to invoke the server. To invoke a client open a new terminal and execute 'telnet localhost 4242' for connecting clients to the server. You'll be asked for your name (sent to the server and the server informs everybody about new clients) and what item you'd like to sell or buy. The server then checks for matching buyers and sellers.
This example uses pattern variables and multi-headed pattern receive clauses.
Pattern variable need to be created explicitly because we implement actors
(i.e. pattern matching over messages) as a library.
Here are some code snippets.
We explicitly create a pattern variable x which we then
use in the message pattern 'arrivedMsg x'.
To distinguish between values and variables we use 'lifted' types.
It's of course pretty clumsy to write down lifted types.
Here's a nicer (type class) interface.
In case of many different types of messages/constructors, this 'boilerplate' code is straightforward but tedious to write down. We should eventually look into Template Haskell (future work).
In
Martin Sulzmann, Edmund S. L. Lam, Peter Van Weert:
Actors with Multi-headed Message Receive Patterns.
COORDINATION 2008: 315-330
we propose an extension of the Actor model with receive clauses supporting multi-headed message patterns.
Here's a simple example of a market-place actor
receive
Seller x, Buyer x -> "match found"
We employ the combination of multiple messages in a receive pattern and non-linear patterns to test for a matching seller and a buyer. Non-linear patterns are in fact a short-hand for guards. That is, the above is equivalent to
receive
Seller x, Buyer y when x == y -> "match found"
The formal details of a such an enriched actor model are described in the above mentioned paper. We have also implemented the system as a library extension in Haskell. More on this below.
Haskell-Actor Implementation
Download
Available via
http://hackage.haskell.org
(look for the actor library among the Concurrency packages)
Overview
The Haskell-Actor implementation makes use of
- Haskell channels to represent the actors mailbox, and
- user-definable pattern matching implemented via type class overloading.
Haskell channels provide the basic abstraction to write (send) and read (receive) from a channel (mailbox). Thus, we can straightforwardly model actors with *single-headed* receive clauses. That is, we read messages one at a time and check for the occurrence of a specific message. The novelty of Haskell-Actor mailboxes is that we can test for the ocurrence of multiple messages via *multi-headed* receive clauses (see the above market-place example).
Messages are user-definable via Haskell data types. The user needs to provide some boiler-plate code (type class instances) to define message pattern matching.
Details
To use Haskell-Actor library you'll need
to understand the following combinators.
- receive
- send
- createActor
- runActor
- kill
We'll discuss each of the above in turn.
receive
receive is similar to case statements in Haskell. One difference is that we can match against multiple messages (see the above market-place actor).
Haskell doesn't allow us to overload the pattern matching syntax (it's a library extension). We solve this by providing (generic) primitives to implement multi-headed message pattern matching in receive clauses by providing a (generic) set of primitives which need to be extended by the user for the specific message type (described as a data type).
For example, consider the following simple message type found in the Chain.hs example
data Msg = Blah deriving (Eq,Show)
There are two things, the user needs to provide.
- Hash-map: Message are indexed based on their constructor names to speed up the search for matching message patterns.
valhashOp = HashOp { numberOfTables = 1, hashMsg = \ _ -> 1 } - Specific pattern matcher:
instance EMatch Msg where
match tags m1 m2 = return (m1 == m2, tags)
We extend the generic matcher by a message specific case.
By providing the hash-map and the message-specific matcher, we can define an actor which waits for the 'Blah' message to arrive and then sends the same message to its neighbor.
actorChain neighbor self =
receive self
[ [Blah] .->. send (toPID neighbor) Blah ]
NOTE: The receive statement is similar to case statements in Haskell. That is, we make explicit the actor/mailbox to which we apply a list of receive clauses. In Erlang, the actor/mailbox is implicit.
send
Given the pid (process identification number, similar to Erlang) we can send a message to an actor. For example,
send (toPID neighbor) Blah
toPID is a primitive which extracts the pid from the neighbor actor
createActor
createActor :: HashOp msg -> IO (Act msg)
creates a new actor for a specific message type, given
a hash-map. For example,
(initialActor :: Act Msg) <- createActor valhashOp
runActor
runActor :: Act msg -> (Act msg -> IO ()) -> IO ()
We spawn a new (Haskell) thread in which we apply the first argument (the actor) to the second argument (the behavior). For example,
runActor curr (actorChain prev)
where curr refers to the current actor and prev to the previous actor.
kill
kill :: PID msg -> IO ()
simply kills the thread (we don't kill any sub-actor threads, must be taken care of by the user).
Examples
The below examples are part of the distribution.
Chain.hs
Creates some n number of actors which pass around some message.
PingPong.hs
The standard ping-pong actor example. Simply call the main function and see what's happening.
MarketPlace.hs
A market-place using server and client actors. Call the main function to invoke the server. To invoke a client open a new terminal and execute 'telnet localhost 4242' for connecting clients to the server. You'll be asked for your name (sent to the server and the server informs everybody about new clients) and what item you'd like to sell or buy. The server then checks for matching buyers and sellers.
This example uses pattern variables and multi-headed pattern receive clauses.
Pattern variable need to be created explicitly because we implement actors
(i.e. pattern matching over messages) as a library.
Here are some code snippets.
; x <- newVar :: IO (VAR String)
; let go =
receive client
[ [arrivedMsg x] .->.
do { v1 <- readVar x
; hPutStrLn hdl ("\n Arrived: " ++ show v1)
; go
}
, ... ]
We explicitly create a pattern variable x which we then
use in the message pattern 'arrivedMsg x'.
To distinguish between values and variables we use 'lifted' types.
data L a = Val a
| Var (VAR a) deriving Eq
-- see ActorBase.hs for the internal variable representation
-- (only for the curious reader/user)
data MsgClient = Arrived (L String)
-- notifies about newly arrived clients
It's of course pretty clumsy to write down lifted types.
Here's a nicer (type class) interface.
-- client interface
class ArrivedMsg a where
arrivedMsg :: a -> MsgClient
instance ArrivedMsg (VAR String) where
arrivedMsg x = Arrived (Var x)
instance ArrivedMsg String where
arrivedMsg s = Arrived (Val s)
In case of many different types of messages/constructors, this 'boilerplate' code is straightforward but tedious to write down. We should eventually look into Template Haskell (future work).
Subscribe to:
Posts (Atom)