restrict is not good for modular reasoning

ACSL

There were quite a few posts recently that were concerned with ACSL, and a few more are planned for the near future. ACSL is a specification language for C (comparable with JML for Java, for those who know about JML). Some people call it a BISL, for “Behavioral Interface Specification Language”, but considering that this acronym's definition needs to be introduced everytime, on account of nobody in the world having ever seen it before, and that it has very little reuse potential, please forget that we mentioned it.

ACSL is Frama-C's annotation language, and it is partially implemented in Frama-C, but it is not intended to be just Frama-C's. According to this message [remove dead link] Microsoft Research's VCC now uses an annotation language with ACSL-like syntax and semantics.

ACSL allows to write function contracts the stuff that modular reasoning about programs is made of. A function contract is supposed to tell you everything you need to know about the function so that you do not need to look at its code. The function might still be unimplemented even.

ACSL also allows to write annotations that go inside the function and are specific to one particular implementation. These annotations are typically hints to allow the verification that the specific implementation satisfies the contract. They can be for instance loop invariants or assertions.

It is good on several levels to be able to write and read properties about a C program in a formal language with unambiguous meaning. A compiler could parse and interpret ACSL to obtain information about the programmer's intentions and take advantage of the opportunity to generate faster code. Hey compiler makers I said FASTER CODE.

The restrict type qualifier again

Recently Stephen Canon reminded me that the good thing about restrict is that it is part of the function prototype and I showed the differences with ACSL's approach.

Why does ACSL introduce an new notion the \separated predicate where C99 already has restrict? One reason that I pointed out is that while restrict offers a very concise syntax for some specialized uses \separated is useful for other things that are not convenient to express with restrict.

Another reason is that a C prototype with restrict annotations still does not work very well as a contract. The restrict qualifier in the prototype implicitly refers to the function's code. This blog post expands on this.

The meaning of restrict

The restrict qualifier applied to a pointer more or less means that any offset of the pointer can only alias with an offset of the pointer. Please read C99's 6.7.3.1 section for the exact definition. I will simply quote the example from paragraph 8 there:

---

The function parameter declarations in the following example

void f(int n  int * restrict p  int * restrict q) 
{  
  while (n-- > 0)  
  *p++ = *q++;  
} 

assert that during each execution of the function if an object is accessed through one of the pointer parameters then it is not also accessed through the other.

---

Note that the notion of any offset of a pointer p being separated from everything else that is not also an offset of p is a relative notion. In the absolute p has to point somewhere. If for instance p points inside a global array t then p aliases with t. The restrict qualifier only means that locally inside the function f for what f does an offset of p does not alias with any lvalue not based on p. As the next paragraph in the standard puts it:

---

The benefit of the restrict qualifiers is that they enable a translator to make an effective dependence analysis of function f without examining any of the calls of f in the program. The cost is that the programmer has to examine all of those calls to ensure that none give undefined behavior. For example the second call of f in g has undefined behavior because each of d[1] through d[49] is accessed through both p and q.

void g(void)  
{  
  extern int d[100];  
  f(50  d + 50  d); //valid  
  f(50  d + 1  d); //undefined behavior  
}  

---

The call f(50 d + 50 d) is valid because although offsets of d+50 can obviously alias with offsets of d they do not alias inside the function for what the function does. When calling f(50 d + 1 d); offsets of the two restrict-qualified pointers do alias and the call invokes undefined behavior.

No modular reasoning

And this sums up why restrict alone would not be good for modular reasoning about programs. It is part of the prototype and the prototype is a kind of limited contract but the exact meaning of restrict depends on the function's implementation. If the function computes p + 49 then p + 49 is part of the offsets of p that must not alias with the rest of the memory locations accessed by f. If f accesses the global variable G by name then p must not point to G. if f does not access G by name then p is allowed to point to G. It is only one particular implementation of f that gives meaning to restrict.

By contrast a proper contract is supposed to be self-contained. The ACSL precondition \separated(p+(0..n-1) q+(0..n-1)); tells the programmer exactly how the arguments p and q are allowed to alias. An implementation for f needs not exist for the programmer to start using it with the confidence that ey is calling f properly.