Specification and verification of synchronization with condition variables

Pedro de Carvalho Gomes (Corresponding Author), Dilian Gurov, Marieke Huisman, Cyrille Artho

    Research output: Contribution to journalArticleAcademicpeer-review

    4 Citations (Scopus)
    54 Downloads (Pure)

    Abstract

    This paper proposes a technique to specify and verify the correct synchronization of concurrent programs with condition variables. We define correctness of synchronization as the liveness property: “every thread synchronizing under a set of condition variables eventually exits the synchronization block”, under the assumption that every such thread eventually reaches its synchronization block. Our technique does not avoid the combinatorial explosion of interleavings of thread behaviours. Instead, we alleviate it by abstracting away all details that are irrelevant to the synchronization behaviour of the program, which is typically significantly smaller than its overall behaviour. 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 behaviour of the underlying program. We show that every Java program annotated according to the scheme (and satisfying the assumption mentioned above) has a correct synchronization iff its corresponding SyncTask program terminates. We then show how to transform the verification of termination of the SyncTask program into a standard reachability problem over Coloured 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.
    Original languageEnglish
    Pages (from-to)174-189
    Number of pages16
    JournalScience of computer programming
    Volume163
    Early online date8 May 2018
    DOIs
    Publication statusPublished - 1 Oct 2018

    Fingerprint

    Synchronization
    Specifications
    Petri nets
    Explosions
    Economics

    Keywords

    • Concurrency
    • Formal verification
    • Java
    • Condition variables

    Cite this

    Gomes, Pedro de Carvalho ; Gurov, Dilian ; Huisman, Marieke ; Artho, Cyrille. / Specification and verification of synchronization with condition variables. In: Science of computer programming. 2018 ; Vol. 163. pp. 174-189.
    @article{457d0609eaf24d949715280bf95fad61,
    title = "Specification and verification of synchronization with condition variables",
    abstract = "This paper proposes a technique to specify and verify the correct synchronization of concurrent programs with condition variables. We define correctness of synchronization as the liveness property: “every thread synchronizing under a set of condition variables eventually exits the synchronization block”, under the assumption that every such thread eventually reaches its synchronization block. Our technique does not avoid the combinatorial explosion of interleavings of thread behaviours. Instead, we alleviate it by abstracting away all details that are irrelevant to the synchronization behaviour of the program, which is typically significantly smaller than its overall behaviour. 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 behaviour of the underlying program. We show that every Java program annotated according to the scheme (and satisfying the assumption mentioned above) has a correct synchronization iff its corresponding SyncTask program terminates. We then show how to transform the verification of termination of the SyncTask program into a standard reachability problem over Coloured 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.",
    keywords = "Concurrency, Formal verification, Java, Condition variables",
    author = "Gomes, {Pedro de Carvalho} and Dilian Gurov and Marieke Huisman and Cyrille Artho",
    year = "2018",
    month = "10",
    day = "1",
    doi = "10.1016/j.scico.2018.05.001",
    language = "English",
    volume = "163",
    pages = "174--189",
    journal = "Science of computer programming",
    issn = "0167-6423",
    publisher = "Elsevier",

    }

    Specification and verification of synchronization with condition variables. / Gomes, Pedro de Carvalho (Corresponding Author); Gurov, Dilian; Huisman, Marieke; Artho, Cyrille.

    In: Science of computer programming, Vol. 163, 01.10.2018, p. 174-189.

    Research output: Contribution to journalArticleAcademicpeer-review

    TY - JOUR

    T1 - Specification and verification of synchronization with condition variables

    AU - Gomes, Pedro de Carvalho

    AU - Gurov, Dilian

    AU - Huisman, Marieke

    AU - Artho, Cyrille

    PY - 2018/10/1

    Y1 - 2018/10/1

    N2 - This paper proposes a technique to specify and verify the correct synchronization of concurrent programs with condition variables. We define correctness of synchronization as the liveness property: “every thread synchronizing under a set of condition variables eventually exits the synchronization block”, under the assumption that every such thread eventually reaches its synchronization block. Our technique does not avoid the combinatorial explosion of interleavings of thread behaviours. Instead, we alleviate it by abstracting away all details that are irrelevant to the synchronization behaviour of the program, which is typically significantly smaller than its overall behaviour. 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 behaviour of the underlying program. We show that every Java program annotated according to the scheme (and satisfying the assumption mentioned above) has a correct synchronization iff its corresponding SyncTask program terminates. We then show how to transform the verification of termination of the SyncTask program into a standard reachability problem over Coloured 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.

    AB - This paper proposes a technique to specify and verify the correct synchronization of concurrent programs with condition variables. We define correctness of synchronization as the liveness property: “every thread synchronizing under a set of condition variables eventually exits the synchronization block”, under the assumption that every such thread eventually reaches its synchronization block. Our technique does not avoid the combinatorial explosion of interleavings of thread behaviours. Instead, we alleviate it by abstracting away all details that are irrelevant to the synchronization behaviour of the program, which is typically significantly smaller than its overall behaviour. 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 behaviour of the underlying program. We show that every Java program annotated according to the scheme (and satisfying the assumption mentioned above) has a correct synchronization iff its corresponding SyncTask program terminates. We then show how to transform the verification of termination of the SyncTask program into a standard reachability problem over Coloured 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.

    KW - Concurrency

    KW - Formal verification

    KW - Java

    KW - Condition variables

    U2 - 10.1016/j.scico.2018.05.001

    DO - 10.1016/j.scico.2018.05.001

    M3 - Article

    VL - 163

    SP - 174

    EP - 189

    JO - Science of computer programming

    JF - Science of computer programming

    SN - 0167-6423

    ER -