Orca is a novel garbage collection protocol for actor-based, object-oriented programming languages for multicore machines. It supports fully concurrent garbage collection, where an actor can trigger garbage collection at any time without synchronising with any other actor. It does so while supporting copy-less message passing and sharing of mutable state. By leveraging a type system’s guarantees of actor isolation, Orca can perform GC fully concurrently, without any form of barrier synchronisation in mutator threads, as commonly found in state-of-the-art concurrent collectors. Although Orca has been successfully implemented in Pony and in Encore, it had never been evaluated nor proven correct. Indeed, these are the two main contributions of this thesis.
In this thesis, we model Orca and prove that it will never collect reachable objects (i.e., execution of programs managed by Orca will never result in dangling pointers) and that it will eventually deallocate all unreachable objects (i.e., execution of programs managed by Orca will never result in memory leaks). We model Orca in three steps: firstly, we define a set of requirements that must be ensured by the host language; secondly, assuming these requirements are in place, we model all the garbage collection related operations atomically; and thirdly, we extend our model to take into consideration that, in fact, in a fully concurrent system every instruction is interleaved with the execution of other operations.
Moreover, we evaluate Orca ’s performance by measuring scalability, footprint, responsiveness and
its overhead in the execution of a program. We perform this evaluation in the context of Pony, the
language with which Orca was co-designed, and compare it against the JVM, BEAM and Boehm-Demers-Weiser.