Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Safe Concurrency for Aggregate Objects with Invariants

Bart Jacobs, Frank Piessens, K. Rustan M. Leino, and Wolfram Schulte

Abstract

Developing safe multithreaded software systems is difficult due to the potential unwanted interference among concurrent threads. This paper presents a flexible methodology for object-oriented programs that protects object structures against inconsistency due to race conditions. It is based on a recent methodology for single-threaded programs where developers define aggregate object structures using an ownership system and declare invariants over them. The methodology is supported by a set of language elements and by both a sound modular static verification method and run-time checking support. The paper reports on preliminary experience with a prototype implementation.

Details

Publication typeInproceedings
Published inSEFM
Pages137-147
ISBN0-7695-2435-4
PublisherIEEE Computer Society
> Publications > Safe Concurrency for Aggregate Objects with Invariants