12 September 2015

Push/Pull for Transactions

A unified model for understanding many transactional systems.

There is little doubt about how one should write concurrent programs. Like in all programming, you must care about correctness first, efficiency second. If you care about correctness, you do not want to use compare-and-swap. You don't even want to use locks. What you want to use is atomic blocks. When you mark a piece of code as atomic, you effectively say, ‘I want to reason about the correctness of this code as if nothing runs concurrently’. Now it is up to the language implementor to ensure that the as if part holds. The part of the language implementation that is responsible for this is called a transactional system.

When the transactional system is implemented, there is a similar tension between correctness and efficiency. At one end of the spectrum, one could use a global lock that each atomic block must hold while executing. This is correct: Atomic blocks run as if nothing runs concurrently because nothing runs concurrently. (I am assuming that every statement in the program is in an atomic block: If a statement is not in an atomic block, then it is by default wrapped in a tiny atomic block, made just for it.) At the other end of the spectrum, you let everything run concurrently, and pray that there is no interference. This is really fast. (And incorrect, obviously.) Needless to say, no one wants an implementation at either end of the spectrum. But, crafting something in the middle seems like a dark art.

This dark art may not remain so dark for long. At least one recent paper aims to shed some light on it. The paper is [Koskinen, Parkinson, The Push/Pull Model of Transactions, PLDI 2015].

Here is how it works. We start with some underlying sequential language. It can be pretty much anything: We model its statements as relations on stores. Then we add a few concurrency features: fork, atomic, and operations on the shared state. (The latter are called methods in the paper.) Now we have a language for concurrent programming, and we can give it an operational semantics, which just encodes the intuitive idea that atomic blocks aren't interrupted by other threads. This is the reference semantics.

The second step is to compile a program with atomic blocks into one without. Instead of atomic blocks, we will use a small set of operations, the most important of which are push and pull. For this compilation to be correct, certain conditions need to hold. (These conditions appear in Figure 4b as assumptions. And, by the way, the paper does not describe this step as ‘compilation’. I do.)

And here's the bang.

As long as the compilation is correct, the program with push and pull is guaranteed to do the same as the given one, the one with atomic. This is a big deal because the correctness conditions in Figure 4b are fairly simple, and because they allow you to do rather weird-looking stuff.

Now let's step back. I described above my understanding of the paper and its claims. I think the idea is really cool and useful. But.

The paper did not convince me that the conditions in Figure 4b are sufficient. The authors know this: They repeatedly say that for lack of space they include only a proof sketch, and that their proof (from the technical report) needs to be checked mechanically in the future. (By the way, the idea of the proof is a bisimulation that doesn't observe the insides of atomic blocks.) On the one hand, I rather trust Erik and Matt. (Although my trust was slightly shaken when I saw that t in Figure 1 is unused. Just joking.) On the other hand, this kind of proof seems extremely brittle. The authors are right: a mechanically checked proof would be cool.

Now go see the paper for yourself: [Koskinen, Parkinson, The Push/Pull Model of Transactions, PLDI 2015].

No comments:

Post a Comment

Note: (1) You need to have third-party cookies enabled in order to comment on Blogger. (2) Better to copy your comment before hitting publish/preview. Blogger sometimes eats comments on the first try, but the second works. Crazy Blogger.