We study deadlock detection in an actor model with wait-by-necessity synchronizations, a lightweight technique that synchronizes invocations when the corresponding values are strictly needed. This approach relies on the use of futures that are not given an explicit "Future" type. The approach we adopt explicits the synchronization on futures, and on the availability of some values, instead of the synchronization on the termination of a process existing in previous works. This way we are able to analyse the data-flow synchronization inherent to languages that feature wait-by-necessity. We provide a type-system and a solver inferring the type of a program so that deadlocks can be identified statically. As a consequence we can automatically verify the absence of deadlocks in actor programs with wait-by-necessity synchronizations.

Actors may synchronize, safely! / Giachino, Elena; Henrio, Ludovic; Laneve, Cosimo; Mastandrea, Vincenzo. - STAMPA. - (2016), pp. 118-131. (Intervento presentato al convegno 18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016 tenutosi a Edinburgh, Scotland nel September 05-07, 2016) [10.1145/2967973.2968599].

Actors may synchronize, safely!

GIACHINO, ELENA;LANEVE, COSIMO;MASTANDREA, VINCENZO
2016

Abstract

We study deadlock detection in an actor model with wait-by-necessity synchronizations, a lightweight technique that synchronizes invocations when the corresponding values are strictly needed. This approach relies on the use of futures that are not given an explicit "Future" type. The approach we adopt explicits the synchronization on futures, and on the availability of some values, instead of the synchronization on the termination of a process existing in previous works. This way we are able to analyse the data-flow synchronization inherent to languages that feature wait-by-necessity. We provide a type-system and a solver inferring the type of a program so that deadlocks can be identified statically. As a consequence we can automatically verify the absence of deadlocks in actor programs with wait-by-necessity synchronizations.
2016
Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016
118
131
Actors may synchronize, safely! / Giachino, Elena; Henrio, Ludovic; Laneve, Cosimo; Mastandrea, Vincenzo. - STAMPA. - (2016), pp. 118-131. (Intervento presentato al convegno 18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016 tenutosi a Edinburgh, Scotland nel September 05-07, 2016) [10.1145/2967973.2968599].
Giachino, Elena; Henrio, Ludovic; Laneve, Cosimo; Mastandrea, Vincenzo
File in questo prodotto:
Eventuali allegati, non sono esposti

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/11585/588186
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 9
  • ???jsp.display-item.citation.isi??? 3
social impact