Reasoning about the Implementation of Concurrency Abstractions on x86-TSO

ncy Abstractions on x86-TSO Scott Owens University of Cambridge Abstract. With the rise of multi-core processors, shared-memory concurrency has become a widespread feature of computation, from hardware, to operating systems, to programming languages such as C++ and Java. However, none of these provide sequentially consistent shared memory; instead they have relaxed memory models, which make concurrent programs even more challenging to understand. Programming language implementations run on hardware memory models, so VM and run-time system implementors must reason at both levels. Of particurest are the low-level implementations of the abstractions that support language-level concurrency—especially because they invariably contain data races. In this paper, we develop a novel principle for reasoning about assembly programs on our previous x86-TSO memory model, and we use it to an

• Type: Conference
• Year: 2010
• Where: ECOOP
• Authors: Scott Owens
• Keywords: ECOOP 2010, Programming Languages