On the Limits of Causal Observation in Shared-Memory Systems Gilde Valeria Rodríguez # Posgrado en Ciencia e Ingeniería de la Computación, Universidad Nacional Autónoma de México, Mexico
Armando Castañeda # Instituto de Matemáticas, Universidad Nacional Autónoma de México, Mexico
Miguel Piña # Independent research, México
arXiv:2606.14093v1 [cs.DC] 12 Jun 2026
Abstract Determining whether one concurrent operation completed before another began is a fundamental prerequisite for reasoning about the correctness of concurrent systems. We formalize this challenge as the Causal Observability Problem (COP): assign timestamps to the observable boundary events of a concurrent execution—invocations and responses—that faithfully reflect real-time operation order. A solution is complete if it never misses a genuine precedence, and sound if it never reports a spurious one. We prove that a strongly consistent solution, one that is simultaneously complete and sound, is unachievable at the observable boundary. We then show that the placement of instrumentation events relative to operation boundaries deterministically governs what a monitor can guarantee: internal placement yields completeness, external placement yields soundness, and neither achieves both. This dichotomy holds independently of the underlying timestamp mechanism. We instantiate this framework with three non-blocking implementations of a Causal Monitor object: FAInc (centralized atomic counter), Striped (decentralized counter), and Collect (iterative register snapshot). FAInc and Striped are linearizable; Collect is only quiescently consistent. Despite this internal consistency gap, we prove that all three provide identical COP guarantees: placement alone determines observable behavior. We validate these claims empirically on a 64-core NUMA architecture, showing that Striped matches Collect in throughput while preserving linearizability, resolving the cache-contention bottleneck of FAInc at high thread counts. 2012 ACM Subject Classification Theory of computation; Theory of computation → Distributed computing models; Theory of computation → Distributed algorithms; Theory of computation → Concurrency; Theory of computation → Concurrent algorithms Keywords and phrases Causality, Linearizability, Quiescent Consistency, Causal Observability
Contents 1 Introduction
2
2 Model
4
3 The Causal Observability Problem 3.1 Observable Events and Lamport Causality . . . . . . . . . . . . . . . . . . . . 3.2 The Problem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.3 The Gap Between <H and ≺L Eobs . . . . . . . . . . . . . . . . . . . . . . . . .
5 6 6 7
4 The Interface Event Layer 4.1 Interface Events and Monitors . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.2 The Placement Dichotomy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.3 Impossibility of Strong Consistency . . . . . . . . . . . . . . . . . . . . . . . .
7 8 8 8
2
On the Limits of Causal Observation in Shared-Memory Systems
5 The Causal Monitor Object
9
6 Implementations 9 6.1 Counter Monitor . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 6.2 Collect Monitor . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 7 Correctness 7.1 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7.2 Consistency of the Collect Monitor . . . . . . . . . . . . . . . . . . . . . . . . 7.3 Both monitors solve the same problem . . . . . . . . . . . . . . . . . . . . . .
11 11 12 13
8 Empirical Evaluation 13 8.1 RQ1: Verdict Consistency . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 8.2 RQ2: Scalability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 9 Related Work
15
10 Discussion and Further Work
16
A Placement Cases
18
B Proof of Theorem 12
20
C Linearizability of the Striped Counter
21
D Proof of Lemma 17
22
E Proof of Theorem 18
23
F Proof of Theorem 19
24
1
Introduction
Determining whether a concurrent system is correct requires observing its execution. But in asynchronous shared-memory systems, observation is fundamentally limited: an external monitor can only see the boundaries of operations — their invocations and responses — not the internal memory accesses that determine their real-time order. This gap between what a monitor can observe and what correctness requires is the central challenge of runtime verification of linearizability [2, 19]. Linearizability requires that every operation appear to take effect at some point between its invocation and response, preserving the real-time order <H of non-overlapping operations [11]. Tracking <H is notoriously difficult: real-time precedence can exist between operations on different processes with no underlying information flow between them. Because asynchronous processes have no access to a physical clock, causality-tracking techniques based on Lamport timestamps [13] or vector clocks [6, 16] cannot capture it — they track information flow, not elapsed time. It has been shown that any monitor restricted to the observable boundary faces a fundamental impossibility [2, 3]: no protocol can simultaneously be complete (capturing every genuine real-time precedence) and sound (reporting only genuine ones). Any monitor that tries must either miss precedences or report spurious ones.
G. V. Rodríguez, A. Castañeda, M. Piña
We formalize this limitation as the Causal Observability Problem (COP): assign timestamps to the observable boundary events — invocations and responses — that faithfully reflect <H . We prove that strong consistency, meaning both completeness and soundness simultaneously, is unachievable at this boundary. We then ask what is achievable, and show that the answer depends entirely on a single structural decision: where the monitor places its instrumentation relative to the true operation boundaries. We study the instrumentation strategies used by existing monitors in the literature [2, 3, 18, 5] and identify a placement dichotomy that explains their guarantees. Monitors that instrument operations by writing events into shared memory before invoking and after completing each operation — enclosing the true interval from outside — yield a sound monitor: every reported precedence is genuine. Monitors that write events after the operation starts and before it finishes — strictly inside the true interval — yield a complete monitor: every genuine precedence is captured. Monitors that instrument only one boundary, rather than both, are neither sound nor complete [5]. This dichotomy is tight: no placement achieves both simultaneously, as we prove via an indistinguishability argument that holds regardless of the shared-memory objects used for instrumentation. To implement sound monitors without blocking bottlenecks under high contention, we analyze three non-blocking implementations. The first uses a shared counter. FAInc, a centralized atomic increment introduced in [18], is linearizable. Striped, a decentralized counter built on Java’s LongAdder restricted to increment-only operations, is introduced in this work and is linearizable. The restriction to increments is essential: it preserves the monotonicity argument on which linearizability depends. The second implementation, Collect, reads a snapshot of process registers iteratively [18] and is only quiescently consistent. The consistency properties of FAInc and Collect with respect to the Causal Monitor specification were not established in [18], nor were the two distinguished from each other. A key result of this paper is that while Collect is not linearizable and both counters are, all three provide identical COP guarantees: placement alone determines what the problem guarantees, and the internal consistency of the timestamp mechanism does not. We validate this empirically on a 64-core NUMA architecture. Prior work [19] showed that Collect outperforms FAInc in scalability; we show here that Striped is a linearizable counter that matches Collect in throughput while eliminating the cache-contention collapse of FAInc at high thread counts.
Contributions 1. Formalization of the observability limit. We define COP at the observable boundary of a concurrent object and prove that strong consistency is unachievable there, making precise the impossibility identified informally in [2, 19]. 2. Placement dichotomy. We analyze the instrumentation strategies of existing monitors and prove that placement — internal or external — determines the soundness and completeness profile of any monitor, independently of the underlying timestamp algorithm. 3. Consistency analysis of the Causal Monitor. We establish the consistency properties of the Counter Monitor (linearizable) and the Collect Monitor (quiescently consistent but not linearizable) with respect to the Causal Monitor sequential specification, a result absent from [18]. 4. COP invariance. We prove that all implementations are equivalent with respect to COP: the internal consistency gap between linearizability and quiescent consistency is invisible at the observable boundary.
3
4
On the Limits of Causal Observation in Shared-Memory Systems
5. Scalable linearizable implementation. We introduce Striped, a new linearizable implementation of the Causal Monitor, and show empirically that it matches the scalability of Collect and eliminates the contention bottleneck of FAInc. Prior work [19] established that Collect outperforms FAInc; Striped shows that a linearizable monitor can achieve the same scalability advantage. Section 2 presents the system model. Section 3 defines COP and proves the impossibility of strong consistency. Section 4 analyzes the placement strategies of existing monitors and proves the completeness and soundness characterization. Section 5 specifies the Causal Monitor object. Section 6 presents the Counter and Collect implementations. Section 7 contains the correctness proofs and the COP invariance result. Section 8 presents the empirical evaluation. Section 9 discusses related work.
2
Model
We consider N processes p1 , . . . , pN that run asynchronously and communicate via an atomic shared-memory model [11]. Shared-memory systems are organized around objects. An object is a shared data structure that supports a set of operations; processes interact with the system exclusively by invoking operations on objects and receiving their responses. Each object has an abstract type T , which names its operations and, together with a specification, defines their legal behaviors [11]. An operation is a pair consisting of an invocation inv(op), issued when a process calls the operation, and a matching response res(op), returned when the call completes. An operation is pending if its invocation has occurred but its response has not yet been received. We consider that each event takes effect instantaneously at a single point in time; no two events are simultaneous. We write e ≺ f if event e occurs before event f in real time. This assumption is a property of the model — namely, that the underlying memory is atomic [11]. A history H is a finite sequence of invocation and response events. We say H is wellformed if every response is preceded by a matching invocation; sequential if every invocation is immediately followed by its matching response with no interleaving; and complete if no invocation is pending. The real-time order <H on the operations of H is defined by op1 <H op2 ⇐⇒ res(op1 ) ≺ inv(op2 ). Two operations are concurrent when neither precedes the other: op1 ∥ op2 ⇐⇒ ¬(op1 <H op2 ) ∧ ¬(op2 <H op1 ). The behavior of an object of type T is described by a sequential specification. ▶ Definition 1 (Sequential specification [11]). The sequential specification of type T is a prefix-closed set Seq(T ) of sequential histories over the operations of T . A sequential history S is legal if S ∈ Seq(T ). The specification Seq(T ) thus determines which sequences of operations, each completing before the next begins, constitute valid behaviors of T . Intuitively, Seq(T ) describes what the object is supposed to do when its operations are called one at a time. A correctness condition then relates the concurrent histories produced by an implementation to this sequential ideal, Linearizability being the most well-known such condition. ▶ Definition 2 (Linearizability [11]). An implementation of type T is linearizable with respect to Seq(T ) if for every well-formed history H it produces there exists a legal sequential history S ∈ Seq(T ) such that: (L1) S is equivalent to some completion of H — pending operations may be dropped or completed, and
G. V. Rodríguez, A. Castañeda, M. Piña
(L2) op1 <H op2 in H implies op1 <S op2 . Condition (L2) is the real-time order condition: a linearizable implementation must respect the physical execution order of non-overlapping operations. Linearizability is equivalent to assigning each operation op a linearization point LP(op) ∈ [inv(op), res(op)] such that the sequential history obtained by ordering operations by their linearization points is legal. Sequential consistency [12] occupies an intermediate position in the hierarchy: it is weaker than linearizability, since it drops the real-time order requirement across processes, yet stronger than quiescent consistency, since it preserves the per-process program order at all times, not only across quiescent instants. ▶ Definition 3 (Sequential consistency [12]). An implementation of type T is sequentially consistent with respect to Seq(T ) if for every well-formed history H it produces there exists a legal sequential history S ∈ Seq(T ) such that: (SC1) S is equivalent to some completion of H: every completed operation appears in S, and pending operations may be dropped or completed; and (SC2) S respects program order: for each process pi , the operations of pi appear in S in the same order as in H. In high-contention concurrent systems, maintaining the real-time order of non-overlapping operations imposes a significant synchronization cost. Quiescent Consistency (QC) [10] addresses this by relaxing the real-time order requirement: rather than ordering all nonoverlapping operations, it requires only that operations separated by a period of complete system inactivity be ordered relative to one another. We first recall the relevant notions of quiescence [10]. A quiescent instant is a real-time instant at which no operation is pending. A quiescent interval is any open interval (Qk , Qk+1 ) between two consecutive quiescent instants Qk and Qk+1 . The operations that execute entirely within the k-th quiescent interval form the quiescent group Gk . Two operations are separated by quiescence if they belong to different groups: op1 ∈ Gk and op2 ∈ Gk′ with k ̸= k ′ . ▶ Definition 4 (Quiescent consistency [10]). An implementation of type T is quiescently consistent with respect to Seq(T ) if for every well-formed history H it produces there exists a legal sequential history S ∈ Seq(T ) equivalent to some completion of H such that: if res(op1 ) ≺ Q ≺ inv(op2 ) for some quiescent instant Q, then op1 <S op2 . Operations within the same quiescent group may be reordered freely, provided the result is legal. The three conditions are strictly ordered by strength. Neither implication reverses [11, 10], yielding the strict containment:Linearizable ⊊ Sequentially Consistent ⊊ Quiescently Consistent.
3
The Causal Observability Problem
In a concurrent execution, an external client observes only the boundaries of operations — their invocations and responses — and uses this information to reason about the order in which operations executed. The client’s goal is to determine the real-time order <H : whether one operation completed before another began. A timestamping protocol runs inside the system, on the processes themselves, and assigns timestamps to boundary events so that the client can answer order queries by comparing timestamps. The protocol has access to the flow of information through shared memory — it can observe Lamport causality ≺L — but it cannot directly observe the true operation
5
6
On the Limits of Causal Observation in Shared-Memory Systems
boundaries, which are transfers of control rather than shared-memory steps. The central question is whether a protocol can assign timestamps that faithfully reflect <H using only what it can observe.
3.1
Observable Events and Lamport Causality
Recall from Section 2 that an execution produces a history H: a sequence of invocation and response events over the processes p1 , . . . , pN . The observable boundary is the set of events in H: Eobs ≜ inv(op), res(op) op ∈ H . These are the events the client observes: when each operation starts and when it finishes. They are also the events to which the protocol must assign timestamps — the domain of the problem. The order the protocol must report is the real-time order <H of Section 2. Since opA <H opB holds exactly when res(opA ) ≺ inv(opB ), this is already a relation on boundary events: it links the response of one operation to the invocation of a later one. The order the protocol can construct from shared memory is Lamport’s happenedbefore [13]. ▶ Definition 5 (Lamport causality, ≺L ). ≺L is the smallest transitive relation over the events of an execution such that: (L1) Program order: if e1 and e2 occur at the same process and e1 ≺ e2 , then e1 ≺L e2 . (L2) Object communication: if e1 is an operation on a shared object O whose effect is observable by e2 — that is, the state change produced by e1 influences the response of e2 —then e1 ≺L e2 (e.g., e1 writes to O and e2 reads from O). (L3) Transitivity: if e1 ≺L e2 and e2 ≺L e3 , then e1 ≺L e3 . In the special case where shared objects are read/write registers, condition (L2) reduces to the standard read-from relation: e1 writes a value to register r and e2 reads that value from r. L Restricted to Eobs , we write ≺L Eobs for the relation ≺ induced on boundary events. Vector L L clocks [6, 16] reconstruct ≺Eobs exactly: e1 ≺ e2 ⇐⇒ vc(e1 ) < vc(e2 ). However, as we show below, ≺L Eobs is not the relation the protocol needs to report.
3.2
The Problem
Let (T, <T ) be a totally ordered set. A timestamping protocol assigns ts(e) ∈ T to each e ∈ Eobs . The client then answers a precedence query by checking whether ts(res(opA )) <T ts(inv(opB )). ▶ Definition 6 (Causal Observability Problem, COP). The Causal Observability Problem asks for a timestamping protocol assigning ts(e) ∈ T to each e ∈ Eobs such that, for all operations opA , opB : (i) Completeness: opA <H opB ⇒ ts(res(opA )) <T ts(inv(opB )). (ii) Soundness: ts(res(opA )) <T ts(inv(opB )) ⇒ opA <H opB . A protocol satisfying only (i) is complete; one satisfying only (ii) is sound; one satisfying both is strongly consistent. Both conditions are stated directly in terms of <H : the protocol’s timestamps must faithfully reflect real-time operation order, not merely information flow. Completeness forbids missing a genuine precedence: if opA truly completed before opB began, the timestamps must reflect that. Soundness forbids reporting a spurious precedence:
G. V. Rodríguez, A. Castañeda, M. Piña
if the timestamps say opA preceded opB , then opA must have truly completed before opB began. A strongly consistent protocol does both: its timestamp order is equivalent to <H . Note that soundness does not require timestamps to imply precedence for concurrent operations — two concurrent operations will inevitably be ordered by any total order on T, and that is acceptable. What soundness prohibits is asserting a precedence that did not occur in real time.
3.3
The Gap Between <H and ≺LEobs
The order the protocol must report, <H , and the order it can construct, ≺L Eobs , both live on Eobs . They are, however, incomparable as relations. L ▷ Claim 7. <H ̸⊆ ≺L Eobs and ≺Eobs ̸⊆ <H .
Proof. <H ̸⊆≺L Eobs . Let op A complete at pi before op B begins at pj , with no register written by pi during opA subsequently read by pj . Then res(opA ) ≺ inv(opB ), so opA <H opB , yet no ≺L -chain links res(opA ) to inv(opB ): time elapsed, but no information was exchanged. ≺L Eobs ̸⊆ <H . Let op A and op B overlap (op A ∥ op B ), and let pi write a register during opA that pj reads during opB . By (L1) and (L2), inv(opA ) ≺L Eobs res(op B ), yet op A ∥ op B means neither opA <H opB nor opB <H opA . ◀ The two failures have distinct causes. <H sees real-time precedences that leave no informational trace: one operation finishes before another begins, but the processes never communicate. ≺L Eobs sees informational chains that carry no real-time precedence: concurrent operations can exchange information through shared registers without one completing before the other starts. This incomparability explains why vector clocks do not solve COP: they reconstruct L ≺L Eobs exactly, but that is not <H . A protocol that tracks ≺Eobs will miss real-time precedences that left no informational trace, violating completeness. A protocol that reports every <H precedence may assign timestamps that contradict ≺L Eobs , violating soundness. The following section shows that no protocol can be strongly consistent for COP: completeness and soundness are irreconcilable at Eobs .
4
The Interface Event Layer
Section 3 showed that the order a protocol must report (<H ) and the order it can construct from shared memory (≺L Eobs ) are incomparable. A protocol that wants to approximate <H L must construct ≺Eobs by invoking shared-memory objects around the operation boundaries it wants to observe, using the causal relationships among those invocations as a proxy for real-time order. We now show that the position of those invocations relative to the true boundaries determines exactly what the protocol can guarantee, and that no position achieves both soundness and completeness simultaneously. We study the instrumentation strategies used by existing monitors [2, 3, 18, 5] and identify two classes. Monitors that invoke objects only at one boundary are neither sound nor complete [5] (Lemma 20, Appendix A). Monitors that invoke objects at both boundaries fall into one of two classes: those whose invocations fall strictly inside the operation interval (internal placement) and those whose invocations strictly enclose it (external placement). Internal placement yields completeness; external placement yields soundness (Lemmas 11, 21, and 22, Appendix A). No combination achieves both (Theorem 12, Appendix B).
7
8
On the Limits of Causal Observation in Shared-Memory Systems
4.1
Interface Events and Monitors
A protocol that monitors COP cannot observe the true boundaries inv(op) and res(op) directly: these mark the transfer of control between a process and its caller, and are not steps in shared memory. The only tool available is to invoke shared-memory objects around those boundaries, producing observable actions whose causal relationships reconstruct ≺L Eobs . ▶ Definition 8 (Monitor). A monitor for COP is a protocol that, for each operation op, invokes a finite set of shared-memory objects before and after each true boundary, producing observable actions called interface events. The monitor answers Precedes(A, B) = true iff L c the interface events establish res(()op c A ) ≺ inv(()op B ). We place no restriction on what objects the monitor may invoke: interface events may be operations on objects of any type, including objects with infinite consensus number [9]. The obstacle is not the synchronization power of the objects but the position of their invocations relative to the true boundaries. We assume every shared-memory operation takes effect at a single linearization point, formalized through an ideal log. ▶ Definition 9 (Ideal log). A monitor operates under an ideal log if every interface event e has a linearization point lp(e) such that: e1 ≺L e2 ⇐⇒ lp(e1 ) ≺ lp(e2 ). An ideal log grants the monitor perfect knowledge of the real-time order among its own interface events. Any impossibility result under an ideal log is unconditional: it cannot be attributed to imprecision in logging or to the choice of objects invoked. Because what matters for a precedence query is the last interface event before res(op) and the first after inv(op), intermediate events carry no additional causal information. Without loss of generality, we model each monitor as emitting exactly one interface event per boundary: c inv(()op) and res(()op). c
4.2
The Placement Dichotomy
Under an ideal log, each interface event and each true boundary occur at distinct points in real time, since interface events are shared-memory invocations and true boundaries are control transfers. This forces every monitor that instruments both boundaries into one of two classes. c ▶ Definition 10 (Placement). A monitor has internal placement if inv(op) ≺ lp(inv(()op)) c and lp(res(()op)) c ≺ res(op), and external placement if lp(inv(()op)) ≺ inv(op) and res(op) ≺ lp(res(()op)). c Internal placement corresponds to online checkers that instrument the object’s internal steps [2]. External placement corresponds to offline verifiers that wrap each call site [3]. ▶ Lemma 11 (Placement characterization). Assuming an ideal log, a monitor with internal placement is complete for COP, and a monitor with external placement is sound. Neither achieves the other property. See Appendix A for the full proof.
4.3
Impossibility of Strong Consistency
▶ Theorem 12 (Impossibility of strong consistency). No monitor can be strongly consistent for COP, even with an ideal log.
G. V. Rodríguez, A. Castañeda, M. Piña
Proof sketch. Fix any monitor M and two operations opA , opB on distinct processes. Since interface events are shared-memory invocations and true boundaries are control transfers, they can never coincide, forcing an open real-time window around each boundary inside which the true boundary can move without altering any interface event or its position in the log. Because the processes are asynchronous, an adversary can schedule their steps so that the two windows overlap. Inside the overlap, two executions identical in every shared-memory step — producing identical ≺L Eobs under any ideal log — can place res(op A ) ≺ inv(op B ) (requiring Precedes(A, B) = true) or inv(opB ) ≺ res(opA ) (requiring Precedes(A, B) = false). No single answer satisfies both. See Appendix B for the full proof. ◀ This impossibility was first identified in [2, 3] as a structural limitation of runtime verification of linearizability. Theorem 12 shows it is an unconditional consequence of the observable boundary of any concurrent object, independent of the verification algorithm and of the shared-memory objects the monitor invokes.
5
The Causal Monitor Object
The Causal Monitor is a concurrent object that instruments a target algorithm A. Processes invoke Add_Inv(id) at the start of each operation and Add_Res(id) at its end, creating the interface events of Section 4. Clients query the monitor via Precedes to determine whether one completed operation preceded another in real time. The sequential specification defines the ideal behavior of the monitor. The key design decision is that Precedes(A, B) checks whether A’s response record appears before B’s invocation record in the log, directly mirroring the definition of <H . Queries require both response records to be present, since <H is only defined for completed operations. ▶ Definition 13 (Causal Monitor — Sequential Specification). Let I be a universe of operation identifiers. The abstract state is a sequence S ∈ ({I, R} × I)∗ , initially empty; idx(e, S) denotes the position of e in S, or ∞ if absent. Modification. Add_Inv(id) requires (I, id) ∈ / S and appends (I, id). Add_Res(id) requires (I, id) ∈ S and (R, id) ∈ / S, and appends (R, id). Queries (both require (R, id A ), (R, id B ) ∈ S; state unchanged). Precedes(id A , id B ) returns true iff idx((R, id A ), S)idx((I, id B ), S). Concurrent(id A , id B ) returns true iff ¬ Precedes(id A , id B ) ∧ ¬ Precedes(id B , id A ).
6
Implementations
We present two implementations of the Causal Monitor. The first uses a shared counter and is linearizable. The second uses an iterative collect of process registers and is only quiescently consistent. Despite this internal difference, Section 7 shows that both resolve COP with identical external guarantees: under external placement, both are sound, and neither can be complete (Theorem 12). The placement of interface events determines what COP guarantees a monitor provides; the internal consistency of the timestamp mechanism does not. Both implementations were introduced in [18] as practical monitoring tools. However, [18] did not establish their consistency properties with respect to the Causal Monitor sequential specification, nor did it recognize that the two mechanisms provide the same COP guarantees despite their internal differences. That analysis is a contribution of the present work.
9
10
On the Limits of Causal Observation in Shared-Memory Systems
6.1
Counter Monitor
The Counter Monitor assigns each interface event a numeric timestamp read from a shared counter C. Precedence reduces to integer comparison: Precedes(A, B) holds iff the timestamp of A’s response is strictly less than the timestamp of B’s invocation. We consider two variants, formalized in Algorithm 1. FAInc reads the counter with a single atomic getAndIncrement, producing distinct timestamps in real-time order. Striped uses a striped counter structured as an array of per-process cells (analogous to Java’s LongAdder [14]), where each process increments its own cell and reads the global sum nonatomically. This eliminates the cache-line contention of a centralized atomic counter at the cost of allowing two concurrent events to receive the same timestamp. Algorithm 1 Counter-based Causal Monitor
Shared: Reg[1 . . . N ] (SWMR, append-only); counter C Parameter: Mode ∈ {FAInc, Striped} 1: function Stamp 2: if Mode = FAInc then 3: return C.getAndIncrement() ▷ single atomic step 4: else 5: C.increment() 6: return C.sum() ▷ non-atomic: increment own cell, read all cells 7: end if 8: end function 9: procedure Add_Inv(id) 10: t ← Stamp(); Reg[i] ← Reg[i] · ⟨(I, id, t)⟩ 11: end procedure 12: procedure Add_Res(id) 13: t ← Stamp(); Reg[i] ← Reg[i] · ⟨(R, id, t)⟩ 14: end procedure 15: function Precedes(id A , id B ) 16: tA ← timestamp stored with (R, id A ) 17: tB ← timestamp stored with (I, id B ) 18: return tA < tB 19: end function
▶ Proposition 14 (Counter Monitor is linearizable). Both FAInc and Striped produce linearizable executions of the Causal Monitor. Proof. FAInc. The linearization point of each Add_Inv or Add_Res call is the atomic getAndIncrement instruction. Timestamps are strictly increasing in real time, so the sequential history ordered by timestamp satisfies the specification. Striped. See Appendix C. ◀ The FAInc counter was introduced in [18] grouped with the Collect monitor (Algorithm 2) as a variant of the same approach. Striped is introduced in this work and was first described in [14]. We show in Section 7 that this grouping was imprecise: both counters are linearizable, whereas Collect is only quiescently consistent. All three are sound for COP under external placement, but they are not equivalent as concurrent objects.
G. V. Rodríguez, A. Castañeda, M. Piña
6.2
Collect Monitor
The Collect Monitor keeps the state explicit. On Add_Res, the calling process reads all process registers iteratively — a non-atomic collect — and stores the resulting view v alongside the response event. Precedence is then a membership test on stored views. Algorithm 2 Collect-based Causal Monitor
Shared: Reg[1 . . . N ] (SWMR, append-only sequences of events) 1: procedure Add_Inv(id)
Reg[i] ← Reg[i] · ⟨(I, id)⟩ 3: end procedure 4: procedure Add_Res(id) SN 5: v ← j=1 Reg[j] ▷ iterative, non-atomic read 6: Reg[i] ← Reg[i] · ⟨(R, id, v)⟩ 7: end procedure 8: function Precedes(id A , id B ) 9: vA ← view stored with (R, id A ) 10: vB ← view stored with (R, id B ) 11: return [(R, id A ) ∈ vB ] ∧ [(I, id B ) ∈ / vA ] ∧ [vA ⊆ vB ] 12: end function 2:
The first two conjuncts capture precedence directly: A’s response was visible when B’s collect ran, and B’s invocation was not yet visible when A’s collect ran. The third conjunct, vA ⊆ vB , is needed for transitivity: without it, concurrent collects may produce incomparable views that break transitivity of the reported order. Its role is purely structural and does not affect soundness.
7
Correctness
This section establishes two independent facts. First, both monitors are sound for COP under external placement (Theorems 15 and 16): whenever a monitor reports Precedes(A, B) = true, the operation opA genuinely completed before opB began in real time, i.e. opA <H opB . Second, the Counter Monitor is linearizable (Proposition 14) while the Collect Monitor is quiescently consistent but not linearizable (Theorems 19 and 18). The main consequence is that the internal consistency gap between the two monitors is invisible at the level of COP: placement alone determines what the problem guarantees.
7.1
Soundness
▶ Theorem 15 (Counter Monitor is sound for COP). Under external placement, Algorithm 1 is sound: Precedes(A, B) = true ⇒ opA <H opB . Proof. Precedes(A, B) = true means tA < tB , where tA is the timestamp stamped during Add_Res(A) and tB is the timestamp stamped during Add_Inv(B). In both FAInc and Striped, timestamps are monotone in real time: a strictly smaller timestamp means the corresponding Stamp call completed before the other began. Let σA be the linearization point of the Stamp call inside Add_Res(A), and σB the linearization point of the Stamp call inside Add_Inv(B). Then tA < tB implies σA ≺ σB .
11
12
On the Limits of Causal Observation in Shared-Memory Systems
External placement gives res(opA ) ≺ σA , since Add_Res(A) is invoked after opA returns and σA lies within Add_Res(A)’s execution interval. Similarly, σB ≺ inv(opB ), since Add_Inv(B) is invoked before opB starts and σB lies within Add_Inv(B)’s execution interval. Chaining, res(opA ) ≺ σA ≺ σB ≺ inv(opB ), so res(opA ) ≺ inv(opB ), i.e. opA <H opB .
◀
▶ Theorem 16 (Collect Monitor is sound for COP). Under external placement, Algorithm 2 is sound: Precedes(A, B) = true ⇒ opA <H opB . Proof. Suppose Precedes(A, B) = true. The predicate has three conjuncts; we use only the second: (I, id B ) ∈ / vA . This means that when A’s collect read Reg[proc(B)], the write of (I, id B ) had not yet occurred. Let ρ be the physical time of that read and wI the physical time of the write of (I, id B ); then ρ ≺ wI . External placement gives two facts. First, Add_Res(A) is invoked after opA returns, so res(opA ) ≺ inv(Add_Res(A)); since ρ occurs during Add_Res(A)’s collect, res(opA ) ≺ ρ. Second, Add_Inv(B) is invoked before opB starts, so the write wI of (I, id B ), which occurs inside Add_Inv(B), satisfies wI ≺ inv(opB ). Chaining, res(opA ) ≺ ρ ≺ wI ≺ inv(opB ), so res(opA ) ≺ inv(opB ), i.e. opA <H opB .
◀
This proof uses only the conjunct (I, id B ) ∈ / vA . The first conjunct (R, id A ) ∈ vB and the view-containment conjunct vA ⊆ vB play no role in soundness. Their purpose is structural: the first contributes to detecting precedence, and the second restores transitivity of Precedes, as established in Lemma 17. Soundness holds independently of whether Precedes is transitive.
7.2
Consistency of the Collect Monitor
▶ Lemma 17 (Precedes is a strict partial order under Collect). With the view-containment conjunct, Precedes is irreflexive, antisymmetric, and transitive. Proof sketch. Irreflexivity follows because a collect completes before its own response is written, so (R, A) ∈ / vA . Antisymmetry follows because if Precedes(A, B) then (I, A) ∈ vB , which refutes the conjunct (I, A) ∈ / vB required by Precedes(B, A). Transitivity follows from view-containment: if Precedes(A, B) and Precedes(B, C) then vA ⊆ vB ⊆ vC , from which all three conjuncts of Precedes(A, C) can be derived. See Appendix D for the full proof. ◀ ▶ Theorem 18 (Collect Monitor is not linearizable). Algorithm 2 is not sequentially consistent, hence not linearizable. Proof sketch. We exhibit an execution of four operations A, B, C, D on distinct processes where the collect intervals cross: B observes A’s response but not C’s, while D observes C’s response but not A’s. This yields Precedes(A, B) = Precedes(C, D) = true and Precedes(C, B) = Precedes(A, D) = false, which forces any sequential history to satisfy RA ≺S IB ≺S RC ≺S ID ≺S RA , a cycle. See Appendix E for the full construction. ◀
G. V. Rodríguez, A. Castañeda, M. Piña
▶ Theorem 19 (Collect Monitor is quiescently consistent). Under external placement, Algorithm 2 is quiescently consistent: if a quiescent instant Q satisfies res(opA ) ≺ Q ≺ inv(opB ), then Precedes(A, B) = true. Proof sketch. External placement ensures all of A’s monitor calls complete before Q and all of B’s begin after Q. Since Q is quiescent, A’s response is written before Q and B’s invocation after, so B’s collect observes (R, A) and A’s collect cannot have observed (I, B); view-containment follows from the fact that everything A observed was written before Q, which B also observes. All three conjuncts hold. See Appendix F for the full proof. ◀
7.3
Both monitors solve the same problem
The Counter Monitor is linearizable and the Collect Monitor is only quiescently consistent. Nevertheless, both are sound for COP under external placement, and neither can be complete (Theorem 12). This has a practical consequence identified in [18] but not formally justified there: the Collect Monitor and the FAInc Counter Monitor were presented as variants of the same approach, without distinguishing their consistency properties. We now see that this grouping was correct at the level of COP — both solve the same problem with the same guarantees — but incorrect at the level of the concurrent object: the Counter Monitor is linearizable while the Collect Monitor is not. The COP framework is what makes precise why, despite this difference, they are equivalent for the purpose of causal observation.
8
Empirical Evaluation
The theoretical results of Section 7 establish that the Counter Monitor (FAInc and Striped) and the Collect Monitor solve COP with identical guarantees under external placement, despite their internal consistency difference. We evaluate this claim empirically in the context of runtime verification (RV) of linearizability [19], which provides a concrete setting where COP soundness has a direct operational meaning. In RV of linearizability, a monitor observes the execution of a concurrent object and decides whether the observed history is linearizable [3]. A monitor is RV-complete if it never rejects a genuinely linearizable execution, and RV-sound if it never accepts a non-linearizable one. By Lemma 11, external placement guarantees COP soundness: every reported precedence is real. This means the monitor never introduces false ordering constraints, so a genuinely linearizable execution will never be falsely rejected — both monitors are RV-complete by construction. RV-soundness, however, is not guaranteed: a non-linearizable execution may go undetected if the violation falls inside a concurrent window that the monitor cannot resolve. The comparison between FAInc and Collect was carried out in [18, 19], where Collect was shown to match or outperform FAInc in scalability while providing the same detection behavior. The contribution of the present evaluation is to introduce Striped into this comparison. Striped is a linearizable counter that eliminates the cache-line contention of FAInc by distributing increments across per-process cells. We ask two questions: RQ1 (Verdict consistency): Does Striped detect linearizability violations at the same rate as FAInc, or does its non-atomic sum introduce observable differences in detection behavior? RQ2 (Scalability): Does Striped eliminate the contention bottleneck of FAInc while remaining competitive with Collect?
13
On the Limits of Causal Observation in Shared-Memory Systems Bug Detection Rate for NonLinearizableQueue (100 Runs/Cell) 100
Detection Rate (% False Verdicts)
14
80
60
40
20
0
CounterF&I (Linearizable) Collect (Quiescent) CounterStripped (Linearizable) 2
4
8
16
Number of Threads
32
64
Figure 1 Bug detection rate on NonLinearizableQueue (100 runs per cell). Striped converges to the same detection rate as FAInc at 16 threads and above.
We implemented all three monitors in Java and evaluated them on a 64-core AMD NUMA architecture using the benchmarking methodology of Georges et al. [8] (5 warmup rounds, 10 measured rounds, 100 runs per cell for verdict experiments).
8.1
RQ1: Verdict Consistency
Figure 1 shows the detection rate on a NonLinearizableQueue across thread counts. FAInc reaches 100% detection consistently from low thread counts. Striped starts slightly below FAInc at 2 threads but converges to 100% at 16 threads and remains there. The Collect Monitor lags behind both counters at low thread counts. The minor gap between Striped and FAInc at low concurrency is a direct consequence of the non-atomic sum(): the traversal takes physical time, slightly widening the observed interval of each operation and granting the verifier a marginally larger concurrent window in which violations can be hidden. This is the same mechanism that limits Collect at low concurrency, though Collect’s effect is more pronounced because its widening is proportional to the number of registers read rather than counter cells. As thread contention grows, the widening becomes negligible relative to the actual concurrency in the execution, and Striped converges to FAInc. These results confirm that, in practice, the three monitors are equivalent for the purpose of RV: all are RV-complete, and all achieve equivalent detection rates at realistic thread counts.
8.2
RQ2: Scalability
Figure 2 shows mean execution time and maximum latency at 10,000 operations per thread. Up to 16 threads, all three monitors perform similarly: modern cache coherency protocols mask the contention on the centralized FAInc counter. Beyond 16 threads the difference becomes visible, and at 64 threads FAInc suffers a severe degradation: mean time reaches 700 ms and maximum latency exceeds 1,200 ms, evidencing cache-line bouncing on the centralized atomic counter under maximum hardware concurrency. Striped and Collect remain stable across all thread counts, with mean times near 575 ms and maximum latency near 580 ms at 64 threads. Striped is marginally faster than Collect at low thread counts, where the per-register traversal of Collect adds a small but measurable overhead; at high thread counts the two are effectively indistinguishable.
G. V. Rodríguez, A. Castañeda, M. Piña
15
Mean Execution Time (10,000 Ops)
Monitor CounterF&I (Linearizable) Collect (Quiescent) CounterStripped (Linearizable)
1200
600
Max Execution Time (ms)
Mean Execution Time (ms)
Maximum Latency / Jitter (10,000 Ops)
Monitor CounterF&I (Linearizable) Collect (Quiescent) CounterStripped (Linearizable)
700
500
400
1000
800
600
400
300
2 4
8
16
32
Number of Threads
64
200
2 4
8
16
32
Number of Threads
64
Figure 2 Mean execution time (left) and maximum latency (right) at 10,000 operations per thread. FAInc collapses at 64 threads due to cache-line contention on the centralized counter. Striped and Collect remain stable across all thread counts.
These results answer RQ2 affirmatively: Striped eliminates the scalability bottleneck of FAInc while matching Collect in throughput. Combined with the verdict results of RQ1, the conclusion is that Striped is a strictly better choice than FAInc as a linearizable implementation of the Causal Monitor: it provides the same COP guarantees, the same detection behavior at realistic concurrency, and scales to high thread counts without contention collapse. The comparison with Collect, however, is not one of dominance. Collect was shown in [18, 19] to outperform FAInc precisely because it avoids centralized synchronization. Striped now shows that a linearizable counter can match that performance. The theoretical gap between linearizability and quiescent consistency — which Theorems 18 and 19 make precise — does not translate into a performance gap at the scale tested. Whether the two diverge under more adversarial workloads is left for future work.
9
Related Work
The problem of monitoring linearizability at runtime was studied in [2, 3], where the impossibility of simultaneously achieving soundness and completeness at the observable boundary was identified as a structural limitation. Those works introduced a monitor based on atomic snapshots. A follow-up [18] introduced the Collect Monitor and the FAInc Counter Monitor as more practical tools, presenting both under internal placement and treating them as equivalent implementations. In [19], Collect was shown empirically to outperform FAInc in scalability. The present paper formalizes that limitation as COP, proves the placement dichotomy that explains it, establishes the consistency properties of both monitors with respect to the Causal Monitor sequential specification — showing that the two are not equivalent as concurrent objects, despite solving the same problem — and introduces Striped as a linearizable monitor that matches the scalability of Collect while providing stronger internal consistency guarantees. El-Hoyakem and Falcone [5] proposed a monitor that instruments only one boundary of each operation. As noted in Section 4, such monitors are neither sound nor complete: they do not solve COP. Lowe [15] studied linearizability checking offline, where the full history is available after execution; that setting does not face the observability constraints that define COP.
16
On the Limits of Causal Observation in Shared-Memory Systems
Classical causal monitoring was designed for the message-passing model, where the goal is to reconstruct the flow of information across the entire execution [13, 6, 16, 21, 17]. In the terminology of this paper, those tools address a different instance of the problem: the observable set is the entire execution Eall and the target relation is Lamport causality ≺L . Scalar clocks [13] assign a single integer to each event and achieve completeness for ≺L over Eall , but not soundness: a smaller timestamp does not imply causal precedence. Vector clocks [6, 16] achieve strong consistency for ≺L over Eall : e1 ≺L e2 ⇐⇒ vc(e1 )vc(e2 ). Matrix clocks [21] extend this with second-order knowledge, at O(n2 ) cost per event. These tools do not solve COP because, as shown in Claim 7, ≺L Eobs and <H are incomparable: deploying vector clocks at the observable boundary neither captures all real-time precedences nor avoids reporting spurious ones. The Causal Monitor operates on a fundamentally different instance, tracking real-time order <H from Eobs , where strong consistency is unattainable and the best achievable guarantee is determined by placement. Table 1 summarizes the comparison. Table 1 Causal monitoring tools as instances of the observability problem. Completeness and soundness are with respect to the stated target relation over the stated event set. Tool
Events
Target
Compl.
Sound
Cost
Scalar clock [13]
Eall
≺L
✓
×
O(1)
Eall
L
✓
✓
O(n)
L
✓
O(n2 )
Vector clock [6, 16]
≺
Matrix clock [21]
Eall
≺
✓
Causal Monitor (this work)
Eobs
<H
mutually exclusive
O(1)/O(N )
The COP invariance result shows that this gap in internal consistency is not observable at the level of the problem the monitors solve: both achieve the same soundness guarantee under external placement. To our knowledge, this is the first result showing that a quiescently consistent object and a linearizable object are provably equivalent with respect to a welldefined external problem.
10
Discussion and Further Work
The Causal Monitor is a tool for observing real-time precedence in concurrent executions, and COP is the problem of designing such a monitor under the constraints imposed by the observable boundary. This paper motivated COP through runtime verification of linearizability, but the framework applies wherever a system needs to track operation order from an external vantage point. Two domains where COP arises naturally are causally consistent replication and distributed debugging. In causally consistent distributed storage systems — such as those underlying social networks, collaborative editing tools, and geo-replicated databases — replicas must agree on the causal order of updates: if one update causally depends on another, all replicas must observe them in that order [13]. Systems such as GentleRain and Cure [4, 1] enforce this by tracking causal timestamps, which is precisely an instance of COP where the observable set is the boundary of client transactions and the target relation is real-time
G. V. Rodríguez, A. Castañeda, M. Piña
transaction order. The placement dichotomy predicts that any monitor tracking this order faces the same soundness/completeness trade-off identified here. In distributed debugging and tracing, tools such as Dapper [20] and X-Trace [7] record causal chains across service boundaries to reconstruct execution order for post-hoc analysis. These tools face exactly the observable boundary problem: they can only instrument the entry and exit points of service calls, not the internal steps. COP formalizes the guarantees such tools can provide and explains why some tracing systems report spurious dependencies while others miss genuine ones. It would be interesting to explore instances of the observability problem with different target relations. If the target relation is Lamport causality ≺L rather than real-time order <H , and the observable set is the full execution Eall , then strong consistency is achievable — vector clocks solve it exactly. The placement dichotomy still holds, but both placements achieve strong consistency because ≺L and ≺L Eall coincide. The interesting case is the boundary: when the observable set shrinks to Eobs , the Claim of Section 3 shows that ≺L Eobs and <H diverge, and strong consistency becomes unachievable. Characterizing exactly which pairs of observable sets and target relations admit strong consistency is an open question. The Collect Monitor is the only quiescently consistent implementation studied here. A natural question is whether it is optimal among quiescently consistent monitors for COP: does every sound quiescently consistent monitor for COP require at least the state and communication complexity of Collect? Conversely, is there a quiescently consistent monitor that is sound for COP and strictly cheaper than Collect? We leave this as future work. References 1
2
3 4
5
6 7
8 9
Deepthi Devaki Akkoorath, Alejandro Tomsic, Manuel Bravo, Zhongmiao Li, Tyler Crain, Annette Bieniusa, Nuno Preguiça, and Marc Shapiro. Cure: Strong semantics meets high availability and low latency. In 36th IEEE International Conference on Distributed Computing Systems (ICDCS), pages 485–494. IEEE, 2016. doi:10.1109/ICDCS.2016.42. Armando Castañeda and Gilde Valeria Rodríguez. Asynchronous wait-free runtime verification and enforcement of linearizability. In Proceedings of the 2023 ACM Symposium on Principles of Distributed Computing, PODC ’23, page 90–101, New York, NY, USA, 2023. Association for Computing Machinery. doi:10.1145/3583668.3594563. Armando Castañeda and Gilde Valeria Rodríguez. Asynchronous wait-free runtime verification and enforcement of linearizability. J. ACM, 73(1), February 2026. doi:10.1145/3777409. Jiaqing Du, Călin Iorgulescu, Amitabha Roy, and Willy Zwaenepoel. GentleRain: Cheap and scalable causal consistency with physical clocks. In Proceedings of the ACM Symposium on Cloud Computing (SoCC), pages 1–13. ACM, 2014. doi:10.1145/2670979.2670983. Antoine El-Hokayem and Yliès Falcone. Can we monitor all multithreaded programs? In Christian Colombo and Martin Leucker, editors, Runtime Verification, pages 64–89, Cham, 2018. Springer International Publishing. Colin J. Fidge. Timestamps in message-passing systems that preserve the partial ordering. In Proceedings of the 11th Australian Computer Science Conference, pages 56–66, 1988. Rodrigo Fonseca, George Porter, Randy H. Katz, Scott Shenker, and Ion Stoica. X-Trace: A pervasive network tracing framework. In 4th USENIX Symposium on Networked Systems Design and Implementation (NSDI), pages 271–284. USENIX, 2007. Andy Georges, Dries Buytaert, and Lieven Eeckhout. Statistically rigorous java performance evaluation. SIGPLAN Not., 42(10):57–76, October 2007. doi:10.1145/1297105.1297033. Maurice Herlihy. Wait-free synchronization. ACM Trans. Program. Lang. Syst., 13(1):124–149, January 1991. doi:10.1145/114005.102808.
17
18
On the Limits of Causal Observation in Shared-Memory Systems
10 11
12 13 14 15
16 17 18
19
20
21
A
Maurice Herlihy and Nir Shavit. The Art of Multiprocessor Programming. Morgan Kaufmann, 2008. Revised edition, 2012. Maurice Herlihy and Jeannette M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems, 12(3):463–492, 1990. doi:10.1145/78969.78972. L. Lamport. How to make a correct multiprocess program execute correctly on a multiprocessor. IEEE Transactions on Computers, 46(7):779–782, 1997. doi:10.1109/12.599898. Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558–565, 1978. doi:10.1145/359545.359563. Doug Lea. LongAdder and Striped64, java.util.concurrent.atomic. JDK 8 (JSR-166e), 2014. Accessed: 2026. URL: https://gee.cs.oswego.edu/dl/concurrent/. Gavin Lowe. Testing for linearizability. Concurrency and Computation: Practice and Experience, 29(4):e3928, 2017. e3928 cpe.3928. URL: https://onlinelibrary.wiley.com/ doi/abs/10.1002/cpe.3928, arXiv:https://onlinelibrary.wiley.com/doi/pdf/10.1002/ cpe.3928, doi:10.1002/cpe.3928. Friedemann Mattern. Virtual time and global states of distributed systems. In Parallel and Distributed Algorithms, pages 215–226. North-Holland, 1988. Michel Raynal and Mukesh Singhal. Logical time: Capturing causality in distributed systems. Computer, 29(2):49–56, February 1996. doi:10.1109/2.485846. Gilde Valeria Rodríguez and Armando Castañeda. Towards efficient runtime verified linearizable algorithms. In Erika Ábrahám and Houssam Abbas, editors, Runtime Verification, pages 262–281, Cham, 2024. Springer Nature Switzerland. Gilde Valeria Rodríguez, Miguel Piña, and Armando Castañeda. A reliable non-intrusive runtime verification framework for linearizability. Science of Computer Programming, 254:103509, 2026. URL: https://www.sciencedirect.com/science/article/pii/S0167642326000754, doi:10.1016/j.scico.2026.103509. Benjamin H. Sigelman, Luiz André Barroso, Mike Burrows, Pat Stephenson, Manoj Plakal, Donald Beaver, Saul Jaspan, and Chandan Shanbhag. Dapper, a large-scale distributed systems tracing infrastructure. Technical Report dapper-2010-1, Google, 2010. URL: https: //research.google/pubs/pub36356/. Gene T.J. Wuu and Arthur J. Bernstein. Efficient solutions to the replicated log and dictionary problems. In Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing, PODC ’84, page 233–242, New York, NY, USA, 1984. Association for Computing Machinery. doi:10.1145/800222.806750.
Placement Cases
We systematically analyze all possible placements of interface events relative to true operation boundaries. In each case, the monitor may invoke objects of any type, including objects with infinite consensus number. The argument in each case is the same: what matters is not the power of the object invoked but the position of its invocation relative to the true boundary. Recall that under an ideal log, every object invocation takes effect at a single linearization point lp(·), and the causal order observable by the monitor agrees with the real-time order of these points: e1 ≺L e2 ⇐⇒ lp(e1 ) ≺ lp(e2 ).
Unilateral Placement ▶ Lemma 20 (Unilateral placement achieves neither soundness nor completeness). Let M be a monitor that invokes objects only before both boundaries (only before inv(op) and res(op)) or only after both boundaries. Then M is neither sound nor complete for COP.
G. V. Rodríguez, A. Castañeda, M. Piña
Proof. We prove both cases. Case 1: only before both boundaries. The monitor invokes objects before inv(op) and before c c res(op), producing interface events inv(()op) and res(()op) c with lp(inv(()op)) ≺ inv(op) and lp(res(()op)) c ≺ res(op). Not complete. Consider opA <H opB , so res(opA ) ≺ inv(opB ). The monitor’s event for the response of opA fires before res(opA ), and the monitor’s event for the invocation of opB c fires before inv(opB ). No causal chain is established between res(()op c A ) and inv(()op B ): c res(()op c ) fires before res(op ) and ) fires before inv(op ), but res(()op c inv(()op A A B B A ) may fire c after inv(()opB ) even when opA <H opB . Concretely: if pi delays firing res(()op c A ) until just c before res(opA ), and pj fires inv(()op B ) early, the real-time order of the interface events may c be inv(()op c B ) ≺ res(()op A ) despite op A <H op B . The monitor misses a genuine precedence. Not sound. Consider opA ∥ opB . The monitor fires res(()op c A ) before res(op A ) and c c inv(()opB ) before inv(opB ). If res(()op c A ) happens to fire before inv(()op B ) in real time, the monitor reports Precedes(A, B) = true, but opA ∥ opB means opA <H opB is false. A spurious precedence is reported. Case 2: only after both boundaries. The monitor invokes objects after inv(op) and after c res(op), producing interface events with inv(op) ≺ lp(inv(()op)) and res(op) ≺ lp(res(()op)). c Not complete. Consider opA <H opB , so res(opA ) ≺ inv(opB ). The monitor fires c c res(()op c A ) after res(op A ) and inv(()op B ) after inv(op B ). If pj fires inv(()op B ) immediately c after inv(opB ) while pi delays res(()op c ), the real-time order may be inv(()op c A B ) ≺ res(()op A) despite opA <H opB . The monitor misses a genuine precedence. Not sound. Consider opA ∥ opB . The monitor fires res(()op c A ) after res(op A ) and c c inv(()op ) after inv(op ). If res(()op c ) fires before inv(()op ), the monitor reports B B A B Precedes(A, B) = true, but opA ∥ opB so no real precedence exists. A spurious precedence is reported. ◀
External Placement: Sound but Not Complete ▶ Lemma 21 (External placement is not complete). A monitor with external placement is sound for COP (Lemma 11) but not complete: there exist executions where opA <H opB yet Precedes(A, B) = false. c Proof. External placement gives lp(inv(()op)) ≺ inv(op) and res(op) ≺ lp(res(()op)). c Consider two operations opA on pi and opB on pj with opA <H opB : res(opA ) ≺ inv(opB ). c The monitor fires res(()op c A ) after res(op A ) and inv(()op B ) before inv(op B ). There is no c c constraint forcing lp(res(()op c A )) ≺ lp(inv(()op B )): if pj fires inv(()op B ) very early (long c before inv(opB )) and pi fires res(()op c ) late (just after res(op A A )), then lp(inv(()op B )) ≺ c c c lp(res(()op A )) even though op A <H op B . The monitor observes inv(()op B ) before res(()op A) and reports Precedes(A, B) = false, missing a genuine precedence. ◀
Internal Placement: Complete but Not Sound ▶ Lemma 22 (Internal placement is not sound). A monitor with internal placement is complete for COP (Lemma 11) but not sound: there exist executions where opA ∥ opB yet Precedes(A, B) = true. c Proof. Internal placement gives inv(op) ≺ lp(inv(()op)) and lp(res(()op)) c ≺ res(op). Consider two operations opA on pi and opB on pj with opA ∥ opB : their execution intervals c overlap. The monitor fires res(()op c A ) before res(op A ) and inv(()op B ) after inv(op B ). Since the operations overlap and the processes are asynchronous, it is possible that lp(res(()op c A )) ≺
19
20
On the Limits of Causal Observation in Shared-Memory Systems
c lp(inv(()op c B )) even though the operations are concurrent: pi fires res(()op A ) early in its c interval while pj fires inv(()op c B ) late in its interval. The monitor observes res(()op A ) before c ) and reports Precedes(A, B) = true, but op ∥ op so no real precedence exists. inv(()op B A B A spurious precedence is reported. ◀
B
Proof of Theorem 12
Proof. We prove that no monitor M can be strongly consistent for COP, even under an ideal log (Definition 9) and even if M uses shared-memory objects of arbitrary power.
Setup. Fix any monitor M and any two operations opA on process pi and opB on process pj , where pi = ̸ pj . By Definition 8 and the WLOG argument of Section 4, we may assume without loss of generality that M emits exactly one interface event per boundary: res(()op c A ) associated c with the response of opA , and inv(()op B ) associated with the invocation of op B . Under an ideal log, each interface event takes effect at a single linearization point: lp(res(()op c A )) and c lp(inv(()op )). B The true boundary res(opA ) is a transfer of control between pi and its caller. The interface event res(()op c A ) is a shared-memory step. These are events of distinct categories and therefore have distinct points in real time: res(opA ) ̸= lp(res(()op c A )). − Let a be the linearization point of the last interface event of opA that precedes res(opA ) in program order, and let a+ = lp(res(()op c A )). The true boundary res(op A ) lies strictly inside the open interval (a− , a+ ): it cannot equal a− because a− is a shared-memory step that precedes the response in program order, and it cannot equal a+ for the same reason. This window (a− , a+ ) is unavoidable: the only way to close it would be to make res(opA ) and res(()op c A ) the same event, which is impossible since one is a control transfer and the other is a shared-memory write. c Define the window (b− , b+ ) around inv(opB ) symmetrically, where b− = lp(inv(()op B )) + and b is the linearization point of the first interface event of opB that follows inv(opB ) in program order. By the same argument, inv(opB ) lies strictly inside (b− , b+ ) and this window cannot be closed. The following diagram illustrates the two windows and their overlap: window (a− ,a+ )
window (b− ,b+ )
z z }| { }| { a− · · · res(opA ) · · · a+ b− · · · inv(opB ) · · · b+ | {z } overlap W ̸=∅ by adversarial scheduling
Because pi and pj are asynchronous — no bound on relative speeds — an adversary can schedule their steps so that the two windows overlap: W = max(a− , b− ), min(a+ , b+ ) ̸= ∅. c Concretely: the adversary slows pj until inv(()op B ) fires at the same time that pi is executing − + − + inside (a , a ), and symmetrically delays pi so that res(()op c A ) fires while pj is inside (b , b ). Since the two processes share no synchronization that could prevent this interleaving, such a schedule always exists.
G. V. Rodríguez, A. Castañeda, M. Piña
21
The indistinguishable executions. With W ̸= ∅, we place res(opA ) and inv(opB ) at two different positions within W :
E1 E2
Position of true boundaries
Relation
res(opA ) ≺ inv(opB ) in W inv(opB ) ≺ res(opA ) in W
opA <H opB opA ∥ opB
Both executions are identical in every shared-memory step: the interface events res(()op c A) + − c and inv(()opB ) fire at the same times a and b respectively, and all other monitor steps are unchanged. Since res(opA ) and inv(opB ) are not shared-memory steps, moving them within W does not alter any linearization point, any register value, or any causal chain observable by M. Under an ideal log, the log of M is therefore identical in E1 and E2 . M must return a single answer for Precedes(A, B) based on its log, and that answer is the same in E1 and E2 . But strong consistency requires: In E1 : opA <H opB , so completeness requires Precedes(A, B) = true. In E2 : opA ∥ opB , so soundness requires Precedes(A, B) = false. No single answer satisfies both. Therefore M cannot be strongly consistent for COP. One might hope that a more powerful logging mechanism — one that somehow resolves the ambiguity inside W — could escape the impossibility. The ideal log already grants the strongest possible logging assumption: perfect knowledge of the real-time order among all interface events. The impossibility does not stem from imprecision in the log. It stems from the fact that res(opA ) and inv(opB ) are not shared-memory steps and therefore cannot appear in any log, no matter how ideal. No logging mechanism, however powerful, can observe events that are not shared-memory operations. ◀
C
Linearizability of the Striped Counter
Implementation The Striped counter is implemented as an array of N per-process atomic cells C[1 . . . N ], where process pi only increments C[i]. The Stamp function for process pi executes: 1. C[i].incrementAndGet() (atomic write to own cell) PN 2. return j=1 C[j].get() (non-atomic traversal of all cells) In Java, this is implemented using an AtomicLongArray with memory padding between cells to prevent false sharing on cache lines [14]. Each cell occupies a full cache line (typically 64 bytes), so increments by different processes do not invalidate each other’s cache entries. This padding is a hardware-level optimization and does not affect the logical behavior of the counter. The key invariant is that the increment always precedes the sum within the same Stamp call. This ensures that the value returned by sum() is at least as large as the contribution of the calling process, and that the global sum is strictly monotone across non-overlapping calls.
Proof of linearizability We prove that Striped satisfies Proposition 14.
22
On the Limits of Causal Observation in Shared-Memory Systems
Proof. We must show that every execution of the Striped Counter Monitor admits a linearization: a legal sequential history in which each operation’s linearization point lp(·) falls within its execution interval. Consider any Stamp call by process pi that returns value t. The call first increments PN C[i], then reads the sum j=1 C[j]. Because each cell C[j] is monotonically non-decreasing and the increment of C[i] occurs before the sum traversal within the same call, the sum at the start of the traversal is at least t (since C[i] already reflects the increment) and at most the sum at the end of the traversal. More precisely: let sstart be the true global sum at the moment the traversal begins and send be the true global sum at the moment it ends. The returned value t satisfies sstart ≤ t ≤ send , since the non-atomic traversal reads each cell at some point between its start and end. Because each cell increments by exactly one at a time, the global sum increases in unit steps. Therefore, there exists a physical instant lp during the traversal at which the true global sum equals exactly t. This instant lp lies within the execution interval of the Stamp call and serves as its linearization point. Let s1 and s2 be two Stamp calls where s1 completes before s2 begins. Since every Stamp increments before summing, the increment of s1 is complete before s2 begins. When s2 executes its sum traversal, it reads every cell after s1 ’s increment has taken effect, so it observes a global sum strictly greater than s1 ’s contribution. In particular, ts(s2 ) ≥ ts(s1 ) + 1 > ts(s1 ): non-overlapping calls receive strictly increasing timestamps. Suppose two calls s1 and s2 return the same value t. By the argument above, nonoverlapping calls receive strictly different timestamps. Therefore s1 and s2 must overlap in real time. The tie may be broken arbitrarily in the sequential history without violating the specification, since the Causal Monitor’s sequential specification imposes no order on concurrent operations. For a query Precedes(A, B) returning true, we have tA < tB , where tA is the timestamp of Add_Res(A) and tB is the timestamp of Add_Inv(B). By monotonicity, tA < tB implies lp(Add_Res(A)) ≺ lp(Add_Inv(B)), so Add_Res(A) precedes Add_Inv(B) in the linearization. This matches the sequential specification, which returns true exactly when A’s response record precedes B’s invocation record in the state. ◀
Note on false sharing and padding The AtomicLongArray with padding is structurally similar to Java’s LongAdder [14], but with a critical difference: LongAdder supports both increment and decrement and is designed for accumulation, not for monotone counting. Striped uses only increment operations, which is what guarantees the monotonicity argument above. Allowing decrements would break the intermediate value argument and invalidate the linearizability proof. The padding prevents cache-line false sharing at the hardware level but does not alter the logical monotonicity or the linearizability of the algorithm in any way.
D
Proof of Lemma 17
We prove that Precedes under the Collect Monitor (Algorithm 2) is a strict partial order, assuming the view-containment conjunct vA ⊆ vB is included in the predicate.
G. V. Rodríguez, A. Castañeda, M. Piña
23
Recall that Precedes(id A , id B ) returns true iff all three of the following hold: (C1) (R, id A ) ∈ vB , (C2) (I, id B ) ∈ / vA , (C3) vA ⊆ vB . Full proof of Lemma 17. Irreflexivity: Precedes(A, A) = false. The collect of Add_Res(A) runs to completion before the write of (R, A) to Reg[proc(A)] occurs — the collect is part of Add_Res(A) and the write happens at the end of it. Therefore (R, A) ∈ / vA , which violates (C1). Hence Precedes(A, A) = false. Antisymmetry: Precedes(A, B) ⇒ ¬Precedes(B, A). Suppose Precedes(A, B) = true. By (C1), (R, A) ∈ vB . Since registers are append-only and process proc(A) appends (I, A) strictly before (R, A) on Reg[proc(A)], and vB is a prefix-closed snapshot of the registers, it follows that (I, A) ∈ vB as well. Now consider Precedes(B, A): it would require (I, A) ∈ / vB by (C2) with the roles of A and B swapped. But we just showed (I, A) ∈ vB , so (C2) fails and Precedes(B, A) = false. Transitivity: Precedes(A, B)∧Precedes(B, C) ⇒ Precedes(A, C). Suppose Precedes(A, B) = true and Precedes(B, C) = true. We verify the three conjuncts of Precedes(A, C). (C1) for Precedes(A, C): (R, A) ∈ vC . From Precedes(A, B), conjunct (C1) gives (R, A) ∈ vB . From Precedes(B, C), conjunct (C3) gives vB ⊆ vC . Therefore (R, A) ∈ vC . (C2) for Precedes(A, C): (I, C) ∈ / vA . From Precedes(B, C), conjunct (C2) gives (I, C) ∈ / vB . From Precedes(A, B), conjunct (C3) gives vA ⊆ vB . Since (I, C) ∈ / vB and vA ⊆ vB , we have (I, C) ∈ / vA . (C3) for Precedes(A, C): vA ⊆ vC . From Precedes(A, B), conjunct (C3) gives vA ⊆ vB . From Precedes(B, C), conjunct (C3) gives vB ⊆ vC . By transitivity of subset inclusion, vA ⊆ vC . All three conjuncts hold, so Precedes(A, C) = true. ◀ Note that view-containment (C3) is essential for transitivity: without it, (C1) and (C2) alone are not transitive. Specifically, (C2) for Precedes(A, C) requires (I, C) ∈ / vA , but knowing (I, C) ∈ / vB and vA ⊆ vB is what allows us to conclude this. Without (C3), vA ⊆ vB would not be available and the derivation would fail.
E
Proof of Theorem 18
We construct a concrete execution of four operations A, B, C, D on distinct processes pA , pB , pC , pD whose verdicts under Algorithm 2 admit no sequential history.
E.0.0.1
Write times.
The interface events are written to shared memory at the following physical times: w(IA )=1,
E.0.0.2
w(IC )=2,
w(IB )=3,
w(ID )=4,
w(RC )=5,
w(RA )=6.
Collect intervals.
Each process performs its collect for Add_Res by reading the registers at the following times: A collects during [2.0, 2.5): reads all registers while only IA and IC have been written. C collects during [2.5, 3.0): reads all registers while only IA and IC have been written. B reads Reg[proc(C)] at t=4 (before w(RC )=5) and Reg[proc(A)] at t=7 (after w(RA )=6).
24
On the Limits of Causal Observation in Shared-Memory Systems
D reads Reg[proc(A)] at t=5 (before w(RA )=6) and Reg[proc(C)] at t=6 (after w(RC )=5). This is the key crossing: B sees A’s response but misses C’s, while D sees C’s response but misses A’s.
E.0.0.3
Resulting views.
vA = {IA , IC }, vB = {IA , RA , IB , IC , ID }, vC = {IA , IC }, vD = {IA , IC , RC , ID , IB }.
E.0.0.4
Evaluating the predicate.
We check Precedes(X, Y ) = [(R, X) ∈ vY ] ∧ [(I, Y ) ∈ / vX ] ∧ [vX ⊆ vY ] for each relevant pair: Precedes(A, B) = true: (R, A) ∈ vB ✓; (I, B) ∈ / vA ✓; vA = {IA , IC } ⊆ vB ✓. Precedes(C, D) = true: (R, C) ∈ vD ✓; (I, D) ∈ / vC ✓; vC = {IA , IC } ⊆ vD ✓. Precedes(C, B) = false: (R, C) ∈ / vB since B read Reg[proc(C)] at t=4 before w(RC )=5. Conjunct (C1) fails. Precedes(A, D) = false: (R, A) ∈ / vD since D read Reg[proc(A)] at t=5 before w(RA )=6. Conjunct (C1) fails.
E.0.0.5
No sequential history exists.
In any sequential history S consistent with these verdicts, the sequential specification requires: Precedes(A, B) = true ⇒ RA ≺S IB ,
Precedes(C, D) = true ⇒ RC ≺S ID .
The false verdicts require: Precedes(C, B) = false ⇒ IB ≺S RC ,
Precedes(A, D) = false ⇒ ID ≺S RA .
Chaining these four constraints: RA ≺S IB ≺S RC ≺S ID ≺S RA , a cycle. No sequential history satisfies all four verdicts simultaneously, so the Collect Monitor is not sequentially consistent and a fortiori not linearizable.
F
Proof of Theorem 19
Proof. Let Q be a quiescent instant with res(opA ) ≺ Q ≺ inv(opB ). Under external placement, A’s Add_Res call is invoked after opA returns and completes before Q, and B’s Add_Inv call is invoked after Q and before opB starts. Since Q is quiescent, no monitor step of any operation is in progress at Q: every write associated with A’s monitor calls is complete before Q, and every write associated with B’s monitor calls begins after Q. We verify the three conjuncts of Precedes(A, B): (C1) (R, A) ∈ vB . The write w(R, A) occurs during A’s Add_Res call, which completes before Q. Hence w(R, A) ≺ Q. B’s collect runs entirely after Q, so it reads every register after Q and therefore observes every event written before Q, including (R, A). Thus (R, A) ∈ vB .
G. V. Rodríguez, A. Castañeda, M. Piña
(C2) (I, B) ∈ / vA . The write w(I, B) occurs during B’s Add_Inv call, which begins after Q. Hence w(I, B) ≻ Q. A’s collect runs entirely before Q, so it cannot have observed any event written after Q. Thus (I, B) ∈ / vA . (C3) vA ⊆ vB . Every event in vA was written before A’s collect completed, hence before Q. B’s collect reads every register after Q and therefore observes all events written before Q. Hence every element of vA is also in vB , so vA ⊆ vB . All three conjuncts hold, so Precedes(A, B) = true. For operations not separated by a quiescent instant, the monitor may return either verdict: quiescent consistency imposes no constraint on the ordering of operations within the same quiescent group, and both true and false are compatible with a legal sequential history for that group. ◀
25