Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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
Specification and verification of synchronization with condition variables
KTH.
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-0074-8786
2017 (English)In: 5th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2016, Springer Verlag , 2017, 3-19 p.Conference paper (Refereed)
Abstract [en]

In this paper we propose a technique to specify and verify the correct synchronization of concurrent programs with condition variables. We define correctness as the liveness property: “every thread synchronizing under a set of condition variables eventually exits the synchronization”, under the assumption that every such thread eventually reaches its synchronization block. Our technique does not avoid the combinatorial explosion of interleavings of thread behaviors. Instead, we alleviate it by abstracting away all details that are irrelevant to the synchronization behavior of the program, which is typically significantly smaller than its overall behavior. First, we introduce SyncTask, a simple imperative language to specify parallel computations that synchronize via condition variables. We consider a SyncTask program to have a correct synchronization iff it terminates. Further, to relieve the programmer from the burden of providing specifications in SyncTask, we introduce an economic annotation scheme for Java programs to assist the automated extraction of SyncTask programs capturing the synchronization behavior of the underlying program. We prove that every Java program annotated according to the scheme (and satisfying the assumption) has a correct synchronization iff its corresponding SyncTask program terminates. We show how to transform the verification of termination into a standard reachability problem over Colored Petri Nets that is efficiently solvable by existing Petri Net analysis tools. Both the SyncTask program extraction and the generation of Petri Nets are implemented in our STaVe tool. We evaluate the proposed framework on a number of test cases as a proof-of-concept.

Place, publisher, year, edition, pages
Springer Verlag , 2017. 3-19 p.
Keyword [en]
Computer software, Explosions, Extraction, Petri nets, Safety engineering, Security systems, Specifications, Synchronization, Automated extraction, Combinatorial explosion, Concurrent program, Imperative languages, Liveness properties, Parallel Computation, Reachability problem, Specification and verification, Java programming language
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-207406DOI: 10.1007/978-3-319-53946-1_1ScopusID: 2-s2.0-85013324816ISBN: 9783319539454 OAI: oai:DiVA.org:kth-207406DiVA: diva2:1103659
Conference
14 November 2016 through 15 November 2016
Note

Funding details: 258405, ERC, European Research Council; Funding text: Marieke Huisman — Supported by ERC grant 258405 for the VerCors project.

QC 20170530

Available from: 2017-05-30 Created: 2017-05-30 Last updated: 2017-05-30Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
De Carvalho Gomes, PedroGurov, Dilian
By organisation
KTHTheoretical Computer Science, TCS
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 5 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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