Skip to content

Permissions

Jump to bottom
Alexander Stekelenburg edited this page May 29, 2024 · 4 revisions

This feature is supported for all languages.

This section discusses the basics of handling ownership using a simple toy example. Ownership is used to express whether a thread (or synchronization object) has access to a specific element on the heap. This access can be shared among multiple threads (or synchronization objects), which allows the threads to read the value of this element, or it can be unique to one, in which case the value can written to or read from. Permission annotations are used to express ownership. We start by considering the following simple example program, written in Java:

class Counter {
  public int val;

  void incr(int n) {
    this.val = this.val + n;
  }
}

If you wish, you can store this file as, say, counter.java, and try to run VerCors on this file by running vct --silicon counter.java in a console (assuming you have VerCors installed). This program currently does not contain any annotations, but we will eventually annotate the program to verify the following simple property: after calling the incr function, the value of val has been increased by an amount n. This can be expressed as a postcondition for the incr method: ensures this.val == \old(this.val) + n. The \old(_) expression is used to evaluate an expression in an earlier state. By default this is in the state as it was just after the precondition. This is explained further later on.

However, if you run VerCors on this example, as it is now, you will see that VerCors fails to verify the correctness of the program and reports an 'AssignmentFailed: InsufficientPermission' error, since the caller of the method has insufficient permission to access this.val. First observe that this.val is shared-memory; there may be other threads that also access the val field, since the field is public. In order to prevent other threads from accessing this.val while the calling thread is executing incr, we need to specify that threads may only call c.incr (on any object c that is an instance of Counter) when they have write permission for c.val:

class Counter {
  public int val;

  /*@
    requires Perm(this.val, 1);
    ensures Perm(this.val, 1);
    ensures this.val == \old(this.val) + n;
  */
  void incr(int n) {
    this.val = this.val + n;
  }
}

We added three things to the counter program. The first is a requires clause, which is a precondition expressing that incr can only be called when the calling thread has permission to write to val. The second is an ensures clause, which is a postcondition expressing that, given that the incr function terminates (which is trivial in the above example), the function returns write permission for val to the thread that made the call to incr. The third is a postcondition that states that after incr has terminated, the value of this.val has indeed been increased by n. If you run this annotated program with VerCors, you will see that it now passes. The remainder of this section mostly focuses on how to use the Perm ownership predicates.

Observe that the clause Perm(this.val, 1) expresses write permission for this.val. Recall that VerCors has a very explicit notion of ownership, and that ownership is expressed via fractional permissions. The second argument to the Perm predicate is a fractional permission; a rational number q in the range 0 < q <= 1. The ownership system in VerCors enforces that all permissions for a shared memory location together cannot exceed 1. This implies that, if some thread has permission 1 for a shared-memory location at some point, then no other thread can have any permission predicate for that location at that point, for otherwise the total amount of permissions for that location exceeds 1 (since fractional permissions are strictly larger than 0). For this reason, we refer to permission predicates of the form Perm(o.f, 1) as write permissions, and Perm(o.f, q) with q < 1 as read permissions. Threads are only allowed to read from shared memory if they have read permission for that shared memory, and may only write to shared memory if they have write permission. In the above example, the function incr both reads and writes this.val, which is fine: having write permission for a field implies having read permission for that field.

Let us now go a bit deeper into the ownership system of VerCors. If one has a permission predicate Perm(o.f, q), then this predicate can be split into Perm(o.f, q\2) ** Perm(o.f, q\2). Moreover, a formula of the form Perm(o.f, q1) ** Perm(o.f, q2) can be merged back into Perm(o.f, q1 + q2). For example, if we change the program annotations as shown below, the program still verifies successfully:

/*@
  requires Perm(this.val, 1\2) ** Perm(this.val, 1\2);
  ensures Perm(this.val, 1\2) ** Perm(this.val, 1\2);
  ensures this.val == \old(this.val) + n;
*/
void incr(int n) {
  this.val = this.val + n;
}

For splitting and merging we use the ** operator, which is known as the separating conjunction, a connective from separation logic. A formula of the form P ** Q can be read as: "P, and separately Q", and comes somewhat close to the standard logical conjunction. In essence, P ** Q expresses that the subformulas P and Q both hold, and in addition, that all ownership resources in P and Q are together disjoint, meaning that all the permission components together do not exceed 1 for any field. Consider the formula Perm(x.f, 1) ** Perm(y.f, 1). The permissions for a field f cannot exceed 1, therefore we can deduce that x != y.

One may also try to verify the following alteration, which obviously does not pass, since write permission for this.val is needed, but only read permission is obtained via the precondition. VerCors will again give an 'InsufficientPermission' failure on this example.

/*@
  requires Perm(this.val, 1\2);
  ensures Perm(this.val, 1\2);
  ensures this.val == \old(this.val) + n;
*/
void incr(int n) {
  this.val = this.val + n;
}

If you replace both ownership predicates for Perm(this.val, 3/2), then the tool will report a 'MethodPreConditionUnsound: MethodPreConditionFalse' error because the precondition can then never by satisfied by any caller, since no thread can have permission greater than 1 for any shared-memory location. VerCors is a verification tool for partial correctness; if the precondition of a method cannot be satisfied because it is absurd, then the program trivially verifies. To illustrate this, try to change the precondition into requires false and see what happens when running VerCors. Note that VerCors does try to help the user identify these cases by showing a 'MethodPreConditionUnsound' if it can derive that the precondition is unsatisfiable. But one has to be a bit careful about the assumptions made on the program as preconditions.

Self-framing

Consider the following variant on our program. Would this verify?

/*@
  requires Perm(this.val, 1);
  ensures this.val == \old(this.val) + n;
*/
void incr(int n) {
  this.val = this.val + n;
}

This program does not verify and gives an 'InsufficientPermission' failure when given to VerCors. The reason is that, also in the specifications one cannot read from shared-memory without the required permissions. In this program, the ensures clause accesses this.val, however no ownership for this.val is ensured by the incr method. Note that, without a notion of ownership, one cannot establish the postcondition: perhaps some other thread changed the contents of this.val while evaluating the postcondition. By having a notion of ownership, no other thread can change the contents of this.val while we evaluate the postcondition of the call, since no other threads can have resources to do so.

Moreover, the order of specifying permissions and functional properties does matter. For example, the following program also does not verify, even though it ensures enough permissions to establish the postcondition:

/*@
  requires Perm(this.val, 1);
  ensures this.val == \old(this.val) + n;
  ensures Perm(this.val, 1);
*/
void incr(int n) {
  this.val = this.val + n;
}

VerCors enforces that shared-memory accesses are framed by ownership resources. Before accessing this.val in the first ensures clause, the permissions for this.val must already be known! In the program given above, the access to this.val in the postcondition is not framed by the ownership predicate: it comes too late.

Permission leaks

So what about the following change? Can VerCors successfully verify the following program?

/*@
  requires Perm(this.val, 1);
  ensures Perm(this.val, 1\2);
  ensures this.val == \old(this.val) + n;
*/
void incr(int n) {
  this.val = this.val + n;
}

VerCors is able to verify the example program given above. However, less permission for this.val is ensured then is required, meaning that any thread that calls c.incr will need to give up write permission for c.val, but only receives read permission back in return, after incr has terminated. So this example has a permission leak. Recall that threads need full permission in order to write to shared heap locations, so essentially, calling c.incr has the effect of losing the ability to ever write to c.val again. In some cases this can be problematic, while in other cases this can be helpful, as losing permissions in such a way causes shared-memory to become read-only, specification-wise. However, in the scenario given below the permission leak will prevent successful verification:

/*@
  requires Perm(this.val, 1);
  ensures Perm(this.val, 1\2);
  ensures this.val == \old(this.val) + n;
*/
void incr(int n) {
  this.val = this.val + n;
}
  
/*@
  requires Perm(this.val, 1);
*/
void incr2(int n) {
  incr(n);
  incr(n);
}

In the incr2 method, the first call incr(n) will consume write permission for this.val, but only produce read permission in return. Therefore, the requirements of the second call incr(n) cannot be satisfied, which causes the verification to be unsuccessful.

Some extra notation

We end the section by mentioning some notational enhancements for handling permissions. Instead of writing Perm(o.f, 1), one may also write Perm(o.f, write), which is perhaps a more readable way to express write permission for o.f.

Similarly, one can write Perm(o.f, read) to express a non-zero read permission. Note that if this is used in a pre- and postcondition, it is not guaranteed to be the same amount of permissions. The underlying amount of permissions is an unspecified fraction and can therefore not be merged back into a write permission. This can be observed in the following program where the assert fails:

class Counter {
	int val;

	/*@
	requires Perm(this.val, write);
	ensures Perm(this.val, write);
	ensures this.val == \old(this.val) + n;
	*/
	void incr(int n) {
		int oldValue = getValue();
		//@ assert Perm(this.val, write);
		this.val = oldValue + n;
	}
	
	/*@
	requires Perm(this.val, read);
	ensures Perm(this.val, read);
	ensures \result == this.val;
	*/
	int getValue() {
		return this.val;
	}
}

read is mostly useful for specifying immutable data structures. One can also write Value(o.f) to express read permission to o.f, where the value of the fractional permission does not matter. Consequently, Value ownership predicates can be split indefinitely.

If you instead want to express that you require some non-zero amount of read permission and that the same amount of permission is returned you an either add a ghost parameter of type frac which must be provided at every call site to specify the amount of available read permission, or you can use AutoValue(o.f). Similarly to Value, AutoValue expresses that some amount of read permission is required. However, unlike Value no amount of read permission is removed when AutoValue is exhaled, it merely checks that there exists some amount of read permission. When the AutoValue in a precondition is inhaled you gain a symbolic non-zero, non-write amount of read permission which must be exhaled at the end of the context again. If the same AutoValue expression does not appear in the postcondition an automatic leak check is added. Usage looks like this (unlike the previous example the assert now passes):

class Counter {
	int val;

	/*@
	requires Perm(this.val, write);
	ensures Perm(this.val, write);
	ensures this.val == \old(this.val) + n;
	*/
	void incr(int n) {
		int oldValue = getValue();
		//@ assert Perm(this.val, write);
		this.val = oldValue + n;
	}
	
	/*@
	requires AutoValue(this.val);
	ensures AutoValue(this.val);
	ensures \result == this.val;
	*/
	int getValue() {
		return this.val;
	}
}

Note

Note that AutoValue may only be used in combination with **, ==>, \let .. in .., and .. ? .. : ... For the implication, let, and ternary expressions the AutoValue may only appear on the right-hand side and in the postcondition the left-hand side will automatically be wrapped in \old(_) because the leak check must always occur at the end of the scope to prevent unsoundness.

If you want to express that a thread has no ownership over a certain heap element, then one can use the keyword none, e.g. Perm(o.f, none). This is equivalent to writing true. It can be useful in situations where the amount of permission is conditional, e.g. Perm(o.f, cond ? 1\2 : none).

If you want to express permissions to multiple locations, one may use \forall* vars; range; expr. For example, (\forall* int j; j >= 0 && j < array.length; Perm(array[j], write) denotes that the thread has write access to all elements in array. It is equivalent to writing Perm(array[0], write) ** Perm(array[1], write) ** … ** Perm(array[array.length-1], write). Another way to specify permissions of all array elements is to use Perm(array[*], write) which is equivalent to the previous expression.

If you want to reason about the value that the variable refers to as well then you can use PointsTo(var, p, val) which denotes that you have permission pfor variable var which has value val. It is similar to saying Perm(var, p) and var == val.

Old Heap State

As mentioned earlier, you can use \old(_) to evaluate an expression in an older state. By state here we mean strictly the heap, and not any local variables. By default, the \old predicate uses the heap just after the precondition as the heap to evaluate the expression in. You can specify a different heap with \old[l](_), where l is either a ghost label (//@ ghost label l) or a regular label in your input language.

As an example, consider the following method:

class Obj { int f; }

context Perm(x.f, write) ** Perm(y.f, write);
void test(Obj x, Obj y) {
    Obj z = x;
    
    y.f = 2;
    label a;
    
    z.f = 30;
    label b;
    
    z.f = 400;
    label c;
    
    z = y;
    z.f = 3000;
    label d;
    
    assert
        z.f + // (1)
        \old[a](
            z.f + // (2) 
            \old[b](
                z.f + // (3) 
                \old[c](
                    z.f + // (4)
                    \old[d](
                        z.f // (5)
                    )
                )
            )
        ) == 6006;
}

Any time that an expression uses the heap to evaluate itself, we look where the nearest \old expression is. For us, that is:

  • (1) has no \old above it, so it is simply the current heap.
  • (2) has \old[a] as its closest parent \old, so it is evaluated in the heap at label a
  • (3) is evaluated in the heap at label b
  • (4) is evaluated at label c
  • (5) is evaluated at label d, which is the same heap that (1) is evaluated with

Now, why is the answer 6006? This is because the expression z.f is evaluated with an old heap, but not with an older value of the variable z. Thus: it only counts that z aliases the same object as y when we enter the assertion. The value for y.f at all our heaps are, repspectively:

  • (1) y.f == 2, since we just assigned it
  • (2) y.f == 2, since an assignment to x has no effect on y
  • (3) y.f == 2, idem
  • (4) y.f == 3000, since we just assigned it
  • (5) y.f == 3000 still, since the heap at (1) is the same heap as at label d

Note

This is just an illustrative example, and as a matter of style you should try to keep the expression you evaluate in an \old as small as possible. Certainly it should not be necessary to nest them.

Another important detail is how \old interacts with \unfolding. (In case you are reading this tutorial in order, you can come back to this section after reading about predicates). The intuition is that \unfolding takes the current heap, and temporarily unfolds a predicate while its body is evaluated, whereas \old discards the current heap and replaces it with a different one. The consequence of this is that nesting them can lead to unexpected effects:

  • An \unfolding nested in an \old: first the \old has replaced the current heap, after which the \unfolding unfolds a predicate in the old heap
  • An \old nested in an \unfolding: first the \unfolding unfolds a predicate in the current heap, but this action is thrown away by \old, since it replaces the entire heap.

An example of the second situation is a program like this:

class Problem {  
  int x;
  resource state() = Perm(x, 1);

  requires state();
  //                                                   [-
  ensures state() ** (\unfolding state() \in (x == \old(x) + 1));
  //                                                    -]
  // ERROR: There may be insufficient permission to access this field here
  void inc() {
    unfold state();
    x++;
    fold state();
  }
}

It is clear what the intended behaviour is: we simply want to relate the value of x between the pre- and postcondition, so we temporarily unfold it and compare the values. This does not work, because the \old nested under \unfolding replaces the whole heap with a heap as it was just past the precondition. In this heap, we can derive from the precondition that it just contains state(), so we do not have permission to x.

The solution is to unfold twice: once in the current heap, and once in the old heap. We first have to enter the old heap before we unfold its state.

class Solution {  
  int x;
  resource state() = Perm(x, 1);

  requires state();
  ensures state() ** (\unfolding state() \in x) == \old((\unfolding state() \in x)) + 1;
  // Verified
  void inc() {
    unfold state();
    x++;
    fold state();
  }
}

Home

Tutorial

Developing for VerCors

Clone this wiki locally