Verifying class invariants in concurrent programs

M. Zaharieva, Marieke Huisman

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

37 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
Zaharieva, M. ; Huisman, Marieke. / Verifying class invariants in concurrent programs. Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE 2014). editor / Stefania Gnesi ; Arend Rensink. Berlin : Springer, 2014. pp. 230-245 (Lecture Notes in Computer Science).
@inproceedings{9714392cce7b4556ae46fb20202c5de9,
title = "Verifying class invariants in concurrent programs",
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.",
keywords = "EWI-24902, CR-D.2.4, Program Verification, METIS-305941, IR-91765, Class Invariants, Concurrency, Separation Logic",
author = "M. Zaharieva and Marieke Huisman",
note = "10.1007/978-3-642-54804-8_16",
year = "2014",
month = "4",
doi = "10.1007/978-3-642-54804-8_16",
language = "Undefined",
isbn = "978-3-642-54803-1",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "230--245",
editor = "Stefania Gnesi and Arend Rensink",
booktitle = "Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE 2014)",

}

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). Lecture Notes in Computer Science, vol. 8411, Springer, Berlin, pp. 230-245, 17th International Conference on Fundamental Approaches to Software Engineering, FASE 2014, Grenoble, France, 5/04/14. https://doi.org/10.1007/978-3-642-54804-8_16

Verifying class invariants in concurrent programs. / Zaharieva, M.; Huisman, Marieke.

Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE 2014). ed. / Stefania Gnesi; Arend Rensink. Berlin : Springer, 2014. p. 230-245 (Lecture Notes in Computer Science; Vol. 8411).

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

TY - GEN

T1 - Verifying class invariants in concurrent programs

AU - Zaharieva, M.

AU - Huisman, Marieke

N1 - 10.1007/978-3-642-54804-8_16

PY - 2014/4

Y1 - 2014/4

N2 - 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.

AB - 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.

KW - EWI-24902

KW - CR-D.2.4

KW - Program Verification

KW - METIS-305941

KW - IR-91765

KW - Class Invariants

KW - Concurrency

KW - Separation Logic

U2 - 10.1007/978-3-642-54804-8_16

DO - 10.1007/978-3-642-54804-8_16

M3 - Conference contribution

SN - 978-3-642-54803-1

T3 - Lecture Notes in Computer Science

SP - 230

EP - 245

BT - Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE 2014)

A2 - Gnesi, Stefania

A2 - Rensink, Arend

PB - Springer

CY - Berlin

ER -

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