that actually terminate. Termination
provers are also typically unable to find
or check non-linear termination arguments (x2, for example) when they are
required. Some preliminary efforts in
this direction have been made, 1, 6 but
these techniques are weak. To improve
the current power of termination provers, further developments in non-linear reasoning are required.
Concurrency. Concurrency adds an
extra layer of difficulty when attempting to prove program termination. The
problem here is that we must consider
all possible interactions between concurrently executing threads. This is especially true for modern fine-grained
concurrent algorithms, in which
threads interact in subtle ways through
dynamically allocated data structures.
Rather than attempting to explicitly
consider all possible interleavings of
the threads (which does not scale to
large programs) the usual method for
proving concurrent programs correct
is based on rely-guarantee or
assume-guarantee style of reasoning, which
considers every thread in isolation
under assumptions on its environment and thus avoids reasoning about
thread interactions directly. Much of
the power of a rely-guarantee proof
system (such as Jones22 and Misra and
Chandy28) comes from the cyclic proof
rules, where we can assume a property of the second thread while proving
property of the first thread, and then
assume the recently proved property
of the first thread when proving the assumed property of the second thread.
This strategy can be extended to liveness properties using induction over
time, for example, Gotsman et al. 20 and
McMillan. 27
As an example, consider the two
code fragments in Figure 10. Imagine
that we are executing these two fragments concurrently. To prove the termination of the left thread we must
prove that it does not get stuck waiting
for the call to lock. To prove this we
can assume the other thread will always eventually release the lock—but
to prove this of the code on the right
we must assume the analogous property of the thread on the left, and so
on. In this case we can certainly just
consider all possible interleavings of
the threads, thus turning the concurrent program into a sequential model
With fresh
advances in
methods for
proving the
termination
of sequential
programs that
operate over
mathematical
numbers, we are
now in the position
to begin proving
termination of
more complex
programs.
representing its executions, but this
approach does not scale well to larger
programs. The challenge is to develop
automatic methods of finding non-cir-cular rely-guarantee termination arguments. Recent steps20 have developed
heuristics that work for non-blocking
algorithms, but more general techniques are still required.
Advanced programming features.
The industrial adoption of high-level
programming features such as virtual
functions, inheritance, higher-order
functions, or closures make the task of
proving industrial programs more of a
challenge. With few exceptions (such
as Giesl et al. 18), this area has not been
well studied.
Untyped or dynamically typed programs also contribute difficulty when
proving termination, as current approaches are based on statically discovering data-structure invariants and
finding arithmetic measures in order
to prove termination. Data in untyped
programs is often encoded in strings,
using pattern matching to marshal
data in and out of strings. Termination
proving tools for JavaScript would be
especially welcome, given the havoc
that nonterminating JavaScript causes
daily for Web browsers.
Finding preconditions that guarantee
termination. In the case that a program
does not guarantee termination from
all initial configurations, we may want
to automatically discover the conditions under which the program does
guarantee termination. That is, when
calling some function provided by a
library: what are the conditions under
which the code is guaranteed to return
with a result? The challenge in this
area is to find the right precondition:
the empty precondition is correct but
useless, whereas the weakest precondition for even very simple programs
can often be expressed only in complex domains not supported by today’s
tools. Furthermore, they should be
computed quickly (the weakest precondition expressible in the target logic may be too expensive to compute).
Recent work has shown some preliminary progress in this direction. 13, 33
Liveness. We have alluded to the
connection between liveness properties and the program termination
problem. Formally, liveness properties expressed in temporal logics can