A Basis for Verifying Multi-threaded Programs

13 years 11 months ago

Download research.microsoft.com

Abstract. Advanced multi-threaded programs apply concurrency concepts in sophisticated ways. For instance, they use ﬁne-grained locking to increase parallelism and change locking orders dynamically when data structures are being reorganized. This paper presents a sound and modular veriﬁcation methodology that can handle advanced concurrency patterns in multi-threaded, object-based programs. The methodology is based on implicit dynamic frames and uses fractional permissions to support ﬁne-grained locking. It supports concepts such as multi-object monitor invariants, thread-local and shared objects, thread pre- and postconditions, and deadlock prevention with a dynamically changeable locking order. The paper prescribes the generation of veriﬁcation conditions in ﬁrst-order logic, well-suited for scrutiny by off-the-shelf SMT solvers. A veriﬁer for the methodology has been implemented for an experimental language, and has been used to verify several challenging examples includ...

K. Rustan M. Leino, Peter Müller

Real-time Traffic