Actors may synchronize, safely! *

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 allow the implicit synchronization on the availability of some value (where the producer of the value might be decided at runtime), whereas previous work allowed only explicit synchronization on the termination of a well-identified request. 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.
Type de document :
Communication dans un congrès
PPDP 2016 18th International Symposium on Principles and Practice of Declarative Programming , Sep 2016, Edinburgh, United Kingdom
Liste complète des métadonnées


https://hal.inria.fr/hal-01345315
Contributeur : Elena Giachino <>
Soumis le : mercredi 13 juillet 2016 - 14:45:09
Dernière modification le : jeudi 14 juillet 2016 - 01:04:40

Fichier

gASP-FULL.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01345315, version 1

Collections

Citation

Elena Giachino, Ludovic Henrio, Cosimo Laneve, Vincenzo Mastandrea. Actors may synchronize, safely! *. PPDP 2016 18th International Symposium on Principles and Practice of Declarative Programming , Sep 2016, Edinburgh, United Kingdom. <hal-01345315>

Partager

Métriques

Consultations de
la notice

249

Téléchargements du document

173