Safe Concurrency for Aggregate Objects with Invariants

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.

• Type: Conference
• Year: 2005
• Where: SEFM
• Authors: Bart Jacobs 0002, Frank Piessens, K. Rustan M. Leino, Wolfram Schulte
• Keywords: Aggregate Object Structures, Methodology, Object Structures, SEFM 2005, Software Engineering