Reasoning about the Implementation of Concurrency Abstractions on x86-TSO

Owens, Scott (2010) Reasoning about the Implementation of Concurrency Abstractions on x86-TSO. In: ECOOP 2010 —- Object-Oriented Programming, 24th European Conference, June 21st-25th, 2010, Maribor, Slovenia. (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided)

The full text of this publication is not available from this repository. (Contact us about this Publication)
Official URL
http://dx.doi.org/10.1007/978-3-642-14107-2_23

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 particular interest 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 analyze five concurrency abstraction implementations: two spinlocks (from Linux); a non-blocking write protocol; the double-checked locking idiom; and java.util.concurrent’s Parker. Our principle, called triangular-race freedom, strengthens the usual data-race freedom style of reasoning.

Item Type: Conference or workshop item (Paper)
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Programming Languages and Systems Group
Depositing User: Scott Owens
Date Deposited: 24 Oct 2012 10:16
Last Modified: 15 May 2014 15:16
Resource URI: https://kar.kent.ac.uk/id/eprint/31901 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year