Specification and Verification of Synchronization with Condition Variables.

P. Gomes, D. Gurov, Marieke Huisman

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2 Citations

Abstract

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. In- stead, 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 vari- ables. 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 reachabil- ity 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.
LanguageUndefined
Title of host publicationProceedings of the Fifth International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2016)
EditorsC Artho, P.C. Ölveczky
Place of PublicationLondon
PublisherSpringer Verlag
Pages3-19
Number of pages16
ISBN (Print)978-3-319-53946-1
DOIs
StatePublished - Nov 2016

Publication series

NameCommunications in Computer and Information Science
PublisherSpringer Verlag
Volume694
ISSN (Print)1865-0929

Keywords

  • EWI-27668

Cite this

Gomes, P., Gurov, D., & Huisman, M. (2016). Specification and Verification of Synchronization with Condition Variables. In C. Artho, & P. C. Ölveczky (Eds.), Proceedings of the Fifth International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2016) (pp. 3-19). (Communications in Computer and Information Science; Vol. 694). London: Springer Verlag. DOI: 10.1007/978-3-319-53946-1_1
Gomes, P. ; Gurov, D. ; Huisman, Marieke. / Specification and Verification of Synchronization with Condition Variables.Proceedings of the Fifth International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2016). editor / C Artho ; P.C. Ölveczky. London : Springer Verlag, 2016. pp. 3-19 (Communications in Computer and Information Science).
@inproceedings{46fa6f0f369648a0a1c56d0ef2d2ac36,
title = "Specification and Verification of Synchronization with Condition Variables.",
abstract = "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. In- stead, 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 vari- ables. 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 reachabil- ity 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.",
keywords = "EWI-27668",
author = "P. Gomes and D. Gurov and Marieke Huisman",
year = "2016",
month = "11",
doi = "10.1007/978-3-319-53946-1_1",
language = "Undefined",
isbn = "978-3-319-53946-1",
series = "Communications in Computer and Information Science",
publisher = "Springer Verlag",
pages = "3--19",
editor = "C Artho and P.C. {\"O}lveczky",
booktitle = "Proceedings of the Fifth International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2016)",
address = "Germany",

}

Gomes, P, Gurov, D & Huisman, M 2016, Specification and Verification of Synchronization with Condition Variables. in C Artho & PC Ölveczky (eds), Proceedings of the Fifth International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2016). Communications in Computer and Information Science, vol. 694, Springer Verlag, London, pp. 3-19. DOI: 10.1007/978-3-319-53946-1_1

Specification and Verification of Synchronization with Condition Variables. / Gomes, P.; Gurov, D.; Huisman, Marieke.

Proceedings of the Fifth International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2016). ed. / C Artho; P.C. Ölveczky. London : Springer Verlag, 2016. p. 3-19 (Communications in Computer and Information Science; Vol. 694).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Specification and Verification of Synchronization with Condition Variables.

AU - Gomes,P.

AU - Gurov,D.

AU - Huisman,Marieke

PY - 2016/11

Y1 - 2016/11

N2 - 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. In- stead, 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 vari- ables. 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 reachabil- ity 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.

AB - 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. In- stead, 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 vari- ables. 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 reachabil- ity 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.

KW - EWI-27668

U2 - 10.1007/978-3-319-53946-1_1

DO - 10.1007/978-3-319-53946-1_1

M3 - Conference contribution

SN - 978-3-319-53946-1

T3 - Communications in Computer and Information Science

SP - 3

EP - 19

BT - Proceedings of the Fifth International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2016)

PB - Springer Verlag

CY - London

ER -

Gomes P, Gurov D, Huisman M. Specification and Verification of Synchronization with Condition Variables. In Artho C, Ölveczky PC, editors, Proceedings of the Fifth International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2016). London: Springer Verlag. 2016. p. 3-19. (Communications in Computer and Information Science). Available from, DOI: 10.1007/978-3-319-53946-1_1