Unique Types

This page summarizes what is supported for unique and const qualifiers in C and GPU verification.

Why qualifiers help performance

Large quantified-permission obligations are often a bottleneck, especially in parallel settings.

• const can reduce mutable-state reasoning.
• unique can reduce aliasing interactions and interference between pointer obligations.

Related reading:

• Scalable Deductive Verification of Data-Level Parallel Programs
  https://link.springer.com/section/10.1007/978-3-032-32519-8_5

const Type

For const pointers, you do not need to supply permission annotations, as we view the data as immutable. Thus the following verifies.

 //@ context x != NULL && \pointer_length(x)>0;
int f(const int* x) {
  return x[0];
}

Unique Type

Generally give each pointer/array variable a different unique type. Only when those variables are assigned to each other, or compared with each other, they should have the same unique type.

void f(/*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1){
  // This function does further not compare x0 and x1 or compares them,
  // so this works.
  // ..
}

  // Here x1 assigns x0 to it, so should have the same unique type
void g(/*@ unique<1> @*/ int* x0, /*@ unique<1> @*/ int* x1){
  x1 = x0;
}
 
 // Here x1 compares x0 to it, so should have the same unique type
void h(/*@ unique<1> @*/ int* x0, /*@ unique<1> @*/ int* x1){
  if (x0 == x1){
    // Does something if the same
  } else {
    // Or something else if different
  }
}

However, you can not mix different types.

// disallowedQualifiedCoercion
void f(/*@ unique<1> @*/ int* x0){ int* x1 = x0;}                   

// disallowedQualifiedCoercion
void f(/*@ unique<1> @*/ int* x0){ /*@ unique<2> @*/ int* x1 = x0;} 

// disallowedQualifiedCoercion
void f(/*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1){x1 = x0;} 

Unique pointer fields in structs

unique_pointer_field<field, k> allows tying a struct field to a unique class.

struct vec {
  int* xs;
};

/*@
  context xs != NULL;
  context x1 != NULL ** \pointer_length(x1)==1 ** Perm(*x1, write);
@*/
int f(/*@unique_pointer_field<xs, 2>@*/ struct vec* x1, /*@ unique<2> @*/ int* xs){
  x1->xs = xs;
  //@ assert x1->xs != NULL;
  return 0;
}

Method/function coercion behaviour

Unique types have a number, but the number is only important to distinguish which pointers can be compared with each other or assign to each other. The exact number does not matter. Thus we allow unique coercions across function calls.

Supported examples

• calling non-unique procedures with unique arguments in safe contexts
• recursive and indirect-recursive calls with consistent unique classes
• coercion through struct-field-qualified getters in valid cases

The following case does not work. h indicates that the x and y may overlap, however in the call site of f we know that x0 and x1 do not overlap.

/*@
context n > 0;
context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i<n; Perm(x0[i], 1\2));
context x1 != NULL ** \pointer_length(x1) == n ** (\forall* int i; 0<=i && i<n; Perm(x1[i], 1\2));
ensures \result == x0[0] + x1[0];
@*/
int f(int n, /*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1){
  return h(x0, x1);
}

/*@
  context x != NULL ** \pointer_length(x) > 0 ** Perm(x[0], 1\4);
  context y != NULL ** \pointer_length(y) > 0 ** Perm(y[0], 1\4);
  ensures \result == x[0] + y[0];
@*/
int h(int* x, int* y){
  return x[0] + y[0];
}

The following would work though, as x0 and x1 are now of different unique type.

/*@
context n > 0;
context x0 != NULL ** \pointer_length(x0) == n ** (\forall* int i; 0<=i && i<n; Perm({:x0[i]:}, 1\2));
context x1 != NULL ** \pointer_length(x1) == n ** (\forall* int i; 0<=i && i<n; Perm({:x1[i]:}, 1\2));
ensures \result == x0[0] + x1[0];
@*/
int f(int n, /*@ unique<1> @*/ int* x0, /*@ unique<2> @*/ int* x1){
  return h(x0, x1);
}

/*@
  context x != NULL ** \pointer_length(x) > 0 ** Perm(x[0], 1\4);
  context y != NULL ** \pointer_length(y) > 0 ** Perm(y[0], 1\4);
  ensures \result == x[0] + y[0];
@*/
int h(int* x, /*@ unique<3> @*/ int* y){
  return x[0] + y[0];
}

Practical guidance

When using unique/const:

1. Keep unique class labels consistent end-to-end across assignments, comparisons and calls.
2. (Helper) functions should be as general as possible: whenever possible a different unique number should be used.
3. Use const where mutation is unnecessary to cut down mutable/quantified obligations.
4. If coercion fails, check not only direct parameter and return types but also subtypes of structs or ADT types.