Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Modular Verification of Finite...

Modular Verification of Finite Blocking in Non-terminating Programs

Pontus Boström, Peter Müller, Modular Verification of Finite Blocking in Non-terminating Programs. ETH-Zürich Research Collection , ETH-Zürich, 2014.

http://dx.doi.org/10.3929/ethz-a-010341095

Abstract:

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 specifi-
cations, 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.

BibTeX entry:

@TECHREPORT{aconv23103,
  title = {Modular Verification of Finite Blocking in Non-terminating Programs},
  author = {Boström, Pontus and Müller, Peter},
  series = {ETH-Zürich Research Collection},
  publisher = {ETH-Zürich},
  year = {2014},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Edit publication