Verification of Shared-Reading Synchronisers

Afshin Amighi, Marieke Huisman, Stefan Blom

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

48 Downloads (Pure)

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.

Original languageEnglish
Title of host publicationProceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (Metrid)
EditorsSaddek Bensalem, Simon Bliudze
Pages107-120
Number of pages14
DOIs
Publication statusPublished - 25 Jun 2018
Event1st International Workshop on Methods and Tools for Rigorous System Design 2018 - Thessaloniki, Greece
Duration: 15 Apr 201815 Apr 2018
Conference number: 1
https://project.inria.fr/metrid2018/programme/

Publication series

NameElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume272
ISSN (Print)2075-2180

Workshop

Workshop1st International Workshop on Methods and Tools for Rigorous System Design 2018
Abbreviated titleMeTRiD 2018
CountryGreece
CityThessaloniki
Period15/04/1815/04/18
Internet address

Fingerprint

Synchronization
Specifications
Data storage equipment

Cite this

Amighi, A., Huisman, M., & Blom, S. (2018). Verification of Shared-Reading Synchronisers. In S. Bensalem, & S. Bliudze (Eds.), Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (Metrid) (pp. 107-120). (Electronic Proceedings in Theoretical Computer Science, EPTCS; Vol. 272). https://doi.org/10.4204/EPTCS.272.9
Amighi, Afshin ; Huisman, Marieke ; Blom, Stefan. / Verification of Shared-Reading Synchronisers. Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (Metrid). editor / Saddek Bensalem ; Simon Bliudze. 2018. pp. 107-120 (Electronic Proceedings in Theoretical Computer Science, EPTCS).
@inproceedings{09855b0bf27041c2a00a5c49ed153d6e,
title = "Verification of 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.",
author = "Afshin Amighi and Marieke Huisman and Stefan Blom",
year = "2018",
month = "6",
day = "25",
doi = "10.4204/EPTCS.272.9",
language = "English",
series = "Electronic Proceedings in Theoretical Computer Science, EPTCS",
pages = "107--120",
editor = "Saddek Bensalem and Simon Bliudze",
booktitle = "Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (Metrid)",

}

Amighi, A, Huisman, M & Blom, S 2018, Verification of Shared-Reading Synchronisers. in S Bensalem & S Bliudze (eds), Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (Metrid). Electronic Proceedings in Theoretical Computer Science, EPTCS, vol. 272, pp. 107-120, 1st International Workshop on Methods and Tools for Rigorous System Design 2018, Thessaloniki, Greece, 15/04/18. https://doi.org/10.4204/EPTCS.272.9

Verification of Shared-Reading Synchronisers. / Amighi, Afshin; Huisman, Marieke; Blom, Stefan.

Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (Metrid). ed. / Saddek Bensalem; Simon Bliudze. 2018. p. 107-120 (Electronic Proceedings in Theoretical Computer Science, EPTCS; Vol. 272).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Verification of Shared-Reading Synchronisers

AU - Amighi, Afshin

AU - Huisman, Marieke

AU - Blom, Stefan

PY - 2018/6/25

Y1 - 2018/6/25

N2 - 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.

AB - 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.

U2 - 10.4204/EPTCS.272.9

DO - 10.4204/EPTCS.272.9

M3 - Conference contribution

T3 - Electronic Proceedings in Theoretical Computer Science, EPTCS

SP - 107

EP - 120

BT - Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (Metrid)

A2 - Bensalem, Saddek

A2 - Bliudze, Simon

ER -

Amighi A, Huisman M, Blom S. Verification of Shared-Reading Synchronisers. In Bensalem S, Bliudze S, editors, Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (Metrid). 2018. p. 107-120. (Electronic Proceedings in Theoretical Computer Science, EPTCS). https://doi.org/10.4204/EPTCS.272.9