Formal Specifications for Java's Synchronisation Classes

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

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

    7 Citations (Scopus)
    25 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. 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 languageEnglish
    Title of host publication22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP 2014)
    Place of PublicationPiscataway, NJ
    PublisherIEEE Computer Society
    Pages725-733
    Number of pages9
    ISBN (Electronic)978-1-4799-2729-6
    DOIs
    Publication statusPublished - 12 Feb 2014
    Event22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2014 - Turin, Italy
    Duration: 12 Feb 201414 Feb 2014
    Conference number: 22

    Publication series

    NameProceedings Euromicro International Conference on Parallel, Distributed, and Network-Based Processing
    PublisherIEEE Computer Society
    Volume2014
    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

    Keywords

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

    Cite this

    Amighi, A., Blom, S., Huisman, M., Mostowski, W., & Zaharieva-Stojanovski, M. (2014). Formal Specifications for Java's Synchronisation Classes. In 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP 2014) (pp. 725-733). (Proceedings Euromicro International Conference on Parallel, Distributed, and Network-Based Processing; Vol. 2014). Piscataway, NJ: IEEE Computer Society. https://doi.org/10.1109/PDP.2014.31