Change search
ReferencesLink to record
Permanent link

Direct link
Algorithmic Verification of Synchronization with Condition Variables
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-6468-1605
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-0074-8786
University of Twente.
2015 (English)Report (Other academic)
Abstract [en]

Condition variables are a common synchronization mechanism present in many programming languages. Still, due to the combinatorial complexity of the behaviours the mechanism induces, it has not been addressed sufficiently with formal techniques. In this paper we propose a fully automated technique to prove the correct synchronization of concurrent programs synchronizing via condition variables, where under correctness we mean the liveness property: "If for every set of condition variables, every thread synchronizing under the variables of the set eventually enters its synchronization block, then every thread will eventually exit the synchronization".First, we introduce SyncTask, a simple imperative language to specify parallel computations that synchronize via condition variables. Next, we model the constructs of the language as Petri Net components, and define rules to extract and compose nets from a SyncTask program. We show that a SyncTask program terminates if and only if the corresponding Petri Net always reaches a particular final marking. We thus transform the verification of termination into a reachability problem on the net, which can be solved efficiently by existing Petri Net analysis tools. Further, to relieve the programmer from the burden of having to provide specifications in SyncTask, we introduce an economic annotation scheme for Java programs to assist the automated extraction of SyncTask programs capturing the synchronization behaviour of the underlying program. We show that, for the Java programs that can be annotated according to the scheme, the above-mentioned liveness property holds if and only if the corresponding SyncTask program terminates. Both the SyncTask program extraction and the generation of Petri Nets are implemented in the STaVe tool. We evaluate the proposed verification framework on a number of test cases

Place, publisher, year, edition, pages
2015. , 26 p.
Keyword [en]
Concurrency, Formal Verification, Coloured Petri Nets, Java
National Category
Computer Systems
Research subject
Computer Science
URN: urn:nbn:se:kth:diva-176006OAI: diva2:865205

QC 20160517

Available from: 2015-10-27 Created: 2015-10-27 Last updated: 2016-05-24Bibliographically approved

Open Access in DiVA

Report(586 kB)11 downloads
File information
File name FULLTEXT04.pdfFile size 586 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
de Carvalho Gomes, PedroGurov, Dilian
By organisation
Theoretical Computer Science, TCS
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar
Total: 60 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 178 hits
ReferencesLink to record
Permanent link

Direct link