tial programs that operate over mathematical numbers, we are now in the position to begin proving termination of more complex programs, such as those with dynamically allocated data structures, or multithreading. Furthermore, these new advances open up new potential for proving properties beyond termination, and finding conditions that would guarantee termination. We now discuss these avenues of future research and development in some detail.

Dynamically allocated heap. Consider the C loop in Figure 8, which walks down a list and removes links with data elements equaling 5. Does this loop guarantee termination? What termination argument should we use?

The problem here is that there are
no arithmetic variables in the program
from which we can begin to construct
an argument—instead we would want
to express the termination argument
over the lengths of paths to NULL via
the next field. Furthermore, the pro-
grammer has obviously intended for
this loop to be used on acyclic sin-
gly linked lists, but how do we know
that the lists pointed to by head will
always be acyclic? The common solu-
tion to these problems is to use shape
analysis tools (which are designed to
automatically discover the shapes of
data-structures) and then to create
new auxiliary variables in the program
that track the sizes of those data struc-
tures, thus allowing for arithmetic
ranking functions to be more easily
expressed (examples include refs4, 5, 25).
The difficultly with this approach is
that we are now dependent on the ac-
curacy and scalability of current shape
analysis tools—to date the best known
shape analysis tool40 supports only
lists and trees (cyclic and acyclic, sin-
gly and doubly linked) and scales only
to relatively simple programs of size
less than 30,000 LOC. Furthermore,
the auxiliary variables introduced by
methods such as Magill et al. 25 some-
times do not track enough informa-
tion in order to prove termination (for
example, imagine a case with lists of
lists in which the sizes of the nested
lists are important). In order to im-
prove the state of the art for termina-
tion proving of programs using data
structures, we must develop better
methods of finding arguments over
data structure shapes, and we must
also improve the accuracy and scal-
ability of existing shape analysis tools.

figure 10. example of multi-threaded terminating producer/consumer program.

1 while x > 0 do 2 x:=x– 1; 3 lock(lck) 4 b := x; 5 unlock(lck) 6 done

1

2

3

5

6

while y > 0 do lock (lck) y:=b; unlock(lck)

done
To prove that the thread on the left terminates we must assume that the thread on the right always
calls unlock when needed. To prove that the thread on the right always calls unlock when needed,
we must prove that the thread on the left always calls unlock when needed, and so on.

figure 11. Collatz program.

1 while x > 1 do 2 if x is divisible by 2 then 3 x := x= 2; 4 else 5 6 7 done

x := 3x + 1;

fi We assume that x ranges over all natural numbers with arbitrary precision (that is, neither 64-bit vectors nor 32-bit vectors). A proof of this program’s termination or non-termination is not known.

programs use variables that range over fixed-width numbers, such as 32-bit integers or 64-bit floating-point numbers, with the possibility of overflow or underflow. If a program uses only fixed-width numbers and does not use dynamically allocated memory, then termination proving is decidable (though still not easy). In this case we simply need to look for a repeated state, as the program will diverge if and only if there exists some state that is repeated during execution. Furthermore, we cannot ignore the fixed-width semantics, as overflow and underflow can cause non-termination in programs that would otherwise terminate, an example is included in Figure 9. Another complication when considering this style of program is that of bit-level operations, such as left- or right-shift.

Binary executables. Until now we have discussed proving termination of programs at their source level, perhaps in C or Java. The difficulty with this strategy is the compilers that then take these source programs and convert them into executable artifacts can introduce termination bugs that do not exist in the original source program. Several potential strategies could help mitigate this problem: We might try to prove termination of the executable binaries instead of the source level programs, or we might try to equip the compiler with the ability to prove that the resulting binary program preserves termination, perhaps by first proving the termination of the source program and then finding a map from the binary to the source-level program and proving that the composition with the source-level termination argument forms a valid termination argument for the binary-level program.

Non-linear systems. Current termination provers largely ignore non-linear arithmetic. When non-linear updates to variables do occur (for example x := y z;), current termination provers typically treat them as if they were the instruction x := input();. This modification is sound— meaning when the termination prover returns the answer “terminating,” we know the proof is valid. Unfortunately, this method is not precise: the treatment of these commands can lead to the result “unknown” for programs