%0 Conference Proceedings
%T Simple Isolation for an Actor Abstract Machine
%+ The MathWorks
%+ Mentor Graphics
%+ Sound Programming of Adaptive Dependable Embedded Systems (SPADES)
%A Claudel, Benoit
%A Sabah, Quentin
%A Stefani, Jean-Bernard
%Z Part 5: Efficient Verification Techniques
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 35th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Grenoble, France
%Y Susanne Graf
%Y Mahesh Viswanathan
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-9039
%P 213-227
%8 2015-06-02
%D 2015
%R 10.1007/978-3-319-19195-9_14
%K Virtual Machine
%K Message Passing
%K Object Graph
%K Call Graph
%K Reduction Semantic
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01767336/document
%2 https://inria.hal.science/hal-01767336/file/978-3-319-19195-9_14_Chapter.pdf
%L hal-01767336
%U https://inria.hal.science/hal-01767336
%~ UGA
%~ CNRS
%~ INRIA
%~ UNIV-GRENOBLE1
%~ UNIV-PMF_GRENOBLE
%~ INPG
%~ INRIA-RHA
%~ LIG
%~ INRIA_TEST
%~ TESTALAIN1
%~ IFIP-LNCS
%~ IFIP
%~ INRIA2
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ LIG-MFML-SPADES
%~ IFIP-FORTE
%~ INRIA-RENGRE
%~ IFIP-LNCS-9039
%~ LIG_SIDCH
%~ INRIA-ALLEMAGNE