Atomics and Locks

VerCors supports three forms of synchronization primitives. Two can only be used in PVL, one can only be used in Java. Each form will be discussed individually.

PVL: Intrinsic locks

Intrinsic locking in PVL consists of three parts:

• Lock invariants
• The lock statement
• The unlock statement

Lock invariants

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

class C {
    ...
    resource lock_invariant() = /* 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;
}

A lock

PVL: Atomics

Java: Synchronized