Substep Linearizability: Relaxing Atomicity While Preserving Sequential Specification

Substep Linearizability: Relaxing Atomicity While Preserving Sequential Specification Finn Hackett1 University of British Columbia, Canada

Evan Wrench1 University of British Columbia, Canada

Ivan Beschastnikh University of British Columbia, Canada

Yuanhao Wei

arXiv:2610.16099v1 [cs.DC] 12 Oct 2026

University of British Columbia, Canada

Abstract Linearizability is a standard correctness condition for concurrent objects. It takes a correct by construction sequential specification of a concurrent data structure, and produces a composable specification under atomic interleavings of operations. However, some operations like atomic exchangers are not specifiable atomically, making it difficult to reason compositionally about their specifications. Interval linearizability is the state of the art in relaxing linearizability’s constraints. Formally it is a powerful framework, but it requires an interval-sequential specification of the target data structure, which we show is challenging to correctly generate or understand, even for simple operations on a single concurrent register. We propose substep linearizability, which we show is equivalent to interval linearizability using X-CCorrectness, a relaxed concurrency framework we created to compare existing linearizability semantics. We show that substep linearizability’s sequential specifications are suitable for previously infeasible specification tasks, while being comparable in complexity to linearizability’s sequential specifications. For evaluation, we model an atomic exchanger, a popular non-linearizable queue structure, and snapshot isolation between database transactions. 2012 ACM Subject Classification Theory of computation → Program specifications; Theory of computation → Concurrency Keywords and phrases Concurrency, Formal Specifications, Linearizability Digital Object Identifier 10.4230/LIPIcs...

1

Introduction

Linearizability [11] is a standard correctness condition for concurrent objects. It has enjoyed relative success when applied in practice, both since the resulting correctness properties are composable, and since the correctness condition for operations on a linearizable concurrent object can be written as a simplified sequential implementation. The same cannot be said of objects whose operations exhibit non-linearizable edge cases by design. Such objects are relatively common in practice, but there is no convenient way to sequentially specify their behavior. Interval linearizability [2] is the state of the art in relaxing linearizability’s atomicity requirement, thus allowing more complex interactions between concurrent operations on the same object, while maintaining linearizability’s compositionality guarantees. Formally it is an expressive and flexible way to reason about non-linearizable behaviors, but its specification style, interval-sequential specifications, is challenging to write. Interval-sequential

1

Both authors contributed to this work equally. © Finn Hackett, Evan Wrench, Ivan Beschastnikh, Yuanhao Wei; licensed under Creative Commons License CC-BY 4.0 Leibniz International Proceedings in Informatics Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

XX:2

Substep Linearizability: Relaxing Atomicity While Preserving Sequential Specification

Figure 1 Two valid substep linearizations of concurrent wrr operations. Each operation wrr(x) → (y, z) is split into 3 substeps which write x (wx), read y (rdy), and read z (rdz) respectively.

specifications work well when multiple non-linearizable operations can be summarized into one aggregate step, but their effectiveness breaks down when an operation takes more than one atomic step. For instance, consider an operation wr(x) (“Write-Read x”), operating on a shared register r, which performs the following atomic operations: write r ← x (write x to r); read and respond with r’s value. Concurrent invocations of wr(x) may interleave read/write steps arbitrarily, leading to non-linearizable results such as two concurrent wr(x) and wr(x′ ) both reading x′ due to x being overwritten before it can be read back. An idiomatic intervalsequential specification of wr(x)’s behavior is possible, but it relies on a subtle argument that informally requires enumerating which of the read and write permutations are actually possible, and formally requires its own proof. Extending wr(x) by just one additional atomic read to get wrr(x) (“Write-Read-Read x”) is easy to write operationally: write r ← x; read r1 ← r; read r2 ← v and respond with the observed tuple (r1 , r2 ). However, our interval-sequential specification for wrr(x) must be completely reworked to explicitly quantify over read-write interleavings, and becomes more complex. Given a sequential specification is typically used as an oracle of correctness on which to base in-depth analysis, writing the specification itself should have minimal complexity. The state of the art does not satisfy this condition. To correct this, we introduce substep linearizability, a compositionality-preserving relaxation of linearizability’s atomicity requirement which we show has power equal to interval linearizability. Under substep linearizability, each of a concurrent object’s operations may be split into an arbitrary non-predetermined number of substeps, which may interleave freely with other operations’ substeps if the two operations are concurrent. A substep linearizable object that always uses one substep is a linearizable object. Crucially, however, a substep-sequential specification may be expressed by taking a sequential specification and dividing it into one or more atomic steps, whose semantics may be specified as directly as when writing a fully sequential specification. That is, the operations wr(x) and wrr(x) may be specified as we describe them, as two and three atomic steps respectively, while preserving the correctness and compositionality properties we expect of linearizability semantics. Figure 1 illustrates two possible substep interleavings when invoking wrr(1) and wrr(2) in parallel. In this paper, we first introduce X-CCorrectness (“Concurrent Correctness for X”), our formal framework for reasoning about linearizability variants in Section 2. Section 2.2 and beyond define simple linearizability, substep linearizability, and interval linearizability. We illustrate in Appendix A that X-CCorrectness is suitable for defining other prior work, such as set linearizability [14] and weaker properties like sequential consistency and quiescent consistency [4, 10]. For substep and interval-sequential linearizability, those subsections contain a detailed comparison of their sequential specification styles using wr(x) and wrr(x). Section 3 defines subsumption and composability properties for X-CCorrectness, and Section

F. Hackett, E. Wrench, I. Beschastnikh, and Y. Wei

4 uses those definitions to compare substep and interval linearizability. Sections 5–7 are case studies with substep-sequential specifications of atomic exchangers [9], a popular nonlinearizable queue structure [5], and strong snapshot isolation for database transactions [3].

2

Definitions of Linearizability

We first give a general definition that supports a variety of correctness conditions, including many common notations used in this paper. We then apply these definitions to specific forms of linearizability: classical (as baseline), substep, and interval. As part of our precise definitions of substep and interval linearizability, we provide detailed comparisons of their sequential specifications in terms of wr and wrr from Section 1.

2.1

Generalized Concurrent Correctness

We generalize correctness of concurrent objects and histories as X-CCorrectness. The condition is shown in Definition 1, constraining a history H of an object Obj, parametrized over total functions f and predicates P . If X-CCorrectness satisfies composability (defined in section 3), then we instead refer to it as X-Linearizability. Notation and context needed to understand the definition follow. ▶ Definition 1 (X-CCorrect). A history H is X-CCorrect under P iff ∃S ∈ f (H) : P (S). An object Obj is X-CCorrect if all histories H ∈ HObj are X-CCorrect. Histories. Histories may be either complete or incomplete. Incomplete histories contain operations which have an invocation but not a response. This can occur if a thread crashes in the middle of an operation, or if an ongoing execution is being tested. A history H is comprised of an ordered sequence of m invocations i = ⟨name, arg, pid⟩ and n ≤ m responses r = ⟨name, ret, pid⟩. Here, name identifies the operation invoked/responding, arg is an argument, ret is a return value, pid identifies the invoking thread/process. For convenience, we assume that all invocations and responses have a unique index in H. We can construct this from any H by tagging each arg and ret with that index. Each response is matched to a unique invocation and inv(r) returns said invocation. res(i) returns the response matched to i or ⊥ if none exist. Let all histories H ∈ H satisfy the following criteria, where < totally orders invocations and responses by idx: ∀j ∈ 1..mr : inv(rj ) < rj For all i = ⟨ni , A, pi ⟩ and r = ⟨nr , R, pr ⟩, inv(r) = i =⇒ ni = nr ∧ pi = pr ∧ ∄i′ : i = ⟨n′i , A′ , p′i ⟩ ∧ i < i′ < r In other words, the response to an invocation always occurs after it in the history, they share a name and pid, and no operation with the same pid can be invoked between them. Operations. For every invocation ik in a history H, the operation ok = ⟨ik , res(ik )⟩. That is, the operation identifies either a matching pair of invocation and response, or if H is incomplete, an invocation that does not have a response where res(ik ) = ⊥. We write an operation’s invocation as inv(ok ) = ik , and the response as res(ok ) = res(ik ). Operations are indexed by their invocation, so idx(ok ) = idx(inv(ok )). For any history H and all ik in H, ops(H) is the set of all operations ⟨ik , res(ik )⟩. Happens-Before. Operations are partially ordered by the happens-before relation <H , such that oa <H ob iff res(oa ) ̸= ⊥ and res(oa ) < inv(ob ) in H. Objects. Each operation ok corresponds to some action on some object obj(ok ). The corresponding invocation and response ok = ⟨ik , rk ⟩ necessarily refer to the same object,

XX:3

XX:4

Substep Linearizability: Relaxing Atomicity While Preserving Sequential Specification

therefore obj(ik ) = obj(rk ) = obj(ok ). Each object Obj has a set of well-formed concurrent histories HObj ⊆ H. Restriction. When reasoning about compositionality, we often restrict histories or collections of operations to a specific object A. That is, H|A contains all ik , rk in H such that obj(ik ) = obj(rk ) = A. We use the same notation for any collection whose elements are associated with objects in this sense. Parameters. X-CCorrectness is parametrized over: 1. A total function f : H → S which maps a history to a set of ordered sequences of events {S1 , S2 , ..., Sp }, where each Si = e1 , ..., ek . The meaning of e is defined by the type of linearizability. We assume that each event e has an associated object obj(e) from H. Similar to histories, we define S|A as sequences restricted to events associated with object A. 2. A predicate P (S) that identifies whether S is a valid sequence of events. For a sequence S that involves two objects A and B, we assume that P is defined independently for each object. That is, P (S) = P (S|A ) ∧ P (S|B ). We use S1 ≤p S2 to denote S1 being a prefix of S2 . We require that P is prefix-preserving in that if P (S) holds then P (S ′ ) holds for all S ′ ≤p S. We place no restriction on P , other than it must be a predicate on valid sequences. Let P red(X) be the set of all valid predicates for X-CCorrectness. History Completions. Incomplete histories, where there is an i in H such that res(i) = ⊥, can be difficult to reason about, so we define their completions. This definition mirrors those in [2, 11]. While history completions are known to disallow some specifications [15], they are often useful. We define the set of completions C(H) of a history H such that: C(H) contains all invocation-response pairs ⟨i, r⟩ in the same relative order as in H. For all invocations i in H where res(i) = ⊥, either: ∨ i is not in C(H). ∨ i is in C(H) and there is r ∈ C(H) such that res(i) = r in C(H). r may have any value. C(H) only contains invocations and responses defined in the previous two conditions. To define P over only complete histories, we can define the function f (H) = Unless otherwise stated, we assume complete histories in this paper.

2.2

S

′ H ′ ∈C(H) f (H ).

Classic Linearizability

What we call classic linearizability, more commonly referred to as simply linearizability, was first introduced by Herlihy and Wing [11]. In this case, the set of events is exactly the set of operations ops(H). The function f (H) produces all permutations of n = |ops(H)| operations o1 , ..., on ∈ ops(H) consistent with happens-before in H. That is: o1 , ..., on ∈ f (H) iff ∀x, y ∈ 1..n : x < y =⇒ ¬(ox >H oy ) Then, P (o1 , ..., on ) is a sequential specification, specifying valid sequences of atomic operations applied to the underlying object. P is often modeled as a state machine whose transitions are labeled by operations, such that it accepts a subset of sequences o1 , ..., on .

F. Hackett, E. Wrench, I. Beschastnikh, and Y. Wei

2.3

Substep Linearizability

Substep linearizability is a contribution of this paper. Like classical linearizability, we consider permutations of the operations implied by a history H that are consistent with happens-before. Substep linearizability differs by allowing operations to split into multiple atomic parts we call substeps. The last substep taken by an operation may be marked final, meaning that extensions of that linearization cannot show the operation taking further substeps. For any history H, we define a substep as s = ⟨o, m⟩ where o ∈ ops(H) and m ∈ {true, false} is a final marker. A substep’s operation is written op(s), and its finality is written as the predicate f in(s). We define f (H) as containing all sequences of substeps s1 , ..., sn such that: s1 , ..., sn ∈ f (H) iff ((∀o ∈ ops(H) : res(o) = ⊥ ∨ ∃x ∈ 1..n : op(sx ) = o) ∧ (∀x, y ∈ 1..n : x < y =⇒ ¬(op(sx ) >H op(sy ))) ∧ ∀x ∈ 1..n : ((f in(sx ) =⇒ ∄y ∈ (x + 1)..n : op(sx ) = op(sy )) ∧ ((¬f in(sx ) ∧ res(op(sx )) ̸= ⊥) =⇒ ∃y ∈ (x + 1)..n : op(sx ) = op(sy ) ∧ f in(sy )))) That is, all completed operations in ops(H) occur at least once in op(s1 ), op(s2 ), ..., op(sn ) (and vice versa), and no operations may disagree with partial history order <H . The sequence op(s1 ), op(s2 ), ..., op(sn ) may contain duplicate operations. For all substeps involving the same operation, if the operation has a response then its last substep must be marked final, meaning extensions of s1 , ..., sn may not add substeps to that operation. Incomplete operations do not need a final substep. The predicate P (s1 , ..., sn ) is called a substep-sequential specification, which defines valid substep interleavings. Note that per this definition, substep linearizability does not require complete histories. An incomplete operation may take substeps, meaning that the limitations of history completion do not apply. However, defining P where response values may be missing is more complex, so we restrict our treatment in this paper to complete histories. Annotated Substeps. We optionally annotate an operation’s substeps with indices to make writing substep-sequential specifications easier. For any substep sequence s1 , ..., sn ∈ f (H), we can count repetitions of each operation o ∈ ops(H) and assign each one a sequential index i ∈ N. Indices give us the option to specify P as P (e1 , ..., en ), in terms of annotated substeps ek for k ∈ 1..n, rather than the underlying sequence of substeps. The annotated substep ek for some underlying operation sk , given its assigned index i, has the form ek = ⟨op(sk ), f in(i)⟩ if f in(sk ), and ek = ⟨op(sk ), step(i)⟩ otherwise. The advantage of specifying P in this way is that indexing steps is very common in concrete specifications of P . Especially when describing P as a state machine, having access to this information is much easier than extending the state machine to calculate it. For convenience, we define properties of the underlying operation on ek and sk respectively. For example, assume res(ek ) = res(sk ) = res(op(sk )). We model P as a possibly non-deterministic state machine with arbitrarily labeled states q, where transitions are determined by substeps e. Thus, P (e1 , ..., en ) becomes the assertion that our state machine accepts the sequence of transitions e1 , ..., en starting at an initial state q0 . Acceptable transitions are defined by the relation δ(q, e, q ′ ), which may be written in terms of all information available in q and e: any information with which q is labeled, the substep index and finality, and the invocation and response of the underlying operation ok .

XX:5

XX:6

Substep Linearizability: Relaxing Atomicity While Preserving Sequential Specification

See the following sections for simple examples of defining P , as well as a proof that substep linearizability is non-blocking in Section 2.4. For larger scale examples, see Sections 5–7.

2.3.1

Example: Write-Read Substep-Sequentially

We model wr substep-sequentially as a state machine whose states q are labeled with a current register value q.r. Each operation o is considered as two substeps, vali (o) is the value passed to the invocation of o (x in the original description), and valr (o) is the response value. The transition relation δ(q, e, q ′ ) can be defined as: If e = ⟨o, step(1)⟩, q ′ .r = vali (o) Write r ← x If e = ⟨o, f in(2)⟩, valr (o) = q.r ∧ q ′ .r = q.r Read and respond with r’s value The specification directly matches the original description, as annotated on the right.

2.3.2

Example: Write-Read-Read Substep-Sequentially

We extend the substep-sequential specification of wr to wrr by adding one substep to it. Each state q is still labeled with the current register value q.r. The operation o still has the invocation value vali (o). We write operation’s two result values as val r1 (o) and val r2 (o), respectively. With this, the transition relation δ(q, e, q ′ ) can be defined as: If e = ⟨o, step(1)⟩, q ′ .r = vali (o) Write r ← x If e = ⟨o, step(2)⟩, val r1 (o) = q.r ∧ q ′ .r = q.r Read r1 ← v If e = ⟨o, f in(3)⟩, val r2 (o) = q.r ∧ q ′ .r = q.r Read r2 ← v and respond with (r1 , r2 ) Again, this specification can be read as a one to one transcription of our operational description, as annotated on the right. Producing a behavioral specification like this takes no more effort than writing an imperative program, which gives substep-sequential specifications a similar level of accessibility to fully sequential specifications.

2.4

Substep Linearizability is Non-Blocking

Ideally, we would like a definition of linearizability to be non-blocking in that no total operation has to wait for a different operation in order to progress. We say an operation name N is total with respect to a predicate P if for all i = ⟨N, arg, pid⟩ and S such that P (S) holds, there exists a response r = ⟨N, ret, pid⟩ with o = ⟨i, r⟩, such that P (S · ⟨o, step(1)⟩ · ⟨o, step(2)⟩ · ... · ⟨o, f in(k)⟩) holds for some k ≥ 1. In other words, there is some response to i such that a finite sequence of substeps of operation o that can be appended to S while maintaining its validity with respect to P . We show this is the case for substep linearizability. Note that we only consider predicates that hold uniquely for sequences of completed operations, since if the object itself is blocking, there is no point in the definition being non-blocking. Let H · r be the result of appending a response r to the end of H and S · e be the result of appending a substep to the end of a sequence of substeps. Theorem 2 implies that substep linearizability is non-blocking: ▶ Theorem 2. Let H be a history containing an unmatched invocation i = ⟨N, arg, pid⟩ of a total operation name N where H is substep-linearizable with respect to a predicate P ∈ P red(substep). Then there exists return value ret such that H · ⟨N, ret, pid⟩ where ⟨N, ret, pid⟩ = res(i) is in the set H and is substep-linearizable with respect to P .

F. Hackett, E. Wrench, I. Beschastnikh, and Y. Wei

Proof. Since H is substep-linearizable, there exists an S ∈ f (H) such that P (S) holds. If S contains a substep of an operation o such that inv(oj ) = ij , then we must have S ∈ f (H · ⟨N, ret, pid⟩) for some ret with ⟨N, ret, pid⟩ = res(ij ) by definition of substeplinearizability, so the Theorem holds. If S does not contain a substep of such an operation o, then since N is total, there exist N , ret, pid, and a sequence of substeps such that for o = ⟨i, ⟨N, ret, pid⟩⟩, P (S · ⟨o, step(1)⟩ · ⟨o, step(2)⟩ · ... · ⟨o, f in(k)⟩) holds. Furthermore, S · ⟨o, step(1)⟩ · ⟨o, step(2)⟩ · ... · ⟨o, f in(k)⟩ ∈ f (H · ⟨N, ret, pid⟩), so the Theorem holds in this case as well. ◀

2.5

Interval Linearizability

Interval linearizability [2] generalizes linearizability by fusing a set of invocations I and a set of responses R into one step, or interval (I, R). Note that unlike substep linearizability, f (H) is only well defined on complete histories. The resulting f (H) contains sequences of intervals such that: I1 , R1 , ..., In , Rn ∈ f (H) iff (∀ ⟨i, r⟩ ∈ ops(H) : (∃x, y ∈ 1..n : i ∈ Ix ∧ r ∈ Ry ∧ ∀x ∈ 1..n : r ∈ / Ix ∧ i ∈ / Rx ) ∧ ∀x, y ∈ 1..n : (Ix ∩ Iy = Rx ∩ Ry = ∅ ∧ ∀i ∈ Ix , r ∈ Ry : op(i) = op(r) =⇒ x ≤ y ∧ ∀r ∈ Rx , i ∈ Iy : r < i =⇒ x < y)) The definition above can be explained via three rules: Every invocation and response in H must be assigned to exactly one set I and R respectively, where sets I contain only invocations, and sets R contain only responses. An operation’s invocation must occur in an interval no later than its response. A response that happens-before an invocation must occur in an earlier interval than that invocation. The predicate P (I1 , R1 , ..., In , Rn ) is called an interval-sequential specification. It is modeled as a state machine with arbitrarily labeled states q, whose transitions are determined by intervals I, R. Acceptable transitions are defined by the relation δ(q, I, R, q ′ ). More precisely, the sequence I1 , R1 , ..., In , Rn is accepted by P if and only if there exists q0 , q1 , ..., qn such that q0 is a valid initial state and for all i ∈ {1, 2, ..., n}, (qi−1 , Ii , Ri , qi ) ∈ δ. As we comment in Section 1, δ can be challenging to define correctly. It can work well for operations that combine operations into fewer steps – see the atomic exchanger case study in Section 5. However, it is challenging to express even simple interval-sequential specifications outside of that situation. We show this by giving interval-sequential specifications of wr and wrr in the following sections.

2.5.1

Example: Write-Read Interval-Sequentially

To give an interval-sequential specification for wr as defined in Section 1, we need to map each invocation’s two atomic steps onto one interval, interpreting multiple invocations and responses at once (the sets I and R respectively). First consider two concurrent invocations: wr(1) → x which writes 1 and reads x, and wr(2) → y which writes 2 and reads y. Our interval-sequential specification must specify

XX:7

XX:8

Substep Linearizability: Relaxing Atomicity While Preserving Sequential Specification

what values of x and y are possible, so we examine the valid permutations of the operations’ 4 atomic steps. We write the step where wr(1) writes its value as wr(1)writes , and the step where it reads a value p as wr(1)reads p . If x = 1 and y = 2, then the invocations are sequential and not concurrent: this is the effect of wr(1)writes , wr(1)reads 1 , wr(2)writes , wr(1)reads 2 . No concurrent execution can have this outcome, since a concurrent execution would start wr(2) earlier, preventing wr(1) from reading its own value. Our interval-sequential specification does not need to specify this, since two sequential intervals achieve the same result. In a concurrent execution, sequences where x = 2 have the form wr(1)writes , wr(2)writes , ..., wr(1)reads 2 , ... This case requires that y = 2, since wr(2)reads can only occur on either side of wr(1)reads , nor before wr(1)writes since that would not be sequentially consistent. By swapping 1 and 2, the same argument means y = 1 =⇒ x = 1. Generalizing, writes by concurrent executions of wr can never interleave with reads. Every concurrent operation must start by writing its own value. To have wr(p)reads , we must also have an earlier instance of wr(p)writes . For a read to be followed by a write, that write must belong to a new non-concurrent invocation of wr. That is, for an operation to not read its own write, the only concurrent interleaving looks like wr(v1 )writes , wr(vn )writes , ..., wr(v1 )reads vn , ..., wr(vm )reads vn , where n and m are the sizes of I and R respectively. Given this insight, our interval-sequential specification of wr is an automaton with one state q. Each invocation i has an argument val(i) (x in the original description), and every response r ∈ R has a response value val(r). That is, the invocation looks like wr(val(i)) → val(r). In this case, the transition relation δ(q, I, R, q) can be defined iff there exists i ∈ I such that for all r ∈ R, val(r) = val(i). This specification treats invocations as write operations and responses are read operations. For any interval (q, I, R, q), every response in R must read the value written by some invocation in the preceding set of invocations, and every response in R must read the same value. It is not satisfying, however. As we show above, it takes nontrivial reasoning to claim this specification truly represents the intended behavior of wr. Observing this property during analysis given a clear statement of intended behavior makes sense. Requiring the derivation of such a property in order to write an initial specification does not.

2.5.2

Example: Write-Read-Read Interval-Sequentially

Unlike wr, to divide wrr into sets of invocations and responses we must explicitly model the possible interleavings of the three component operations. Consider a pair of concurrent operations wrr(1) and wrr(2). Aside from completing each operation sequentially, there are four valid outcomes. Figure 1 illustrates the first two. If wrr(1) writes first, we get these interleavings: wrr(1)writes , wrr(2)writes , wrr(∗)reads 2 (4×) – meaning wrr(1) and wrr(2) both return (2, 2); and wrr(1)writes , wrr(1)reads 1 , wrr(2)writes , wrr(∗)reads 2 (3×) – meaning wrr(1) returns (1, 2) and wrr(2) returns (2, 2). If wrr(2) writes first, we get the same pattern but with 1 and 2 swapped. The result (1, 2) being possible proves our property for wr does not apply to wrr. Instead, we must directly express possible sequences of interleavings. More formally, an interval-sequential specification of wrr is a non-deterministic state machine with states q labeled with the set of pending operations q.pend and q.obs a function from any operation in q.pend to either a value or ⊥. Invocations i ∈ I have values val(i), and responses r ∈ R have two values each, val 1 (r) and val 2 (r). For I and R, ops(I) and ops(R) are the sets of corresponding operations respectively. The transition relation δ can be defined such that (q, I, R, q ′ ) ∈ δ iff there exists a permutation s of all elements of I, such that:

F. Hackett, E. Wrench, I. Beschastnikh, and Y. Wei

Let pos(i) be the position of i ∈ I in the sequence s. Let obs(x) be a function from x ∈ q.pend ∪ ops(I) to a value or ⊥ such that: Where q.obs(x) ̸= ⊥, obs(x) = q.obs(x) Where q.obs(x) = ⊥, non-deterministically either obs(x) = ⊥, or obs(x) = val(i) where i ∈ I such that if inv(x) ∈ I then pos(inv(x)) ≤ pos(i). For all r ∈ R: ∧ obs(op(r)) ̸= ⊥ and val 1 (r) = obs(op(r)) ∧ val 2 (r) = val(i) where i is the last invocation in s q ′ .pend = q.pend ∪ ops(I) \ ops(R) q ′ .obs(x) = obs(x), where x ∈ q ′ .pend Intuitively, the resulting state machine non-deterministically tracks the middle step of each operation using obs(x). During any substep in which an operation is pending, some “middle” value may optionally be read into obs(x), meaning the middle step occurs at any point between invocation and response of its corresponding operation. We implicitly discard cases where obs(x) stays ⊥, since the response cannot be ⊥. Following the selected sequence s, obs(x) observes only invocations on or after inv(x). While this specification works, it has significant incidental complexity. For example, a previous draft allowed obs(x) to capture invocations before inv(x), which was missed for some time by multiple co-authors. Furthermore, the specification starts to resemble manually keeping track of all possible substeps, which is the use case for substep linearizability.

3

Defining Subsumption and Composability

In this section, we establish two definitions important for creating definitions of linearizability: Subsumption and composability. Intuitively, a definition of CCorrectness subsumes another if it can define an equivalent predicate for all predicates of the other definition. To fit with the common meaning of linearizability, we want our definitions to be composable. That is, for any history composed of multiple objects, if the histories restricted to each individual object are X-CCorrect under a predicate, then the entire history is X-CCorrect under the same predicates and vice-versa. First, Theorem 6 states that substep linearizability is composable. Theorem 7 generalizes conditions for composability of X-CCorrectness, and Theorem 8 states that composability follows from being subsumed by a composable definition. For two definitions of CCorrectness, X-CCorrectness and Y-CCorrectness, we say that YCCorrectness subsumes X-CCorrectness if for all Px ∈ P red(X), there exists a Py ∈ P red(Y ) such that H is X-CCorrect with respect to Px if and only if H is Y-CCorrect with respect to Py . We say that X-CCorrectness and Y-CCorrectness are equivalent if each subsumes the other. ▶ Definition 3 (Subsumes). Y-CCorrectness subsumes X-CCorrectness if ∀PX ∈ P red(X) : ∃PY ∈ P red(Y ) : ∀H ∈ H : (∃S ∈ fX (H) : PX (S)) ⇐⇒ (∃S ′ ∈ fY (H) : PY (s)). ▶ Definition 4 (Equivalence). X-CCorrectness is equivalent to Y-CCorrectness if X-CCorrectness subsumes Y-CCorrectness and Y-CCorrectness subsumes X-CCorrectness. As a reminder, we require P (S) = P (S|A ) ∧ P (S|B ) for a sequence composed of operations on 2 objects, A and B. This can easily be extended to histories composed of more than 2 objects, but we only handle this case for simplicity.

XX:9

XX:10

Substep Linearizability: Relaxing Atomicity While Preserving Sequential Specification

▶ Definition 5 (Composability). A history H is composable under X-CCorrectness if ∀P ∈ P red(X) : (((∃SA ∈ f (H|A ) : P (SA )) ∧ (∃SB ∈ f (H|B ) : P (SB ))) ⇐⇒ ∃S ∈ f (H) : P (S)). X-CCorrectness is composable if all possible histories H ∈ H are composable. ▶ Theorem 6. Substep linearizability is composable. This theorem can be proven using the same proof method as for classical linearizability. Intuitively, if there exist an S ∈ f (H) that satisfies P , then S|A and S|B both satisfy P and are in H|A and H|B , respectively since these sub-histories maintain the same happens-before ordering of H. Furthermore, given an SA ∈ f (H|A ) : P (SA ) and SB ∈ f (H|B ) : P (SB ), an S ∈ f (H) : P (S) can be constructed by interleaving SA and SB in such a way that does not violate happens-before. It can be shown that such an interleaving must exist by proving that the transitive closure between the happens-before ordering of operations in H with the ordering of operations in SA and SB cannot form a cycle. We show that a history H being composable can be reduced to saying that: (1) For each object A and for all sequences S generated from f (H), there is some sequence SA generated from f (H|A ) such that SA is a prefix of S|A (2) for each set of sequences generated from each object, there is some sequence S generated from f (H) such that S|A is a prefix of the sequence SA generated from each object A. The proof follows from the from the definition of a predicate on a sequence composed on multiple objects. ▶ Theorem 7. A history H is composable under X-CCorrectness if and only if the following conditions hold: 1. ∀S ∈ f (H) : (∃SA ∈ f (H|A ) : SA ≤p S|A ) ∧ (∃SB ∈ f (H|B ) : SB ≤p S|B ) 2. ∀SA ∈ f (H|A ), SB ∈ f (H|B ) : ∃S ∈ f (H) : S|A ≤p SA ∧ S|B ≤p SB Proof. We first show conditions 1 and 2 imply H is composable under X-CCorrectness. Given P ∈ P red(X) without loss of generality, we show the bidirectional implication in Definition 5 holds for X. Assuming the left-hand side of Definition 5 holds, then by condition 2 there exists an S ∈ f (H) such that S|A ≤p SA ∧ S|B ≤p SB holds. Therefore, since P is prefix-preserving and P (SA ) ∧ P (SB ) holds, we have that P (S|A ) ∧ P (S|B ) holds which by definition is P (S) so the right-hand side must be true. Assuming the right-hand side, then by condition 1 there exist SA , SB such that SA ≤p S|A ∧ SB ≤p S|B . Thus, since P (S) = P (S|A ) ∧ P (S|B ), the left-hand side must be true. Secondly, we show that the negation of either condition 1 or 2 implies H is not composable under X-CCorrectness. (a) Negating condition 1, there must exist an S ∈ f (H) such that ∀SA ∈ f (H|A ) : SA ̸≤p S|A or ∀SB ∈ f (H|B ) : SB ̸≤p S|B . We choose P ∈ P red(X) where P (S ′ ) = S ′ |A ≤p S|A ∧ S ′ |B ≤p S|B . P (S) holds by definition, but the definition of P combined with the negation of condition 1 imply that ∀SA ∈ f (H|A ) : ¬P (SA ) or ∀SB ∈ f (H|B ) : ¬P (SB ). This contradicts definition 5. (b) Negating condition 2, there exist SA ∈ f (H|A ) and SB ∈ f (H|B ) such that ∀S ∈ f (H) : S|A ̸≤p SA ∨ S|B ̸≤p SB . We choose P ∈ P red(X) where P (S ′ ) = S ′ |A ≤p SA ∧ S ′ |B ≤p SB . By definition of P , P (SA ) ∧ P (SB ) must hold, but the negation of condition 2 implies that ∀S ∈ f (H) : ¬P (S|A ) ∨ ¬P (S|B ). Therefore, ∀S ∈ f (H) : ¬P (S) contradicts Definition 5. ◀ Theorem 8 shows that a definition of CCorrectness is composable if it is subsumed by a definition known to be composable. Intuitively, for any predicate in the original definition, there must be an equivalent predicate in the composable definition. ▶ Theorem 8. If Y-CCorrectness subsumes X-CCorrectness and Y-CCorrectness is composable, then X-CCorrectness is composable.

F. Hackett, E. Wrench, I. Beschastnikh, and Y. Wei

Proof. For a proof by contradiction, assume Y-CCorrectness is composable and subsumes X-CCorrectness, and X-CCorrectness is not composable. Since X-CCorrectness is not composable, there exist some history H, predicate P ∈ P red(X) and objects A, B such that either (a) ∃SA ∈ fX (H|A ) : P (SA ) ∧ ∃SB ∈ fX (H|B ) : P (SB ) but ∀S ∈ fX (H) : ¬P (S) or (b) ∃S ∈ fX (H) : P (S) but ∀SA ∈ fX (H|A ) : ¬P (SA ) ∨ ∀SB ∈ fX (H|B ) : ¬P (SB ). By subsumption of X-CCorrectness, there must exist a P ′ ∈ P red(Y ) such that ∀H0 ∈ H : (∃S ∈ fX (H0 ) : P (S)) ⇐⇒ (∃S ′ ∈ fY (H) : P (S ′ )). Then in case (a), we have that ′ ′ ′ ′ ∃SA ∈ fY (H|A ) : P ′ (SA ) ∧ ∃SB ∈ fY (H|B ) : P ′ (SB ) and ∀S ′ ∈ fY (H) : ¬P ′ (S ′ ). In case ′ ′ ′ (b), we have that ∃S ′ ∈ fY (H) : P ′ (S ′ ) and ∀SA ∈ fY (H|A ) : ¬P ′ (SA ) ∨ ∀SB ∈ fY (H|B ) : ′ ¬P (SB ). Either case contradicts the definition of composability for Y-CCorrectness. ◀

4

Relationship Between Substep and Interval Linearizability

In this section, we first prove that substep linearizability subsumes interval linearizability. This shows that any interval-sequential specification can be expressed using substeps. We also show that interval linearizability subsumes substep linearizability under a restricted class of predicates that we describe in Definition 10. We begin by proving that substep linearizability subsumes interval linearizability. In this direction, we can treat the invocations and responses in an interval linearization as pairs of substeps. This means that any predicate defined for interval linearizability can be translated directly to a predicate defined for substep linearizability. Let fI (H) and fS (H) be the function f (H) defined for interval and substep linearizability, respectively. ▶ Theorem 9. Substep linearizability subsumes interval linearizability. Proof. Let H ∈ H be some history and PI ∈ P red(interval) be some arbitrary predicate defined without loss of generality. We prove the existence of a predicate PS ∈ P red(substep) such that H is substep-linearizable with respect to PS iff H is interval-linearizable with respect to PI . For an arbitrary sequence of substeps S ∈ fS (H) such that each substep occurs exactly twice, we define a sequence of alternating sets of invocations and responses S0 . First, combine maximal adjacent sets of the first occurrence of oK ’s in S into sets I1 , I2 , ..., In . Combine maximal adjacent sets of the second occurrence of oK ’s in S into sets R1 , R2 , ..., Rn . Let S0 = I1 , R1 , I2 , R2 , ..., In , Rn . Let PS (S) be the predicate that holds if and only if the following conditions hold: Each ok in the history H appear exactly twice in S PI (S0 ) The equivalence between PI and PS follows from the definitions of interval and substep linearizability. ◀ Note that the function f (H) for substep linearizability allows for substeps of incomplete operations, while f (H) for interval linearizability only allows sequences such that each invocation has a matching response. Therefore, in general we can define predicates that are substep-linearizable but not interval-linearizable. However, we define a class of predicates N BP red(substep) ⊂ P red(substep) such that interval-linearizability subsumes substep linearizability over these predicates. Intuitively, this set defines predicates P such that if P is substep-linearizable with respect to an incomplete history H, it is also substep linearizable with respect to a history H ′ ∈ C(H). ▶ Definition 10 (Non-blocking predicates). A Non-blocking predicate P ∈ N BP red(substep) is a predicate P ∈ P red(substep) : ∀H ∈ H : (∃S ∈ f (H) : P (S) =⇒ ∃H ′ ∈ C(H) : ∃S ′ ∈ f (H ′ ) : P (S ′ ))

XX:11

XX:12

Substep Linearizability: Relaxing Atomicity While Preserving Sequential Specification

Even with this restriction, finding a predicate defined for interval linearizability that is equivalent to an arbitrary predicate defined for substep linearizability is less straightforward since a specification could require more than two substeps. However, a key observation is that some sequence S ∈ fI (H) can be interpreted as representing each of the completions of the original history C(H). In other words, no information about the original history is lost when computing f (H). This allows us to test any substep predicate PS using the set of sequences fI (H). ▶ Theorem 11. Interval linearizability subsumes substep linearizability under non-blocking predicates. Proof. Let H ∈ H be some history and PS ∈ N BP red(substep) be some arbitrary predicate defined without loss of generality. We prove the existence of a predicate PI ∈ P red(interval) such that H is substep-linearizable with respect to PS if and only if H is interval-linearizable with respect to PI . For an arbitrary sequence S0 = I1 , R1 , I2 , R2 , ..., Im , Rm ∈ fI (H), we define the history HS0 as some ordering of the invocations and responses in S0 while maintaining that if a happens before b in HS0 , then b was in the same set as a or a later one in the sequence S0 . Since all possible choices of HS0 result in the same happens-before order between operations, the result is deterministic. Let PI be the predicate that holds for a sequence S ′ if and only if HS ′ is substep linearizable with respect to PS . We prove that this predicate holds for H if and only if PS holds for H. If ∃S ∈ fS (H) : PS (S), then by definition of N BP red, for some H ′ ∈ C(H), ∃S ′ ∈ f (H ′ ) : PS (S ′ ). By definition of interval linearizability, we have that ∀HC ∈ C(H) : ∃S0 ∈ fI (H) : HS0 = HC . Let S0 be the sequence such that HS0 = H ′ . By definition, if ∃S ′ ∈ fS (H ′ ) : PS (S) then ∃S ∈ fS (HS0 ) : PS (S) which is the definition of PI (S0 ). Since ∃S ′ ∈ fI (H) : S ′ = S0 , we have that ∃S ′ ∈ fI (H) : PI (S ′ ). Finally, we assume ∃S ′ ∈ fI (H) : PI (S ′ ) and prove ∃S ∈ fS (H) : PS (S). By definition of PI , ∃S ∈ fS (HS ′ ) : PS (S). But since by construction, HS ′ preserves the happens-before order of operations in H, S ∈ fS (H). Therefore, ∃S ∈ fS (H) : PS (S) which completes the proof. ◀

5

Case Study: Atomic Exchanger

The atomic exchanger is a common example of a non-linearizable object, which can be specified as set-linearizable and motivates the concurrency-aware linearizability proof system [9]. It offers one operation exchange(v) which either atomically exchanges v with a concurrent operation, producing pairs of invocations such that exchange(v1 ) = v2 ||exchange(v2 ) = v1 , or exchange(v1 ) = ⊥ and exchange(v2 ) = ⊥. That is, either two operations successfully exchange values atomically, or no exchange can occur and failure is indicated via ⊥. This case study has already been explored by the state of the art, and is known to be setand interval-sequentially specifiable. We first show an interval-sequential specification, then show that a similarly convenient substep-sequential specification is possible. Our interval-sequential specification is a state machine with unlabeled states q. Each invocation i has a proposed value prop(i), and each response r has a received value recv(r). Transitions are accepted by δ(q, I, R, q ′ ) such that either (1) I = {i}, R = {res(i)}, and recv(res(i)) = ⊥; or (2) I = {i1 , i2 }, i1 = ̸ i2 , R = {res(i1 ), res(i2 )}, prop(i1 ) = recv(res(i2 )), and prop(i2 ) = recv(res(i1 )). That is, any pair of concurrent operations may exchange values, or a non-paired operation may fail and receive ⊥. We only need to specify pairs of invocations and responses, since larger numbers of concurrent operations are automatically decomposed sequences of intervals by interval semantics. A substep-sequential specification can emulate an interval-sequential one, as shown in Theorem 9. When the intervals would allow groups of operations to execute as one (pairs in

F. Hackett, E. Wrench, I. Beschastnikh, and Y. Wei

this case), we propose a convenience notation for substep-sequential state machines. Rather than specify each substep individually, we accept atomic sequences of substeps. That is, we define δ(q, S, q ′ ) where S is a non-empty sequence of substeps, such that if S = e1 , ..., en , then the state machine accepts the sequence of transitions q, e1 , ..., en , q ′ iff δ(q, S, q ′ ). If the intention is to accept e1 , ..., en and none of its permutations, then this notation is simpler than specifying each step individually and logically ruling out other invalid sequences. With this notation, we can specify an atomic exchanger substep-sequentially as a state machine with unlabeled states q. Each operation o has a proposed value prop(o) and a received value recv(o). We define δ(q, S, q ′ ) such that: If S = ⟨o1 , step(1)⟩, ⟨o2 , f in(1)⟩, ⟨o1 , f in(2)⟩ and o1 ̸= o2 , then prop(o1 ) = recv(o2 ) and prop(o2 ) = recv(o1 ). If S = ⟨o, f in(1)⟩, then recv(o) = ⊥. The success case is an atomic triple of substeps: o1 takes two steps that surround o2 , meaning that they must be concurrent. Such concurrent operations may exchange values if the proposed and received values match. Swapping o1 and o2 produces an equivalent symmetrical behavior. The failure case is a single atomic step which may occur at any time. As with the interval-sequential specification, cases with more than two concurrent operations are implicitly decomposed into sequential instances of the specified patterns. The specification above is easy to translate into single steps. Multi-step sequences can be encoded using state labels storing position within the step sequence and information needed by multi-step assertions. For the exchanger, an implementation of mutual exclusion with explicit “propose” and “accept” labels is sufficient.

6

Case Study: Cameron Desrochers’ Queue

High performance queue data structures are often necessary in multithreaded applications. A common use case is managing thread pools. Cameron’s queue [5] is a popular2 C++ library whose design aims for competitive performance in scenarios where fully linearizable behavior is not necessary. The queue respects insertion order per producer (thread that enqueues), but not globally since many use cases do not require it. Since it relies heavily on operations with multiple visible side-effects, an interval-sequential specification would be difficult to write for similar reasons to our wrr example in Section 2.5. We show the applicability of substep-sequential specification by specifying three representative operations: enqueue by producer, dequeue, and approximate size. Per their documentation, Cameron’s queue may be considered as a list of sub-queues indexed by producer. Each producer enqueues to its own sub-queue, and dequeue operations non-deterministically select the head of any sub-queue, or ⊥ if all sub-queues non-atomically appear empty. While enqueue is a single atomic operation, dequeue is not. It performs a non-atomic check on each sub-queue, and if it is possible to witness all sub-queues transiently be empty (even if they were never simultaneously empty), then ⊥ may be produced. Similarly, approximate size is specified to perform a non-atomic scan of sub-queue sizes, and may return any sum of sub-queue sizes that individually occur during the operation. For a set of producers P , we specify Cameron’s queue as a substep-sequential state machine. For each operation o, we define its name name(o) ∈ {enqueue, dequeue, size}. All operations have a value val(o), which is either argument of an enqueue, the return

2

It has 12.5k stars on GitHub as of writing and is a prominent search result for “lock free queue C++”.

XX:13

XX:14

Substep Linearizability: Relaxing Atomicity While Preserving Sequential Specification

value of a dequeue, or the return value of a size operation. prod(o) ∈ P is an enqueue operation’s producer. States q are labeled with a total function from producers p ∈ P to sub-queues q.s(p) = v1 , ..., vn , where a sub-queue is a sequence of arbitrary values v1 , ..., vn . For every operation o and producer p, q.z(o, p) = n where n ∈ N ∪ {⊥}. That is, q.z tracks a per-operation mapping from producer to witnessed sub-queue size, which is ⊥ when no size has been witnessed. In the initial state q0 , q0 .s(p) = ∅ for all p, and q0 .z(o, p) = ⊥ for all o and p. We define δ(q, e, q ′ ) such that: If e = ⟨o, f in(1)⟩, name(o) = enqueue, and q.s(prod(o)) = v1 , ..., vn then: ∧ q ′ .s = q.s except q ′ .s(prod(o)) = v1 , ..., vn , val(o) ∧ q ′ .z = q.z If e = ⟨o, f in(1)⟩, name(o) = dequeue, and (∃p ∈ P : q.s(p) = v1 , ..., vn ) ∧ (v1 = val(o)) then: ∧ q ′ .s = q.s except q ′ .s(p) = v2 , ..., vn ∧ q ′ .z = q.z If e = ⟨o, step(∗)⟩, name(o) ∈ {dequeue, size}, there exists p ∈ P such that q.z(o, p) = ⊥ and q.s(p) = v1 , ..., vn , then: ∧ q ′ .z = q.z except q ′ .z(o, p) = n ∧ q ′ .s = q.s If e = ⟨o, f in(∗)⟩, name(o) = dequeue, val(o) = ⊥, and ∀p ∈ p : q.z(o, p) = 0, then q ′ = q. P If e = ⟨o, f in(∗)⟩, name(o) = size, ∀p ∈ P : q.z(o, p) ̸= ⊥, and val(o) = p∈P q.z(o, p), then q ′ = q. The enqueue operation is atomic and takes a single substep to add the element val(o) to the producer’s sub-queue. The success case of the dequeue operation takes a single substep when one of the sub-queues is observed to have val(o) at its head, in which case that element is dequeued. Otherwise, dequeue and size share |P | substeps: they non-deterministically observe each sub-queue’s size one by one and accumulate the results into q.z. For dequeue, the operation may report ⊥, indicating a possibly empty queue, if all sub-queues transiently have size 0. For the size operation, the observed sizes must sum to the operation’s reported value. As an extension, consider that Cameron’s queue also has optimized bulk enqueue and dequeue operations which operate on sequences of elements to enqueue or dequeue at once. These operations are non-atomic, and can also be given substep-sequential specifications. The bulk enqueue repeats the single-value semantics for each value it enqueues, assigning each value a substep. The bulk dequeue operation is involves a request for M elements, as well as a sequence of N ≤ M actually dequeued elements. Comparably to the ⊥ rule for single dequeues, if N < M , it must be possible to non-atomically view a sequence of sub-queues whose length sums to N , and which contain the dequeued elements in the right order. An advantage of substep-sequential specifications in practice is that specifying these operations should not interfere much with the specification above. They may involve additional state labels or operation types, but in principle the change should be additive.

7

Case Study: Database Transactions with Strong Snapshot Isolation

The semantics of concurrent database transactions are often studied [1, 13] when describing the allowable behaviors of a given database implementation under concurrency. We show a substep-sequential specification of strong snapshot isolation [3], where each operation is

F. Hackett, E. Wrench, I. Beschastnikh, and Y. Wei

a transaction, and snapshots be placed at any point between the transaction’s invocation and response. Note that assuming strong snapshot isolation is a convenience. Schultz and Demirbas [17] specify a more complete transaction system as totally ordered sequences of steps, which may also be viewed as a substep-sequential specification. A transaction is a sequence of reads and writes of values v ∈ V in relation to a set of keys K. We call reads and writes effects. A read has the form read(k) → v, and a write has the form write(k) := v. Transactions are assumed to commit once all reads and writes have completed. We ignore aborted transactions since snapshot isolation never allows reading aborted writes. These semantics are broadly similar to existing studies of database semantics, and make no particular assumptions about architecture. Strong snapshot isolation can be informally defined as the situation where otherwise linearizable transactions exhibit write skew, and concurrent overlapping writes are not permitted (in practice they abort). Consider two concurrent transactions t1 and t2 that read overlapping keys x and y (which we assume refer to integers here). Assume t1 writes x − y to x and then commits. Then, t2 writes x − y to y and also commits. The result is non-linearizable, since neither instance of x − y accounted for the other transaction’s update of x or y respectively. Linearizably, t1 should have written x − (x − y), or t2 should have written (x − y) − y. If the two transactions both wrote to x or y, the execution would be invalid. Our substep-sequential specification of this phenomenon is a state machine with states q, labeled by a function q.kv : K → (V × Z) mapping each key to a value and a version number, and a function q.s from operations to either a snapshot in the partial function K ⇀ (V × Z) or ⊥ indicating no snapshot. For convenience value-version pairs may be decomposed as, value(⟨v, ∗⟩) = v and version(⟨∗, z⟩) = z. Initially, q0 .kv assigns an arbitrary value and version number 0 to every key, and q.s assigns ⊥ to every operation. Each operation has an associated transaction t(o) which is a sequence of effects. We write the set of all keys read by reads in t(o) as reads(o). Note that this is not just the set of k where read(k) → ∗ is in t(o): reads(o) excludes reads where k is overwritten before being read. The transition relation θ(q, e, q ′ ) is defined such that: If e = ⟨o, step(1)⟩, then q ′ .s(o) = s, where s is defined for all k ∈ reads(o), s(k) = q.kv(k), and undefined otherwise. If e = ⟨o, f in(2)⟩, then let f1 , ..., fn be the sequence of effects in t(o), there exists kv0 , ..., kvn ∈ K ⇀ V , inductively defining kvp+1 in terms of fp+1 and kvp , with initially kv0 = ∅, such that: If fp+1 = read(k) → v, then v = kvp (k) if kvp (k) is defined, otherwise v = value(q.s(o)(k)). In either case, kvp+1 = kvp . If fp+1 = write(k) := v, then kvp+1 = kvp except kvp+1 (k) = v. Given the final kvn , for all k ∈ K, q ′ .kv(k) = (kvn (k), version(q.kv(k)) + 1) and version(q.kv(k)) = version(q.s(o)(k)) where kvn (k) is defined, and q ′ .kv(k) = q.kv(k) otherwise. Intuitively, our specification splits each transaction into two steps. First, we read a snapshot q.s(o) of the database’s relevant keys read(o) in one step. This substep marks where the snapshot occurs, on which the later atomic write will base its view of the database, including which version of each key was observed. The second substep is specified as an interpreter for effect sequences, accumulating the set of writes performed as kvp . A transaction can read its own writes according its internal order of operations, so we specify read operations both in terms of the snapshot q.s(o) and already-performed writes kvp . The final kvn contains each key-value pair that is atomically written to q ′ .kv, iff the value being

XX:15

XX:16

Substep Linearizability: Relaxing Atomicity While Preserving Sequential Specification

overwritten in q.kv has the same version as the value in q.s(o). If the version differs between snapshot and write, there were concurrent writes to the same key and the execution must be rejected.

8

Related Work

Beyond the definitions of linearizability discussed in this paper [2, 11, 14], many variants have been proposed in the literature. Derrick et al. [4] define and give a proof method for quiescent consistency, originally proposed by Shavit & Herlihy [10], which allows operations to execute atomically in any order as long as at least one operation is pending. We show quiescent consistency is expressible using X-CCorrectness in Appendix A.3. Haas et al. [7] define local linearizability for a restricted category of containers, which asserts linearizability when the history is projected onto values coming from any specific thread. Rinberg & Keidar [16] define intermediate-value linearizability in which numerical values can vary non-linearizably within a range. Hemed et al. [9] formalize set-linearizability with their definition of concurrency-aware linearizability and show a technique for verifying said definition. All of these have restrictive conditions, are not composable, or are less expressive than interval linearizability. Goubault et al. [6] argue that any reasonable definition of linearizability satisfies a set of axioms. Using these axioms, they show that interval-linearizability is the weakest possible correctness condition for concurrent histories, which by our proof of equivalence would imply the same for substep linearizability. Oliveira Vale et al. [15] show that linearizability and modular composition are intrinsically related, and Eashan et al. [8] apply the concept to program logics. They define compositional linearizability, a relaxation of linearizability equivalent to interval linearizability with incomplete histories. Their work improves modular verification, whereas substep linearizability improves sequential specifications. We leave integration between the two and investigation of substep linearizability without history completion as future work.

9

Conclusion

In this paper we present substep linearizability, a correctness condition that allows for operations to take effect at multiple atomic points. We show how this definition is composable, non-blocking and equivalent to interval linearizability in its ability to capture concurrent behavior. We also give examples of how the specification of many objects are simpler to represent using substep linearizability. We leave as future work the development and evaluation of proof systems and model checking techniques to verify conformance with substep-sequential specifications in practice. However, we are optimistic that substeps having the same basis in sequences of atomic steps as plain linearizability will enable significant re-use of existing techniques. References 1

2

Hal Berenson, Phil Bernstein, Jim Gray, Jim Melton, Elizabeth O’Neil, and Patrick O’Neil. A critique of ansi sql isolation levels. In Proceedings of the 1995 ACM SIGMOD International Conference on Management of Data, SIGMOD ’95, page 1–10, New York, NY, USA, 1995. Association for Computing Machinery. doi:10.1145/223784.223785. Armando Castañeda, Sergio Rajsbaum, and Michel Raynal. Unifying concurrent objects and distributed tasks: Interval-linearizability. J. ACM, 65(6), November 2018. doi:10.1145/ 3266457.

F. Hackett, E. Wrench, I. Beschastnikh, and Y. Wei

3

Khuzaima Daudjee and Kenneth Salem. Lazy database replication with snapshot isolation. In Proceedings of the 32nd International Conference on Very Large Data Bases, VLDB ’06, page 715–726. VLDB Endowment, 2006.

4

John Derrick, Brijesh Dongol, Gerhard Schellhorn, Bogdan Tofan, Oleg Travkin, and Heike Wehrheim. Quiescent consistency: Defining and verifying relaxed linearizability. In Cliff Jones, Pekka Pihlajasaari, and Jun Sun, editors, FM 2014: Formal Methods, pages 200–214, Cham, 2014. Springer International Publishing.

5

Cameron Desrochers and other contributors. cameron314/concurrentqueue: A fast multiproducer, multi-consumer lock-free concurrent queue for C++11. https://github.com/ cameron314/concurrentqueue/, 2013. Accessed: 2025-11-13.

6

Éric Goubault, Jérémy Ledent, and Samuel Mimram. Concurrent Specifications Beyond Linearizability. In Jiannong Cao, Faith Ellen, Luis Rodrigues, and Bernardo Ferreira, editors, 22nd International Conference on Principles of Distributed Systems (OPODIS 2018), volume 125 of Leibniz International Proceedings in Informatics (LIPIcs), pages 28:1–28:16, Dagstuhl, Germany, 2019. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2018.28, doi:10.4230/LIPIcs.OPODIS.2018.28.

7

Andreas Haas, Thomas A. Henzinger, Andreas Holzer, Christoph M. Kirsch, Michael Lippautz, Hannes Payer, Ali Sezgin, Ana Sokolova, and Helmut Veith. Local Linearizability for Concurrent Container-Type Data Structures. In Josée Desharnais and Radha Jagadeesan, editors, 27th International Conference on Concurrency Theory (CONCUR 2016), volume 59 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1–6:15, Dagstuhl, Germany, 2016. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/entities/ document/10.4230/LIPIcs.CONCUR.2016.6, doi:10.4230/LIPIcs.CONCUR.2016.6.

8

Eashan Hatti, Arthur Oliveira Vale, Zhongye Wang, Yueyang Feng, and Zhong Shao. A Complete Program Logic for Compositional Linearizability. In Robbert Krebbers and Alexandra Silva, editors, 40th European Conference on Object-Oriented Programming (ECOOP 2026), volume 372 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1–11:28, Dagstuhl, Germany, 2026. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https: //drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.11, doi:10.4230/ LIPIcs.ECOOP.2026.11.

9

Nir Hemed, Noam Rinetzky, and Viktor Vafeiadis. Modular verification of concurrency-aware linearizability. In Lecture Notes in Computer Science, Volume 9363, DISC 2015, page 371–387, Berlin, Heidelberg, 2015. Springer-Verlag. doi:10.1007/978-3-662-48653-5_25.

10

Maurice Herlihy and Nir Shavit. The Art of Multiprocessor Programming. Morgain Kaufmann Publishers, 2008. doi:10.5555/1734069.

11

Maurice P. Herlihy and Jeannette M. Wing. Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3):463–492, July 1990. doi: 10.1145/78969.78972.

12

L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput., 28(9):690–691, September 1979. doi:10.1109/TC.1979. 1675439.

13

Jepsen LLC. Snapshot isolation. https://jepsen.io/consistency/models/ snapshot-isolation, 2026. Accessed: 2026-09-06.

14

Gil Neiger. Set-linearizability. In Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing, PODC ’94, page 396, New York, NY, USA, 1994. Association for Computing Machinery. doi:10.1145/197917.198176.

15

Arthur Oliveira Vale, Zhong Shao, and Yixuan Chen. A compositional theory of linearizability. Proc. ACM Program. Lang., 7(POPL), January 2023. doi:10.1145/3571231.

16

Arik Rinberg and Idit Keidar. Intermediate value linearizability: A quantitative correctness criterion. J. ACM, 70(2), April 2023. doi:10.1145/3584699.

XX:17

XX:18

Substep Linearizability: Relaxing Atomicity While Preserving Sequential Specification

17

William Schultz and Murat Demirbas. Design and modular verification of distributed transactions in mongodb. Proc. VLDB Endow., 18(12):5045–5058, August 2025. doi: 10.14778/3750601.3750626.

A

Additional X-CCorrectness Forms

A.1

Set Linearizability

Set linearizability [14] was proposed by Neiger as an extension to classic linearizability that allows multiple operations to be linearized at the same point. Operations sharing the same point can be evaluated together non-atomically. It is subsumed by interval linearizability, but we define it here as another demonstration of X-CCorrectness. In this case, f (H) is a sequence of sets of operations O1 , ..., On such that: [ O1 , ..., On ∈ f (H) iff (ops(H) = Ox x∈1..n

∧ ∀x ∈ {1..n} : ∀o, o′ ∈ Ox : ¬(o <H o′ ∨ o′ <H o) ∧ ∀x, y ∈ {1..n} : (Ox ∩ Oy = ∅ ∧ x < y =⇒ ∀ox ∈ Ox , oy ∈ Oy : ¬(ox <H oy ))) The definition above is equivalent to these rules: Every operation o ∈ ops(H) appears in exactly one set O. All operations in the same set must be concurrent (no pairs may be related by <H ). Operations in an earlier set may not happen-after any operation in a later set. P (O1 , ..., On ) is a set-sequential specification, which might be modeled as a state machine accepting transitions labeled by any set of operations O.

A.2

Sequential Consistency

Sequential consistency [12] (Sequential-CCorrectness by our terminology) is a foundational correctness condition for concurrent objects proposed by Lamport. Similar to linearizability, operations are mapped to a sequential history, however sequential consistency only requires happens-before ordering between operations with the same process id. Let pid(oi ) return the process id of operation oi . f (H) is defined such that:

o1 , ..., on ∈ f (H) iff ∀x, y ∈ 1..n : (x < y ∧ pid(ox ) = pid(oy )) =⇒ ¬(ox >H oy ) P (o1 , ..., on ) accepts valid sequences of atomic operations applied to the underlying object. However, f (H) is more permissive, and fails condition 2 of Theorem 7. ▶ Proposition 12. Sequential consistency is not composable. Proof. Consider a history of four operations o1 , o2 , o3 , o4 such that obj(o1 ) = obj(o4 ) = A, obj(o2 ) = obj(o3 ) = B, pid(o1 ) = pid(o2 ) = 1, pid(o3 ) = pid(o4 ) = 2, o1 <H o2 and o3 <H o4 . By definition, f (H|A ) includes the sequence (o4 , o1 ) and f (H|B ) includes (o3 , o2 ). However, due to the happens-before ordering of H, there does not exist a sequence S ∈ F (H) such that S|A = (o4 , o1 ) and S|B = (o3 , o2 ). By Theorem 7, H is not composable which implies that sequential consistency is not composable. ◀

F. Hackett, E. Wrench, I. Beschastnikh, and Y. Wei

A.3

Quiescent Consistency

Quiescent consistency is similar to sequential consistency and classical linearizability in that it requires that a permutation of the operations in the original history satisfy some predicate. However, it only prohibits reordering of operations oa , ob if they act on the same object and are separated by a period of “quiescence” where the object has no pending operations, i.e. a point where all invoked operations have responded. Formally, define: IsQ(oa , ob , H) iff obj(oa ) = obj(ob ) = A ∧ ∃o ∈ H|A : res(oa ) ≤H|A res(o) <H|A inv(ob ) ∧ (¬∃o′ ∈ H|A : inv(o′ ) <H|A res(o) <H|A res(o′ )) With a ≤H b being shorthand for a = b ∨ a <H b. If this predicate is satisfied, then we must have that any sequence generated orders oa before ob . Thus, f (H) returns all permutations of the operations in the original history such that: o1 , ..., on ∈ f (H) iff ∀x, y ∈ 1..n : x < y =⇒ ¬IsQ(oy , ox , H) Then we have that P (o1 , ..., on ) checks if this sequence satisfies the sequential specification of each object. Using Theorem 7, we can easily show that quiescent consistency is composable. ▶ Proposition 13. Quiescent consistency is composable. Proof. First note that by definition of IsQ, obj(oa ) = obj(ob ) = A =⇒ (IsQ(oa , ob , H) iff IsQ(oa , ob , H|A )). Thus, by definition of quiescent consistency, for any sequence S composed of operations on objects A and B, S|A ∈ f (H|A ) ∧ S|B ∈ f (H|B ) ⇐⇒ S ∈ f (H). Therefore, we have that ∀S ∈ f (H) : (∃SA ∈ f (H|A ) : SA ≤p S|A ) ∧ (∃SB ∈ f (H|B ) : SB ≤p S|B ) and ∀SA ∈ f (H|A ), SB ∈ f (H|B ) : ∃S ∈ f (H) : S|A ≤p SA ∧ S|B ≤p SB . By Theorem 7, this implies that quiescent consistency is composable. ◀

XX:19

Related documents

• Substep Linearizability: Relaxing Atomicity While Preserving Sequential Specification#1327689
• Status report of a scalable data taking system at a test beam for LHC#1056755
• Linear complexity#780514
• Hybrid Adaptive Tuning for Tiered Memory Systems#13182
• Do transposable elements have functions of their very own?#72411