Formal specifications for Java’s synchronisation classes

Afshin Amighi, Stefan Blom, Marieke Huisman, Wojciech Mostowski, Marina Zaharieva-Stojanovski

Research output: Book/ReportReportProfessional

19 Downloads (Pure)

Abstract

This paper discusses formal specification and verification of the synchronisation classes of the Java API. In many verification systems for concurrent programs, synchronisation is treated as a primitive operation. As a result, verification rules for synchronisation are hard-coded in the logic, and not verified. These rules describe the concrete semantics of the given synchronisation primitive, and manage how resources are protected by synchronisation. In contrast, this paper describes several synchronisation primitives at the specification level, by specifying the behaviour of synchronisation routines from the Java API at method level using permission-based Separation Logic. This gives a generalised, high-level, and easily extendable approach to formalisation of arbitrary synchronisation mechanisms, which allows for modular treatment of synchronisation in verification. Notably, our approach does not only apply to locks, but also to other synchronisation mechanisms such as semaphores and latches that we also discuss in the paper. Finally, we used the verification tool that we are developing and successfully verified (so far simplified) reference implementations of all presented synchronisers; the paper discusses the verification of one of them.
Original languageEnglish
Place of PublicationEnschede
PublisherCentre for Telematics and Information Technology (CTIT)
Number of pages8
Publication statusPublished - 11 Sep 2013

Publication series

NameCTIT Technical Report Series
PublisherUniversity of Twente, Centre for Telematics and Information Technology
No.TR-CTIT-13-18
ISSN (Print)1381-3625

Fingerprint

Synchronization
Application programming interfaces (API)
Formal specification
Semantics
Concretes
Specifications

Keywords

  • Separation logic
  • Synchronisation
  • Concurrency
  • Formal verification
  • Java
  • Formal specification

Cite this

Amighi, A., Blom, S., Huisman, M., Mostowski, W., & Zaharieva-Stojanovski, M. (2013). Formal specifications for Java’s synchronisation classes. (CTIT Technical Report Series; No. TR-CTIT-13-18). Enschede: Centre for Telematics and Information Technology (CTIT).
Amighi, Afshin ; Blom, Stefan ; Huisman, Marieke ; Mostowski, Wojciech ; Zaharieva-Stojanovski, Marina. / Formal specifications for Java’s synchronisation classes. Enschede : Centre for Telematics and Information Technology (CTIT), 2013. 8 p. (CTIT Technical Report Series; TR-CTIT-13-18).
@book{65649145c39b449bafc73e3f87ee2ae3,
title = "Formal specifications for Java’s synchronisation classes",
abstract = "This paper discusses formal specification and verification of the synchronisation classes of the Java API. In many verification systems for concurrent programs, synchronisation is treated as a primitive operation. As a result, verification rules for synchronisation are hard-coded in the logic, and not verified. These rules describe the concrete semantics of the given synchronisation primitive, and manage how resources are protected by synchronisation. In contrast, this paper describes several synchronisation primitives at the specification level, by specifying the behaviour of synchronisation routines from the Java API at method level using permission-based Separation Logic. This gives a generalised, high-level, and easily extendable approach to formalisation of arbitrary synchronisation mechanisms, which allows for modular treatment of synchronisation in verification. Notably, our approach does not only apply to locks, but also to other synchronisation mechanisms such as semaphores and latches that we also discuss in the paper. Finally, we used the verification tool that we are developing and successfully verified (so far simplified) reference implementations of all presented synchronisers; the paper discusses the verification of one of them.",
keywords = "Separation logic, Synchronisation, Concurrency, Formal verification, Java, Formal specification",
author = "Afshin Amighi and Stefan Blom and Marieke Huisman and Wojciech Mostowski and Marina Zaharieva-Stojanovski",
year = "2013",
month = "9",
day = "11",
language = "English",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "TR-CTIT-13-18",
address = "Netherlands",

}

Amighi, A, Blom, S, Huisman, M, Mostowski, W & Zaharieva-Stojanovski, M 2013, Formal specifications for Java’s synchronisation classes. CTIT Technical Report Series, no. TR-CTIT-13-18, Centre for Telematics and Information Technology (CTIT), Enschede.

Formal specifications for Java’s synchronisation classes. / Amighi, Afshin; Blom, Stefan; Huisman, Marieke; Mostowski, Wojciech; Zaharieva-Stojanovski, Marina.

Enschede : Centre for Telematics and Information Technology (CTIT), 2013. 8 p. (CTIT Technical Report Series; No. TR-CTIT-13-18).

Research output: Book/ReportReportProfessional

TY - BOOK

T1 - Formal specifications for Java’s synchronisation classes

AU - Amighi, Afshin

AU - Blom, Stefan

AU - Huisman, Marieke

AU - Mostowski, Wojciech

AU - Zaharieva-Stojanovski, Marina

PY - 2013/9/11

Y1 - 2013/9/11

N2 - This paper discusses formal specification and verification of the synchronisation classes of the Java API. In many verification systems for concurrent programs, synchronisation is treated as a primitive operation. As a result, verification rules for synchronisation are hard-coded in the logic, and not verified. These rules describe the concrete semantics of the given synchronisation primitive, and manage how resources are protected by synchronisation. In contrast, this paper describes several synchronisation primitives at the specification level, by specifying the behaviour of synchronisation routines from the Java API at method level using permission-based Separation Logic. This gives a generalised, high-level, and easily extendable approach to formalisation of arbitrary synchronisation mechanisms, which allows for modular treatment of synchronisation in verification. Notably, our approach does not only apply to locks, but also to other synchronisation mechanisms such as semaphores and latches that we also discuss in the paper. Finally, we used the verification tool that we are developing and successfully verified (so far simplified) reference implementations of all presented synchronisers; the paper discusses the verification of one of them.

AB - This paper discusses formal specification and verification of the synchronisation classes of the Java API. In many verification systems for concurrent programs, synchronisation is treated as a primitive operation. As a result, verification rules for synchronisation are hard-coded in the logic, and not verified. These rules describe the concrete semantics of the given synchronisation primitive, and manage how resources are protected by synchronisation. In contrast, this paper describes several synchronisation primitives at the specification level, by specifying the behaviour of synchronisation routines from the Java API at method level using permission-based Separation Logic. This gives a generalised, high-level, and easily extendable approach to formalisation of arbitrary synchronisation mechanisms, which allows for modular treatment of synchronisation in verification. Notably, our approach does not only apply to locks, but also to other synchronisation mechanisms such as semaphores and latches that we also discuss in the paper. Finally, we used the verification tool that we are developing and successfully verified (so far simplified) reference implementations of all presented synchronisers; the paper discusses the verification of one of them.

KW - Separation logic

KW - Synchronisation

KW - Concurrency

KW - Formal verification

KW - Java

KW - Formal specification

M3 - Report

T3 - CTIT Technical Report Series

BT - Formal specifications for Java’s synchronisation classes

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -

Amighi A, Blom S, Huisman M, Mostowski W, Zaharieva-Stojanovski M. Formal specifications for Java’s synchronisation classes. Enschede: Centre for Telematics and Information Technology (CTIT), 2013. 8 p. (CTIT Technical Report Series; TR-CTIT-13-18).