Nowadays there is a strong demand for programming frameworks which can help the systems programmers to effectively exploit, in a natural way, the computing potential of modern clusters of multi-core machines. This paper proposes a methodology for the development of concurrent/parallel programs in Java which depends on UPPAAL, for modelling and exhaustive verification of a concurrent system, and the Terracotta middleware for the parallel execution concerns. The use of UPPAAL is assisted by a library of reusable concurrent control structures, which facilitates the derivation of verified Java code. The library is extended in this paper with light-weight semaphores which are without a built-in blocked-queue whilst remaining starvation-free. The approach is demonstrated by an example.

An approach to concurrent/parallel programming in Java

Cicirelli Franco;
2016

Abstract

Nowadays there is a strong demand for programming frameworks which can help the systems programmers to effectively exploit, in a natural way, the computing potential of modern clusters of multi-core machines. This paper proposes a methodology for the development of concurrent/parallel programs in Java which depends on UPPAAL, for modelling and exhaustive verification of a concurrent system, and the Terracotta middleware for the parallel execution concerns. The use of UPPAAL is assisted by a library of reusable concurrent control structures, which facilitates the derivation of verified Java code. The library is extended in this paper with light-weight semaphores which are without a built-in blocked-queue whilst remaining starvation-free. The approach is demonstrated by an example.
2016
Istituto di Calcolo e Reti ad Alte Prestazioni - ICAR
9781467398688
concurrent/parallel programming
Java
light-weight semaphore
Modelling and verification
Terracotta
UPPAAL
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.14243/321053
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact