Participating in the RERS 2012 competition: liveness questions

This third installment discusses the diagnosis of liveness properties of particular C programs, using Frama-C's value analysis, for the RERS 2012 competition.

[Note added in September 2012: the diagnostic found for the example in this post disagrees with the diagnostic found later and sent to the competition organizers. I am unable to reproduce the result obtained here. Perhaps it was obtain with a version of Frama-C that had a bug.]

Liveness properties 101

Here is another extract of two properties found in the property list attached to Problem 1 in the competition:

(G ! oW)
output W does never occur
----------------------------------------
(F oW)
output W occurs eventually

To tell you how unaccustomed to temporal properties I am I first read the second formula as a negation of the first one. There are redundancies in the lists of formulas to evaluate and I thought this was one more of them. It is of course not the case: (F oW) is not the negation of (G ! oW).

(G ! oW) says that there is no execution path that leads to W being output; the negation of that is that there is at least one such execution path. By contrast (F oW) expresses that all execution paths have a W being output at some point a much stronger property.

Indeed (F oW) expressing that a state in which W is output is eventually reached is a typical liveness property. Checking this kind of property is at odds with traditional abstract interpretation practices where the analysis is considered done when a fixpoint has been reached: the fixpoint does not tell whether all executions eventually leave the loop. It only tells what is guaranteed for those executions that leave the loop.

Semi-solution: a simple program transformation

Please bear with me and consider the simple modification of Problem1.c below applied on top of the previous instrumentation:

--- Problem1.c	2012-08-08 10:15:00.000000000 +0200
+++ Problem1_terminate_at_W.c	2012-08-21 17:00:38.000000000 +0200
@@ -1 9 +1 8 @@
 void assert(int x)
 {
   if (!x)
     {
-      Frama_C_show_each_assert_reached();
       /*@ assert \false; */
     }
 }
@@ -594 6 +593 8 @@
         // operate eca engine
         output = calculate_output(input);
+	// continue only if output not W yet
+	/*@ assert output != w ; */
     }
 }

We remove the user message in our assert() function because we want to temporarily forget about assertions. Besides by instrumenting the main loop we make the program stop when the output is W.

You should be able to convince yourself that the modified program terminates if and only if the original program does not admit any infinite execution that never outputs W (for any infinite sequence of values assigned to variable input).

Earlier posts (1 2) in this blog pointed out how Frama-C's value analysis could be made to forget that it was an abstract interpreter and verify the termination of programs.

Application

Since everything is ready for this particular property of Problem1.c let us run the verification. The command to prove that the program terminates is as follows:

$ frama-c -val -obviously-terminates -no-val-show-progress Problem1_terminate_at_W.c
...
[value] Semantic level unrolling superposing up to 400 states
[value] done for function main
[value] ====== VALUES COMPUTED ======

We should have used a timeout because the analysis fails to terminate when the analyzer is unable to prove that the target program terminate. Nevertheless we were lucky the target program terminates the analyzer is able to verify that the program terminates and we can conclude that there are no infinite executions of the original Program1.c that fail to emit W.

Assertions and consequences on liveness properties

The previous section only tells us that there is no infinite execution that does not emit W. Depending on the organizers' intentions this may or may not answer the question of whether (F oW) holds.

It still depends whether you count an execution that reaches one of the assert(0); in the program as well an execution. If it count as an execution to which the formula should apply then an execution that does not emit W and terminates on such an assert(0); certainly does not eventually output W.

There is an argument to say that it shouldn't count however: although it is impossible to understand what these programs are supposed to do assertions usually characterize illegal behaviors. Perhaps the LTL formulas are to be evaluated only on the legal infinite behaviors of the system?

In the latter case we are done: (F oW) holds because W is eventually emitted in all legal executions. In the former case the additional question is whether an original assert(0); is reached before W is output which is a simple reachability question on the instrumented Problem1_terminate_at_W.c. The answer is then that (F oW) does not hold because there are plenty of assert(0); calls that are reached without W having been emitted.

We e-mailed the organizers and they said it was the first simpler case. Only infinite executions need be taken into account for evaluating LTL formulas and interrupted executions can be ignored. Our answer for the formula (F oW) of Problem 1 in the competition is therefore that the property holds.

Proving that something does not eventually happen

In the first part of the post we set out to prove that the liveness property (F oW) was true. Verifying that the property is false requires a different approach. With the toolset provided by Frama-C I only see the scheme below. We reduce the problem to the seemingly harder but actually easier problem of computing the maximum number of iterations before W is emitted.

1. Obtain the number N of reachable states for the system by running the value analysis on the original program.
2. Instrument the program as previously making execution terminate when W is emitted and also maintaining a transition counter (incremented at each iteration of the loop).
3. Using sound and complete propagation on the instrumented program either reach a fixpoint (with a finite bound computed for the counter) or find an execution with N+1 transitions that does not emit W. The former case means that the program eventually emits W. The latter that in the transition graph there is a reachable cycle along which W is not emitted and therefore an infinite execution that does not output W.

This technique likely gets pretty heavy in practice. Adding a counter that may go up to N+1 to a system that already has N states can probably cause the new system to have of the order of N² states. This segues into at least one perhaps two more blog posts to answer the questions “what is the value analysis actually doing when it is applied on these questions?” “how much work would it be to do the same thing closer to the metal executing the C function as compiled instead of laboriously interpreting it?” and “why don't we make a C model checker while we are at it?”