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.