arXiv subjects

Raïssa Nataf

Publications and source records attributed to Raïssa Nataf.

3 recordsLinked to original sources

arXiv2026

Communication Requirements for Linearizable Registers

While linearizability is a fundamental correctness condition for distributed systems, ensuring the linearizability of implementations can be quite complex. An essential aspect of linearizable implementations of concurrent objects is the need to preserve the real-time order of operations. In many settings, however, processes cannot determine the precise timing and relative real-time ordering of operations. Indeed, in an asynchronous system, the only ordering information available to them is based on the fact that sending a message precedes its delivery. We show that as a result, message chains must be used extensively to ensure linearizability. This paper studies the communication requirements of linearizable implementations of atomic registers in asynchronous message passing systems. We start by proving two general theorems that relate message chains to the ability to delay and reorder actions and operations in an execution of an asynchronous system, without the changes being noticeable to the processes. These are then used to prove that linearizable register implementations must create extensive message chains among operations of \emph{all} types. In particular, our results imply that linearizable implementations in asynchronous systems are necessarily costly and nontrivial, and provide insight into their structure.

cs.DC↗

arXiv2025

Time, Fences and the Ordering of Events in TSO

The Total Store Order (TSO) is arguably the most widely used relaxed memory model in multiprocessor architectures, widely implemented, for example in Intel's x86 and x64 platforms. It allows processes to delay the visibility of writes through store buffering. While this supports hardware-level optimizations and makes a significant contribution to multiprocessor efficiency, it complicates reasoning about correctness, as executions may violate sequential consistency. Ensuring correct behavior often requires inserting synchronization primitives such as memory fences ($F$) or atomic read-modify-write ($RMW$) operations, but this approach can incur significant performance costs. In this work, we develop a semantic framework that precisely characterizes when such synchronization is necessary under TSO. We introduce a novel TSO-specific occurs-before relation, which adapts Lamport's celebrated happens-before relation from asynchronous message-passing systems to the TSO setting. Our main result is a theorem that proves that the only way to ensure that two events that take place at different sites are temporally ordered is by having the execution create an occurs-before chain between the events. By studying the role of fences and $RMW$s in creating occurs-before chains, we are then able to capture cases in which these costly synchronization operations are unavoidable. Since proper real-time ordering of events is a fundamental aspect of consistency conditions such as Linearizability, our analysis provides a sound theoretical understanding of essential aspects of the TSO model. In particular, we are able to generalize prior lower bounds for linearizable implementations of shared memory objects. Our results capture the structure of information flow and causality in the TSO model by extending the standard communication-based reasoning from asynchronous systems to the TSO memory model.

cs.DC↗

arXiv2023

Null Messages, Information and Coordination

This paper investigates the role that null messages play in synchronous systems with and without failures, and provides necessary and sufficient conditions on the structure of protocols for information transfer and coordination there. We start by introducing a new and more refined definition of null messages. A generalization of message chains that allow these null messages is provided, and is shown to be necessary and sufficient for information transfer in reliable systems. Coping with crash failures requires a much richer structure, since not receiving a message may be the result of the sender's failure. We introduce a class of communication patterns called {\em resilient message blocks}, which impose a stricter condition on protocols than the {\em silent choirs} of Goren and Moses (2020). Such blocks are shown to be necessary for information transfer in crash-prone systems. Moreover, they are sufficient in several cases of interest, in which silent choirs are not. Finally, a particular combination of resilient message blocks is shown to be necessary and sufficient for solving the Ordered Response coordination problem.

cs.DC↗