Correctness of a concurrent object collector for actor languages
File(s)main.pdf (1.44 MB)
Accepted version
Author(s)
Vicente Franco, J
Clebsch, S
Drossopoulou, S
Vitek, J
Wrigstad, T
Type
Conference Paper
Abstract
ORCA
is a garbage collection protocol for actor-based pro-
grams. Multiple actors may mutate the heap while the collector is run-
ning without any dedicated synchronisation.
ORCA
is applicable to any
actor language whose type system prevents data races and which sup-
ports causal message delivery. We present a model of
ORCA
which is
parametric to the host language and its type system. We describe the
interplay between the host language and the collector. We give invariants
preserved by
ORCA
, and prove its soundness and completeness.
is a garbage collection protocol for actor-based pro-
grams. Multiple actors may mutate the heap while the collector is run-
ning without any dedicated synchronisation.
ORCA
is applicable to any
actor language whose type system prevents data races and which sup-
ports causal message delivery. We present a model of
ORCA
which is
parametric to the host language and its type system. We describe the
interplay between the host language and the collector. We give invariants
preserved by
ORCA
, and prove its soundness and completeness.
Date Issued
2018-04-14
Date Acceptance
2017-12-22
Publisher
Springer
Copyright Statement
© 2018 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
Sponsor
Engineering & Physical Science Research Council (EPSRC)
Commission of the European Communities
Description
ORCA
is a garbage collection protocol for actor-based pro-
grams. Multiple actors may mutate the heap while the collector is run-
ning without any dedicated synchronisation.
ORCA
is applicable to any
actor language whose type system prevents data races and which sup-
ports causal message delivery. We present a model of
ORCA
which is
parametric to the host language and its type system. We describe the
interplay between the host language and the collector. We give invariants
preserved by
ORCA
, and prove its soundness and completeness.
is a garbage collection protocol for actor-based pro-
grams. Multiple actors may mutate the heap while the collector is run-
ning without any dedicated synchronisation.
ORCA
is applicable to any
actor language whose type system prevents data races and which sup-
ports causal message delivery. We present a model of
ORCA
which is
parametric to the host language and its type system. We describe the
interplay between the host language and the collector. We give invariants
preserved by
ORCA
, and prove its soundness and completeness.
Grant Number
EP/K011715/1
612985
Source
27th European Symposium on Programming
Publication Status
Accepted
Start Date
2018-04-14
Finish Date
2018-04-20
Coverage Spatial
Thessaloniki, Greece