Verification of Shared-Reading Synchronisers

TL;DR

This paper introduces a verification technique for shared-reading synchronisers using permission-based Separation Logic, enabling formal reasoning about their correctness in concurrent Java programs.

Contribution

It extends existing methods to verify both exclusive and shared-reading synchronisers, based on specifications for AtomicInteger and applied to real Java concurrency classes.

Findings

Successfully verified Semaphore, CountDownLatch, and Lock implementations.

Demonstrated applicability to real-world Java synchronisation classes.

Enhanced formal reasoning for shared-reading synchronisers.

Abstract

Synchronisation classes are an important building block for shared memory concurrent programs. Thus to reason about such programs, it is important to be able to verify the implementation of these synchronisation classes, considering atomic operations as the synchronisation primitives on which the implementations are built. For synchronisation classes controlling exclusive access to a shared resource, such as locks, a technique has been proposed to reason about their behaviour. This paper proposes a technique to verify implementations of both exclusive access and shared-reading synchronisers. We use permission-based Separation Logic to describe the behaviour of the main atomic operations, and the basis for our technique is formed by a specification for class AtomicInteger, which is commonly used to implement synchronisation classes in java.util.concurrent. To demonstrate the applicability of our approach, we mechanically verify the implementation of various synchronisation classes like Semaphore, CountDownLatch and Lock.