1 Search Results for "Boström, Pontus"

Document
DOI: 10.4230/LIPIcs.ECOOP.2015.639
Modular Verification of Finite Blocking in Non-terminating Programs

Authors: Pontus Boström and Peter Müller

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)

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 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.
Cite as

Pontus Boström and Peter Müller. Modular Verification of Finite Blocking in Non-terminating Programs. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 639-663, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{bostrom_et_al:LIPIcs.ECOOP.2015.639,
  author =	{Bostr\"{o}m, Pontus and M\"{u}ller, Peter},
  title =	{{Modular Verification of Finite Blocking in Non-terminating Programs}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{639--663},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.639},
  URN =		{urn:nbn:de:0030-drops-52416},
  doi =		{10.4230/LIPIcs.ECOOP.2015.639},
  annote =	{Keywords: Program verification, concurrency, liveness, progress, obligations}
}
  • Refine by Author
  • 1 Boström, Pontus
  • 1 Müller, Peter

  • Refine by Classification

  • Refine by Keyword
  • 1 Program verification
  • 1 concurrency
  • 1 liveness
  • 1 obligations
  • 1 progress

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2015

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact