Verifying class invariants in concurrent programs

M. Zaharieva, Marieke Huisman

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    49 Downloads (Pure)

    Abstract

    Class invariants are a highly useful feature for the verification of object-oriented programs, because they can be used to capture all valid object states. In a sequential program setting, the validity of class invariants is typically described in terms of a visible state semantics, i.e., invariants only have to hold whenever a method begins or ends execution, and they may be broken inside a method body. However, in a concurrent setting, this restriction is no longer usable, because due to thread interleavings, any program state is potentially a visible state. In this paper we present a new approach for reasoning about class invariants in multithreaded programs. We allow a thread to explicitly break an invariant at specific program locations, while ensuring that no other thread can observe the broken invariant. We develop our technique in a permission-based separation logic environment. However, we deviate from separation logic's standard rules and allow a class invariant to express properties over shared memory locations (the invariant footprint), independently of the permissions on these locations. In this way, a thread may break or reestablish an invariant without holding permissions to all locations in its footprint. To enable modular verification, we adopt the restrictions of Muller's ownership-based type system.
    Original languageUndefined
    Title of host publicationProceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE 2014)
    EditorsStefania Gnesi, Arend Rensink
    Place of PublicationBerlin
    PublisherSpringer
    Pages230-245
    Number of pages16
    ISBN (Print)978-3-642-54803-1
    DOIs
    Publication statusPublished - Apr 2014
    Event17th International Conference on Fundamental Approaches to Software Engineering, FASE 2014 - Grenoble, France
    Duration: 5 Apr 201413 Apr 2014
    Conference number: 17

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume8411
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference17th International Conference on Fundamental Approaches to Software Engineering, FASE 2014
    Abbreviated titleFASE
    CountryFrance
    CityGrenoble
    Period5/04/1413/04/14

    Keywords

    • EWI-24902
    • CR-D.2.4
    • Program Verification
    • METIS-305941
    • IR-91765
    • Class Invariants
    • Concurrency
    • Separation Logic

    Cite this

    Zaharieva, M., & Huisman, M. (2014). Verifying class invariants in concurrent programs. In S. Gnesi, & A. Rensink (Eds.), Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE 2014) (pp. 230-245). (Lecture Notes in Computer Science; Vol. 8411). Berlin: Springer. https://doi.org/10.1007/978-3-642-54804-8_16