Specification and Verification of Synchronisation Classes in Java: A Practical Approach

Afshin Amighi

promotor: prof.dr. Marieke Huisman (UT)
University of Twente
Date: 17 January 2018
Thesis: PDF 

Summary

Nowadays, concurrent programming is becoming a mainstream technique to achieve high-performance computing.
Implementing a correct program using shared memory concurrency is challenging. This is because of the unpredictable interleavings of threads that may cause unaccepted access to the shared memory, known as data race.
Programmers use synchronisers to control thread interleaving and prevent data races.
Coarse-grained synchronisation constructs block threads for large parts of execution tasks, while fine-grained synchronisation primitives employ atomic operations.

Using testing techniques to catch possible errors in concurrent programs is not feasible, because the appearance of errors depends on the execution order of the participating threads, which varies in different runs.
And moreover, testing techniques are able only to show the presence of errors.
Formal techniques are needed to guarantee the absence of errors independently from execution environments.
Axiomatic based approaches are one of the common techniques that can verify the correctness of a given program with respect to its specifications without executing the program.
Axiomatic based program verification employs a collection of formal rules that expresses the correct behaviour of the program using a program logic.
Program logic shows how to formally derive correctness of the implementation w.r.t its specification.

Permission-based Separation Logic is a program logic that has been developed to reason about concurrent programs.
In permission-based Separation Logic one can express and reason about the ownership of memory locations.
This is an important and powerful feature of this logic because any data race becomes detectable.
Verification techniques of concurrent programs based on permission-based Separation Logic exploit this feature of the logic to verify that a concurrent program is free from data races.

In this thesis, we propose an approach to specify and verify synchronisation constructs which are at the heart of any concurrent program.
The class of synchronisers that we study here includes both coarse-grained and fine-grained synchronisers.
In our approach we lift formalised rules of permission-based Separation Logic to the specification level.
Our method offers a generalised, high-level and extendable approach to specify and verify arbitrary synchronisation constructs.
Our approach is a practical technique. Using the VERCORS tool set we demonstrate the practicality of our approach by verifying a variety of examples implemented in Java. The VERCORS tool set and all the tool verified examples are available online.

In this thesis, first, we start with the basics of threads communication and synchronisation primitives in Java. As a result, we verify the correctness of a concurrent Java program where threads have multiple join points.
Then, we study the general behaviour of commonly used synchronisation classes in Java. We propose a unified approach to specify the correct behaviour of synchronisers. Concretely, we discuss the formal specification of the synchronisation classes implemented in the java.util.concurrent package.
This enables us to verify the correctness of the concurrent Java programs that are using these synchronisation classes.
Next, in order to verify that the implementation of synchronisers satisfies our specifications we develop techniques to reason about the verification of synchronisers. A common way to implement such sychronisers is by using atomic operations.
We identify different synchronisation patterns that can be implemented by using atomic operations. Moreover, we propose a specification of these operations in Java’s AtomicInteger class, which is an essential class in the implementation of Java’s synchronisers.
We use our specification of the atomic operations to verify the implementation of both exclusive access and shared-reading synchronisation classes developed in java.util.concurrent.

Further to the results of reasoning about atomic operations, we propose a verification stack where several concurrent program verification techniques are combined. In each layer of the stack a particular property of a concurrent program is verified.
In our three layer verification stack, the bottom layer, reasons about data race freedom of programs.
The second layer reasons about properties that ties properties of both thread-local and shared variables.
The top layer adds a notion of histories to reason about functional properties of concurrent data structures.
We illustrate our technique on the verification of a lock-free queue and reentrant lock both implemented in Java.

Finally, we propose a specification and verification technique to reason about data race freedom and functional correctness of GPU kernels that use atomic operations as synchronisation mechanism.

Altogether, the techniques proposed in this thesis are a step forward towards the practical verification of non-trivial Java(-like) concurrent programs that are using either fine-grained or coarse-grained synchronisers. The verified programs are guaranteed to be free from data races and the verification is done with a rich specification language that relies on the rules developed by permission-based Separation Logic.