Verification of Shared-Reading Synchronisers

Afshin Amighi
(Hogeschool Rotterdam)
Marieke Huisman
(University of Twente)
Stefan Blom
(Better Be)

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.

In Simon Bliudze and Saddek Bensalem: Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (MeTRiD 2018), Thessaloniki, Greece, 15th April 2018, Electronic Proceedings in Theoretical Computer Science 272, pp. 107–120.
Published: 25th June 2018.

ArXived at: http://dx.doi.org/10.4204/EPTCS.272.9 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org