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. (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):
