Permissions

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.

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 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).

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.