This project is read-only.

Always wrap on function boundary?

Jul 9, 2009 at 3:32 PM

Hi all:

First, kudos for getting VCC published here. Now some questions on wrapping ... 

(1) do I (really) always have to wrap when the control flow passes a function boundary?

(2) if I don't really have to: is it good practice to always wrap in between functions in a concurrent setting? (this is a more "semantic" question)

(3) in either case: does production verification code do this wrapping/unwrapping manually (it looks not so beautiful) or would you suggest to hide it (in the medium term) into some more generic (project-dependent) function entry/exit specification functions or (now I am guessing) things like expose/skinny_expose? (this is more a "syntactic" question)

~$ cat intercourse_safe.c
#include "vcc.h"
struct a {
        int b;
} e;
void sub(struct a *c)
        writes(c)
        maintains(wrapped(c))
        ensures(c->b == 0) {
        unwrap(c);
        c->b = 0;
        wrap(c);
}
void main ()
        writes(&e)
        requires(wrapped(&e)) {
        sub(&e);
        assert(e.b == 0);
}
~$ vcc /v intercourse_safe.c
Verification of sub succeeded.
Verification of main succeeded.

~$ cat intercourse_unsafe.c
#include "vcc.h"
struct a {
        int b;
} e;
void sub(struct a *c)
        writes(c) {
        c->b = 0;
}
void main ()
        writes(&e)
        requires(wrapped(&e)) {
        unwrap(&e);
        sub(&e);
        return;
}

~$ vcc /v intercourse_unsafe.c
Verification of sub failed.
intercourse_unsafe.c(7,2) : error VC8507: Assertion 'c->b is writable' did not verify.
Verification of main succeeded.
Exiting with 2 (1 errors)

Jul 9, 2009 at 4:00 PM

Hi Holger,

no, you don't always need to wrap objects on function boundaries, but you have to provide sufficient information about the state of objects: in your case, the contract of the failing version of sub does not say anything about the mutability of c. If you specify

void sub(struct a *c)
        writes(span(c)){
        c->b = 0;
}

then VCC will generate the mutability preconditions for you, and it verifies. But beware that you need to add an "ensures(mutable(c))" to make the state of c visible to callers of sub (or indeed wrap(c) at the end of sub).

Wrapping at the boundaries of function calls often is advisable even for sequential verification, because it makes sure that a function (re-)establishes the invariants of data. Invariants don't need to hold for mutable objects. It also makes framing (writes...) easier, because you don't need to talk about the span of objects, i.e., their fields, but only say that a (wrapped) object is written to - the function may than change all objects in the ownership domain of that object.

For concurrency, function boundaries are not the important things. There, you are more concerned with entry/exit of critical sections for locked data or atomic sections for volatile data. Remember that the only thing you basically know about an object in a concurrent context is its invariant. In particular for volatile data, you basically don't know anything else.

This is why you use claims to keep objects closed - so you know their invariants. Claims also offer the possibility to keep additional information about an object in a concurrent setting, because they may be associated with properties (in conjunction with the one that the claimed objects are closed as long as there is a claim to them).

For a mutable object (not closed), you basically know everything about non-volatile fields (because they are owned by the current thread) but nothing about volatile fields (because they can change arbitrarily - not even a two-state invariant restricts they way they can change).

RE 3): yes, you do have to introduce ghost code to control wrapping/unwrapping of objects. You can, however, use the more readable

expose(c){ ... }

instead of

unwrap(c); ... ; wrap(c)

Hope that helps,

Thomas

 

Jul 9, 2009 at 4:27 PM

Hi Holger!

Just a small addition to Thomas remarks regarding your question (2):

Once you are in a concurrent setting, you basically only have claims to ensure that objects are closed. If you just require wrapped() on functions from which you know that they will be called in a concurrent context, you will have to prove at some point in your code, that the current thread actually owns the object and that other threads cannot modify it. Therefore you should be really sure about your invariants on the datatypes before you start annotating your functions, because finding out later that certain parts of data structures are acutally lock protected will trigger large changes throughout your code base.

For unwrapping claimable objects VCC requires that there are no outstanding claims to that object. Otherwise you will not be able to unwrap that object. In general your real code will have to employ concurrency primitives like locks which enable you to get sequential access to an object while you hold the lock. In many cases you will very likely have to pass claims to functions in a concurrent setting instead of requiring that a passed object is actually wrapped.

HTH,
Markus

Jul 20, 2009 at 7:59 AM
Just a small update: for mutable objects, the volatile modifier doesn’t matter. This is because only closed objects can be modified by threads not owning them, therefore, if you have an open object, you know other threads are not touching it.