Atomicity Abstractions in Relaxed Memory Architectures

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

• Brijesh Dongol, Brunel University London
• Friday 26 January 2018, 14:00-15:00
• FW26.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.