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).

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.