Modular reasoning about non-blocking concurrent data structures is crucial to establish the correctness of concurrent applications. To achieve this, specifications of the synchronization mechanisms used by these non-blocking concurrent classes to prevent concurrent access to shared data, are essential. This paper presents an approach to specifying such lock-free synchronization mechanisms in terms of the thread's role and permissions. The approach is formalized in a specification for the AtomicInteger class from the java.util.concurrent library, using abstract predicates and permission-based concurrent Separation Logic. The specification is set up to capture different synchronization patterns, both cooperative and competitive. We illustrate the use of the patterns in three case studies, where for each case study we verify that it indeed correctly synchronizes access to the protected data.
|Place of Publication||Enschede|
|Publisher||Centre for Telematics and Information Technology (CTIT)|
|Number of pages||14|
|Publication status||Published - 1 May 2013|
|Name||CTIT Technical Report Series|
|Publisher||University of Twente, Centre for Telematica and Information Technology (CTIT)|
- Separation Logic
- Java volatiles
Amighi, A., Blom, S., & Huisman, M. (2013). Resource protection using atomics: patterns and verifications. (CTIT Technical Report Series; No. TR-CTIT-13-10). Enschede: Centre for Telematics and Information Technology (CTIT).