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.
Giachino, E., Henrio, L., Laneve, C., Mastandrea, V. (2016). Actors may synchronize, safely!. Association for Computing Machinery, Inc [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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
