16
IRUS Total
Downloads
  Altmetric

Lock Inference Proven Correct

File Description SizeFormat 
lock-inference-proven.pdfAccepted version223.24 kBAdobe PDFView/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