Safe Concurrency for Aggregate Objects with Invariants: Soundness Proof
Bart Jacobs, K. Rustan M. Leino, Frank Piessens, Wolfram Schulte · 2005
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.