On the Limits of Causal Observation in Shared-Memory Systems
Extracted source text · arXiv 2606.14093
\pdfoutput=1 % mandatory to ensure pdflatex processing by arXiv
\documentclass[a4paper,USenglish,cleveref,autoref,thm-restate,nolinenumbers]{lipics-v2021}
\hideLIPIcs % removes references to LIPIcs series (logo, DOI, ...) for arXiv upload
%This is a template for producing LIPIcs articles.
%See lipics-v2021-authors-guidelines.pdf for further information.
%for A4 paper format use option "a4paper", for US-letter use option "letterpaper"
%for british hyphenation rules use option "UKenglish", for american hyphenation rules use option "USenglish"
%for section-numbered lemmas etc., use "numberwithinsect"
%for enabling cleveref support, use "cleveref"
%for enabling autoref support, use "autoref"
%for anonymousing the authors (e.g. for double-blind review), add "anonymous"
%for enabling thm-restate support, use "thm-restate"
%for enabling a two-column layout for the author/affilation part (only applicable for > 6 authors), use "authorcolumns"
%for producing a PDF according the PDF/A standard, add "pdfa"
%\pdfoutput=1 %uncomment to ensure pdflatex processing (mandatatory e.g. to submit to arXiv)
%\hideLIPIcs %uncomment to remove references to LIPIcs series (logo, DOI, ...), e.g. when preparing a pre-final version to be uploaded to arXiv or another public repository
%\graphicspath{{./graphics/}}%helpful if your graphic files are in another directory
\usepackage{amsmath, amssymb, amsthm}
\usepackage{mathtools}
\usepackage{booktabs}
%\usepackage[expansion=false]{microtype}
\usepackage{algorithm}
\usepackage{algpseudocode}
\newcommand{\precedes}{\textsc{Precedes}}
\newcommand{\concurrent}{\textsc{Concurrent}}
\newcommand{\addinv}{\textsc{Add\_Inv}}
\newcommand{\addres}{\textsc{Add\_Res}}
\newcommand{\snap}{\mathit{snap}}
\newcommand{\lp}{\mathit{lp}}
\newcommand{\tsnap}{t_{\mathit{snap}}}
\newcommand{\Reg}{\mathit{Reg}}
\newcommand{\inv}{\mathit{inv}}
\newcommand{\res}{\mathit{res}}
\newcommand{\cprec}{\sqsubset} % abstract causal order (Sec. 1), instantiated as <_H in Sec. 2
\newcommand{\view}{\mathit{view}}
\newcommand{\rt} {<_{H}}
\newcommand{\ocp} {<^{OCP}_{H}}
\newcommand{\Msnap}{M_{\mathit{snap}}}
\newcommand{\Mcoll}{M_{\mathit{coll}}}
\newcommand{\Vset}[1]{\mathcal{V}_{\mathit{OCP}}(\alpha,\,#1)}
\newcommand{\PREC}{\texttt{PRECEDES}}
\newcommand{\CONC}{\texttt{CONCURRENT}}
\newcommand{\hbL}[1][]{\prec^{L}_{#1}}
\newcommand{\Eall} {E_{\mathit{all}}}
\newcommand{\Eobs} {E_{\mathit{obs}}}
\newcommand{\Eint} {E_{\mathit{int}}}
\newcommand{\hball} {<^{L}_{H}}
\newcommand{\hbR}[1]{<^{L}_{H|#1}}
\newcommand{\cm} {<^{cm}_{H}}
\newcommand{\lhat} {\widehat{<}^{L}_{H}}
\newcommand{\ts} {\mathit{ts}}
\newcommand{\winv} {\mathit{winv}}
\newcommand{\wres} {\mathit{wres}}
\newcommand{\tFA} {t_{\mathit{FA}}}
\newcommand{\tCN} {t_{\mathit{CN}}}
\newcommand{\einv}[1]{\widehat{\mathit{inv}}(#1)}
\newcommand{\eres}[1]{\widehat{\mathit{res}}(#1)}
\newcommand{\recprec}{\prec_{\mathsf{rec}}} % record order observed in the log
\bibliographystyle{plainurl}% the mandatory bibstyle
\title{On the Limits of Causal Observation in Shared-Memory Systems} %TODO Please add
%\titlerunning{Dummy short title} %TODO optional, please use if title is longer than one line
\author{Gilde Valeria Rodríguez}{Posgrado en Ciencia e Ingeniería de la Computación, Universidad Nacional Autónoma de México, Mexico}{gilde@ciencias.unam.mx}{https://orcid.org/0009-0009-1463-7786}{}
\author{Armando Castañeda}{Instituto de Matemáticas, Universidad Nacional Autónoma de México, Mexico}{armando.castaneda@im.unam.mx}{https://orcid.org/0000-0002-8017-8639}{}
\author{Miguel Piña}{Independent research, México}{miguelpinia1@gmail.com}{https://orcid.org/0000-0002-2135-2131}{}
% FIXED: LIPIcs variables for header and copyright administration
\authorrunning{G. V. Rodríguez, A. Castañeda, M. Piña}
\Copyright{Gilde Valeria Rodríguez, Armando Castañeda, Miguel Piña}
\ccsdesc{Theory of computation}
\ccsdesc{Theory of computation~Distributed computing models}
\ccsdesc{Theory of computation~Distributed algorithms}
\ccsdesc{Theory of computation~Concurrency}
\ccsdesc{Theory of computation~Concurrent algorithms}
\keywords{Causality, Linearizability, Quiescent Consistency, Causal Observability} %TODO mandatory; please add comma-separated list of keywords
\category{} %optional, e.g. invited paper
\relatedversion{} %optional, e.g. full version hosted on arXiv, HAL, or other respository/website
%\relatedversiondetails[linktext={opt. text shown instead of the URL}, cite=DBLP:books/mk/GrayR93]{Classification (e.g. Full Version, Extended Version, Previous Version}{URL to related version} %linktext and cite are optional
%\supplement{}%optional, e.g. related research data, source code, ... hosted on a repository like zenodo, figshare, GitHub, ...
%\supplementdetails[linktext={opt. text shown instead of the URL}, cite=DBLP:books/mk/GrayR93, subcategory={Description, Subcategory}, swhid={Software Heritage Identifier}]{General Classification (e.g. Software, Dataset, Model, ...)}{URL to related version} %linktext, cite, and subcategory are optional
%\funding{(Optional) general funding statement \dots}%optional, to capture a funding statement, which applies to all authors. Please enter author specific funding statements as fifth argument of the \author macro.
%\acknowledgements{I want to thank \dots}%optional
%\nolinenumbers %uncomment to disable line numbering
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\nolinenumbers
\begin{document}
\maketitle
%TODO mandatory: add short abstract of the document
\begin{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 \emph{Causal Observability Problem} ($\mathbf{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 \emph{complete}
if it never misses a genuine precedence, and \emph{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 \emph{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: \textsc{FAInc}
(centralized atomic counter), \textsc{Striped} (decentralized
counter), and \textsc{Collect} (iterative register snapshot).
\textsc{FAInc} and \textsc{Striped} are linearizable;
\textsc{Collect} is only quiescently consistent. Despite this
internal consistency gap, we prove that all three provide
identical $\mathbf{COP}$ guarantees: placement alone determines
observable behavior. We validate these claims empirically on a
64-core NUMA architecture, showing that \textsc{Striped} matches
\textsc{Collect} in throughput while preserving linearizability,
resolving the cache-contention bottleneck of \textsc{FAInc} at
high thread counts.
\end{abstract}
\tableofcontents
%=======================================================================
\section{Introduction}
\label{sec:intro}
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
\emph{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 \emph{runtime verification of
linearizability}~\cite{CR23, RPC26}.
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~\cite{HW90}.
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~\cite{Lamport78} or vector clocks~\cite{Fidge88,Mattern88}
cannot capture it --- they track \emph{information flow}, not
\emph{elapsed time}.
It has been shown that any monitor restricted to the observable
boundary faces a fundamental
impossibility~\cite{CR23, CR26_JACM}: no protocol can simultaneously
be \emph{complete} (capturing every genuine real-time precedence)
and \emph{sound} (reporting only genuine ones).
Any monitor that tries must either miss precedences or report
spurious ones.
We formalize this limitation as the \emph{Causal Observability
Problem} $(\mathbf{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 \emph{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~\cite{CR23, CR26_JACM, RC24, EF18} and identify
a placement dichotomy that explains their guarantees.
Monitors that instrument operations by writing events into shared
memory \emph{before} invoking and \emph{after} completing each
operation --- enclosing the true interval from outside --- yield a
\emph{sound} monitor: every reported precedence is genuine.
Monitors that write events \emph{after} the operation starts and
\emph{before} it finishes --- strictly inside the true interval ---
yield a \emph{complete} monitor: every genuine precedence is
captured.
Monitors that instrument only one boundary, rather than both, are
neither sound nor complete~\cite{EF18}.
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.
\textsc{FAInc}, a centralized atomic increment introduced
in~\cite{RC24}, is linearizable.
\textsc{Striped}, a decentralized counter built on Java's
\texttt{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, \textsc{Collect}, reads a snapshot of
process registers iteratively~\cite{RC24} and is only quiescently
consistent.
The consistency properties of \textsc{FAInc} and \textsc{Collect}
with respect to the Causal Monitor specification were not
established in~\cite{RC24}, nor were the two distinguished from
each other.
A key result of this paper is that while \textsc{Collect} is not
linearizable and both counters are, all three provide identical
$\mathbf{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~\cite{RPC26} showed that \textsc{Collect} outperforms
\textsc{FAInc} in scalability; we show here that \textsc{Striped}
is a linearizable counter that matches \textsc{Collect} in
throughput while eliminating the cache-contention collapse of
\textsc{FAInc} at high thread counts.
\subsection*{Contributions}
\begin{enumerate}
\item \textbf{Formalization of the observability limit.}
We define $\mathbf{COP}$ at the observable boundary of a
concurrent object and prove that strong consistency is
unachievable there, making precise the impossibility identified
informally in~\cite{CR23, RPC26}.
\item \textbf{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.
\item \textbf{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~\cite{RC24}.
\item \textbf{COP invariance.}
We prove that all implementations are equivalent with respect
to $\mathbf{COP}$: the internal consistency gap between
linearizability and quiescent consistency is invisible at the
observable boundary.
\item \textbf{Scalable linearizable implementation.}
We introduce \textsc{Striped}, a new linearizable implementation
of the Causal Monitor, and show empirically that it matches the
scalability of \textsc{Collect} and eliminates the contention
bottleneck of \textsc{FAInc}.
Prior work~\cite{RPC26} established that \textsc{Collect}
outperforms \textsc{FAInc}; \textsc{Striped} shows that a
linearizable monitor can achieve the same scalability advantage.
\end{enumerate}
%\subsection*{Organization}
Section~\ref{sec:model} presents the system model.
Section~\ref{sec:cop} defines $\mathbf{COP}$ and proves the
impossibility of strong consistency.
Section~\ref{sec:eint} analyzes the placement strategies of
existing monitors and proves the completeness and soundness
characterization.
Section~\ref{sec:monitor} specifies the Causal Monitor object.
Section~\ref{sec:implementations} presents the Counter and Collect
implementations.
Section~\ref{sec:correctness} contains the correctness proofs and
the COP invariance result.
Section~\ref{sec:evaluation} presents the empirical evaluation.
Section~\ref{sec:cmp} discusses related work.
\section{Model}
\label{sec:model}
We consider $N$ processes $p_1, \dots, p_N$ that run asynchronously and
communicate via an atomic shared-memory model~\cite{HW90}.
Shared-memory systems are organized around \emph{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 \emph{abstract type} $T$, which names
its operations and, together with a specification, defines
their legal behaviors~\cite{HW90}.
An \emph{operation} is a pair consisting of an
\emph{invocation} $\mathit{inv}(\mathit{op})$, issued when
a process calls the operation, and a matching
\emph{response} $\mathit{res}(\mathit{op})$, returned when
the call completes.
An operation is \emph{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 \prec f$ if event $e$ occurs before event $f$ in real time.
This assumption is a property of the \emph{model} --- namely, that the
underlying memory is atomic~\cite{HW90}.
%--- and is independent of the
% \emph{correctness condition} imposed on implementations.
% Linearizability, sequential consistency, and quiescent consistency are
% all defined over histories drawn from this same model; they differ only
% in which orderings they require the equivalent sequential history to
% respect.
A \emph{history} $H$ is a finite sequence of invocation and
response events.
We say $H$ is \emph{well-formed} if every response is
preceded by a matching invocation; \emph{sequential} if
every invocation is immediately followed by its matching
response with no interleaving; and \emph{complete} if no
invocation is pending.
The \emph{real-time order} $<_H$ on the operations of $H$
is defined by $\mathit{op}_1 <_H \mathit{op}_2$
$ \;\;\iff\;\;$
$ \mathit{res}(\mathit{op}_1) \prec \mathit{inv}(\mathit{op}_2)$.
Two operations are \emph{concurrent} when neither precedes
the other:
$\mathit{op}_1 \parallel \mathit{op}_2 \iff
\lnot(\mathit{op}_1 <_H \mathit{op}_2) \land
\lnot(\mathit{op}_2 <_H \mathit{op}_1)$.
The behavior of an object of type $T$ is described by a
\emph{sequential specification}.
\begin{definition}[Sequential specification~{\cite{HW90}}]
\label{def:seqspec}
The \emph{sequential specification} of type $T$ is a prefix-closed set
$\mathit{Seq}(T)$ of sequential histories over the operations of $T$.
A sequential history $S$ is \emph{legal} if $S \in \mathit{Seq}(T)$.
The specification $\mathit{Seq}(T)$ thus determines which sequences of
operations, each completing before the next begins, constitute valid
behaviors of $T$.
\end{definition}
Intuitively, $\mathit{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.
%% LIN
\begin{definition}[Linearizability~{\cite{HW90}}]
\label{def:lin}
An implementation of type $T$ is \emph{linearizable} with
respect to $\mathit{Seq}(T)$ if for every well-formed history
$H$ it produces there exists a legal sequential history
$S \in \mathit{Seq}(T)$ such that:
\begin{itemize}
\item \textbf{(L1)} $S$ is equivalent to some completion
of $H$ — pending operations may be dropped or
completed, and
\item \textbf{(L2)} $\mathit{op}_1 <_H \mathit{op}_2$
in $H$ implies $\mathit{op}_1 <_S \mathit{op}_2$.
\end{itemize}
Condition (L2) is the \emph{real-time order} condition:
a linearizable implementation must respect the physical
execution order of non-overlapping operations.
\end{definition}
Linearizability is equivalent to assigning each operation
$\mathit{op}$ a \emph{linearization point}
$\mathit{LP}(\mathit{op}) \in
[\mathit{inv}(\mathit{op}), \mathit{res}(\mathit{op})]$
such that the sequential history obtained by ordering
operations by their linearization points is legal.
%In the language of interval-sequential specifications,
%a linearization point is a degenerate interval $[t, t]$.
Sequential consistency~\cite{Lamport97} 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.
\begin{definition}[Sequential consistency~{\cite{Lamport97}}]
\label{def:sc}
An implementation of type $T$ is \emph{sequentially consistent} with
respect to $\mathit{Seq}(T)$ if for every well-formed history $H$ it
produces there exists a legal sequential history $S \in \mathit{Seq}(T)$
such that:
\begin{itemize}
\item \textbf{(SC1)} $S$ is equivalent to some completion of $H$:
every completed operation appears in $S$, and pending operations
may be dropped or completed; and
\item \textbf{(SC2)} $S$ respects \emph{program order}: for each
process $p_i$, the operations of $p_i$ appear in $S$ in the
same order as in $H$.
\end{itemize}
\end{definition}
In high-contention concurrent systems, maintaining the real-time
order of non-overlapping operations imposes a significant
synchronization cost.
\emph{Quiescent Consistency} (QC)~\cite{HS08} addresses this by
relaxing the real-time order requirement: rather than ordering all
non-overlapping 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~\cite{HS08}.
A \emph{quiescent instant} is a real-time instant at which no
operation is pending.
A \emph{quiescent interval} is any open interval
$(Q_k, Q_{k+1})$ between two consecutive quiescent instants
$Q_k$ and $Q_{k+1}$.
The operations that execute entirely within the $k$-th quiescent
interval form the \emph{quiescent group} $G_k$.
Two operations are \emph{separated by quiescence} if they belong
to different groups: $\mathit{op}_1 \in G_k$ and
$\mathit{op}_2 \in G_{k'}$ with $k \ne k'$.
\begin{definition}[Quiescent consistency~{\cite{HS08}}]
\label{def:qc}
An implementation of type $T$ is \emph{quiescently consistent}
with respect to $\mathit{Seq}(T)$ if for every well-formed
history $H$ it produces there exists a legal sequential history
$S \in \mathit{Seq}(T)$ equivalent to some completion of $H$
such that: if $\res(\mathit{op}_1) \prec Q \prec
\inv(\mathit{op}_2)$ for some quiescent instant $Q$, then
$\mathit{op}_1 <_S \mathit{op}_2$.
Operations within the same quiescent group may be reordered
freely, provided the result is legal.
\end{definition}
\noindent
The three conditions are strictly ordered by strength.
Neither implication reverses~\cite{HW90, HS08}, yielding the
strict containment:$\text{Linearizable}
\;\subsetneq\;
\text{Sequentially Consistent}
\;\subsetneq\;
\text{Quiescently Consistent}$.
%=======================================================================
%=======================================================================
%=======================================================================
\section{The Causal Observability Problem}
\label{sec:cop}
%=======================================================================
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 \emph{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 $\hbL$ --- but it
cannot directly observe the true operation 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.
%-----------------------------------------------------------------------
\subsection{Observable Events and Lamport Causality}
\label{sec:obs-events}
%-----------------------------------------------------------------------
Recall from Section~\ref{sec:model} that an execution produces a
history $H$: a sequence of invocation and response events over the
processes $p_1,\dots,p_N$.
The \emph{observable boundary} is the set of events in $H$:
$\Eobs \;\triangleq\;
\bigl\{\,\inv(\mathit{op}),\;\res(\mathit{op})
\;\bigm|\; \mathit{op} \in H \,\bigr\}$.
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 \emph{must report} is the real-time order
$<_H$ of Section~\ref{sec:model}.
Since $\mathit{op}_A <_H \mathit{op}_B$ holds exactly when
$\res(\mathit{op}_A) \prec \inv(\mathit{op}_B)$, 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 \emph{can construct} from shared memory
is Lamport's happened-before~\cite{Lamport78}.
\begin{definition}[Lamport causality, $\hbL$]
\label{def:lamport}
$\hbL$ is the smallest transitive relation over the events of an
execution such that:
\begin{enumerate}[(L1)]
\item \emph{Program order}: if $e_1$ and $e_2$ occur at the same
process and $e_1 \prec e_2$, then $e_1 \hbL e_2$.
\item \emph{Object communication}: if $e_1$ is an operation on a
shared object $O$ whose effect is observable by $e_2$---
that is, the state change produced by $e_1$ influences the
response of $e_2$---then $e_1 \hbL e_2$ (e.g., $e_1$ writes to $O$ and $e_2$ reads from $O$).
\item \emph{Transitivity}: if $e_1 \hbL e_2$ and $e_2 \hbL e_3$,
then $e_1 \hbL e_3$.
\end{enumerate}
\end{definition}
\noindent
In the special case where shared objects are read/write registers,
condition~(L2) reduces to the standard read-from relation:
$e_1$ writes a value to register $r$ and $e_2$ reads that value
from $r$.
\noindent
Restricted to $\Eobs$, we write $\hbL[\Eobs]$ for the relation
$\hbL$ induced on boundary events.
Vector clocks~\cite{Fidge88,Mattern88} reconstruct $\hbL[\Eobs]$
exactly: $e_1 \hbL e_2 \iff \mathit{vc}(e_1) < \mathit{vc}(e_2)$.
However, as we show below, $\hbL[\Eobs]$ is not the relation the
protocol needs to report.
%-----------------------------------------------------------------------
\subsection{The Problem}
\label{sec:cop-def}
%-----------------------------------------------------------------------
Let $(\mathbb{T}, <_\mathbb{T})$ be a totally ordered set.
A \emph{timestamping protocol} assigns $\ts(e) \in \mathbb{T}$
to each $e \in \Eobs$.
The client then answers a precedence query by checking whether
$\ts(\res(\mathit{op}_A)) <_\mathbb{T} \ts(\inv(\mathit{op}_B))$.
\begin{definition}[Causal Observability Problem, $\mathbf{COP}$]
\label{def:cop}
The \emph{Causal Observability Problem} asks for a timestamping
protocol assigning $\ts(e) \in \mathbb{T}$ to each $e \in \Eobs$
such that, for all operations $\mathit{op}_A, \mathit{op}_B$:
\begin{enumerate}[(i)]
\item \emph{Completeness}:
$\mathit{op}_A <_H \mathit{op}_B
\;\Rightarrow\;
\ts(\res(\mathit{op}_A)) <_\mathbb{T} \ts(\inv(\mathit{op}_B))$.
\item \emph{Soundness}:
$\ts(\res(\mathit{op}_A)) <_\mathbb{T} \ts(\inv(\mathit{op}_B))
\;\Rightarrow\;
\mathit{op}_A <_H \mathit{op}_B$.
\end{enumerate}
A protocol satisfying only~(i) is \emph{complete};
one satisfying only~(ii) is \emph{sound};
one satisfying both is \emph{strongly consistent}.
\end{definition}
\noindent
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 \emph{missing} a genuine precedence: if
$\mathit{op}_A$ truly completed before $\mathit{op}_B$ began,
the timestamps must reflect that.
Soundness forbids \emph{reporting} a spurious precedence: if the
timestamps say $\mathit{op}_A$ preceded $\mathit{op}_B$, then
$\mathit{op}_A$ must have truly completed before $\mathit{op}_B$
began.
A strongly consistent protocol does both: its timestamp order
is equivalent to $<_H$.
Note that soundness does \emph{not} require timestamps to imply
precedence for concurrent operations --- two concurrent operations
will inevitably be ordered by any total order on $\mathbb{T}$,
and that is acceptable.
What soundness prohibits is asserting a precedence that did not
occur in real time.
%-----------------------------------------------------------------------
\subsection{The Gap Between $<_H$ and $\hbL[\Eobs]$}
\label{sec:gap}
%-----------------------------------------------------------------------
The order the protocol must report, $<_H$, and the order it can
construct, $\hbL[\Eobs]$, both live on $\Eobs$.
They are, however, incomparable as relations.
\begin{claim}
\label{claim:incomparable}
$<_H \,\not\subseteq\, \hbL[\Eobs]$ and
$\hbL[\Eobs] \,\not\subseteq\, {<_H}$.
\end{claim}
\begin{proof}
\emph{$<_H \not\subseteq \hbL[\Eobs]$.}
Let $\mathit{op}_A$ complete at $p_i$ before $\mathit{op}_B$
begins at $p_j$, with no register written by $p_i$ during
$\mathit{op}_A$ subsequently read by $p_j$.
Then $\res(\mathit{op}_A) \prec \inv(\mathit{op}_B)$, so
$\mathit{op}_A <_H \mathit{op}_B$, yet no $\hbL$-chain links
$\res(\mathit{op}_A)$ to $\inv(\mathit{op}_B)$: time elapsed,
but no information was exchanged.
\emph{$\hbL[\Eobs] \not\subseteq {<_H}$.}
Let $\mathit{op}_A$ and $\mathit{op}_B$ overlap
($\mathit{op}_A \parallel \mathit{op}_B$), and let $p_i$ write a
register during $\mathit{op}_A$ that $p_j$ reads during
$\mathit{op}_B$.
By~(L1) and~(L2),
$\inv(\mathit{op}_A) \hbL[\Eobs] \res(\mathit{op}_B)$,
yet $\mathit{op}_A \parallel \mathit{op}_B$ means neither
$\mathit{op}_A <_H \mathit{op}_B$ nor
$\mathit{op}_B <_H \mathit{op}_A$.
\end{proof}
\noindent
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.
$\hbL[\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
$\mathbf{COP}$: they reconstruct $\hbL[\Eobs]$ exactly, but
that is not $<_H$.
A protocol that tracks $\hbL[\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 $\hbL[\Eobs]$, violating soundness.
The following section shows that no protocol can be strongly
consistent for $\mathbf{COP}$: completeness and soundness are
irreconcilable at $\Eobs$.
%=======================================================================
%=======================================================================
%=======================================================================
\section{The Interface Event Layer}
\label{sec:eint}
%=======================================================================
Section~\ref{sec:cop} showed that the order a protocol must report
($<_H$) and the order it can construct from shared memory
($\hbL[\Eobs]$) are incomparable.
A protocol that wants to approximate $<_H$ must construct
$\hbL[\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~\cite{CR23, CR26_JACM, RC24, EF18} and identify two
classes.
Monitors that invoke objects only at one boundary are neither
sound nor complete~\cite{EF18}
(Lemma~\ref{lem:unilateral}, Appendix~\ref{app:placement}).
Monitors that invoke objects at both boundaries fall into one of
two classes: those whose invocations fall strictly inside the
operation interval (\emph{internal placement}) and those whose
invocations strictly enclose it (\emph{external placement}).
Internal placement yields completeness; external placement yields
soundness
(Lemmas~\ref{lem:placement},
\ref{lem:external-not-complete},
and~\ref{lem:internal-not-sound},
Appendix~\ref{app:placement}).
No combination achieves both
(Theorem~\ref{thm:impossibility},
Appendix~\ref{app:impossibility}).
%-----------------------------------------------------------------------
\subsection{Interface Events and Monitors}
%-----------------------------------------------------------------------
A protocol that monitors $\mathbf{COP}$ cannot observe the true
boundaries $\inv(\mathit{op})$ and $\res(\mathit{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 $\hbL[\Eobs]$.
\begin{definition}[Monitor]
\label{def:monitor}
A \emph{monitor} for $\mathbf{COP}$ is a protocol that, for each
operation $\mathit{op}$, invokes a finite set of shared-memory
objects before and after each true boundary, producing observable
actions called \emph{interface events}.
The monitor answers $\precedes(A, B) = \mathtt{true}$ iff the
interface events establish
$\eres(\mathit{op}_A) \hbL \einv(\mathit{op}_B)$.
\end{definition}
\noindent
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~\cite{H91}.
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 \emph{ideal log}.
\begin{definition}[Ideal log]
\label{def:ideal-log}
A monitor operates under an \emph{ideal log} if every interface
event $e$ has a linearization point $\lp(e)$ such that: $e_1 \hbL e_2 \;\iff\; \lp(e_1) \prec \lp(e_2)$.
\end{definition}
\noindent
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(\mathit{op})$ and the first after
$\inv(\mathit{op})$, intermediate events carry no additional
causal information.
Without loss of generality, we model each monitor as emitting
exactly one interface event per boundary: $\einv(\mathit{op})$
and $\eres(\mathit{op})$.
%-----------------------------------------------------------------------
\subsection{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.
\begin{definition}[Placement]
\label{def:placement}
A monitor has \emph{internal placement} if
$\inv(\mathit{op}) \prec \lp(\einv(\mathit{op}))$ and
$\lp(\eres(\mathit{op})) \prec \res(\mathit{op})$, and
\emph{external placement} if
$\lp(\einv(\mathit{op})) \prec \inv(\mathit{op})$ and
$\res(\mathit{op}) \prec \lp(\eres(\mathit{op}))$.
\end{definition}
\noindent
Internal placement corresponds to online checkers that
instrument the object's internal steps~\cite{CR23}.
External placement corresponds to offline verifiers that wrap
each call site~\cite{CR26_JACM}.
\begin{lemma}[Placement characterization]
\label{lem:placement}
Assuming an ideal log, a monitor with internal placement is
complete for $\mathbf{COP}$, and a monitor with external
placement is sound.
Neither achieves the other property.
See Appendix~\ref{app:placement} for the full proof.
\end{lemma}
%-----------------------------------------------------------------------
\subsection{Impossibility of Strong Consistency}
%-----------------------------------------------------------------------
\begin{theorem}[Impossibility of strong consistency]
\label{thm:impossibility}
No monitor can be strongly consistent for $\mathbf{COP}$, even
with an ideal log.
\end{theorem}
\begin{proof}[Proof sketch]
Fix any monitor $\mathcal{M}$ and two operations $\mathit{op}_A$,
$\mathit{op}_B$ 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 $\hbL[\Eobs]$ under
any ideal log --- can place
$\res(\mathit{op}_A) \prec \inv(\mathit{op}_B)$
(requiring $\precedes(A,B) = \mathtt{true}$) or
$\inv(\mathit{op}_B) \prec \res(\mathit{op}_A)$
(requiring $\precedes(A,B) = \mathtt{false}$).
No single answer satisfies both.
See Appendix~\ref{app:impossibility} for the full proof.
\end{proof}
\noindent
This impossibility was first identified in~\cite{CR23, CR26_JACM}
as a structural limitation of runtime verification of
linearizability.
Theorem~\ref{thm:impossibility} 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.
%=======================================================================
\section{The Causal Monitor Object}
\label{sec:monitor}
The Causal Monitor is a concurrent object that instruments a
target algorithm $A$.
Processes invoke $\addinv(\mathit{id})$ at the start of each
operation and $\addres(\mathit{id})$ at its end, creating the
interface events of Section~\ref{sec:eint}.
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.
\begin{definition}[Causal Monitor --- Sequential Specification]
\label{def:causal-monitor}
Let $\mathcal{I}$ be a universe of operation identifiers.
The abstract state is a sequence
$\mathcal{S} \in (\{I,R\} \times \mathcal{I})^*$,
initially empty; $\mathit{idx}(e,\mathcal{S})$ denotes the
position of $e$ in $\mathcal{S}$, or $\infty$ if absent.
\smallskip\noindent
\textbf{Modification.}
$\addinv(\mathit{id})$ requires $(I,\mathit{id}) \notin
\mathcal{S}$ and appends $(I,\mathit{id})$.
$\addres(\mathit{id})$ requires $(I,\mathit{id}) \in \mathcal{S}$
and $(R,\mathit{id}) \notin \mathcal{S}$, and appends
$(R,\mathit{id})$.
\smallskip\noindent
\textbf{Queries} (both require $(R,\mathit{id}_A),
(R,\mathit{id}_B) \in \mathcal{S}$; state unchanged).
$\precedes(\mathit{id}_A, \mathit{id}_B)$ returns $\mathtt{true}$
iff $\mathit{idx}((R,\mathit{id}_A),\mathcal{S})
\mathit{idx}((I,\mathit{id}_B),\mathcal{S})$.
$\concurrent(\mathit{id}_A,\mathit{id}_B)$ returns $\mathtt{true}$
iff $\neg\,\precedes(\mathit{id}_A,\mathit{id}_B) \land
\neg\,\precedes(\mathit{id}_B,\mathit{id}_A)$.
\end{definition}
%=======================================================================
\section{Implementations}
\label{sec:implementations}
%=======================================================================
We present two implementations of the Causal Monitor.
The first uses a shared counter and is \emph{linearizable}.
The second uses an iterative collect of process registers and is only
\emph{quiescently consistent}.
Despite this internal difference, Section~\ref{sec:correctness} shows
that both resolve $\mathbf{COP}$ with identical external guarantees:
under external placement, both are sound, and neither can be complete
(Theorem~\ref{thm:impossibility}).
The placement of interface events determines what $\mathbf{COP}$
guarantees a monitor provides; the internal consistency of the
timestamp mechanism does not.
Both implementations were introduced in~\cite{RC24} as practical
monitoring tools.
However, \cite{RC24} 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 $\mathbf{COP}$
guarantees despite their internal differences.
That analysis is a contribution of the present work.
%-----------------------------------------------------------------------
\subsection{Counter Monitor}
\label{sec:counter}
%-----------------------------------------------------------------------
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~\ref{alg:counter}.
\textsc{FAInc} reads the counter with a single atomic
\texttt{getAndIncrement}, producing distinct timestamps in real-time
order.
\textsc{Striped} uses a striped counter structured as an array of
per-process cells (analogous to Java's \texttt{LongAdder}~\cite{lea-longadder}),
where each process increments its own cell and reads the global sum
non-atomically.
This eliminates the cache-line contention of a centralized atomic
counter at the cost of allowing two concurrent events to receive the
same timestamp.
\begin{algorithm}[htb]
\caption{Counter-based Causal Monitor}
\label{alg:counter}
\begin{algorithmic}[1]
\Statex \textbf{Shared:} $\Reg[1\dots N]$ (SWMR, append-only);\quad
counter $C$
\Statex \textbf{Parameter:} $\mathit{Mode} \in
\{\textsc{FAInc},\,\textsc{Striped}\}$
\Function{Stamp}{}
\If{$\mathit{Mode} = \textsc{FAInc}$}
\State \Return $C.\texttt{getAndIncrement}()$
\Comment{single atomic step}
\Else
\State $C.\texttt{increment}()$
\State \Return $C.\texttt{sum}()$
\Comment{non-atomic: increment own cell, read all cells}
\EndIf
\EndFunction
\Procedure{Add\_Inv}{$\mathit{id}$}
\State $t \gets \textsc{Stamp}()$;\quad
$\Reg[i] \gets \Reg[i]\cdot\langle(I,\mathit{id},t)\rangle$
\EndProcedure
\Procedure{Add\_Res}{$\mathit{id}$}
\State $t \gets \textsc{Stamp}()$;\quad
$\Reg[i] \gets \Reg[i]\cdot\langle(R,\mathit{id},t)\rangle$
\EndProcedure
\Function{Precedes}{$\mathit{id}_A,\mathit{id}_B$}
\State $t_A \gets$ timestamp stored with $(R,\mathit{id}_A)$
\State $t_B \gets$ timestamp stored with $(I,\mathit{id}_B)$
\State \Return $t_A < t_B$
\EndFunction
\end{algorithmic}
\end{algorithm}
\begin{proposition}[Counter Monitor is linearizable]
\label{prop:counter-lin}
Both \textsc{FAInc} and \textsc{Striped} produce linearizable
executions of the Causal Monitor.
\end{proposition}
\begin{proof}
\emph{\textsc{FAInc}.}
The linearization point of each $\addinv$ or $\addres$ call is the
atomic \texttt{getAndIncrement} instruction.
Timestamps are strictly increasing in real time, so the sequential
history ordered by timestamp satisfies the specification.
\emph{\textsc{Striped}.}
See Appendix~\ref{app:striped}.
\end{proof}
\noindent
The \textsc{FAInc} counter was introduced in~\cite{RC24} grouped
with the Collect monitor (Algorithm~\ref{alg:collect}) as a variant of the same approach.
\textsc{Striped} is introduced in this work and was first described in~\cite{lea-longadder}.
We show in Section~\ref{sec:correctness} that this grouping was
imprecise: both counters are linearizable, whereas \textsc{Collect}
is only quiescently consistent.
All three are sound for $\mathbf{COP}$ under external placement,
but they are not equivalent as concurrent objects.
%-----------------------------------------------------------------------
\subsection{Collect Monitor}
\label{sec:collect}
%-----------------------------------------------------------------------
The Collect Monitor keeps the state explicit.
On $\addres$, the calling process reads all process registers
iteratively --- a non-atomic \emph{collect} --- and stores the
resulting \emph{view} $v$ alongside the response event.
Precedence is then a membership test on stored views.
\begin{algorithm}[H]
\caption{Collect-based Causal Monitor}
\label{alg:collect}
\begin{algorithmic}[1]
\Statex \textbf{Shared:} $\Reg[1\dots N]$ (SWMR, append-only sequences
of events)
\Procedure{Add\_Inv}{$\mathit{id}$}
\State $\Reg[i] \gets \Reg[i]\cdot\langle(I,\mathit{id})\rangle$
\EndProcedure
\Procedure{Add\_Res}{$\mathit{id}$}
\State $v \gets \bigcup_{j=1}^{N}\Reg[j]$
\Comment{iterative, non-atomic read}
\State $\Reg[i] \gets \Reg[i]\cdot\langle(R,\mathit{id},v)\rangle$
\EndProcedure
\Function{Precedes}{$\mathit{id}_A,\mathit{id}_B$}
\State $v_A \gets$ view stored with $(R,\mathit{id}_A)$
\State $v_B \gets$ view stored with $(R,\mathit{id}_B)$
\State \Return
$[(R,\mathit{id}_A) \in v_B]$
$\;\land\;[(I,\mathit{id}_B) \notin v_A]$
$\;\land\;[v_A \subseteq v_B]$
\EndFunction
\end{algorithmic}
\end{algorithm}
\noindent
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, $v_A \subseteq v_B$, 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.
%=======================================================================
\section{Correctness}
\label{sec:correctness}
%=======================================================================
This section establishes two independent facts.
First, both monitors are sound for $\mathbf{COP}$ under external
placement (Theorems~\ref{thm:counter-sound}
and~\ref{thm:collect-sound}): whenever a monitor reports
$\precedes(A,B) = \mathtt{true}$, the operation $\mathit{op}_A$
genuinely completed before $\mathit{op}_B$ began in real time,
i.e.\ $\mathit{op}_A <_H \mathit{op}_B$.
Second, the Counter Monitor is linearizable
(Proposition~\ref{prop:counter-lin}) while the Collect Monitor is
quiescently consistent but not linearizable
(Theorems~\ref{thm:collect-qc} and~\ref{thm:collect-not-lin}).
The main consequence is that the internal
consistency gap between the two monitors is invisible at the
level of $\mathbf{COP}$: placement alone determines what the
problem guarantees.
%-----------------------------------------------------------------------
\subsection{Soundness}
\label{sec:soundness}
%-----------------------------------------------------------------------
\begin{theorem}[Counter Monitor is sound for $\mathbf{COP}$]
\label{thm:counter-sound}
Under external placement, Algorithm~\ref{alg:counter} is sound:
\[
\precedes(A,B) = \mathtt{true}
\;\Rightarrow\; \mathit{op}_A <_H \mathit{op}_B.
\]
\end{theorem}
\begin{proof}
$\precedes(A,B) = \mathtt{true}$ means $t_A < t_B$, where $t_A$
is the timestamp stamped during $\addres(A)$ and $t_B$ is the
timestamp stamped during $\addinv(B)$.
In both \textsc{FAInc} and \textsc{Striped}, timestamps are
monotone in real time: a strictly smaller timestamp means the
corresponding \textsc{Stamp} call completed before the other
began.
Let $\sigma_A$ be the linearization point of the \textsc{Stamp}
call inside $\addres(A)$, and $\sigma_B$ the linearization point
of the \textsc{Stamp} call inside $\addinv(B)$.
Then $t_A < t_B$ implies $\sigma_A \prec \sigma_B$.
External placement gives
$\res(\mathit{op}_A) \prec \sigma_A$,
since $\addres(A)$ is invoked after $\mathit{op}_A$ returns and
$\sigma_A$ lies within $\addres(A)$'s execution interval.
Similarly, $\sigma_B \prec \inv(\mathit{op}_B)$,
since $\addinv(B)$ is invoked before $\mathit{op}_B$ starts and
$\sigma_B$ lies within $\addinv(B)$'s execution interval.
Chaining,
\[
\res(\mathit{op}_A)
\prec \sigma_A
\prec \sigma_B
\prec \inv(\mathit{op}_B),
\]
so $\res(\mathit{op}_A) \prec \inv(\mathit{op}_B)$,
i.e.\ $\mathit{op}_A <_H \mathit{op}_B$.
\end{proof}
\begin{theorem}[Collect Monitor is sound for $\mathbf{COP}$]
\label{thm:collect-sound}
Under external placement, Algorithm~\ref{alg:collect} is sound:
\[
\precedes(A,B) = \mathtt{true}
\;\Rightarrow\; \mathit{op}_A <_H \mathit{op}_B.
\]
\end{theorem}
\begin{proof}
Suppose $\precedes(A,B) = \mathtt{true}$.
The predicate has three conjuncts; we use only the second:
$(I,\mathit{id}_B) \notin v_A$.
This means that when $A$'s collect read $\Reg[\mathrm{proc}(B)]$,
the write of $(I,\mathit{id}_B)$ had not yet occurred.
Let $\rho$ be the physical time of that read and $w_I$ the
physical time of the write of $(I,\mathit{id}_B)$;
then $\rho \prec w_I$.
External placement gives two facts.
First, $\addres(A)$ is invoked after $\mathit{op}_A$ returns,
so $\res(\mathit{op}_A) \prec \inv(\addres(A))$; since $\rho$
occurs during $\addres(A)$'s collect,
$\res(\mathit{op}_A) \prec \rho$.
Second, $\addinv(B)$ is invoked before $\mathit{op}_B$ starts,
so the write $w_I$ of $(I,\mathit{id}_B)$, which occurs inside
$\addinv(B)$, satisfies $w_I \prec \inv(\mathit{op}_B)$.
Chaining,
\[
\res(\mathit{op}_A) \prec \rho \prec w_I \prec \inv(\mathit{op}_B),
\]
so $\res(\mathit{op}_A) \prec \inv(\mathit{op}_B)$,
i.e.\ $\mathit{op}_A <_H \mathit{op}_B$.
\end{proof}
\noindent
This proof uses only the conjunct $(I,\mathit{id}_B) \notin v_A$.
The first conjunct $(R,\mathit{id}_A) \in v_B$ and the
view-containment conjunct $v_A \subseteq v_B$ 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~\ref{lem:partial-order}.
Soundness holds independently of whether $\precedes$ is transitive.
%-----------------------------------------------------------------------
\subsection{Consistency of the Collect Monitor}
\label{sec:collect-consistency}
%-----------------------------------------------------------------------
% En el cuerpo, reemplaza el lema y su prueba con esto:
\begin{lemma}[$\precedes$ is a strict partial order under Collect]
\label{lem:partial-order}
With the view-containment conjunct, $\precedes$ is irreflexive,
antisymmetric, and transitive.
\end{lemma}
\begin{proof}[Proof sketch]
\emph{Irreflexivity} follows because a collect completes before
its own response is written, so $(R,A) \notin v_A$.
\emph{Antisymmetry} follows because if $\precedes(A,B)$ then
$(I,A) \in v_B$, which refutes the conjunct $(I,A) \notin v_B$
required by $\precedes(B,A)$.
\emph{Transitivity} follows from view-containment: if
$\precedes(A,B)$ and $\precedes(B,C)$ then
$v_A \subseteq v_B \subseteq v_C$, from which all three conjuncts
of $\precedes(A,C)$ can be derived.
See Appendix~\ref{app:partial-order} for the full proof.
\end{proof}
% En el cuerpo, reemplaza los dos teoremas y sus pruebas con esto:
\begin{theorem}[Collect Monitor is not linearizable]
\label{thm:collect-not-lin}
Algorithm~\ref{alg:collect} is not sequentially consistent, hence
not linearizable.
\end{theorem}
\begin{proof}[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) = \mathtt{true}$ and
$\precedes(C,B) = \precedes(A,D) = \mathtt{false}$, which forces
any sequential history to satisfy
$R_A \prec_S I_B \prec_S R_C \prec_S I_D \prec_S R_A$,
a cycle.
See Appendix~\ref{app:not-lin} for the full construction.
\end{proof}
\begin{theorem}[Collect Monitor is quiescently consistent]
\label{thm:collect-qc}
Under external placement, Algorithm~\ref{alg:collect} is quiescently
consistent: if a quiescent instant $Q$ satisfies
$\res(\mathit{op}_A) \prec Q \prec \inv(\mathit{op}_B)$,
then $\precedes(A,B) = \mathtt{true}$.
\end{theorem}
\begin{proof}[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~\ref{app:collect-qc} for the full proof.
\end{proof}
%-----------------------------------------------------------------------
\subsection{Both monitors solve the same problem}
\label{sec:cop-invariance}
%-----------------------------------------------------------------------
The Counter Monitor is linearizable and the Collect Monitor is only
quiescently consistent.
Nevertheless, both are sound for $\mathbf{COP}$ under external
placement, and neither can be complete
(Theorem~\ref{thm:impossibility}).
This has a practical consequence identified in~\cite{RC24} but not
formally justified there: the Collect Monitor and the \textsc{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
$\mathbf{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 $\mathbf{COP}$ framework is what makes precise why, despite this
difference, they are equivalent for the purpose of causal observation.
%=======================================================================
\section{Empirical Evaluation}
\label{sec:evaluation}
%=======================================================================
The theoretical results of Section~\ref{sec:correctness} establish
that the Counter Monitor (\textsc{FAInc} and \textsc{Striped}) and
the Collect Monitor solve $\mathbf{COP}$ with identical guarantees
under external placement, despite their internal consistency
difference.
We evaluate this claim empirically in the context of
\emph{runtime verification (RV) of linearizability}~\cite{RPC26},
which provides a concrete setting where $\mathbf{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~\cite{CR26_JACM}.
A monitor is \emph{RV-complete} if it never rejects a genuinely
linearizable execution, and \emph{RV-sound} if it never accepts a
non-linearizable one.
By Lemma~\ref{lem:placement}, external placement guarantees
$\mathbf{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 \textsc{FAInc} and Collect was carried out
in~\cite{RC24, RPC26}, where Collect was shown to match or outperform
\textsc{FAInc} in scalability while providing the same detection
behavior.
The contribution of the present evaluation is to introduce
\textsc{Striped} into this comparison.
\textsc{Striped} is a linearizable counter that eliminates the
cache-line contention of \textsc{FAInc} by distributing increments
across per-process cells.
We ask two questions:
\begin{itemize}
\item \textbf{RQ1 (Verdict consistency):} Does \textsc{Striped}
detect linearizability violations at the same rate as
\textsc{FAInc}, or does its non-atomic sum introduce
observable differences in detection behavior?
\item \textbf{RQ2 (Scalability):} Does \textsc{Striped} eliminate
the contention bottleneck of \textsc{FAInc} while remaining
competitive with Collect?
\end{itemize}
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.~\cite{georges2007java} (5 warmup rounds,
10 measured rounds, 100 runs per cell for verdict experiments).
%-----------------------------------------------------------------------
\subsection{RQ1: Verdict Consistency}
\label{sec:rq1}
%-----------------------------------------------------------------------
\begin{figure}[t]
\centering
\includegraphics[width=0.6\columnwidth]{figures/detection_rate_nonlinearizable.pdf}
\caption{Bug detection rate on \texttt{NonLinearizableQueue}
(100 runs per cell). \textsc{Striped} converges to the
same detection rate as \textsc{FAInc} at 16 threads and
above.}
\label{fig:detection}
\end{figure}
Figure~\ref{fig:detection} shows the detection rate on a
\texttt{NonLinearizableQueue} across thread counts.
\textsc{FAInc} reaches 100\% detection consistently from low thread
counts.
\textsc{Striped} starts slightly below \textsc{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 \textsc{Striped} and \textsc{FAInc} at low
concurrency is a direct consequence of the non-atomic
\texttt{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 \textsc{Striped}
converges to \textsc{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.
%-----------------------------------------------------------------------
\subsection{RQ2: Scalability}
\label{sec:rq2}
%-----------------------------------------------------------------------
\begin{figure*}[t]
\centering
\includegraphics[width=\textwidth]{figures/instrumentation_overhead_10k.pdf}
\caption{Mean execution time (left) and maximum latency (right)
at 10,000 operations per thread.
\textsc{FAInc} collapses at 64 threads due to cache-line
contention on the centralized counter.
\textsc{Striped} and Collect remain stable across all
thread counts.}
\label{fig:overhead}
\end{figure*}
Figure~\ref{fig:overhead} 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
\textsc{FAInc} counter.
Beyond 16 threads the difference becomes visible, and at 64 threads
\textsc{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.
\textsc{Striped} and Collect remain stable across all thread counts,
with mean times near 575\,ms and maximum latency near 580\,ms at
64 threads.
\textsc{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.
These results answer RQ2 affirmatively: \textsc{Striped} eliminates
the scalability bottleneck of \textsc{FAInc} while matching Collect
in throughput.
Combined with the verdict results of RQ1, the conclusion is that
\textsc{Striped} is a strictly better choice than \textsc{FAInc}
as a linearizable implementation of the Causal Monitor: it provides
the same $\mathbf{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~\cite{RC24, RPC26} to outperform \textsc{FAInc}
precisely because it avoids centralized synchronization.
\textsc{Striped} now shows that a \emph{linearizable} counter can
match that performance.
The theoretical gap between linearizability and quiescent consistency
--- which Theorems~\ref{thm:collect-not-lin}
and~\ref{thm:collect-qc} 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.
%=======================================================================
\section{Related Work}
\label{sec:cmp}
The problem of monitoring linearizability at runtime was studied
in~\cite{CR23, CR26_JACM}, 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~\cite{RC24} introduced the Collect Monitor and the
\textsc{FAInc} Counter Monitor as more practical tools, presenting
both under internal placement and treating them as equivalent
implementations.
In~\cite{RPC26}, Collect was shown empirically to outperform
\textsc{FAInc} in scalability.
The present paper formalizes that limitation as $\mathbf{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
\emph{not} equivalent as concurrent objects, despite solving the
same problem --- and introduces \textsc{Striped} as a linearizable
monitor that matches the scalability of Collect while providing
stronger internal consistency guarantees.
El-Hoyakem and Falcone~\cite{EF18} proposed a monitor that instruments only
one boundary of each operation.
As noted in Section~\ref{sec:eint}, such monitors are neither sound
nor complete: they do not solve $\mathbf{COP}$.
Lowe~\cite{Lowe17} studied linearizability checking offline, where
the full history is available after execution; that setting does not
face the observability constraints that define $\mathbf{COP}$.\\
%\paragraph{Causality tracking: scalar, vector, and matrix clocks.}
Classical causal monitoring was designed for the message-passing
model, where the goal is to reconstruct the flow of information
across the entire execution~\cite{Lamport78, Fidge88, Mattern88,
Wuu84, RS96}.
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 $\hbL$.
Scalar clocks~\cite{Lamport78} assign a single integer to each
event and achieve completeness for $\hbL$ over $\Eall$, but not
soundness: a smaller timestamp does not imply causal precedence.
Vector clocks~\cite{Fidge88, Mattern88} achieve strong consistency
for $\hbL$ over $\Eall$: $e_1 \hbL e_2 \iff \mathit{vc}(e_1)
\mathit{vc}(e_2)$.
Matrix clocks~\cite{Wuu84} extend this with second-order knowledge,
at $O(n^2)$ cost per event.
These tools do not solve $\mathbf{COP}$ because, as shown in
Claim~\ref{claim:incomparable}, $\hbL[\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~\ref{tab:cmp} summarizes the comparison.
\begin{table}[ht]
\centering
\caption{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.}
\label{tab:cmp}
\renewcommand{\arraystretch}{1.3}
\begin{tabular}{@{}lllllc@{}}
\toprule
\textbf{Tool}
& \textbf{Events}
& \textbf{Target}
& \textbf{Compl.}
& \textbf{Sound}
& \textbf{Cost} \\
\midrule
Scalar clock~\cite{Lamport78}
& $\Eall$ & $\hbL$ & \checkmark & $\times$ & $O(1)$ \\
Vector clock~\cite{Fidge88,Mattern88}
& $\Eall$ & $\hbL$ & \checkmark & \checkmark & $O(n)$ \\
Matrix clock~\cite{Wuu84}
& $\Eall$ & $\hbL$ & \checkmark & \checkmark & $O(n^2)$ \\
\midrule
Causal Monitor (this work)
& $\Eobs$ & $<_H$ & \multicolumn{2}{c}{mutually exclusive} & $O(1)$/$O(N)$ \\
\bottomrule
\end{tabular}
\end{table}
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 well-defined external
problem.
\section{Discussion and Further Work}
\label{sec:discussion}
The Causal Monitor is a tool for observing real-time precedence
in concurrent executions, and $\mathbf{COP}$ is the problem of
designing such a monitor under the constraints imposed by the
observable boundary.
This paper motivated $\mathbf{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 $\mathbf{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~\cite{Lamport78}.
Systems such as \textit{GentleRain} and \textit{Cure}~\cite{GentleRain, Cure}
enforce this by tracking causal timestamps, which is precisely
an instance of $\mathbf{COP}$ where the observable set is the
boundary of client transactions and the target relation is
real-time 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~\cite{Dapper10} and X-Trace~\cite{XTrace07} 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.
$\mathbf{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 $\hbL$ 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 $\hbL$ and $\hbL[\Eall]$ coincide.
The interesting case is the boundary: when the observable set
shrinks to $\Eobs$, the Claim of Section~\ref{sec:cop} shows
that $\hbL[\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 $\mathbf{COP}$: does every sound
quiescently consistent monitor for $\mathbf{COP}$ require at
least the state and communication complexity of Collect?
Conversely, is there a quiescently consistent monitor that is
sound for $\mathbf{COP}$ and strictly cheaper than Collect?
We leave this as future work.
\bibliography{biblio}
\appendix
% %=======================================================================
%-----------------------------------------------------------------------
\section{Placement Cases}
\label{app:placement}
%-----------------------------------------------------------------------
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(\cdot)$, and the
causal order observable by the monitor agrees with the real-time
order of these points:
$e_1 \hbL e_2 \iff \lp(e_1) \prec \lp(e_2)$.
%-----------------------------------------------------------------------
\subsection*{Unilateral Placement}
%-----------------------------------------------------------------------
\begin{lemma}[Unilateral placement achieves neither soundness nor
completeness]
\label{lem:unilateral}
Let $\mathcal{M}$ be a monitor that invokes objects only before
both boundaries (only before $\inv(\mathit{op})$ and
$\res(\mathit{op})$) or only after both boundaries.
Then $\mathcal{M}$ is neither sound nor complete for
$\mathbf{COP}$.
\end{lemma}
\begin{proof}
We prove both cases.
\emph{Case 1: only before both boundaries.}
The monitor invokes objects before $\inv(\mathit{op})$ and before
$\res(\mathit{op})$, producing interface events
$\einv(\mathit{op})$ and $\eres(\mathit{op})$ with
$\lp(\einv(\mathit{op})) \prec \inv(\mathit{op})$ and
$\lp(\eres(\mathit{op})) \prec \res(\mathit{op})$.
\emph{Not complete.}
Consider $\mathit{op}_A <_H \mathit{op}_B$, so
$\res(\mathit{op}_A) \prec \inv(\mathit{op}_B)$.
The monitor's event for the response of $\mathit{op}_A$ fires
before $\res(\mathit{op}_A)$, and the monitor's event for the
invocation of $\mathit{op}_B$ fires before $\inv(\mathit{op}_B)$.
No causal chain is established between $\eres(\mathit{op}_A)$ and
$\einv(\mathit{op}_B)$: $\eres(\mathit{op}_A)$ fires before
$\res(\mathit{op}_A)$ and $\einv(\mathit{op}_B)$ fires before
$\inv(\mathit{op}_B)$, but $\eres(\mathit{op}_A)$ may fire after
$\einv(\mathit{op}_B)$ even when $\mathit{op}_A <_H \mathit{op}_B$.
Concretely: if $p_i$ delays firing $\eres(\mathit{op}_A)$ until
just before $\res(\mathit{op}_A)$, and $p_j$ fires
$\einv(\mathit{op}_B)$ early, the real-time order of the interface
events may be $\einv(\mathit{op}_B) \prec \eres(\mathit{op}_A)$
despite $\mathit{op}_A <_H \mathit{op}_B$.
The monitor misses a genuine precedence.
\emph{Not sound.}
Consider $\mathit{op}_A \parallel \mathit{op}_B$.
The monitor fires $\eres(\mathit{op}_A)$ before $\res(\mathit{op}_A)$
and $\einv(\mathit{op}_B)$ before $\inv(\mathit{op}_B)$.
If $\eres(\mathit{op}_A)$ happens to fire before
$\einv(\mathit{op}_B)$ in real time, the monitor reports
$\precedes(A,B) = \mathtt{true}$, but $\mathit{op}_A \parallel
\mathit{op}_B$ means $\mathit{op}_A <_H \mathit{op}_B$ is false.
A spurious precedence is reported.
\emph{Case 2: only after both boundaries.}
The monitor invokes objects after $\inv(\mathit{op})$ and after
$\res(\mathit{op})$, producing interface events with
$\inv(\mathit{op}) \prec \lp(\einv(\mathit{op}))$ and
$\res(\mathit{op}) \prec \lp(\eres(\mathit{op}))$.
\emph{Not complete.}
Consider $\mathit{op}_A <_H \mathit{op}_B$, so
$\res(\mathit{op}_A) \prec \inv(\mathit{op}_B)$.
The monitor fires $\eres(\mathit{op}_A)$ after $\res(\mathit{op}_A)$
and $\einv(\mathit{op}_B)$ after $\inv(\mathit{op}_B)$.
If $p_j$ fires $\einv(\mathit{op}_B)$ immediately after
$\inv(\mathit{op}_B)$ while $p_i$ delays $\eres(\mathit{op}_A)$,
the real-time order may be $\einv(\mathit{op}_B) \prec
\eres(\mathit{op}_A)$ despite $\mathit{op}_A <_H \mathit{op}_B$.
The monitor misses a genuine precedence.
\emph{Not sound.}
Consider $\mathit{op}_A \parallel \mathit{op}_B$.
The monitor fires $\eres(\mathit{op}_A)$ after $\res(\mathit{op}_A)$
and $\einv(\mathit{op}_B)$ after $\inv(\mathit{op}_B)$.
If $\eres(\mathit{op}_A)$ fires before $\einv(\mathit{op}_B)$,
the monitor reports $\precedes(A,B) = \mathtt{true}$, but
$\mathit{op}_A \parallel \mathit{op}_B$ so no real precedence
exists.
A spurious precedence is reported.
\end{proof}
%-----------------------------------------------------------------------
\subsection*{External Placement: Sound but Not Complete}
%-----------------------------------------------------------------------
\begin{lemma}[External placement is not complete]
\label{lem:external-not-complete}
A monitor with external placement is sound for $\mathbf{COP}$
(Lemma~\ref{lem:placement}) but not complete: there exist
executions where $\mathit{op}_A <_H \mathit{op}_B$ yet
$\precedes(A,B) = \mathtt{false}$.
\end{lemma}
\begin{proof}
External placement gives
$\lp(\einv(\mathit{op})) \prec \inv(\mathit{op})$ and
$\res(\mathit{op}) \prec \lp(\eres(\mathit{op}))$.
Consider two operations $\mathit{op}_A$ on $p_i$ and
$\mathit{op}_B$ on $p_j$ with $\mathit{op}_A <_H \mathit{op}_B$:
$\res(\mathit{op}_A) \prec \inv(\mathit{op}_B)$.
The monitor fires $\eres(\mathit{op}_A)$ after $\res(\mathit{op}_A)$
and $\einv(\mathit{op}_B)$ before $\inv(\mathit{op}_B)$.
There is no constraint forcing
$\lp(\eres(\mathit{op}_A)) \prec \lp(\einv(\mathit{op}_B))$:
if $p_j$ fires $\einv(\mathit{op}_B)$ very early (long before
$\inv(\mathit{op}_B)$) and $p_i$ fires $\eres(\mathit{op}_A)$
late (just after $\res(\mathit{op}_A)$), then
$\lp(\einv(\mathit{op}_B)) \prec \lp(\eres(\mathit{op}_A))$
even though $\mathit{op}_A <_H \mathit{op}_B$.
The monitor observes $\einv(\mathit{op}_B)$ before
$\eres(\mathit{op}_A)$ and reports
$\precedes(A,B) = \mathtt{false}$, missing a genuine precedence.
\end{proof}
%-----------------------------------------------------------------------
\subsection*{Internal Placement: Complete but Not Sound}
%-----------------------------------------------------------------------
\begin{lemma}[Internal placement is not sound]
\label{lem:internal-not-sound}
A monitor with internal placement is complete for $\mathbf{COP}$
(Lemma~\ref{lem:placement}) but not sound: there exist executions
where $\mathit{op}_A \parallel \mathit{op}_B$ yet
$\precedes(A,B) = \mathtt{true}$.
\end{lemma}
\begin{proof}
Internal placement gives
$\inv(\mathit{op}) \prec \lp(\einv(\mathit{op}))$ and
$\lp(\eres(\mathit{op})) \prec \res(\mathit{op})$.
Consider two operations $\mathit{op}_A$ on $p_i$ and
$\mathit{op}_B$ on $p_j$ with $\mathit{op}_A \parallel
\mathit{op}_B$: their execution intervals overlap.
The monitor fires $\eres(\mathit{op}_A)$ before
$\res(\mathit{op}_A)$ and $\einv(\mathit{op}_B)$ after
$\inv(\mathit{op}_B)$.
Since the operations overlap and the processes are asynchronous,
it is possible that $\lp(\eres(\mathit{op}_A)) \prec
\lp(\einv(\mathit{op}_B))$ even though the operations are
concurrent: $p_i$ fires $\eres(\mathit{op}_A)$ early in its
interval while $p_j$ fires $\einv(\mathit{op}_B)$ late in its
interval.
The monitor observes $\eres(\mathit{op}_A)$ before
$\einv(\mathit{op}_B)$ and reports
$\precedes(A,B) = \mathtt{true}$, but
$\mathit{op}_A \parallel \mathit{op}_B$ so no real precedence
exists.
A spurious precedence is reported.
\end{proof}
%-----------------------------------------------------------------------
\section{Proof of Theorem~\ref{thm:impossibility}}
\label{app:impossibility}
%-----------------------------------------------------------------------
\begin{proof}
We prove that no monitor $\mathcal{M}$ can be strongly consistent
for $\mathbf{COP}$, even under an ideal log
(Definition~\ref{def:ideal-log}) and even if $\mathcal{M}$ uses
shared-memory objects of arbitrary power.
\subsection*{Setup.}
Fix any monitor $\mathcal{M}$ and any two operations
$\mathit{op}_A$ on process $p_i$ and $\mathit{op}_B$ on process
$p_j$, where $p_i \ne p_j$.
By Definition~\ref{def:monitor} and the WLOG argument of
Section~\ref{sec:eint}, we may assume without loss of generality
that $\mathcal{M}$ emits exactly one interface event per boundary:
$\eres(\mathit{op}_A)$ associated with the response of
$\mathit{op}_A$, and $\einv(\mathit{op}_B)$ associated with the
invocation of $\mathit{op}_B$.
Under an ideal log, each interface event takes effect at a single
linearization point: $\lp(\eres(\mathit{op}_A))$ and
$\lp(\einv(\mathit{op}_B))$.\\
%\paragraph{The unavoidable windows.}
The true boundary $\res(\mathit{op}_A)$ is a transfer of control
between $p_i$ and its caller.
The interface event $\eres(\mathit{op}_A)$ is a shared-memory
step.
These are events of distinct categories and therefore have
distinct points in real time: $\res(\mathit{op}_A) \ne
\lp(\eres(\mathit{op}_A))$.
Let $a^-$ be the linearization point of the last interface event
of $\mathit{op}_A$ that precedes $\res(\mathit{op}_A)$ in program
order, and let $a^+ = \lp(\eres(\mathit{op}_A))$.
The true boundary $\res(\mathit{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(\mathit{op}_A)$ and $\eres(\mathit{op}_A)$
the same event, which is impossible since one is a control
transfer and the other is a shared-memory write.
Define the window $(b^-, b^+)$ around $\inv(\mathit{op}_B)$
symmetrically, where $b^- = \lp(\einv(\mathit{op}_B))$ and $b^+$
is the linearization point of the first interface event of
$\mathit{op}_B$ that follows $\inv(\mathit{op}_B)$ in program
order.
By the same argument, $\inv(\mathit{op}_B)$ lies strictly inside
$(b^-, b^+)$ and this window cannot be closed.
%\paragraph{Constructing the overlapping schedule.}
The following diagram illustrates the two windows and their
overlap:
\[
\underbrace{%
\overbrace{a^- \;\cdots\; \res(\mathit{op}_A) \;\cdots\; a^+}^{%
\text{window } (a^-, a^+)}
\qquad
\overbrace{b^- \;\cdots\; \inv(\mathit{op}_B) \;\cdots\; b^+}^{%
\text{window } (b^-, b^+)}
}_{\text{overlap } W \ne \emptyset \text{ by adversarial scheduling}}
\]
Because $p_i$ and $p_j$ are asynchronous --- no bound on relative
speeds --- an adversary can schedule their steps so that the two
windows overlap:
\[
W = \bigl(\max(a^-, b^-),\;\min(a^+, b^+)\bigr) \ne \emptyset.
\]
Concretely: the adversary slows $p_j$ until $\einv(\mathit{op}_B)$
fires at the same time that $p_i$ is executing inside $(a^-, a^+)$,
and symmetrically delays $p_i$ so that $\eres(\mathit{op}_A)$ fires
while $p_j$ is inside $(b^-, b^+)$.
Since the two processes share no synchronization that could prevent
this interleaving, such a schedule always exists.
\subsection*{The indistinguishable executions.}
With $W \ne \emptyset$, we place $\res(\mathit{op}_A)$ and
$\inv(\mathit{op}_B)$ at two different positions within $W$:
\medskip
\begin{center}
\begin{tabular}{lll}
\toprule
& \textbf{Position of true boundaries} & \textbf{Relation} \\
\midrule
$E_1$ & $\res(\mathit{op}_A) \prec \inv(\mathit{op}_B)$ in $W$
& $\mathit{op}_A <_H \mathit{op}_B$ \\
$E_2$ & $\inv(\mathit{op}_B) \prec \res(\mathit{op}_A)$ in $W$
& $\mathit{op}_A \parallel \mathit{op}_B$ \\
\bottomrule
\end{tabular}
\end{center}
\medskip
Both executions are identical in every shared-memory step: the
interface events $\eres(\mathit{op}_A)$ and $\einv(\mathit{op}_B)$
fire at the same times $a^+$ and $b^-$ respectively, and all other
monitor steps are unchanged.
Since $\res(\mathit{op}_A)$ and $\inv(\mathit{op}_B)$ are not
shared-memory steps, moving them within $W$ does not alter any
linearization point, any register value, or any causal chain
observable by $\mathcal{M}$.
Under an ideal log, the log of $\mathcal{M}$ is therefore
identical in $E_1$ and $E_2$.
%\paragraph{The contradiction.}
$\mathcal{M}$ must return a single answer for $\precedes(A,B)$
based on its log, and that answer is the same in $E_1$ and $E_2$.
But strong consistency requires:
\begin{itemize}
\item In $E_1$: $\mathit{op}_A <_H \mathit{op}_B$, so
completeness requires $\precedes(A,B) = \mathtt{true}$.
\item In $E_2$: $\mathit{op}_A \parallel \mathit{op}_B$, so
soundness requires $\precedes(A,B) = \mathtt{false}$.
\end{itemize}
No single answer satisfies both.
Therefore $\mathcal{M}$ cannot be strongly consistent for
$\mathbf{COP}$.
%\paragraph{Why the ideal log does not help.}
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(\mathit{op}_A)$ and
$\inv(\mathit{op}_B)$ 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.
\end{proof}
%=======================================================================
%-----------------------------------------------------------------------
\section{Linearizability of the \textsc{Striped} Counter}
\label{app:striped}
%-----------------------------------------------------------------------
\subsection*{Implementation}
The \textsc{Striped} counter is implemented as an array of $N$
per-process atomic cells $C[1\dots N]$, where process $p_i$ only
increments $C[i]$.
The \textsc{Stamp} function for process $p_i$ executes:
\begin{enumerate}
\item $C[i].\texttt{incrementAndGet}()$
\hfill (atomic write to own cell)
\item \textbf{return} $\sum_{j=1}^{N} C[j].\texttt{get}()$
\hfill (non-atomic traversal of all cells)
\end{enumerate}
In Java, this is implemented using an \texttt{AtomicLongArray} with
memory padding between cells to prevent false sharing on cache
lines~\cite{lea-longadder}.
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 \textsc{Stamp} call.
This ensures that the value returned by \texttt{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.
\subsection*{Proof of linearizability}
We prove that \textsc{Striped} satisfies
Proposition~\ref{prop:counter-lin}.
\begin{proof}
We must show that every execution of the \textsc{Striped} Counter
Monitor admits a linearization: a legal sequential history in which
each operation's linearization point $\lp(\cdot)$ falls within its
execution interval.\\
%\paragraph{Existence of a linearization point.}
Consider any \textsc{Stamp} call by process $p_i$ that returns
value $t$.
The call first increments $C[i]$, then reads the sum
$\sum_{j=1}^{N} 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 $s_{\mathit{start}}$ be the true global sum at
the moment the traversal begins and $s_{\mathit{end}}$ be the true
global sum at the moment it ends.
The returned value $t$ satisfies
$s_{\mathit{start}} \le t \le s_{\mathit{end}}$,
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
\textsc{Stamp} call and serves as its linearization point.\\
%\paragraph{Monotonicity across non-overlapping calls.}
Let $s_1$ and $s_2$ be two \textsc{Stamp} calls where $s_1$
completes before $s_2$ begins.
Since every \textsc{Stamp} increments before summing, the
increment of $s_1$ is complete before $s_2$ begins.
When $s_2$ executes its sum traversal, it reads every cell after
$s_1$'s increment has taken effect, so it observes a global sum
strictly greater than $s_1$'s contribution.
In particular, $\ts(s_2) \ge \ts(s_1) + 1 > \ts(s_1)$:
non-overlapping calls receive strictly increasing timestamps.\\
%\paragraph{Ties imply overlap.}
Suppose two calls $s_1$ and $s_2$ return the same value $t$.
By the argument above, non-overlapping calls receive strictly
different timestamps.
Therefore $s_1$ and $s_2$ 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.\\
%\paragraph{Correctness of \textsc{Precedes}.}
For a query $\precedes(A,B)$ returning \texttt{true}, we have
$t_A < t_B$, where $t_A$ is the timestamp of $\addres(A)$ and
$t_B$ is the timestamp of $\addinv(B)$.
By monotonicity, $t_A < t_B$ implies $\lp(\addres(A)) \prec
\lp(\addinv(B))$, so $\addres(A)$ precedes $\addinv(B)$ in the
linearization.
This matches the sequential specification, which returns
\texttt{true} exactly when $A$'s response record precedes $B$'s
invocation record in the state.
\end{proof}
\subsection*{Note on false sharing and padding}
The \texttt{AtomicLongArray} with padding is structurally similar
to Java's \texttt{LongAdder}~\cite{lea-longadder}, but with a
critical difference: \texttt{LongAdder} supports both increment
and decrement and is designed for accumulation, not for
monotone counting.
\textsc{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.
%-----------------------------------------------------------------------
\section{Proof of Lemma~\ref{lem:partial-order}}
\label{app:partial-order}
%-----------------------------------------------------------------------
We prove that $\precedes$ under the Collect Monitor
(Algorithm~\ref{alg:collect}) is a strict partial order, assuming
the view-containment conjunct $v_A \subseteq v_B$ is included in
the predicate.
Recall that $\precedes(\mathit{id}_A, \mathit{id}_B)$ returns
$\mathtt{true}$ iff all three of the following hold:
\begin{enumerate}[(C1)]
\item $(R,\mathit{id}_A) \in v_B$,
\item $(I,\mathit{id}_B) \notin v_A$,
\item $v_A \subseteq v_B$.
\end{enumerate}
\begin{proof}[Full proof of Lemma~\ref{lem:partial-order}]
\emph{Irreflexivity: $\precedes(A,A) = \mathtt{false}$.}
The collect of $\addres(A)$ runs to completion before the write
of $(R,A)$ to $\Reg[\mathrm{proc}(A)]$ occurs --- the collect
is part of $\addres(A)$ and the write happens at the end of it.
Therefore $(R,A) \notin v_A$, which violates~(C1).
Hence $\precedes(A,A) = \mathtt{false}$.
\emph{Antisymmetry: $\precedes(A,B) \Rightarrow \neg\precedes(B,A)$.}
Suppose $\precedes(A,B) = \mathtt{true}$.
By~(C1), $(R,A) \in v_B$.
Since registers are append-only and process $\mathrm{proc}(A)$
appends $(I,A)$ strictly before $(R,A)$ on $\Reg[\mathrm{proc}(A)]$,
and $v_B$ is a prefix-closed snapshot of the registers, it follows
that $(I,A) \in v_B$ as well.
Now consider $\precedes(B,A)$: it would require $(I,A) \notin v_B$
by~(C2) with the roles of $A$ and $B$ swapped.
But we just showed $(I,A) \in v_B$, so~(C2) fails and
$\precedes(B,A) = \mathtt{false}$.
\emph{Transitivity: $\precedes(A,B) \land \precedes(B,C)
\Rightarrow \precedes(A,C)$.}
Suppose $\precedes(A,B) = \mathtt{true}$ and
$\precedes(B,C) = \mathtt{true}$.
We verify the three conjuncts of $\precedes(A,C)$.
\emph{(C1) for $\precedes(A,C)$: $(R,A) \in v_C$.}
From $\precedes(A,B)$, conjunct~(C1) gives $(R,A) \in v_B$.
From $\precedes(B,C)$, conjunct~(C3) gives $v_B \subseteq v_C$.
Therefore $(R,A) \in v_C$.
\emph{(C2) for $\precedes(A,C)$: $(I,C) \notin v_A$.}
From $\precedes(B,C)$, conjunct~(C2) gives $(I,C) \notin v_B$.
From $\precedes(A,B)$, conjunct~(C3) gives $v_A \subseteq v_B$.
Since $(I,C) \notin v_B$ and $v_A \subseteq v_B$, we have
$(I,C) \notin v_A$.
\emph{(C3) for $\precedes(A,C)$: $v_A \subseteq v_C$.}
From $\precedes(A,B)$, conjunct~(C3) gives $v_A \subseteq v_B$.
From $\precedes(B,C)$, conjunct~(C3) gives $v_B \subseteq v_C$.
By transitivity of subset inclusion, $v_A \subseteq v_C$.
All three conjuncts hold, so $\precedes(A,C) = \mathtt{true}$.
\end{proof}
\noindent
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) \notin v_A$, but knowing $(I,C) \notin v_B$ and
$v_A \subseteq v_B$ is what allows us to conclude this.
Without~(C3), $v_A \subseteq v_B$ would not be available and
the derivation would fail.
%-----------------------------------------------------------------------
\section{Proof of Theorem~\ref{thm:collect-not-lin}}
\label{app:not-lin}
%-----------------------------------------------------------------------
We construct a concrete execution of four operations $A, B, C, D$
on distinct processes $p_A, p_B, p_C, p_D$ whose verdicts under
Algorithm~\ref{alg:collect} admit no sequential history.
\paragraph{Write times.}
The interface events are written to shared memory at the following
physical times:
\[
w(I_A){=}1,\quad
w(I_C){=}2,\quad
w(I_B){=}3,\quad
w(I_D){=}4,\quad
w(R_C){=}5,\quad
w(R_A){=}6.
\]
\paragraph{Collect intervals.}
Each process performs its collect for $\addres$ by reading the
registers at the following times:
\begin{itemize}
\item $A$ collects during $[2.0, 2.5)$: reads all registers
while only $I_A$ and $I_C$ have been written.
\item $C$ collects during $[2.5, 3.0)$: reads all registers
while only $I_A$ and $I_C$ have been written.
\item $B$ reads $\Reg[\mathrm{proc}(C)]$ at $t{=}4$
(before $w(R_C){=}5$) and $\Reg[\mathrm{proc}(A)]$
at $t{=}7$ (after $w(R_A){=}6$).
\item $D$ reads $\Reg[\mathrm{proc}(A)]$ at $t{=}5$
(before $w(R_A){=}6$) and $\Reg[\mathrm{proc}(C)]$
at $t{=}6$ (after $w(R_C){=}5$).
\end{itemize}
This is the key crossing: $B$ sees $A$'s response but misses
$C$'s, while $D$ sees $C$'s response but misses $A$'s.
\paragraph{Resulting views.}
\[
\begin{aligned}
v_A &= \{I_A, I_C\}, \\
v_B &= \{I_A, R_A, I_B, I_C, I_D\}, \\
v_C &= \{I_A, I_C\}, \\
v_D &= \{I_A, I_C, R_C, I_D, I_B\}.
\end{aligned}
\]
\paragraph{Evaluating the predicate.}
We check $\precedes(X,Y)$
$= [(R,X) \in v_Y] \land [(I,Y) \notin v_X] \land [v_X \subseteq v_Y]$
for each relevant pair:
\emph{$\precedes(A,B) = \mathtt{true}$:}
$(R,A) \in v_B$ \checkmark;\;
$(I,B) \notin v_A$ \checkmark;\;
$v_A = \{I_A,I_C\} \subseteq v_B$ \checkmark.
\emph{$\precedes(C,D) = \mathtt{true}$:}
$(R,C) \in v_D$ \checkmark;\;
$(I,D) \notin v_C$ \checkmark;\;
$v_C = \{I_A,I_C\} \subseteq v_D$ \checkmark.
\emph{$\precedes(C,B) = \mathtt{false}$:}
$(R,C) \notin v_B$ since $B$ read $\Reg[\mathrm{proc}(C)]$
at $t{=}4$ before $w(R_C){=}5$.
Conjunct~(C1) fails.
\emph{$\precedes(A,D) = \mathtt{false}$:}
$(R,A) \notin v_D$ since $D$ read $\Reg[\mathrm{proc}(A)]$
at $t{=}5$ before $w(R_A){=}6$.
Conjunct~(C1) fails.
\paragraph{No sequential history exists.}
In any sequential history $S$ consistent with these verdicts, the
sequential specification requires:
\[
\precedes(A,B) = \mathtt{true}
\;\Rightarrow\; R_A \prec_S I_B,
\qquad
\precedes(C,D) = \mathtt{true}
\;\Rightarrow\; R_C \prec_S I_D.
\]
The false verdicts require:
\[
\precedes(C,B) = \mathtt{false}
\;\Rightarrow\; I_B \prec_S R_C,
\qquad
\precedes(A,D) = \mathtt{false}
\;\Rightarrow\; I_D \prec_S R_A.
\]
Chaining these four constraints:
\[
R_A \prec_S I_B \prec_S R_C \prec_S I_D \prec_S R_A,
\]
a cycle. No sequential history satisfies all four verdicts
simultaneously, so the Collect Monitor is not sequentially
consistent and a fortiori not linearizable. \qedhere
%-----------------------------------------------------------------------
\section{Proof of Theorem~\ref{thm:collect-qc}}
\label{app:collect-qc}
%-----------------------------------------------------------------------
\begin{proof}
Let $Q$ be a quiescent instant with
$\res(\mathit{op}_A) \prec Q \prec \inv(\mathit{op}_B)$.
Under external placement, $A$'s $\addres$ call is invoked after
$\mathit{op}_A$ returns and completes before $Q$, and $B$'s
$\addinv$ call is invoked after $Q$ and before $\mathit{op}_B$
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)$:
\emph{(C1) $(R,A) \in v_B$.}
The write $w(R,A)$ occurs during $A$'s $\addres$ call, which
completes before $Q$.
Hence $w(R,A) \prec 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) \in v_B$.
\emph{(C2) $(I,B) \notin v_A$.}
The write $w(I,B)$ occurs during $B$'s $\addinv$ call, which
begins after $Q$.
Hence $w(I,B) \succ Q$.
$A$'s collect runs entirely before $Q$, so it cannot have
observed any event written after $Q$.
Thus $(I,B) \notin v_A$.
\emph{(C3) $v_A \subseteq v_B$.}
Every event in $v_A$ 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 $v_A$ is also in $v_B$,
so $v_A \subseteq v_B$.
All three conjuncts hold, so $\precedes(A,B) = \mathtt{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 \texttt{true} and \texttt{false} are compatible
with a legal sequential history for that group.
\end{proof}
\end{document}
\begin{thebibliography}{10}
\bibitem{Cure}
Deepthi~Devaki Akkoorath, Alejandro Tomsic, Manuel Bravo, Zhongmiao Li, Tyler
Crain, Annette Bieniusa, Nuno Preguiça, and Marc Shapiro.
\newblock {Cure}: Strong semantics meets high availability and low latency.
\newblock In {\em 36th {IEEE} International Conference on Distributed Computing
Systems ({ICDCS})}, pages 485--494. IEEE, 2016.
\newblock \href {https://doi.org/10.1109/ICDCS.2016.42}
{\path{doi:10.1109/ICDCS.2016.42}}.
\bibitem{CR23}
Armando Casta\~{n}eda and Gilde~Valeria Rodr\'{\i}guez.
\newblock Asynchronous wait-free runtime verification and enforcement of
linearizability.
\newblock In {\em 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.
\newblock \href {https://doi.org/10.1145/3583668.3594563}
{\path{doi:10.1145/3583668.3594563}}.
\bibitem{CR26_JACM}
Armando Casta\~{n}eda and Gilde~Valeria Rodr\'{\i}guez.
\newblock Asynchronous wait-free runtime verification and enforcement of
linearizability.
\newblock {\em J. ACM}, 73(1), February 2026.
\newblock \href {https://doi.org/10.1145/3777409} {\path{doi:10.1145/3777409}}.
\bibitem{GentleRain}
Jiaqing Du, C\u{a}lin Iorgulescu, Amitabha Roy, and Willy Zwaenepoel.
\newblock {GentleRain}: Cheap and scalable causal consistency with physical
clocks.
\newblock In {\em Proceedings of the ACM Symposium on Cloud Computing (SoCC)},
pages 1--13. ACM, 2014.
\newblock \href {https://doi.org/10.1145/2670979.2670983}
{\path{doi:10.1145/2670979.2670983}}.
\bibitem{EF18}
Antoine El-Hokayem and Yli{\`e}s Falcone.
\newblock Can we monitor all multithreaded programs?
\newblock In Christian Colombo and Martin Leucker, editors, {\em Runtime
Verification}, pages 64--89, Cham, 2018. Springer International Publishing.
\bibitem{Fidge88}
Colin~J. Fidge.
\newblock Timestamps in message-passing systems that preserve the partial
ordering.
\newblock In {\em Proceedings of the 11th Australian Computer Science
Conference}, pages 56--66, 1988.
\bibitem{XTrace07}
Rodrigo Fonseca, George Porter, Randy~H. Katz, Scott Shenker, and Ion Stoica.
\newblock {X-Trace}: A pervasive network tracing framework.
\newblock In {\em 4th {USENIX} Symposium on Networked Systems Design and
Implementation ({NSDI})}, pages 271--284. USENIX, 2007.
\bibitem{georges2007java}
Andy Georges, Dries Buytaert, and Lieven Eeckhout.
\newblock Statistically rigorous java performance evaluation.
\newblock {\em SIGPLAN Not.}, 42(10):57–76, October 2007.
\newblock \href {https://doi.org/10.1145/1297105.1297033}
{\path{doi:10.1145/1297105.1297033}}.
\bibitem{H91}
Maurice Herlihy.
\newblock Wait-free synchronization.
\newblock {\em ACM Trans. Program. Lang. Syst.}, 13(1):124–149, January 1991.
\newblock \href {https://doi.org/10.1145/114005.102808}
{\path{doi:10.1145/114005.102808}}.
\bibitem{HS08}
Maurice Herlihy and Nir Shavit.
\newblock {\em The Art of Multiprocessor Programming}.
\newblock Morgan Kaufmann, 2008.
\newblock Revised edition, 2012.
\bibitem{HW90}
Maurice Herlihy and Jeannette~M. Wing.
\newblock Linearizability: {A} correctness condition for concurrent objects.
\newblock {\em ACM Transactions on Programming Languages and Systems},
12(3):463--492, 1990.
\newblock \href {https://doi.org/10.1145/78969.78972}
{\path{doi:10.1145/78969.78972}}.
\bibitem{Lamport97}
L.~Lamport.
\newblock How to make a correct multiprocess program execute correctly on a
multiprocessor.
\newblock {\em IEEE Transactions on Computers}, 46(7):779--782, 1997.
\newblock \href {https://doi.org/10.1109/12.599898}
{\path{doi:10.1109/12.599898}}.
\bibitem{Lamport78}
Leslie Lamport.
\newblock Time, clocks, and the ordering of events in a distributed system.
\newblock {\em Communications of the ACM}, 21(7):558--565, 1978.
\newblock \href {https://doi.org/10.1145/359545.359563}
{\path{doi:10.1145/359545.359563}}.
\bibitem{lea-longadder}
Doug Lea.
\newblock {LongAdder} and {Striped64}, \texttt{java.util.concurrent.atomic}.
\newblock JDK 8 (JSR-166e), 2014.
\newblock Accessed: 2026.
\newblock URL: \url{https://gee.cs.oswego.edu/dl/concurrent/}.
\bibitem{Lowe17}
Gavin Lowe.
\newblock Testing for linearizability.
\newblock {\em Concurrency and Computation: Practice and Experience},
29(4):e3928, 2017.
\newblock e3928 cpe.3928.
\newblock URL: \url{https://onlinelibrary.wiley.com/doi/abs/10.1002/cpe.3928},
\href
{https://arxiv.org/abs/https://onlinelibrary.wiley.com/doi/pdf/10.1002/cpe.3928}
{\path{arXiv:https://onlinelibrary.wiley.com/doi/pdf/10.1002/cpe.3928}},
\href {https://doi.org/10.1002/cpe.3928} {\path{doi:10.1002/cpe.3928}}.
\bibitem{Mattern88}
Friedemann Mattern.
\newblock Virtual time and global states of distributed systems.
\newblock In {\em Parallel and Distributed Algorithms}, pages 215--226.
North-Holland, 1988.
\bibitem{RS96}
Michel Raynal and Mukesh Singhal.
\newblock Logical time: Capturing causality in distributed systems.
\newblock {\em Computer}, 29(2):49–56, February 1996.
\newblock \href {https://doi.org/10.1109/2.485846}
{\path{doi:10.1109/2.485846}}.
\bibitem{RC24}
Gilde~Valeria Rodr{\'i}guez and Armando Casta{\~{n}}eda.
\newblock Towards efficient runtime verified linearizable algorithms.
\newblock In Erika {\'A}brah{\'a}m and Houssam Abbas, editors, {\em Runtime
Verification}, pages 262--281, Cham, 2024. Springer Nature Switzerland.
\bibitem{RPC26}
Gilde~Valeria Rodríguez, Miguel Piña, and Armando Castañeda.
\newblock A reliable non-intrusive runtime verification framework for
linearizability.
\newblock {\em Science of Computer Programming}, 254:103509, 2026.
\newblock URL:
\url{https://www.sciencedirect.com/science/article/pii/S0167642326000754},
\href {https://doi.org/10.1016/j.scico.2026.103509}
{\path{doi:10.1016/j.scico.2026.103509}}.
\bibitem{Dapper10}
Benjamin~H. Sigelman, Luiz~André Barroso, Mike Burrows, Pat Stephenson, Manoj
Plakal, Donald Beaver, Saul Jaspan, and Chandan Shanbhag.
\newblock {Dapper}, a large-scale distributed systems tracing infrastructure.
\newblock Technical Report dapper-2010-1, Google, 2010.
\newblock URL: \url{https://research.google/pubs/pub36356/}.
\bibitem{Wuu84}
Gene~T.J. Wuu and Arthur~J. Bernstein.
\newblock Efficient solutions to the replicated log and dictionary problems.
\newblock In {\em 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.
\newblock \href {https://doi.org/10.1145/800222.806750}
{\path{doi:10.1145/800222.806750}}.
\end{thebibliography}