Simple Isolation for an Actor Abstract Machine - Formal Techniques for Distributed Objects, Components, and Systems
Conference Papers Year : 2015

Simple Isolation for an Actor Abstract Machine

Abstract

The actor model is an old but compelling concurrent programming model in this age of multicore architectures and distributed services. In this paper we study an as yet unexplored region of the actor design space in the context of concurrent object-oriented programming. Specifically, we show that a purely run-time, annotation-free approach to actor state isolation with reference passing of arbitrary object graphs is perfectly viable. In addition, we show, via a formal proof using the Coq proof assistant, that our approach indeed enforces actor isolation.
Fichier principal
Vignette du fichier
978-3-319-19195-9_14_Chapter.pdf (1.15 Mo) Télécharger le fichier
Origin Files produced by the author(s)
Loading...

Dates and versions

hal-01767336 , version 1 (16-04-2018)

Licence

Identifiers

Cite

Benoit Claudel, Quentin Sabah, Jean-Bernard Stefani. Simple Isolation for an Actor Abstract Machine. 35th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2015, Grenoble, France. pp.213-227, ⟨10.1007/978-3-319-19195-9_14⟩. ⟨hal-01767336⟩
215 View
228 Download

Altmetric

Share

More