Emerging non-volatile memory (NVM) technologies promise the durability of disks with the performance of RAM. To describe the persistency guarantees of NVM, several memory persistency models have been proposed in the literature. However, the persistency semantics of the ubiquitous x86 architecture remains unexplored to date. To close this gap, we develop the Px86 (‘persistent x86’) model, formalising the persistency semantics of Intel-x86 for the first time. We formulate Px86 both operationally and declaratively, and prove that the two characterisations are equivalent. To demonstrate the application of Px86, we develop two persistent libraries over Px86: a persistent transactional library, and a persistent variant of the Michael–Scott queue. Finally, we encode our declarative Px86 model in Alloy and use it to generate persistency litmus tests automatically.

The difficulty of designing fault-tolerant distributed algorithms incr eases with the severity of failures that an algorithm must tolerate, especially for systems with synchronous message passing. This paper considers methods that automatically translate algorithms tolerant of simple crash failures into ones tolerant of more severe failures. These translations simplify the design task by allowing algorithm designers to assume that processors fail only by stopping. Such translations can be quantified by two measures: fault-tolerance , which is a measure of how many processors must remain correct for the translation to be correct, and round-complexity , which is a measure of how the translation increases the running time of an algorithm. Understanding these translations and their limitations with respect to these measures can provide insight into the relative impact of different models of faculty behavior on the ability to provide fault-tolerant applications for systems with synchronous message passing. This paper considers translations fr om crash failures to each of the following types of more severe failures: omission to send messages; omission to send and receive messages; and totally arbitrary behavior. It shows that previously developed translaions to send-omission failures are optimal with respect to both fault-tolerance and round-complexity. It exhibits a hierarchy of translations to general (send/receive) omission failures that improves upon the fault-tolerance of previously developed translations. These translations are optimal in that they cannot be improved with respect to one measure without negatively affecting the other; that is, the hierarchy of translations is matched by corresponding hierarchy of impossibility results. The paper also gives a hierarchy of translations to arbitrary failures that improves upon the round-complexity of previously developed translations. These translations are near-optimal;

In a seminal paper, Chandra and Toueg showed how unreliable failure detectors could allows processors to achieve consensus in asynchronous message passing systems. Since then, other researchers have developed consensus algorithms for other systems or based on different failure detectors. Each algorithm was developed and proven independently. This paper shows how a consensus algorithm for any of the standard models can be automatically converted to run in any other. These results show more clearly how the different system models and failure detectors can be related. In addition, they may permit the development of new results for new models also through transformations. 1 Introduction The problem of achieving consensus among processors in a distributed system is fundamental in distributed computing. Unfortunately, consensus cannot be achieved in the presence of failures in completely asynchronous systems, either those with message passing [8,9] or those with shared memory [7,8,12]. Thi...

Psrmiseion to mckc digitehsrd ccpiss of d or partof tits outctil lbr pcNooelor Clecsroom usei-~withoutfeo pmvidsd thet the c~ies Srenotmedc ordictributed for I&w Conunewiel Sdventege, Ibe c~yright ootics, ths title of the pub qtton end its dets eppear, d notice IS givco thet ocpyright is by permission of the ACM, fnc.To COPYctbenviee, to mpublieh, to pod on scrvcm or to rediitc to lists, requires cpecific pmmission Sndlor fe.PODC!'%, Philadelphia PA, USA o 199(j ACM &897914~7J9(jJ05, .$3-Mthat, at all times, at least one process be aware of a group's membership.However, the new specification cannot be trivially satisfied because it prohibits a potential solution from arbitrarily removing a process for no reason.This specification thus represents an important step towards a better understanding of membership services in completely asynchronous systems.

No abstract available.

The traditional consistency requirements of shared memory are expensive to provide both in large scale multiprocessor systems and in distributed systems that implement a shared memory abstraction. As a result, several memory systems have been proposed that enhance performance and scalabil ity by providing weaker consistency. The differing models used to describe such memories make it difficult to relate and compare them. We develop a simple non-operational model and identify parameters that can be varied to de scribe existing memories and to identify new ones. We show how a uniform framework makes it easy to compare and relate various memories.

Shared memories that provide weaker consistency guarantees than the traditional sequentially consistent or atomic memories have been claimed to provide the key to building scalable systems.One influential memory model, processor considency, has been cited widely in the literature but, due to the lack of a precise and formal definition, contradictory claims have been made regarding its power.We use a formal model to give two distinct definitions of processors consistency: one corresponding to Goodman's original proposal and the other corresponding that given by the implementors of the DASH system.These definitions are non-operational and can be easily related to other types of memories.To illustrate the power of processor consistency, we exhibit a non-cooperative solution to the mutual exclusion problem that is correct with processor consistency.As a contrast, we show that Lamport's Bakery algorithm is not correct with processor consistency. 1

Time and knowledge are studied in synchronous and asynchronous distributed systems. A large class of problems that can be solved using logical clocks as if they were perfectly synchronized clocks is formally characterized. For the same class of problems, a broadcast primitive that can be used as if it achieves common knowledge is also proposed. Thus, logical clocks and the broadcast primitive simplify the task of designing and verifying distributed algorithms: The designer can assume that processors have access to perfectly synchronized clocks and the ability to achieve common knowledge.

The problem of fault-tolerant coordination is fundamental in distributed computing. In the past, researchers have considered two types of coordination: general coordination, in which the actions of faulty processors are irrelevant, and consistent coordination, in which the faulty processors are forbidden from acting inconsistently. This paper studies the possibility and complexity of achieving coordination in synchronous and asynchronous systems with crash, send-omission, and general omission failures. We indicate the systems in which coordination cannot be achieved and, when it can, analyze the computational complexity of optimally achieving it. In some cases, optimum solutions can be implemented in polynomial time, while in others they require NP-hard local computation. These results provide a thorough characterization of coordination and will thus aid researchers in determining the approach to take when attempting to achieve fault-tolerant coordination.

The design of fault-tolerant distributed systems is a costly and diflicult task.Its cost and difficulty increase dramatically with the severity of failures that a system must tolerate.We seek to simplify this task by developing methods to automatically translate protocols tolerant of "benign" failures to ones tolerant of more "severe" failures.This paper describes two new translation mechanisms for qr~hronous systems; one translates programs tolerant of crash failures into programs tolerant of general omission failures, and the other translates from gene& omiesion failures to arbitrary failures.Together these can be used to translate any program tolerant of the most benign failures to a program tolerant of the most severe.

We study time and knowledge in reliable distributed systems with asynchronous communication.We first describe an extension of Lamport's logical clocks that can be used as if they were perfectly synchronized real-time clocks in the solution of a large class of problems that we formally characterize.For this same class of problems, we also propose a broadcast primitive that can be used as if it achieves common knowledge.Our logical clocks and broadcast primitive are tools that considerably simplify the design of distributed algorithms: one can now design and prove them correct with the assumption that processors have access to real-time clocks and the ability to achieve common knowledge.The latter can be used to implement the abstraction of shared memory.Extensions to more synchronous systems are considered.