thesis.lyx

#LyX 2.2 created this file. For more info see http://www.lyx.org/
\lyxformat 508
\begin_document
\begin_header
\save_transient_properties true
\origin unavailable
\textclass extreport
\begin_preamble
\usepackage{footnote}
\usepackage{colortbl}
\definecolor{writeable}{gray}{1.0}
\definecolor{readable}{gray}{0.8}
\definecolor{opaque}{gray}{0.6}
\definecolor{gray}{gray}{0.5}
\end_preamble
\use_default_options true
\begin_modules
fixltx2e
fix-cm
theorems-ams-bytype
theorems-chap-bytype
\end_modules
\maintain_unincluded_children false
\language british
\language_package default
\inputencoding auto
\fontencoding global
\font_roman "default" "default"
\font_sans "default" "default"
\font_typewriter "courier" "default"
\font_math "auto" "auto"
\font_default_family default
\use_non_tex_fonts false
\font_sc false
\font_osf false
\font_sf_scale 100 100
\font_tt_scale 100 100
\graphics default
\default_output_format default
\output_sync 0
\bibtex_command default
\index_command default
\paperfontsize default
\spacing onehalf
\use_hyperref false
\papersize a4paper
\use_geometry false
\use_package amsmath 1
\use_package amssymb 1
\use_package cancel 1
\use_package esint 1
\use_package mathdots 1
\use_package mathtools 1
\use_package mhchem 1
\use_package stackrel 1
\use_package stmaryrd 1
\use_package undertilde 1
\cite_engine basic
\cite_engine_type default
\biblio_style plain
\use_bibtopic false
\use_indices false
\paperorientation portrait
\suppress_date true
\justification true
\use_refstyle 1
\index Index
\shortcut idx
\color #008000
\end_index
\secnumdepth 3
\tocdepth 1
\paragraph_separation indent
\paragraph_indentation default
\quotes_language english
\papercolumns 1
\papersides 1
\paperpagestyle default
\listings_params "basicstyle={\ttfamily},commentstyle={\itshape\color{lightgray}},keywords={use, actor, class, primitive, struct, trait, interface, var, let, new, be, fun, iso, trn, ref, val, box, tag, recover, consume, null, if, then, else, while, do, for, in, repeat, until, end, try, and, or, xor, typedef, static, const, return},numbers=left,keywordstyle={\bfseries\color{black}},breaklines=true"
\tracking_changes false
\output_changes false
\html_math_output 0
\html_css_as_file 0
\html_be_strict false
\end_header

\begin_body

\begin_layout Standard
\align center
Imperial College London
\begin_inset Newline newline
\end_inset

Department of Computing
\end_layout

\begin_layout Standard
\begin_inset VSpace vfill
\end_inset


\end_layout

\begin_layout Standard
\align center

\series bold
\size huge
Pony: Co-designing a Type System and a Runtime
\end_layout

\begin_layout Standard
\begin_inset VSpace defskip
\end_inset


\end_layout

\begin_layout Standard
\align center
Sylvan W.
 Clebsch
\end_layout

\begin_layout Standard
\align center
October 2017
\end_layout

\begin_layout Standard
\begin_inset VSpace vfill
\end_inset


\end_layout

\begin_layout Standard
\align center
Submitted in part fulfilment of the requirements for the degree of Doctor
 of Philosophy in Computing of Imperial College London and the Diploma of
 Imperial College London
\end_layout

\begin_layout Standard
\begin_inset Newpage newpage
\end_inset


\end_layout

\begin_layout Section*
Declaration
\end_layout

\begin_layout Standard
This thesis and the work presented within are my own, except where acknowledged
 otherwise.
\end_layout

\begin_layout Standard
\align right
Sylvan Clebsch
\end_layout

\begin_layout Standard
\begin_inset VSpace vfill
\end_inset


\end_layout

\begin_layout Standard
The copyright of this thesis rests with the author and is made available
 under a Creative Commons Attribution Non-Commercial No Derivatives licence.
 Researchers are free to copy, distribute or transmit the thesis on the
 condition that they attribute it, that they do not use it for commercial
 purposes and that they do not alter, transform or build upon it.
 For any reuse or redistribution, researchers must make clear to others
 the licence terms of this work.
\end_layout

\begin_layout Section*
Abstract
\end_layout

\begin_layout Standard
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.
\end_layout

\begin_layout Standard
The core type system feature that enables this is 
\emph on
reference capabilities
\emph default
.
 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.
\end_layout

\begin_layout Standard
Properties of the type system and operational semantics, such as 
\emph on
atomic behaviours 
\emph default
and data-race freedom
\emph on
 
\emph default
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 (
\emph on
MAC
\emph default
) 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
 reflect 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.
\end_layout

\begin_layout Standard
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 asynchron
ous messages (zero-copy message passing).
 This is achieved using Ownership and Reference Counting for Actors (
\emph on
ORCA
\emph default
), a protocol derived from 
\emph on
MAC 
\emph default
that allows passive objects shared across 
\emph on
actor-local heaps 
\emph default
to be garbage collected with no stop-the-world step.
\end_layout

\begin_layout Standard
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.
\end_layout

\begin_layout Section*
Acknowledgements
\end_layout

\begin_layout Standard
Although I developed the type system, operational semantics, and garbage
 collector protocols, and implemented the compiler and runtime, many other
 people have contributed to Pony.
 Sophia Drossopoulou, my advisor, has contributed to every part of the formalisa
tion of Pony, especially the proofs, and has literally taught me everything
 I know about formal methods, as well as being a constant source of help
 and inspiration.
 This project could not possibly have happened without her.
 Other key contributors have been Sebastian Blessing (masters thesis on
 distributed Pony), Andy McNeil (implementation work on the compiler), Juliana
 Franco (formalisation of object garbage collection), Luke Cheeseman (value-depe
ndent types), George Steed (formalisation of type expressions), and the
 SLURP group at Imperial College (invaluable feedback and discussion).
 Also of special note are Tobias Wrigstad, Dave Clarke, and the Upscale
 Project, who have bravely used the Pony runtime for their own language,
 Encore.
 Additional special thanks are due to Constantine Goulimis and Justin Fry.
\end_layout

\begin_layout Standard
More recently, the Pony open-source community has been amazing, including
 (in no particular order) Sean Allen, Joe Eli McIlvain, Benoit Vey, Theo
 Butler, Vid Jain, Chuck Blake, Perelandric, Reini Urban, Gordon Tisher,
 Dipin Hora, Jonas Lasauskas, John Mumm, Andy Turley, George Marrows, Darach
 Ennis, Tommy McGuire, Carl Quinn, Malthe Borch, Kevin Cantú, Markus Fix,
 Chris Double, Dan Connolly, and many others.
 I owe them all a beer, and I owe anyone I've failed to mention two beers.
\end_layout

\begin_layout Standard
\begin_inset CommandInset toc
LatexCommand tableofcontents

\end_inset


\end_layout

\begin_layout Standard
\begin_inset FloatList table

\end_inset


\end_layout

\begin_layout Standard
\begin_inset FloatList figure

\end_inset


\end_layout

\begin_layout Standard
\begin_inset CommandInset include
LatexCommand include
filename "introduction.lyx"

\end_inset


\end_layout

\begin_layout Standard
\begin_inset CommandInset include
LatexCommand include
filename "architecture.lyx"

\end_inset


\end_layout

\begin_layout Standard
\begin_inset CommandInset include
LatexCommand include
filename "opsem.lyx"

\end_inset


\end_layout

\begin_layout Standard
\begin_inset CommandInset include
LatexCommand include
filename "refcaps.lyx"

\end_inset


\end_layout

\begin_layout Standard
\begin_inset CommandInset include
LatexCommand include
filename "actorgc.lyx"

\end_inset


\end_layout

\begin_layout Standard
\begin_inset CommandInset include
LatexCommand include
filename "objectgc.lyx"

\end_inset


\end_layout

\begin_layout Standard
\begin_inset CommandInset include
LatexCommand include
filename "furtherwork.lyx"

\end_inset


\end_layout

\begin_layout Standard
\begin_inset CommandInset include
LatexCommand include
filename "implementation.lyx"

\end_inset


\end_layout

\begin_layout Standard
\begin_inset CommandInset bibtex
LatexCommand bibtex
bibfiles "thesis"
options "bibtotoc,plain"

\end_inset


\end_layout

\end_body
\end_document