This paper presents a static analysis technique based on effects and behavioural types for deriving synchronisation patterns of stateful active objects and verifying the absence of deadlocks in this context. This is challenging because active objects use futures to refer to results of pending asynchronous invocations and because these futures can be stored in object fields, passed as method parameters, or returned by invocations. Our effect system traces the access to object fields, thus allowing us to compute behavioural types that express synchronisation patterns in a precise way. The behavioural types are thereafter analysed by a solver that discovers potential deadlocks.
Analysis of synchronisations in stateful active objects / Henrio, Ludovic; Laneve, Cosimo; Mastandrea, Vincenzo. - STAMPA. - 10510:(2017), pp. 195-210. (Intervento presentato al convegno 13th International Conference on Integrated Formal Methods, IFM 2017 tenutosi a Turin, Italy nel September 20-22, 2017) [10.1007/978-3-319-66845-1_13].
Analysis of synchronisations in stateful active objects
Laneve, CosimoMembro del Collaboration Group
;Mastandrea, Vincenzo
Membro del Collaboration Group
2017
Abstract
This paper presents a static analysis technique based on effects and behavioural types for deriving synchronisation patterns of stateful active objects and verifying the absence of deadlocks in this context. This is challenging because active objects use futures to refer to results of pending asynchronous invocations and because these futures can be stored in object fields, passed as method parameters, or returned by invocations. Our effect system traces the access to object fields, thus allowing us to compute behavioural types that express synchronisation patterns in a precise way. The behavioural types are thereafter analysed by a solver that discovers potential deadlocks.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
