To finish on termination

Enthusiastic reactions to the previous post about verifying the termination of a C program with Frama-C's value analysis lead me to write this post-scriptum.

On detecting both termination and non-termination

The scheme I outlined in the previous post can only confirm the termination of the program. If the program does not terminate the analysis method I outlined runs indefinitely. I recommended to use a timeout and to interpret reaching the timeout as the answer “I don't know”. Off-line a colleague complained about this behavior.

This colleague was of course being facetious. Frama-C's value analysis when used normally (without option -obviously-terminates) is already a sound detector of non-termination. Consider the program below:

unsigned char u = 1;
int main(){
  while (u)
    {
      u = u + 14;
    }
  return u;
}

If you can get Frama-C's value analysis to print that the function is a “NON TERMINATING FUNCTION” it means that the function is guaranteed not to have any defined terminating executions (to put it simply the function is guaranteed not to terminate). In this case it is easy:

$ frama-c -val t4.c
[value] Values at end of function main:
          NON TERMINATING FUNCTION

The values displayed as possible at the end of the function are sound over-approximations of the values that are possible in real (defined) executions. When the value analysis says that there are no possible values you can trust that there are no real executions that reach the end of the function.

For more difficult cases I recommend option -slevel to improve the chances that the analyzer will detect non-termination. The guarantees are the same as before: if the value analysis says “NON TERMINATING FUNCTION” no real execution reaches the end of the function. If it describes possible values for variables at the end of the function it mean that because of over-approximations it doesn't know whether the end of the function is reached at all.

unsigned char u;
int main(){
  while (u * u != 17)
    {
      u = u + 1;
    }
  return u;
}

The program above looks for a number whose square is 17. With the default settings the value analysis is unable to decide whether the program terminates or not:

$ frama-c -val t5.c
...
[value] Values at end of function main:
          u ∈ [--..--]
          __retres ∈ [0..255]

Let us now analyze the program more precisely with option -slevel 300:

~ $ frama-c -slevel 300 -val t5.c
...
[value] Values at end of function main:
          NON TERMINATING FUNCTION

That's better: the above result means that the value analysis can guarantee that the program will keep searching for an unsigned char whose square is 17 until the end of the world.

To summarize:

• If you want to verify non-termination you can hope to do so with Frama-C's value analysis in normal mode.
• If you want to verify termination you can hope to do so with Frama-C's value analysis with option -obviously-terminate.
• If you don't know whether the target program terminates or not and you want to chance to detect both then you can launch both frama-c -val and frama-c -obviously-terminates -val in parallel and see whether one of them is able to conclude one way or the other.
• If you want an analyzer that always tells in finite time whether a given program terminates or not and although a C program without dynamic allocation is not exactly similar to a Turing machine you may be asking too much.

On the Collatz conjecture

An expedient shortcut when trying to explain undecidability to non-computer scientists is to encode a famous well-researched mathematical conjecture into a computer program ideally one with a large monetary prize attached to it. It works well as an intuitive explanation of the difficulty of saying anything about the dynamic behavior of arbitrary programs. The argument is that if it was easy to tell whether an arbitrary program does something or the other some mathematician would have taken the opportunity to become famous and possibly rich by encoding the conjecture as a computer program and analyzing this program. This is of course an informal meta-argument. Perhaps all mathematicians are stupid; we don't know about that. But I find this explanation of undecidability works better than any other I have tried.

A long time ago I was using Fermat's last theorem for the above purpose. When it started to be considered satisfactorily proved I switched to Goldbach's conjecture. But Goldbach's conjecture requires enumerating prime numbers. To encode it into the simplest possible program for the purpose of an informal explanation one needs to write at least a function that recognizes a prime number and explain that this is good enough to encode the conjecture into a program.

All this time I should have been using the Collatz conjecture (that you may also know as “Syracuse problem”). My facetious colleagues reminded me of this in the comments to the previous post.

Let us humor these colleagues:

unsigned long long x;
unsigned long long input();
main(){
  x = input();
  while (x > 1)
    {
      if (x%2 == 0) x = x/2; else x = 3*x + 1;
    }
}

Trying to prove termination:

$ frama-c -obviously-terminates -val syracuse.c
...
[value] Semantic level unrolling superposing up to 53600 states
[value] Semantic level unrolling superposing up to 53700 states
[value] Semantic level unrolling superposing up to 53800 states
^C[kernel] User Interruption (Ctrl-C)

Trying to prove non-termination:

$ frama-c -slevel 44444 -val syracuse.c
...
[value] Values at end of function main:
          x ∈ {0; 1}
          __retres ∈ {0}

Both attempts failed. Ah well at least we tried.