Publications Home » Lock Inference Proven Correct
Lock Inference Proven Correct
David Cunningham, Sophia Drossopoulou, Susan Eisenbach
- Conference or Workshop Paper
- FTfJP
- July, 2008
- Abstract
With the introduction of multi-core CPUs, multi-threaded programming is becoming significantly more popular. Unfortunately, it is difficult for programmers to ensure their code is correct because current languages are too low-level.
Atomic sections are a recent language primitive that expose a higher level interface to programmers. Thus they make concurrent programming more straightforward. Atomic sections can be compiled using transactional memory or lock inference, but ensuring correctness and good performance is a challenge. Transactional memory has problems with IO and contention, whereas lock inference algorithms are often too imprecise which translates to a loss of parallelism at runtime.
We define a lock inference algorithm that has good precision. We give the operational semantics of a model OO language, and define a notion of correctness for our algorithm. We then prove correctness using Isabelle/HOL.
PDF of full publication (223 kilobytes)- (need help viewing PDF files?)
BibTEX file for the publication - N.B.
- Conditions for downloading publications from this site.
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.