Title :
Formal Specifications for Java´s Synchronisation Classes
Author :
Amighi, Afshin ; Blom, Stefan ; Huisman, Magda ; Mostowski, Wojciech ; Zaharieva-Stojanovski, Marina
Author_Institution :
Formal Methods & Tools, Univ. of Twente, Enschede, Netherlands
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 :
Java; application program interfaces; concurrency control; formal specification; formal verification; synchronisation; Java API; Java synchronisation class; concurrent program; formal specification; formal veri- fication; permission-based separation logic; primitive operation; synchronisation modular treatment; synchronisation routines behaviour; Abstracts; Cognition; Concurrent computing; Data structures; Java; Permission; Synchronization; Java; Separation Logic; concurrency; formal specification; formal verification; synchronisation;
Conference_Titel :
Parallel, Distributed and Network-Based Processing (PDP), 2014 22nd Euromicro International Conference on
Conference_Location :
Torino
DOI :
10.1109/PDP.2014.31