Comparison with previous work

Comparison with previous work

What we compare
Results and comparison
More detailed description

Here we will compare our interprocedural method with the one designed by [RS01], see also the corresponding experiments.

What we compare

We will use exactly the same general files as in the first section. We compared the analysis on the 3 following procedures: reversal of a list, (reverse as in the first section), non-deterministic insertion of a cell in a single linked list (insert), non-deterministic deletion of a cell in a single linked list (delete).

We used different versions of the insert and delete procedures defined in [RS01], the difference being that we pass as an input (resp. output) parameter the cell to be inserted (resp. deleted), for precise reasons we develop in the sequel. Thus we obtain much more precise information, as we identify in the resulting list which cell has been inserted (resp. deleted). Unfortunately, but not surprinsingly, the analysis time are much higher.

We also experimented [RS01] method on versions nearer of ours, where the inserted (resp. deleted) cell is pointed to by a global variable cell.

In all cases, we obtain an information of different nature, but which contains the information computed in [RS01]:

In [RS01], the result of the analysis at the last node is (an approximation of) the reachable memory configurations after the call to the recursive procedure.
Here, the result we obtain at node main_end is (an approximation of) the relation between the input memory configuration at node main_entry and the current configuration at node main_end, intersected with the reachable memory configuration at node main_entry.

Typically, we are able to prove that reversing twice a list gives the same list, whereas [RS01] could only shows that it gives a list with the same head.

We analyze the following programs:



type cell = record
  n: ^cell;
  k: int; (* Abstracted *)
end record
type list = ^cell;

procedure main(list : list; cell : list) is
var res : list;
begin
main_entry: res := insert(list, cell);
main_end:
end

(* c is supposed to be a list with one element 
   (eg, with c->n := NULL) *)
function insert(h : list; c : list) : t is
begin
insert_entry: if (h!=NULL && ? (*h->k<c->k*)) then begin
insert1:         t := h->n;
insert2:         t := insert(t,c);
insert3:         h->n := NULL;
insert4:         h->n := t;
insert5:         t := h
insert6:
              end else begin
insert7:         c->n := h;
insert8:         t := c;
insert9:
              end
insert_end:
insert_summary:
end















procedure main(list : list) is
var res,cell : list;
begin
main_entry: (res,cell) := delete(list, (*k*));
main_end:
end

(* c is the deleted cell *)
function delete(h : list; (*k:int*)) : (t,c) is
begin
delete_entry: if (h==NULL) then begin
delete1:         t := h
delete2:         c := NULL;
delete3:
              end else begin
delete4:         t := h->n;
delete5:         if (? (*h->k==k*)) then begin
delete6:            h->n := NULL;
delete7:            c := h;
delete8:
                 end else begin
delete9:            (t,c) := delete(t);
delete10:           h->n := NULL;
delete11:           h->n := t;
delete12:           t := h;
delete13:
                 end
delete14:
              end
delete_end:
delete_summary:
end

Results and comparison

Results are given in the following table.

In the "Number of Structures" field, we indicate the number of reachable structures at the following control points:

at the entry of the recursive procedure;
before the recursive call;
after the recursive call;
after elimination of local variables, which gives the summary function;
main_end

Concerning analysis times,

The "Time" column indicates the execution time with our method;
the "Modified [RS01] Time" column the execution time with [RS01] method applied on a modified version of programs with matches more closely our version (use of an additional global variables which tracks the inserted/deleted cell);
the "[RS01] Time" column the execution time with [RS01] method applied on its original version of programs.

Input	Program	Nb of predicates (abs/total) and constraints	Iterations	Nb of Structures	File	Time	Modified [RS01] Time	[RS01] Time
reverse_input.tvs	reverse.tvp	40/56 & 392	10	3, 4, 8, 7, 3	reverse.ps	11s	37s	37s
insert_input.tvs	insert.tvp	66/112 & 708	11	6, 8, 35, 23, 9	insert.ps.gz	188s	76s	22s
delete_input.tvs	delete.tvp	70/122 & 776	11	6, 8, 47, 32, 13	delete.ps.gz	222s	51s	25s

With respect to analysis time, our method performs better than [RS01] for the list reversal, but worse for the other examples. However, remember that the information computed is not the same, as explained in the previous section. The quite important number of structures in the two last examples comes from the fact that we introduce two additional abstraction instrumentation predicates allowing the invariant to be properly maintained, and that many different cases are distinguished. In the case of insertion, at node main_end the cell may have been inserted at the beginning, at the 2th place, ..., and orthogonnally can be followed by 0, 1, 2 or more than 2 cells: this gives 9 structures.

The greater number of structures for delete compared to insert is due to the fact that delete may not delete any cell which adds additional cases.

Coming back the comparison between our method and [RS01] applied on modified version of their programs, we give some reasons for the greater analysis time of our method:

For insertion, it is mainly due to the additional instrumentation predicates, which causes more cases to be distinguished. However the information delivered by the two methods is quite similar (although the second is not relational). Another reason, more implementation related, is that our method uses many predicates, due to the different modes, but most of them are inactive at a given control point. However, the analysis engine currently does not take advantage of it to reduce its computations.
For deletion, as the second method is not relational, it does not say where the deleted cell was located in the list (first,second, in the middle, the last but one, the last), whereas our method is much more precise on this aspect because it is relational. The [RS01] distinguishes only the case where the removed cell is the head cell from the other cases.

More detailed description

We already describe the list reversal example here, so we focus on insert and delete.

We mentioned that for list insertion we needed a different version than the one used by [RS01], see also the WEB page. In their version, there is only one parameter to insert, and the inserted node is dynamically allocated by a special mechanism allowing to add a new individual to a logical structures. However this cannot be performed in our case, as we model an input/output relation between memory configurations. Thus we add two choices:

Model the free heap by a linked list of free memory cells, pointed by a variable heap, and taking the inserted cell in this list;
Or passing the cell to be inserted as a parameter.

We choosed solution 2. Solution 1 implies that we pass forth and back to insert the variable heap, as we cannot model directly global variables. This would give an insert procedure with 2 input and 2 output parameters.

As the effect of insert and delete is local, a specific cross-instrumentation predicate modelling it is not necessary. However we should allow the analysis to discover the two patterns:

Insertion of a cell in a list

Deletion of a cell in a list

For this purpose, we introduced the following instrumentation predicates, to identify direct successor and predecessor of a cell pointed by a variable via a field f:


%r succ[f,m,z](v) = E(v_1) z(v_1) & f[m](v_1,v) unique abs
%r pred[f,m,z](v) = E(v_1) z(v_1) & f[m](v,v_1) abs

Comparison with previous work