AUGUST2017 | VOL. 60 | NO. 8 | COMMUNICATIONS OF THE ACM 85
finish calculating a response, and it does not have to generate
responses in the order invocations were received.
An implementation M exhibits a history H if, when fed
H’s invocations at the appropriate times, M can produce H’s
responses (so that its external behavior equals H overall).
An implementation M is correct for a specification if M’s
responses always obey the specification. This means that
every history exhibited by M is either in , or contains some
3. 2. Commutativity
SIM commutativity, which we define here, aims to capture state
dependence at the interface level. State dependence means SIM
commutativity must capture when operations commute in some
states, even if those same operations do not commute in other
states; however, we wish to capture this contextually, without
reference to any particular implementation’s state. To reason
about possible implementations, we must capture the scalability inherent in the interface itself. This in turn makes it possible
to use the scalable commutativity rule early in software development, during interface design and initial implementation.
Commutativity states that actions may be reordered without affecting eventual results. We say a history H′ is a
reordering of H when H|t = H′|t for every thread t. This allows actions
to be reordered across threads, but not within them. For
example, if H = [A1, B2, A− 1, C1, B− 2, C− 1], then [B2, B − 2, A1, A− 1, C1, C− 1]
is a reordering of H, but [B2, C1, B− 2, C− 1, A1, A− 1] is not, since it
does not respect the order of actions in H| 1.
Now, consider a history H = X Y (where concatenates
action sequences). We say Y SI-commutes in H when given any
reordering Y′ of Y, and any action sequence Z,
XYZ∈ if and only if XY′Z∈ .
This definition captures state dependence at the interface
level. The action sequence X puts the system into a specific
state, without specifying a representation of that state (which
would depend on an implementation). Switching regions Y
and Y′ requires that the exact responses in Y remain valid
according to the specification even if Y is reordered. The
presence of region Z in both histories requires that reorderings of actions in region Y cannot be distinguished by future
operations, which is an interface-based way of saying that Y
and Y′ leave the system in the same state.
Unfortunately, SI commutativity is not sufficient to prove the
scalable commutativity rule. To avoid certain degenerate cases,
we must further strengthen the definition of commutativity to
be monotonic (the M in SIM). An action sequence Y SIM-commutes
in a history H = X Y when for any prefix P of any reordering of
Y (including P = Y), P SI-commutes in X P. Equivalently,
Y SIM-commutes in H when, given any prefix P of any reordering of Y, any reordering P′ of P, and any action sequence Z,
XPZ∈ if and only if XP′Z∈ .
Both SI commutativity and SIM commutativity capture
state dependence and interface basis. Unlike SI commutativity, SIM commutativity excludes cases where the commutativity of a region changes depending on future operations.
SIM commutativity is what we need to state and prove the
scalable commutativity rule.
do not commute—the second creat call will fail. (Unless, that
is, one or more of the files already exists, in which case the
calls commute after all!) Special cases like this can dominate
analyses that use a strong notion of commutativity. If commutative operations had to commute in all contexts, then only
trivial systems operations could commute, and commutativity would not help us explore interface scalability.
Our work relies on a new definition of commutativity,
called SIM commutativity (State-dependent, Interface-based,
and Monotonic), that captures state- and context-dependence,
and conditional commutativity, independent of any implementation. SIM commutativity lets us prove the scalable
commutativity rule, which says that scalable implementations exist whenever operations commute. Even if an interface is commutative only in a restricted context, there exists
an implementation that scales in that context.
The rest of this section explains this formalism, gives
the rule precisely, and lays out some of its consequences for
3. 1. Specifications
We represent specifications using actions, where an action is
either an invocation (representing an operation call with arguments) or a response (representing the return value). Splitting
each operation into an invocation and a response lets us
model blocking interfaces and concurrent operations. 11 Each
invocation is made by a specific thread and the corresponding response is returned to the same thread. We will write
invocations as creat(“/x”) 1 and responses as , where an over-bar marks responses and subscript numbers are thread IDs.
A particular execution of a system is a history or trace,
which is just a sequence of actions. For example,
H = [A1, B3, C2, A− 1, C− 2, B− 3, D1, D− 1, E2, F3, G1, E − 2, G− 1, F− 3],
consists of seven invocations and seven corresponding responses
across three different threads. In a well-formed history, each
thread’s actions alternate invocations and responses, so each
thread has at most one outstanding invocation at any point. H
above is well-formed; for instance, in the thread-restricted sub-history H| 1 = [A1, A− 1, D1, D− 1, G1, G− 1], which selects 1’s actions
from H, invocations and responses alternate as expected.
A specification models an interface’s behavior as a set of
system histories—specifically, a prefix-closed set of well-formed histories. A system execution is “correct” according
to the specification if its trace is included in the specification. For instance, if corresponded to the POSIX specification, then [getpid1, 92 — 1] ∈ (a process may have PID 92)
but [getpid1, ENOENT1] ∉ (the getpid() system call may not
return that error). A specification constrains both invocations
and responses: [NtAddAtom1] is not in the POSIX specification
because NtAddAtom is not a POSIX system call.
An implementation is an abstract machine that takes invocations and calculates responses. Our constructive proof of
the scalable commutativity rule uses a class of machines on
which conflict-freedom is defined6; a good analogy is a Turing-type machine with a random-access tape, where conflict-freedom follows if the machine’s operations on behalf of
different threads access disjoint portions of the tape. An
implementation may “stutter-step,” taking multiple rounds to