Abstract

Atomicity abstractions, which include concurrent objects and transactional memory, are well studied for sequentially consistent architectures. Here, correctness of an implementation is defined by conditions such as linearizability (concurrent objects), opacity (transactional memory) etc. These notions of correctness however, assume a single global clock (i.e., a total order over memory events), which is not available in a relaxed memory architecture. This talk presents two recent efforts to redefine linearizability, opacity and their variations in a relaxed memory setting. We build on the “herding cats” framework of Alglave et al, and hence, our methods apply to several memory models including SC, TSO , ARMv8 and PPC . For concurrent objects, we show that abstract specifications must be strengthened with additional happens-before information. For transactional memory, we provide flexible and expressive forms of transaction aborts and execution that have hitherto been in the realm of software transactional memory. We also prove abstraction theorems to demonstrate that the programmer API matches the intuitions and expectations about the objects in question.