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 available from this repository)

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 Mar 2013 16:43
Resource URI: http://kar.kent.ac.uk/id/eprint/31901 (The current URI for this page, for reference purposes)
  • Depositors only (login required):