Bart Jacobs, Katholieke Universiteit Leuven Celestijnenlaan, Belgium
Frank Piessens, Katholieke Universiteit Leuven Celestijnenlaan, Belgium
Developing safe multithreaded software systems is diffi- cult 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.
Citation:
Bart Jacobs, K. Rustan M. Leino, Frank Piessens, Wolfram Schulte, "Safe Concurrency for Aggregate Objects with Invariants," sefm, pp.137-147, Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), 2005