Pony: co-designing a type system and a runtime

• Main Author: Clebsch, Sylvan
• Other Authors: Drossopoulou, Sophia, Eisenbach, Susan
• Format: Doctoral or Postdoctoral Thesis
• Language: unknown
• Published: Imperial College London 2018
• Subjects: Orca
• Online Access: http://hdl.handle.net/10044/1/65656; https://doi.org/10.25560/65656

We have developed a new programming language, called Pony, that allows the user to easily write fast, safe, parallel programs. The focus of this work is using a powerful and novel static type system to guarantee properties of a program in order to eliminate many runtime checks. This includes eliminating all forms of locking, as well as enabling a novel fully concurrent garbage collection protocol for both objects and actors that has no stop-the-world step, while also having no read or write barriers. Essentially, the type system is used to enable not just safer computation but faster computation. The core type system feature that enables this is reference capabilities. These are a system of type annotations that guarantee data-race freedom even in the presence of asynchronous messages that can contain mutable data. Reference capabilities show that concepts such as isolation and immutability can be derived rather than being treated as fundamental. Properties of the type system and operational semantics, such as atomic behaviours and data-race freedom are leveraged to allow actors themselves to be garbage collected when it can be proved they will never again have messages in their queue. Message-based Actor Collection (MAC) achieves this using only message passing, without the need for any other form of thread synchronisation or coordination, using a system of deferred, distributed, weighted reference counting in which reference counts do not re ect the number of reachable paths in a heap. This requires a cycle detection actor to be able to collect isolated cyclic graphs of actors. To do this with no stop-the-world step, a novel and inexpensive CNF-ACK protocol is used to determine that the cycle detector's view of the actor topology was the true actor topology when the cycle was detected. Guaranteeing data-race freedom allows the language to use a novel fully concurrent garbage collection protocol. This protocol allows each actor to collect its own heap independently and concurrently, while still allowing objects to be sent by reference in asynchronous messages (zero-copy message passing). This is achieved using Ownership and Reference Counting for Actors (ORCA), a protocol derived from MAC that allows passive objects shared across actor-local heaps to be garbage collected with no stop-the-world step. Guaranteeing data-race freedom allows the language to use a novel fully concurrent garbage collection protocol. This protocol allows each actor to collect its own heap independently and concurrently, while still allowing objects to be sent by reference in asynchronous messages (zero-copy message passing). This is achieved using Ownership and Reference Counting for Actors (ORCA), a protocol derived from MAC that allows passive objects shared across actor- local heaps to be garbage collected with no stop-the-world step. To validate these ideas, we have written a complete runtime (including a work-stealing scheduler, garbage collector, memory allocator, message queuing, asynchronous I/O, and more) and an ahead-of-time optimising compiler. The language is open source. Open Access