Skip to content

Atomics and Locks

Jump to bottom
Bob Rubbens edited this page Aug 31, 2023 · 19 revisions

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

Warning: at the time of writing, VerCors supports only non-reentrant locks. This means locking twice in a row is unsound, which could have implications for code that uses Java's synchronized. See the caveats section at the end of this document for more info.

PVL: Built-in locks

Using built-in locks in PVL consists of the following parts:

  • Lock invariant, which describes the resources that the lock guards
  • The lock statement
  • The unlock statement
  • The commit statement and committed(l) expression, which indicate whether or not a lock is initialized.

Lock invariant

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

lock_invariant true /* or: resource expression involving permissions and boolean assertions */;
class C {

}

Because a lock invariant is defined for 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:

lock_invariant Perm(f, write) ** f > 10;
class C {
    int f;

    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 built-in 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 constraint is that o is not null. The default lock invariant for a class is true, so by default lock o does not give you extra information, until a lock_invariant is specified.

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 or written to. For example, consider the code snippet below. It is similar to the previous example, with the addition of an increment method:

lock_invariant Perm(f, write);
class C {
    int f;

    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.

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:

lock_invariant Perm(f, write);
class C {
    int f;

    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.

commit statement

Before a lock can be locked, it must be initialized. In VerCors, a lock is initialized when it is "committed". This is done using the commit e; statement. The lock must be committed before the end of the constructor. After any commit e; statement, the expression committed(e) is guaranteed to be true.

In the following example, the lock invariant of C requires permission for the field f, and that f has value 3. The constructor writes 3 to f, and then commits the invariant. This ensures that the tryLock method can lock on a newly created object of type C. Without the commit statement, an error would occur. In addition, the postcondition contains committed(this), to indicate that after the constructor the new object is lockable.

lock_invariant Perm(f, 1) ** f == 3;
class C {
  int f;

  ensures committed(this);
  constructor() {
    f = 3;
    commit this;
    assert committed(this);
  }
}

void tryLock() {
  C c = new C();
  lock c;
  assert Perm(c.f, 1) ** c.f == 3;
}

Built-in lock: caveats

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

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 built-in 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 built-in 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:

//@ lock_invariant true;
class C  {
    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

VerCors supports Java's syntax for synchronized blocks. The syntax is as follows:

synchronized(expr) {
    // ...
}

Note the similarity to the atomic block statement. The only requirement is that expr is non-null and of type class. If no lock invariant is specified on the class, the default invariant true will be used.

The only additional behaviour of the synchronized expr is that it accounts for exceptions. That is, when an exception is thrown before the end of the synchronized block, the lock is still closed, and hence the lock invariant still needs to be re-established.

Caveats

There are some caveats to verifying Java locks in VerCors.

Avoid: locking in the constructor

Similar to PVL, VerCors does not allow locking on an object before the lock invariant is established. However, VerCors does not check for this, so the user must manually ensure that this does not occur.

Avoid: locking on an object twice

Similar to PVL, VerCors models Java's locks as single-entrant locks. This is inaccurate, as Java's locks are actually re-entrant. We are working on improving this, but this is currently not yet implemented. Therefore, users have to take care that locking twice on a single object does not occur. If it does occur, it might cause unsoundness.

Avoid: deadlocking interleavings

Some interleaving of synchronized locking sequences might deadlock. VerCors does not warn, nor check for this. Therefore, it is the user's responsibility to ensure that this does not occur.

Home

Tutorial

Developing for VerCors

Clone this wiki locally