The integration of transactions into hardware relaxed memory architectures is a topic of research both in industry and academia. In this paper, we provide a general architectural framework (that includes the SC, TSO and ARM8 models) for the introduction of transactions into models of relaxed memory in hardware. Our model incorporates flexible and expressive forms of transaction abort and execution that have hitherto been in the realm of Software Transactional Memory. In contrast to Software transactional memory, we account for the characteristics of relaxed memory as a (restricted form of a) distributed system without a notion of global time. We prove abstraction theorems to demonstrate that the programmer API matches the intuitions and expectations about transactions.
Wed 10 JanDisplayed time zone: Tijuana, Baja California change
15:50 - 17:30 | |||
15:50 25mTalk | Effective Stateless Model Checking for C/C++ Concurrency Research Papers Michalis Kokologiannakis National Technical University of Athens, Greece, Ori Lahav Tel Aviv University, Israel, Konstantinos (Kostis) Sagonas , Viktor Vafeiadis MPI-SWS, Germany | ||
16:15 25mTalk | Transactions in Relaxed Memory Architectures Research Papers Brijesh Dongol Brunel University London, Radha Jagadeesan DePaul University, James Riely DePaul University Link to publication DOI Pre-print Media Attached | ||
16:40 25mTalk | Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8 Research Papers Christopher Pulte University of Cambridge, Shaked Flur University of Cambridge, Will Deacon ARM Ltd., Jon French University of Cambridge, Susmit Sarkar University of St. Andrews, Peter Sewell University of Cambridge | ||
17:05 25mTalk | Progress of Concurrent Objects with Partial Methods Research Papers Hongjin Liang University of Science and Technology of China, Xinyu Feng University of Science and Technology of China | ||