-
Notifications
You must be signed in to change notification settings - Fork 26
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.
Intrinsic locking in PVL consists of three parts:
- Lock invariant
- The
lock
statement - The
unlock
statement
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.
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.
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.
There are several caveats to look out for when using intrinsic locks in PVL.
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.
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.
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.
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.
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.
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:
- The synchronization done by the atomic block is scoped, so unlocking is done automatically.
- Declaration of the invariant is done at the method level, instead of at the class level.
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.
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.
Tutorial
- Introduction
- Installing and Running VerCors
- Prototypical Verification Language
- Specification Syntax
- Permissions
- GPGPU Verification
- Axiomatic Data Types
- Arrays and Pointers
- Parallel Blocks
- Atomics and Locks
- Process Algebra Models
- Predicates
- Inheritance
- Exceptions & Goto
- VerCors by Error
- VeyMont
- Advanced Concepts
- Annex
- Case Studies
Developing for VerCors