Soundness of a concurrent collector for actors (extended version)
File(s)DTRS18-1.pdf (1.54 MB)
Published version
Author(s)
Franco, Juliana
Clebsch, Sylvan
Drossopoulou, Sophia
Vitek, Jan
Wrigstad, Tobias
Type
Report
Abstract
ORCA is a garbage collection protocol for actor-based programs.
Multiple actors may mutate the heap while the collector is running
without any dedicated synchronisation. ORCA is applicable to any
actor language whose type system prevents data races and which supports
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.
Multiple actors may mutate the heap while the collector is running
without any dedicated synchronisation. ORCA is applicable to any
actor language whose type system prevents data races and which supports
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-01-01
Citation
Departmental Technical Report: 18/1, 2018, pp.1-42
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
42
Journal / Book Title
Departmental Technical Report: 18/1
Copyright Statement
© 2018 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published