University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Atomicity Abstractions in Relaxed Memory Architectures

Atomicity Abstractions in Relaxed Memory Architectures

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Victor Gomes.

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity