Safe Concurrency for Aggregate Objects with Invariants: Soundness Proof

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. This is the companion technical report for the paper presented at the 3rd International Conference on Software Engineering and Formal Methods, Koblenz, Germany, September 5-9, 2005. It includes a proof of soundness.

PDF file

Publisher  Institute of Electrical and Electronics Engineers, Inc.
© 2004 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.


InstitutionMicrosoft Research
> Publications > Safe Concurrency for Aggregate Objects with Invariants: Soundness Proof