Deductive Verification of Concurrent Programs

Technical Report

Author(s):Daniel Bruns
Institution:Department of Informatics, Karlsruhe Institute of Technology
Series:Karlsruhe Reports in Informatics
Year:2015
Number:2015-3
URL:http://digbib.ubka.uni-karlsruhe.de/volltexte/1000045641

Abstract

Verification of concurrent programs still poses one of the major challenges in computer science. Several techniques to tackle this problem have been proposed. However, they often do not scale. We present an adaptation of the rely/guarantee methodology in dynamic logic. Rely/guarantee uses functional specification to symbolically describe the behavior of concurrently running threads: while each thread guarantees adherence to a specified property at any point in time, all other threads can rely on this property being established. This allows to regard threads largely in isolation—only w.r.t. an environment constrained by these specifications. While rely/guarantee based approaches often suffer from a considerable specification overhead, we complement functional thread specifications with frame conditions. We will explain our approach using a simple, but concurrent programing language. Besides the usual constructs for sequential programs, it caters for dynamic thread creation. We define semantics of concurrent programs w.r.t. an underspecified deterministic scheduling function. To formally reason about programs of this language, we introduce a novel multi-modal logic, emphConcurrent Dynamic Trace Logic (CDTL). It combines the strengthes of dynamic logic with those of linear temporal logic and allows to express temporal properties about symbolic program traces. We first develop a sound and complete sequent calculus for the logic subset that uses the sequential part of the language, based on symbolic execution. In a second step, we extend this to a calculus for the complete logic by adding symbolic execution rules for concurrent interleavings and dynamic thread creation based on the rely/guarantee methodology. Again, this calculus is proven sound and complete.

BibTeX

@TechReport{Bruns15,
  author	= {Daniel Bruns},
  title		= {Deductive Verification of Concurrent Programs},
  year		= 2015,
  month		= feb,
  institution	= {Department of Informatics, Karlsruhe Institute of
		   Technology},
  number	= {2015-3},
  series	= {Karlsruhe Reports in Informatics},
  url		= {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000045641},
  urn		= {urn:nbn:de:swb:90-456415},
  issn		= {2190-4782},
  language	= {english},
  license	= {http://creativecommons.org/licenses/by-nc-nd/3.0/},
  abstract	= {Verification of concurrent programs still poses one of the
		   major challenges in computer science. Several techniques to
		   tackle this problem have been proposed. However, they often
		   do not scale. We present an adaptation of the rely/guarantee
		   methodology in dynamic logic. Rely/guarantee uses functional
		   specification to symbolically describe the behavior of
		   concurrently running threads:
		   while each thread \emph{guarantees} adherence to a
		   specified property at any point in time, all other threads
		   can \emph{rely} on this property being established. This
		   allows to regard threads largely in isolation---only
		   w.r.t.\ an environment constrained by these specifications.
		   While rely/guarantee based approaches often suffer from a
		   considerable specification overhead, we complement
		   functional thread specifications with frame conditions.
		   
		   We will explain our approach using a simple, but concurrent
		   programing language. Besides the usual constructs for
		   sequential programs, it caters for dynamic thread creation.
		   We define semantics of concurrent programs w.r.t.\ an
		   underspecified deterministic scheduling function.
		   
		   To formally reason about programs of this language, we
		   introduce a novel multi-modal logic, \emph{Concurrent
		   Dynamic Trace Logic} (CDTL). It combines the strengthes of
		   dynamic logic with those of linear temporal logic and
		   allows to express temporal properties about symbolic
		   program traces. We first develop a sound and complete
		   sequent calculus for the logic subset that uses the
		   sequential part of the language, based on symbolic
		   execution. In a second step, we extend this to a calculus
		   for the complete logic by adding symbolic execution rules
		   for concurrent interleavings and dynamic thread creation
		   based on the rely/guarantee methodology. Again, this
		   calculus is proven sound and complete.}
}