SearcharxivSearch

arXiv subjects

Armando Castañeda

Publications and source records attributed to Armando Castañeda.

At least 19 recordsLinked to original sources

On the Limits of Causal Observation in Shared-Memory Systems

Determining whether one concurrent operation completed before another began is a fundamental prerequisite for reasoning about the correctness of concurrent systems. We formalize this challenge as the Causal Observability Problem (COP): assign timestamps to the observable boundary events of a concurrent execution, invocations and responses, that faithfully reflect real-time operation order. A solution is complete if it never misses a genuine precedence, and sound if it never reports a spurious one. We prove that a strongly consistent solution, one that is simultaneously complete and sound, is unachievable at the observable boundary. We then show that the placement of instrumentation events relative to operation boundaries deterministically governs what a monitor can guarantee: internal placement yields completeness, external placement yields soundness, and neither achieves both. This dichotomy holds independently of the underlying timestamp mechanism. We instantiate this framework with three non-blocking implementations of a Causal Monitor object: FAInc (centralized atomic counter), Striped (decentralized counter), and Collect (iterative register snapshot). FAInc and Striped are linearizable; Collect is only quiescently consistent. Despite this internal consistency gap, we prove that all three provide identical COP guarantees: placement alone determines observable behavior. We validate these claims empirically on a 64-core NUMA architecture, showing that Striped matches Collect in throughput while preserving linearizability, resolving the cache-contention bottleneck of FAInc at high thread counts.

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

Impossibility Results for Strong Linearizability: The Difficulty of Consistent Refereeing

This paper studies the relation between agreement and strongly linearizable implementations of various objects. This leads to new results about implementations of concurrent objects from various primitives including window registers, interfering primitives and stacks. We identify that lock-free, respectively, wait-free, strongly linearizable implementations of several concurrent objects entail a form of agreement that does not require full consensus but cannot be implemented in a strongly-linearizable manner with combinations of non-universal primitives. In both cases, lock-free and wait-free, this form of agreement requires a distinguished process to referee a competition that involves all other processes. Our results show that consistent refereeing of such competitions (i.e., once resolved, the outcome cannot be revised in any extension of the execution) requires high coordination power. More specifically, two contest objects are defined and used to help characterize coordination constraints imposed by strong linearizability in lock-free and wait-free implementations, respectively. Both objects are strictly weaker than consensus, in the sense that they have a wait-free linearizable (in fact, decisively linearizable) implementation from reads and writes. The contest objects capture strong linearizability in two complementary ways. First, they admit strongly linearizable implementations from several high-level objects such as queues, snapshots, and counters, so impossibility results for the contest objects immediately carry over to these objects. Second, they admit powerful impossibility results for strong linearizability that involve window registers, interfering primitives and stacks, which are non-universal.

cs.DC

Equivalence and Separation between Heard-Of and Asynchronous Message-Passing Models

We revisit the relationship between two fundamental models of distributed computation: the asynchronous message-passing model with up to $f$ crash failures ($\operatorname{AMP}_f$) and the Heard-Of model with up to $f$ message omissions ($\operatorname{HO}_f$). We show that for $n > 2f$, the two models are equivalent with respect to the solvability of colorless tasks, and that for colored tasks the equivalence holds only when $f = 1$ (and $n > 2$). The separation for larger $f$ arises from the presence of silenced processes in $\operatorname{HO}_f$, which may lead to incompatible decisions. The proofs proceed through bidirectional simulations between $\operatorname{AMP}_f$ and $\operatorname{HO}_f$ via an intermediate model that captures this notion of silencing. The results extend to randomized protocols against a non-adaptive adversary, indicating that the expressive limits of canonical rounds are structural rather than probabilistic. Together, these results delineate precisely where round-based abstractions capture asynchronous computation, and where they do not.

cs.DC

Read-Modify-Writable Snapshots from Read/Write operations

In the context of asynchronous concurrent shared-memory systems, a snapshot algorithm allows failure-prone processes to concurrently and atomically write on the entries of a shared array MEM , and also atomically read the whole array. Recently, Read-Modify-Writable (RMWable) snapshot was proposed, a variant of snapshot that allows processes to perform operations more complex than just read and write, specifically, each entry MEM[k] is an arbitrary readable object. The known RMWable snapshot algorithms heavily rely on powerful low-level operations such as compare&swap or load-link/store-conditional to correctly produce snapshots of MEM. Following the large body of research devoted to understand the limits of what can be solved using the simple read/write low-level operations, which are known to be strictly weaker than compare&swap and load-link/store-conditional, we explore if RMWable snapshots are possible using only read/write operations. We present two read/write RMWable snapshot algorithms, the first one in the standard concurrent shared-memory model where the number of processes n is finite and known in advance, and the second one in a variant of the standard model with unbounded concurrency, where there are infinitely many processes, but at any moment only finitely many processes participate in an execution.

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

What Cannot Be Implemented on Weak Memory?

We present a general methodology for establishing the impossibility of implementing certain concurrent objects on different (weak) memory models. The key idea behind our approach lies in characterizing memory models by their mergeability properties, identifying restrictions under which independent memory traces can be merged into a single valid memory trace. In turn, we show that the mergeability properties of the underlying memory model entail similar mergeability requirements on the specifications of objects that can be implemented on that memory model. We demonstrate the applicability of our approach to establish the impossibility of implementing standard distributed objects with different restrictions on memory traces on three memory models: strictly consistent memory, total store order, and release-acquire. These impossibility results allow us to identify tight and almost tight bounds for some objects, as well as new separation results between weak memory models, and between well-studied objects based on their implementability on weak memory models.

cs.DC

Strong Linearizability using Primitives with Consensus Number 2

A powerful tool for designing complex concurrent programs is through composition with object implementations from lower-level primitives. Strongly-linearizable implementations allow to preserve hyper-properties, e.g., probabilistic guarantees of randomized programs. However, the only known wait-free strongly-linearizable implementations for many objects rely on compare&swap, a universal primitive that allows any number of processes to solve consensus. This is despite the fact that these objects have wait-free linearizable implementations from read / write primitives, which do not support consensus. This paper investigates a middle-ground, asking whether there are wait-free strongly-linearizable implementations from realistic primitives such as test&set or fetch&add, whose consensus number is 2. We show that many objects with consensus number 1 have wait-free strongly-linearizable implementations from fetch&add. We also show that several objects with consensus number 2 have wait-free or lock-free implementations from other objects with consensus number 2. In contrast, we prove that even when fetch&add, swap and test&set primitives are used, some objects with consensus number 2 do not have lock-free strongly-linearizable implementations. This includes queues and stacks, as well as relaxed variants thereof.

cs.DC

Topological Characterization of Task Solvability in General Models of Computation

The famous asynchronous computability theorem (ACT) relates the existence of an asynchronous wait-free shared memory protocol for solving a task with the existence of a simplicial map from a subdivision of the simplicial complex representing the inputs to the simplicial complex representing the allowable outputs. The original theorem relies on a correspondence between protocols and simplicial maps in round-structured models of computation that induce a compact topology. This correspondence, however, is far from obvious for computation models that induce a non-compact topology, and indeed previous attempts to extend the ACT have failed. This paper shows that in every non-compact model, protocols solving tasks correspond to simplicial maps that need to be continuous. It first proves a generalized ACT for sub-IIS models, some of which are non-compact, and applies it to the set agreement task. Then it proves that in general models too, protocols are simplicial maps that need to be continuous, hence showing that the topological approach is universal. Finally, it shows that the approach used in ACT that equates protocols and simplicial complexes actually works for every compact model. Our study combines, for the first time, combinatorial and point-set topological aspects of the executions admitted by the computation model.

cs.DC

Communication Pattern Logic: Epistemic and Topological Views

We propose communication pattern logic. A communication pattern describes how processes or agents inform each other, independently of the information content. The full-information protocol in distributed computing is the special case wherein all agents inform each other. We study this protocol in distributed computing models where communication might fail: an agent is certain about the messages it receives, but it may be uncertain about the messages other agents have received. In a dynamic epistemic logic with distributed knowledge and with modalities for communication patterns, the latter are interpreted by updating Kripke models. We propose an axiomatization of communication pattern logic, and we show that collective bisimilarity (comparing models on their distributed knowledge) is preserved when updating models with communication patterns. We can also interpret communication patterns by updating simplicial complexes, a well-known topological framework for distributed computing. We show that the different semantics correspond, and propose collective bisimulation between simplicial complexes.

cs.DC

Comparing the Update Expressivity of Communication Patterns and Action Models

Any kind of dynamics in dynamic epistemic logic can be represented as an action model. Right? Wrong! In this contribution we prove that the update expressivity of communication patterns is incomparable to that of action models. Action models, as update mechanisms, were proposed by Baltag, Moss, and Solecki in 1998 and have remained the nearly universally accepted update mechanism in dynamic epistemic logics since then. Alternatives, such as arrow updates that were proposed by Kooi and Renne in 2011, have update equivalent action models. More recently, the picture is shifting. Communication patterns are update mechanisms originally proposed in some form or other by Agotnes and Wang in 2017 (as resolving distributed knowledge), by Baltag and Smets in 2020 (as reading events), and by Velazquez, Castaneda, and Rosenblueth in 2021 (as communication patterns). All these logics have the same expressivity as the base logic of distributed knowledge. However, their update expressivity, the relation between pointed epistemic models induced by such an update, was conjectured to be different from that of action model logic. Indeed, we show that action model logic and communication pattern logic are incomparable in update expressivity. We also show that, given a history-based semantics and when restricted to (static) interpreted systems, action model logic is (strictly) more update expressive than communication pattern logic. Our results are relevant for distributed computing wherein oblivious models involve arbitrary iteration of communication patterns.

cs.LO

Modular Baskets Queue

A modular version of the baskets queue of Hoffman, Shalev and Shavit is presented. It manipulates the head and tail using a novel object called load-link/increment-conditional, which can be implemented using only READ/WRITE instructions, and admits implementations that spread contention. This suggests that there might be an alternative to the seemingly inherent bottleneck in previous queue implementations that manipulate the head and the tail using read-modify-write instructions over a single shared register.

cs.DC

Locally Solvable Tasks and the Limitations of Valency Arguments

An elegant strategy for proving impossibility results in distributed computing was introduced in the celebrated FLP consensus impossibility proof. This strategy is local in nature as at each stage, one configuration of a hypothetical protocol for consensus is considered, together with future valencies of possible extensions. This proof strategy has been used in numerous situations related to consensus, leading one to wonder why it has not been used in impossibility results of two other well-known tasks: set agreement and renaming. This paper provides an explanation of why impossibility proofs of these tasks have been of a global nature. It shows that a protocol can always solve such tasks locally, in the following sense. Given a configuration and all its future valencies, if a single successor configuration is selected, then the protocol can reveal all decisions in this branch of executions, satisfying the task specification. This result is shown for both set agreement and renaming, implying that there are no local impossibility proofs for these tasks.

cs.DC

Communication Pattern Models: An Extension of Action Models for Dynamic-Network Distributed Systems

Halpern and Moses were the first to recognize, in 1984, the importance of a formal treatment of knowledge in distributed computing. Many works in distributed computing, however, still employ informal notions of knowledge. Hence, it is critical to further study such formalizations. Action models, a significant approach to modeling dynamic epistemic logic, have only recently been applied to distributed computing, for instance, by Goubault, Ledent, and Rajsbaum. Using action models for analyzing distributed-computing environments, as proposed by these authors, has drawbacks, however. In particular, a direct use of action models may cause such models to grow exponentially as the computation of the distributed system evolves. Hence, our motivation is finding compact action models for distributed systems. We introduce communication pattern models as an extension of both ordinary action models and their update operator. We give a systematic construction of communication pattern models for a large variety of distributed-computing models called dynamic-network models. For a proper subclass of dynamic-network models called oblivious, the communication pattern model remains the same throughout the computation.

cs.LO

Fully Read/Write Fence-Free Work-Stealing with Multiplicity

Work-stealing is a popular technique to implement dynamic load balancing in a distributed manner. In this approach, each process owns a set of tasks that have to be executed. The owner of the set can put tasks in it and can take tasks from it to execute them. When a process runs out of tasks, instead of being idle, it becomes a thief to steal tasks from a victim. Thus, a work-stealing algorithm provides three high-level operations: Put and Take, which can be invoked only by the owner, and Steal, which can be invoked by a thief. One of the main targets when designing work-stealing algorithms is to make Put and Take as simple and efficient as possible. Unfortunately, it has been shown that any work-stealing algorithm in the standard asynchronous model must use expensive Read- After-Write synchronization patterns or atomic Read-Modify-Write instructions, which may be costly in practice. Thus, prior research has proposed idempotent work-stealing, a relaxation for which there are algorithms with Put and Take devoid of Read-Modify-Write atomic instructions and Read-After-Write synchronization patterns; however, Put uses fences among Write instructions, and Steal uses Compare&Swap and fences among Read instructions. In the TSO model, in which Write (resp. Read) instructions cannot be reordered, there have been proposed fully fence-free work-stealing algorithms whose Put and Take have similar properties but Steal uses Compare&Swap or a lock.

cs.DC

Relaxed Queues and Stacks from Read/Write Operations

Considering asynchronous shared memory systems in which any number of processes may crash, this work identifies and formally defines relaxations of queues and stacks that can be non-blocking or wait-free while being implemented using only read/write operations. Set-linearizability and Interval-linearizability are used to specify the relaxations formally, and precisely identify the subset of executions which preserve the original sequential behavior. The relaxations allow for an item to be returned more than once by different operations, but only in case of concurrency; we call such a property multiplicity. The stack implementation is wait-free, while the queue implementation is non-blocking. Interval-linearizability is used to describe a queue with multiplicity, with the additional relaxation that a dequeue operation can return weak-empty, which means that the queue might be empty. We present a read/write wait-free interval-linearizable algorithm of a concurrent queue. As far as we know, this work is the first that provides formalizations of the notions of multiplicity and weak-emptiness, which can be implemented on top of read/write registers only.

cs.DC

A Topological Perspective on Distributed Network Algorithms

More than two decades ago, combinatorial topology was shown to be useful for analyzing distributed fault-tolerant algorithms in shared memory systems and in message passing systems. In this work, we show that combinatorial topology can also be useful for analyzing distributed algorithms in failure-free networks of arbitrary structure. To illustrate this, we analyze consensus, set-agreement, and approximate agreement in networks, and derive lower bounds for these problems under classical computational settings, such as the LOCAL model and dynamic networks.

cs.DC