A call in VCC makes the prover forget everything that it used to know about data not directly owned by the current thread. This includes fields of wrapped structs. However the version of the wrapped struct is known to remain the same (unless the struct was listed in the writes clause of the called function).

We take advantage of that by introducing an axiom saying that everything that you can possibly read from the sequential ownership domain is a function of the version of the root of the domain. You however need to explicitly assert that things are in the ownership domain to take advantage of that, even that b is in domain of b for example:

#include <vcc.h>

struct A {
  int x;
};

void update(struct A *a)
  maintains(wrapped(a))
  writes(a);

void foo(struct A *a, struct A *b)
  requires(wrapped(a) && wrapped(b) && a != b)
  writes(a,b)
{
  assert(in_domain(b, b));
  update(a);
  assert(b->x == old(b->x));
}


Once you establish that x is in domain of y, you can establish that something in owns(x) is also in domain of y, so in effect you will usually have a sequence of in_domain(...) assertions (TODO: provide a shortcut syntax for that):

#include <vcc.h>

struct A {
  int x;
};

struct B {
  struct A *a;
  invariant(keeps(a))
};

struct C {
  struct B *b;
  invariant(keeps(b))
};

void update(struct A *a)
  maintains(wrapped(a))
  writes(a);


void bar(struct C *c, struct A *unrelated)
  requires(wrapped(c) && wrapped(unrelated))
  writes(c, unrelated)
{
  assert(in_domain(c, c));
  assert(in_domain(c->b, c));
  assert(in_domain(c->b->a, c));
  update(unrelated);
  assert(c->b == old(c->b));        // these two asserts, are not needed
  assert(c->b->a == old(c->b->a));  // explicitly to show the last one
  assert(c->b->a->x == old(c->b->a->x));
}


The in_domain(...) can only be used to show presence of objects in the strictly sequential ownership domain. In other words, if in_domain(x, y) and set_in(z, owns(x)) then in_domain(z, y), provided that x has non-volatile owns set. If x has volatile owns set one can assert in_vdomain(z, y), which will trigger a check that in any state where the version of y is the same as in the current state and invariant of x holds, z is in owns(x). For example:

#include <vcc.h>

struct A {
  int x;
};

typedef struct vcc(volatile_owns) _B {
    struct A *a;
    invariant(set_in(a, owns(this)))
} B;


struct X { int x; };

void wr(struct X *x)
  writes(x)
  maintains(mutable(x));

void foo(B *b)
  requires(wrapped(b))
{
  struct X unrelated;
  assert(in_domain(b, b));
  assert(in_vdomain(b->a, b));
  assume(b->a->x == 12);
  wr(&unrelated);
  assert(b->a->x == 12);
}


This can be even used when ownership is conditional, as long as it follows from the current version of the root of the domain, e.g.:

typedef struct vcc(volatile_owns) _B2 {
    struct A *a;
    int f;
    invariant(f ==> set_in(a, owns(this)))
} B2;

void fooComplex(B2 *b)
  requires(wrapped(b))
  requires(b->f)
{
    assert(in_domain(b, b));
    assert(in_vdomain(b->a, b));
}


However the verification would fail if f was volatile or its value was unknown.

Last edited Nov 13, 2009 at 1:00 PM by stobies, version 6

Comments

No comments yet.