Atomics and Locks

VerCors supports three forms of synchronization primitives. Two can only be used in PVL: intrinsic locks, and atomics. One can only be used in Java: the synchronized block. Each form will be discussed individually in the next sections.

PVL: Intrinsic locks

Intrinsic locking in PVL consists of three parts:

• Lock invariant
• The lock statement
• The unlock statement

Lock invariant

A lock invariant can be defined within a class with the following syntax:

class C {
    // ... 
    resource lock_invariant() = true /* or: resource expression involving permissions and boolean assertions */ ;
    // ...
}

This syntax is very similar to the syntax used for defining predicates. You can find more info about predicates here. However, knowledge of predicates is not needed to understand and use locks in VerCors.

Because a lock invariant is defined in a class, it is always related to a specific class instance. Therefore, it is possible to make assertions about instance fields in the lock invariant. For example, a lock invariant could be specified that contains the permissions for a field, and also the fact that that field must have a value greater than 10, using the following syntax:

class C {
    int f;

    resource lock_invariant() = Perm(f, write) ** f > 10;

    C() {
        f = 11;
        // Lock invariant must hold here!
    }
}

The lock invariant must hold at the end of the constructor. If VerCors cannot prove this, the program will be rejected.

Using Java terminology, in the above example the field f is "guarded" by the intrinsic lock of the object that has the field f. That is, to write permission for this.f, and hence access to this.f, first the lock on this needs to be acquired. This is done using the lock statement, which is described in the next section.

lock statement

The lock statement has the following syntax:

lock o;

Where o can be an arbitrary expression. The only constraints are that o is not nullable and must be of a class type, where the specific class must also have a lock_invariant. This can be the trivial lock invariant true, but it must still be explicitly declared.

The lock statement ensures that only one thread at a time can lock on an object. Once the lock has been acquired, the lock invariant of the object o may be assumed. For example, after the lock statement, often fields of the object o can be accessed. For example, consider the code snippet below. It is similar to the previous example, with the addition of an increment method:

class C {
    int f;

    resource lock_invariant() = Perm(f, write);

    void increment() {
        lock this;
        assert Perm(f, write);
        f = f + 1;
    }
}

Notice how the lock is acquired before f is incremented. Because after lock statement the lock invariant may be assumed, this ensures the thread that is executing increment has write permission for f, which in turn allows reading and writing to f. Additionally, this excludes any data races on f, as the thread that has the lock will be the only thread currently incrementing f.

The above example is still incomplete: when f has been incremented, the lock should be unlocked again. This is done with the unlock statement, which we describe next.

unlock statement

The unlock statement has the following syntax:

unlock o;

Similar to the lock statement, o must be non-null and of a class type that has the lock_invariant predicate defined.

The unlock statement behaves as the inverse of the lock statement. For the program to progress beyond unlock, the lock invariant must be re-established. If this is not possible, VerCors will reject the program. If the lock invariant can be re-established, the lock is unlocked, and the program proceeds. Because the lock is now unlocked, other threads can lock it, and gain access to the resources protected by the lock.

In the code snippet, the previous code snippet is completed with the missing unlock statement:

class C {
    int f;

    resource lock_invariant() = Perm(f, write);

    void increment() {
        lock this;
        assert Perm(f, write);
        f = f + 1;
        unlock this;
    }
}

Because the only thing we did between lock and unlock was increment f, the write permission for f is still available, and hence VerCors can trivially prove that the lock invariant can be re-established. Hence, this example verifies.

Intrinsic locks: caveats

There are several caveats to look out for when using intrinsic locks in PVL.

Avoid: locking in the constructor

Since the lock invariant is established at the end of the constructor, it is of vital importance that the object being constructed is not locked before that. This could otherwise lead to unsoundness. Consider the following example:

class C {
    int f;

    resource lock_invariant() = Perm(f, write);

    C() {
        assert Perm(f, write);
        lock this;
        assert Perm(f, write) ** Perm(f, write);
        assert false;
    }
}

Since the lock invariant is not yet established, we still have a write permission to f. Additionally, because we lock on this, we may also assume the lock invariant after the lock statement. This leads to having two write permissions, which is not allowed by VerCors, and hence allows proving false. Note that this can also happen if a method that locks on its argument is called in the constructor. Therefore, care needs to be taken when calling methods from constructors.

Avoid: locking a lock twice

PVL locks are non-reentrant: locking a lock twice, without unlocking the lock inbetween, will result in a deadlock. VerCors does not warn about this situation if it occurs. Hence, it needs to be checked manually that this situation does not occur.

Avoid: deadlocking interleavings

Deadlocks can occur when using multiple locks. For example, consider a situation with two locks, l1 and l2. Process A first locks l1, and then tries to acquire l2. Process B locks l2, and then tries to acquire l1. Since intrinsic locks in PVL are blocking, this interleaving will deadlock. VerCors does not warn about this situation if it occurs. Hence, it needs to be checked manually that this situation does not occur, because it can otherwise allow unsoundness to occur.

PVL: Atomics

For this section, we assume you are familiar with the concept of "lock invariant", as introduced int the previous section.

Atomics in PVL are used through two statements: the invariant statement and the atomic statement. We will discuss them separately.

invariant block

The syntax of the invariant block is as follows:

invariant invName(true) {
    // ...
}

An invariant block consists of the keyword invariant, then a name, and finally an expression that is the atomic invariant of the block. The invariant block may only occur in methods or procedures, and may be nested, provided that the names of each invariant block are unique.

The invariant block will ensure that the atomic invariant holds at the beginning of the block. Inside the invariant block, you will not have access to the atomic invariant, as it is removed from the state at the beginning of the invariant block. You can get access to the atomic invariant using the atomic block, which is explained in the next section. After the invariant block, the atomic invariant may be assumed again.

atomic block

The syntax of the atomic block is as follows:

atomic(invName) {
    // ...
}

The atomic block consists of the keyword atomic, followed by the name of the invariant the atomic block synchronizes on. The atomic block may only occur in methods or procedures, may not be nested, and the invariant that is referred to must enclose the atomic block.

The atomic block will ensure only one thread at a time will synchronize on the invariant. At the beginning of the atomic block, the atomic invariant is assumed. At any point in the atomic block, this atomic invariant can be used and broken. Finally, when the program exits the atomic block, the atomic invariant needs to be re-established. If VerCors cannot prove that this is always possible, VerCors will reject the program and verification will fail.

The atomic block is similar to the lock invariant and lock/unlock statements, with two subtle differences:

1. The synchronization done by the atomic block is scoped, so unlocking is done automatically.
2. Declaration of the invariant is done at the method level, instead of at the class level.

Java: synchronized

The synchronized statement allows you to work with lock invariants in Java. It is a combination of intrinsic locks from PVL, and atomics from PVL, which are both explained in previous sections. Specifically, VerCors supports the lock invariant syntax for Java classes, and synchronized blocks work almost identically to atomic blocks. Both concepts will be discussed in the next sections.

Java: lock invariants

VerCors supports the lock invariant syntax for Java classes. The syntax is as follows:

class C  {
    //@ resource lock_invariant() = true;

    C() {
        // Lock invariant is established here!
    }
}

Notice how the syntax is identical to the PVL syntax, except that it must now be placed in ghost code, as indicated by the //@ marker. In the above example the trivial lock invariant true is used, but in principle the lock invariant can contain the same things as in PVL: permissions about fields, arrays, and properties about those fields and arrays.

The lock invariant has to hold at the end of a constructor, otherwise verification will fail. The lock invariant is assumed at the beginning of synchronized blocks, and has to be re-established at the end of synchronized blocks. If it cannot be re-established, VerCors will reject the program and verification will fail.

Java: synchronized block