Search arXiv⌕ Search

arXiv subjects

Gilde Valeria Rodríguez

Publications and source records attributed to Gilde Valeria Rodríguez.

4 recordsLinked to original sources

On the Limits of Causal Observation in Shared-Memory Systems

Reasoning about concurrent system correctness requires detecting real-time operation precedence (<_H). In asynchronous shared-memory systems, real-time precedence and information-flow causality diverge, rendering causality-tracking techniques like vector clocks incapable of recovering <_H. An external monitor observing only operation boundaries faces an inherent limitation: it must either miss genuine precedences or report spurious ones. We formalize this challenge as the Causal Observability Problem (COP) and prove that strong consistency---achieving both soundness and completeness simultaneously---is unachievable at the observable boundary. We then establish a tight placement dichotomy: instrumenting externally guarantees soundness, whereas instrumenting internally guarantees completeness, independently of the timestamping algorithm. To construct sound monitors, we analyze three non-blocking implementations: FAInc (a centralized counter), Striped (a decentralized counter), and Collect (an iterative process snapshot). We prove that both FAInc and Striped are linearizable, whereas Collect fails all standard object consistency models---satisfying neither linearizability, sequential consistency, nor quiescent consistency. Crucially, we prove an invariance result: all three implementations provide identical COP soundness guarantees under external placement. This demonstrates a fundamental theoretical decoupling---observational soundness operates on pairwise interval precedence and does not require the global sequential witness that standard object consistency demands. Empirical evaluation on a 64-core NUMA system shows that Striped matches the high throughput and scalability of Collect while preserving linearizability and eliminating central counter contention.

cs.DC↗

Lattice Aggregation in Distributed Verification under Crash and Byzantine Failures

We introduce c-Lattice Aggregation, a fault-tolerant reconstruction problem for distributed verification under crash and Byzantine failures. In our setting, n asynchronous processes supervise a concurrent execution I: each process holds a local sample, and must collaboratively reconstruct I from partial, potentially overlapping observations. A protocol solves c-Lattice Aggregation if at least c correct processes output the complete execution I, while all correct outputs are comparable and bounded by I. This strengthens Lattice Agreement [Attiya, Herlihy and Rachman, 1995] and Byzantine Lattice Agreement [Di Luna et al., 2020; Zheng and Garg, 2020]. We parameterize inputs by a redundancy parameter x -- every element of I appears in at least x initial samples -- and establish tight feasibility thresholds. Under crash failures with at most t faulty processes, Lattice Aggregation is solvable if and only if x >= t + 1. Under Byzantine failures with t < n/3, c-Lattice Aggregation is solvable if and only if x >= 2t + c. All bounds are tight: we present matching algorithms based on SCD-broadcast [Imbs et al., 2018; Khanchandani and Wattenhofer, 2024] and indistinguishability-based lower bounds. Finally, we define globally dependent languages -- those for which no partial view can certify correctness, including consensus, linearizability, k-set agreement, and leader election -- and prove that soundness of any monitoring system is achievable if and only if c-Lattice Aggregation is solved, yielding the first complete characterization of fault-tolerant verification under Byzantine failures.

cs.DC↗

Asynchronous Wait-Free Runtime Verification and Enforcement of Linearizability

This paper presents a {theoretical study} of the problem of verifying linearizability at runtime, where one seeks for a concurrent algorithm for verifying that the current execution of a given concurrent shared object implementation is linearizable. It shows that it is impossible to runtime verify linearizability for some common sequential objects, regardless of the consensus power of base objects. Then, it argues that a variant of the problem, which we call predictive verification, can be solved, if linearizability is verified indirectly. Namely, it shows that (1) linearizability of a class of concurrent implementations can be predictively verified using only read/write base objects (i.e. without the need of consensus), and (2) any implementation can be transformed to its counterpart in the class using only read/write objects. As far as we know, this is the first runtime verification algorithm for any correctness condition that is fully asynchronous and fault-tolerant. As a by-product, it is obtained a simple and generic methodology for deriving linearizable implementations that runtime verify their responses, and are able to produce a history certifying this, properties that allows the design of concurrent systems in a modular manner with accountable and forensic guarantees. We call such implementations self-enforced linearizable. The results hold not only for linearizability but for a correctness condition that includes generalizations of it such as set-linearizability and interval-linearizability.

cs.DC↗

Asynchronous Fault-Tolerant Language Decidability for Runtime Verification of Distributed Systems

Implementing correct distributed systems is an error-prone task. Runtime Verification (RV) offers a lightweight formal method to improve reliability by monitoring system executions against correctness properties. However, applying RV in distributed settings - where no process has global knowledge - poses fundamental challenges, particularly under full asynchrony and fault tolerance. This paper addresses the Distributed Runtime Verification (DRV) problem under such conditions. In our model, each process in a distributed monitor receives a fragment of the input word describing system behavior and must decide whether this word belongs to the language representing the correctness property being verified. Hence, the goal is to decide languages in a distributed fault-tolerant manner. We propose several decidability definitions, study the relations among them, and prove possibility and impossibility results. One of our main results is a characterization of the correctness properties that can be decided asynchronously. Remarkably, it applies to any language decidability definition. Intuitively, the characterization is that only properties with no real-time order constraints can be decided in asynchronous fault-tolerant settings. These results expose the expressive limits of DRV in realistic systems, as several properties of practical interest rely on reasoning about real-time order of events in executions. To overcome these limitations, we introduce a weaker model where the system under inspection is verified indirectly. Under this weaker model we define predictive decidability, a decidability definition that turn some real-time sensitive correctness properties verifiable. Our framework unifies and extends existing DRV theory and sharpens the boundary of runtime monitorability under different assumptions.

cs.DC↗