Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-34281-3_4
Title: Variable permissions for concurrency verification
Authors: Le, D.-K.
Chin, W.-N. 
Teo, Y.-M.
Keywords: concurrency
permission
Variable
verification
Issue Date: 2012
Source: Le, D.-K.,Chin, W.-N.,Teo, Y.-M. (2012). Variable permissions for concurrency verification. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 7635 LNCS : 5-21. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-34281-3_4
Abstract: In the multicore era, verification for concurrent programs is increasingly important. Although state-of-the-art verification systems ensure safe concurrent accesses to heap data structures, they tend to ignore program variables. This is problematic since these variables might also be accessed by concurrent threads. One solution is to apply the same permission system, designed for heap memory, to variables. However, variables have different properties than heap memory and could benefit from a simpler reasoning scheme. In this paper, we propose a new permission system to ensure safe accesses to shared variables. Given a shared variable, a thread owns either a full permission or no permission at all. This ensures data-race freedom when accessing variables. Our goal is to soundly manage the transfer of variable permissions among threads. Moreover, we present an algorithm to automatically infer variable permissions from procedure specifications. Though we propose a simpler permission scheme, we show that our scheme is sufficiently expressive to capture programming models such as POSIX threads and Cilk. We also implement this new scheme inside a tool, called Vperm, to automatically verify the correctness of concurrent programs based on given pre/post-specifications. © 2012 Springer-Verlag.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/40524
ISBN: 9783642342806
ISSN: 03029743
DOI: 10.1007/978-3-642-34281-3_4
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

3
checked on Dec 13, 2017

Page view(s)

55
checked on Dec 16, 2017

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.