Formal Specifications for Java's Synchronisation Classes

A. Amighi, Stefan Blom, Marieke Huisman, Wojciech Mostowski, M. Zaharieva

  • 7 Citations

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. Finally, we used the verification tool that we are developing and successfully verified (so far simplified) implementations of all presented synchronisers; the paper discusses the verification of one of them.
Original languageUndefined
Title of host publicationProceedings of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP 2014)
Place of PublicationUSA
PublisherIEEE Computer Society
Pages725-733
Number of pages9
ISBN (Print)1066-6192
DOIs
StatePublished - 12 Feb 2014
Event22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2014 - Turin, Italy

Publication series

NameIEEE Conference Publications
PublisherIEEE Computer Society
ISSN (Print)1066-6192

Conference

Conference22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2014
Abbreviated titlePDP
CountryItaly
CityTurin
Period12/02/1414/02/14

Fingerprint

Synchronization
Application programming interfaces (API)
Semantics
Specifications

Keywords

  • EWI-25447
  • Separation Logic
  • Java
  • Synchronisation
  • METIS-309739
  • Formal verification
  • Formal Specification
  • IR-94099
  • Concurrency

Cite this

Amighi, A., Blom, S., Huisman, M., Mostowski, W., & Zaharieva, M. (2014). Formal Specifications for Java's Synchronisation Classes. In Proceedings of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP 2014) (pp. 725-733). (IEEE Conference Publications). USA: IEEE Computer Society. DOI: 10.1109/PDP.2014.31

Amighi, A.; Blom, Stefan; Huisman, Marieke; Mostowski, Wojciech; Zaharieva, M. / Formal Specifications for Java's Synchronisation Classes.

Proceedings of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP 2014). USA : IEEE Computer Society, 2014. p. 725-733 (IEEE Conference Publications).

Research output: Scientific - peer-reviewConference contribution

@inbook{7868558e346e4124b1175a4406fd1c87,
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. Finally, we used the verification tool that we are developing and successfully verified (so far simplified) implementations of all presented synchronisers; the paper discusses the verification of one of them.",
keywords = "EWI-25447, Separation Logic, Java, Synchronisation, METIS-309739, Formal verification, Formal Specification, IR-94099, Concurrency",
author = "A. Amighi and Stefan Blom and Marieke Huisman and Wojciech Mostowski and M. Zaharieva",
note = "eemcs-eprint-25447",
year = "2014",
month = "2",
doi = "10.1109/PDP.2014.31",
isbn = "1066-6192",
series = "IEEE Conference Publications",
publisher = "IEEE Computer Society",
pages = "725--733",
booktitle = "Proceedings of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP 2014)",
address = "United States",

}

Amighi, A, Blom, S, Huisman, M, Mostowski, W & Zaharieva, M 2014, Formal Specifications for Java's Synchronisation Classes. in Proceedings of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP 2014). IEEE Conference Publications, IEEE Computer Society, USA, pp. 725-733, 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2014, Turin, Italy, 12-14 February. DOI: 10.1109/PDP.2014.31

Formal Specifications for Java's Synchronisation Classes. / Amighi, A.; Blom, Stefan; Huisman, Marieke; Mostowski, Wojciech; Zaharieva, M.

Proceedings of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP 2014). USA : IEEE Computer Society, 2014. p. 725-733 (IEEE Conference Publications).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Formal Specifications for Java's Synchronisation Classes

AU - Amighi,A.

AU - Blom,Stefan

AU - Huisman,Marieke

AU - Mostowski,Wojciech

AU - Zaharieva,M.

N1 - eemcs-eprint-25447

PY - 2014/2/12

Y1 - 2014/2/12

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. Finally, we used the verification tool that we are developing and successfully verified (so far simplified) 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. Finally, we used the verification tool that we are developing and successfully verified (so far simplified) implementations of all presented synchronisers; the paper discusses the verification of one of them.

KW - EWI-25447

KW - Separation Logic

KW - Java

KW - Synchronisation

KW - METIS-309739

KW - Formal verification

KW - Formal Specification

KW - IR-94099

KW - Concurrency

U2 - 10.1109/PDP.2014.31

DO - 10.1109/PDP.2014.31

M3 - Conference contribution

SN - 1066-6192

T3 - IEEE Conference Publications

SP - 725

EP - 733

BT - Proceedings of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP 2014)

PB - IEEE Computer Society

ER -

Amighi A, Blom S, Huisman M, Mostowski W, Zaharieva M. Formal Specifications for Java's Synchronisation Classes. In Proceedings of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP 2014). USA: IEEE Computer Society. 2014. p. 725-733. (IEEE Conference Publications). Available from, DOI: 10.1109/PDP.2014.31