Please use this identifier to cite or link to this item:
|Title:||Variable permissions for concurrency verification|
|Citation:||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)|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
checked on Jan 18, 2019
checked on Dec 16, 2018
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.