Skip to Main content Skip to Navigation
Conference papers

Simple Isolation for an Actor Abstract Machine

Benoit Claudel 1 Quentin Sabah 2 Jean-Bernard Stefani 3 
3 SPADES - Sound Programming of Adaptive Dependable Embedded Systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
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.
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Monday, April 16, 2018 - 10:19:12 AM
Last modification on : Sunday, June 26, 2022 - 5:04:59 AM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



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⟩



Record views


Files downloads