16
IRUS TotalDownloads
Altmetric
Lock Inference Proven Correct
File | Description | Size | Format | |
---|---|---|---|---|
lock-inference-proven.pdf | Accepted version | 223.24 kB | Adobe PDF | View/Open |
Title: | Lock Inference Proven Correct |
Authors: | Drossopoulou, S Eisenbach, S Cunningham, D |
Item Type: | Conference Paper |
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. |
Issue Date: | 31-Jul-2008 |
URI: | http://hdl.handle.net/10044/1/5965 |
Publisher Link: | http://www-sop.inria.fr/everest/events/FTfJP08/ |
Presented At: | FTfJP |
Start Page: | 24 |
End Page: | 35 |
Copyright Statement: | © The authors |
Conference Location: | Paphos, Cyprus |
Appears in Collections: | Distributed Software Engineering Computing |