ECOOP 2015
Sun 5 - Fri 10 July 2015 Prague, Czech Republic
Fri 10 Jul 2015 15:30 - 16:00 at Bohemia - Verification Chair(s): Pavel Parizek

Most multi-threaded programs synchronize threads via blocking operations such as acquiring locks or joining other threads. An important correctness property of such programs is for each thread to make progress, that is, not to be blocked forever. For programs in which all threads terminate, progress essentially follows from deadlock freedom. However, for the common case that a program contains non-terminating threads such as servers or actors, deadlock freedom is not sufficient. For instance, a thread may be blocked forever by a non-terminating thread if it attempts to join that thread or to acquire a lock held by that thread.

In this paper, we present a verification technique for finite blocking in non-terminating programs. The key idea is to track explicitly whether a thread has an obligation to perform an operation that unblocks another thread, for instance, an obligation to release a lock or to terminate. Each obligation is associated with a measure to ensure that it is fulfilled within finitely many steps. Obligations may be used in specifications, which makes verification modular. We formalize our technique via an encoding into Boogie, which treats different kinds of obligations uniformly. It subsumes termination checking as a special case.

Fri 10 Jul

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:00 - 16:30
VerificationResearch Track at Bohemia
Chair(s): Pavel Parizek Charles University in Prague
15:00
30m
Talk
Lightweight Support for Magic Wands in an Automatic Verifier
Research Track
Malte Schwerhoff ETH Zurich, Switzerland, Alexander J. Summers ETH Zurich
15:30
30m
Talk
Modular Verification of Finite Blocking in Non-terminating Programs
Research Track
Pontus Boström Abo Akademi University, Peter Müller ETH Zurich
16:00
30m
Talk
Modular Termination Verification
Research Track
Bart Jacobs iMinds - Distrinet, KU Leuven, Dragan Bosnacki Eindhoven University of Technology, The Netherlands, Ruurd Kuiper Eindhoven University of Technology, The Netherlands