BibTex format
@inproceedings{Drossopoulou:2008,
author = {Drossopoulou, S and Eisenbach, S and Cunningham, D},
pages = {24--35},
title = {Lock Inference Proven Correct},
url = {http://hdl.handle.net/10044/1/5965},
year = {2008}
}
Publications
Citation
RIS format (EndNote, RefMan)
TY - CPAPER
AB - 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.\r\n\r\nAtomic 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.\r\n\r\nWe 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.\r\n
AU - Drossopoulou,S
AU - Eisenbach,S
AU - Cunningham,D
EP - 35
PY - 2008///
SP - 24
TI - Lock Inference Proven Correct
UR - http://hdl.handle.net/10044/1/5965
ER -