Verification of Shared-Reading Synchronisers
This work addresses the verification of synchronisation classes for developers of concurrent software, representing an incremental extension of existing techniques to include shared-reading synchronisers.
The paper tackles the problem of verifying implementations of both exclusive access and shared-reading synchronisers in concurrent programs, using permission-based Separation Logic and a specification for AtomicInteger, and demonstrates its applicability by mechanically verifying implementations of Semaphore, CountDownLatch, and Lock.
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.