Verifying Class Invariants in Concurrent Programs

M. Zaharieva, Marieke Huisman

Research output: Book/ReportReportProfessional

2 Citations (Scopus)
47 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
Place of PublicationEnschede
PublisherCentre for Telematics and Information Technology (CTIT)
Number of pages20
Publication statusPublished - 17 Jan 2014

Publication series

NameCTIT Technical Report Series
PublisherCentre for Telematics and Information Technology, University of Twente
No.TR-CTIT-14-01
ISSN (Print)1381-3625

Keywords

  • METIS-304003
  • IR-89408
  • Class Invariants
  • FMT-OO: VERIFICATION OF OBJECT-BASED SYSTEMS
  • Separation Logic
  • Permissions
  • EWI-24423
  • Verification

Cite this

Zaharieva, M., & Huisman, M. (2014). Verifying Class Invariants in Concurrent Programs. (CTIT Technical Report Series; No. TR-CTIT-14-01). Enschede: Centre for Telematics and Information Technology (CTIT).
Zaharieva, M. ; Huisman, Marieke. / Verifying Class Invariants in Concurrent Programs. Enschede : Centre for Telematics and Information Technology (CTIT), 2014. 20 p. (CTIT Technical Report Series; TR-CTIT-14-01).
@book{19716e99eed94630a54b0c2e36023eb9,
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 = "METIS-304003, IR-89408, Class Invariants, FMT-OO: VERIFICATION OF OBJECT-BASED SYSTEMS, Separation Logic, Permissions, EWI-24423, Verification",
author = "M. Zaharieva and Marieke Huisman",
year = "2014",
month = "1",
day = "17",
language = "Undefined",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "TR-CTIT-14-01",
address = "Netherlands",

}

Zaharieva, M & Huisman, M 2014, Verifying Class Invariants in Concurrent Programs. CTIT Technical Report Series, no. TR-CTIT-14-01, Centre for Telematics and Information Technology (CTIT), Enschede.

Verifying Class Invariants in Concurrent Programs. / Zaharieva, M.; Huisman, Marieke.

Enschede : Centre for Telematics and Information Technology (CTIT), 2014. 20 p. (CTIT Technical Report Series; No. TR-CTIT-14-01).

Research output: Book/ReportReportProfessional

TY - BOOK

T1 - Verifying Class Invariants in Concurrent Programs

AU - Zaharieva, M.

AU - Huisman, Marieke

PY - 2014/1/17

Y1 - 2014/1/17

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 - METIS-304003

KW - IR-89408

KW - Class Invariants

KW - FMT-OO: VERIFICATION OF OBJECT-BASED SYSTEMS

KW - Separation Logic

KW - Permissions

KW - EWI-24423

KW - Verification

M3 - Report

T3 - CTIT Technical Report Series

BT - Verifying Class Invariants in Concurrent Programs

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -

Zaharieva M, Huisman M. Verifying Class Invariants in Concurrent Programs. Enschede: Centre for Telematics and Information Technology (CTIT), 2014. 20 p. (CTIT Technical Report Series; TR-CTIT-14-01).