Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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
Identifiers
URN: urn:nbn:se:kth:diva-176006OAI: oai:DiVA.org:kth-176006DiVA: diva2:865205
Note

QC 20160517

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

Open Access in DiVA

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

Authority records BETA

de Carvalho Gomes, PedroGurov, Dilian

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: 109 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

urn-nbn

Altmetric score

urn-nbn
Total: 230 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf