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.
@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.}
}