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 language | Undefined |
---|---|
Title of host publication | Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE 2014) |
Editors | Stefania Gnesi, Arend Rensink |
Place of Publication | Berlin |
Publisher | Springer |
Pages | 230-245 |
Number of pages | 16 |
ISBN (Print) | 978-3-642-54803-1 |
DOIs | |
Publication status | Published - Apr 2014 |
Event | 17th International Conference on Fundamental Approaches to Software Engineering, FASE 2014 - Grenoble, France Duration: 5 Apr 2014 → 13 Apr 2014 Conference number: 17 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer Verlag |
Volume | 8411 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 17th International Conference on Fundamental Approaches to Software Engineering, FASE 2014 |
---|---|
Abbreviated title | FASE |
Country/Territory | France |
City | Grenoble |
Period | 5/04/14 → 13/04/14 |
Keywords
- EWI-24902
- CR-D.2.4
- Program Verification
- METIS-305941
- IR-91765
- Class Invariants
- Concurrency
- Separation Logic