introduction.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
\use_default_options true
\begin_modules
fixltx2e
fix-cm
theorems-ams-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 "default" "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 single
\use_hyperref false
\papersize default
\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 2
\paperpagestyle default
\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 Chapter
Introduction
\end_layout

\begin_layout Standard
With the end of the free-lunch era of ever increasing single-core performance,
 parallel computing has become a mainstream requirement.
 The multi-core era requires high-performance programs to be highly parallel:
 Moore's law is still holding, but the increase in transistor count is resulting
 in an increasing number of cores rather than faster individual cores.
\end_layout

\begin_layout Standard
To borrow the terminology of distributed computing, this shift, from 
\emph on
scaling-up 
\emph default
processor performance to 
\emph on
scaling-out 
\emph default
processors for overall system performance, has been problematic for software
 developers.
 Algorithms and patterns that were efficient on single-core or small core-count
 machines may become inefficient when asked to scale-out further, much as
 patterns that are efficient on a single node may be infeasible in a distributed
 context.
 The comparison with distributed computing is particularly apt in that cores
 on a single node share hardware resources, such as memory, via message
 passing.
 In effect, a multi- or many-core node can be considered as a distributed
 system with fast transport links.
\end_layout

\begin_layout Standard
In this context, a programming language that draws from approaches that
 may have been viewed as more suited for distributed systems, such as the
 actor-model and capabilities security, can be designed to scale efficiently
 as single-node core counts increase.
 This thesis introduces Pony, a programming language designed for this purpose.
 Pony is an actor-model, capabilities secure language, that allows the user
 to easily write fast, safe, parallel programs.
\end_layout

\begin_layout Standard
\begin_inset Float figure
wide false
sideways false
status open

\begin_layout Plain Layout
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

actor Main
\end_layout

\begin_layout Plain Layout

  new create(env: Env) =>
\end_layout

\begin_layout Plain Layout

    env.out.print("Hello, world.") 
\end_layout

\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset Caption Standard

\begin_layout Plain Layout
\begin_inset Quotes eld
\end_inset

Hello, world.
\begin_inset Quotes erd
\end_inset

 implemented in Pony.
\end_layout

\end_inset


\end_layout

\begin_layout Plain Layout

\end_layout

\end_inset


\end_layout

\begin_layout Standard
Pony uses 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 Section
Motivation
\end_layout

\begin_layout Standard
Pony is a product of my own frustration with the tools available to me.
 I have spent much of my professional career writing, or managing programmers
 that were writing, concurrent code in systems programming languages, primarily
 multi-threaded C/C++.
 Over and over again, we ran into memory errors.
 There were of course the usual problems with dangling pointers and memory
 leaks that garbage collectors are designed to solve, but the problems that
 consumed the most time and effort in debugging, or required more fundamental
 architecture changes, were problems with data-races and causality.
 Programmers would think about program architecture in terms of ownership
 and sharing between concurrent units of execution, but, without tooling
 support, enforcing this discipline was extremely difficult.
\end_layout

\begin_layout Standard
The motivation for using multi-threaded C/C++ was peformance, and so moving
 to a programming language or library that traded performance for safety
 was problematic.
 In the early 2000s, I developed a flight simulator engine written in C/C++
 that used Lua as an extension language, integrating the Lua garbage collector
 with C++ reference counting.
 I built an asynchronous message queuing system for doing physics simulation
 that allowed the physics code to be written in Lua while the solid-body
 integration and graphics code was written in C++.
 This was useful, and allowed more productive development of physics code
 in a safe, garbage collected environment, but it still had problems.
 Message passing required copying data, the Lua code itself was not concurrent,
 and messages were not causally consistent.
 For example, a design flaw in the physics code for calculating the power
 output of an internal combustion engine resulted in the manifold pressure
 being calculated based on how the 
\emph on
future
\emph default
 exhaust velocity drove the turbocharger, which resulted in the total energy
 in the system increasing and the simulation blowing up.
 Once the flaw in the way messages were propagated was discovered, this
 was trivial to fix, but discovering that this was due to a causality violation
 took months of programmer time.
\end_layout

\begin_layout Standard
Similarly difficult problems occured with data-races in a different context.
 In the early 2010s, I ran European electronic trading infrastructure for
 a major investment bank.
 My team developed infrastructure code for low-latency (a few microseconds)
 high-throughput (hundreds of thousands of messages per second) applications.
 To support this, I wrote a library for writing actors in C/C++.
 It supported zero-copy causal messaging, had a work-stealing scheduler,
 and was used to develop and deploy some high-performance applications.
 However, programmers would sometimes send a pointer from one actor to another,
 convinced that they had accounted for ownership or had correctly controlled
 for immutability, and it would turn out that they had not and a data-race
 existed.
 Without enforcement for data-race freedom, these bugs were extremely difficult
 to track down.
 Sometimes programmers would add non-message-passing based synchronisation,
 such as locks or lock-free data structures, to control data-races where
 ownership or sharing discipline had failed.
 This usually resulted in subtle deadlock conditions, which often appeared
 only occasionally and only under high load on production systems, but even
 when such bugs were not encountered (which is not to say they were not
 present) there was a performance cost.
\end_layout

\begin_layout Standard
There are existing languages and tools that would solve some of these problems.
 Clearly, there are many interesting garbage collectors that can provide
 a memory-safe, if not data-race free, programming environment.
 But most come at a cost in the form of a stop-the-world phase or significant
 mutator performance costs.
 Erlang provides an actor-model, data-race free programming environment,
 but it is neither causally consistent, due to allowing pattern matching
 on message queues, nor is the sequential code performance competitive with
 C/C++.
 There are existing data-race free type systems, including type systems
 that provide isolation and immutability, but they are not leveraged by
 a strongly integrated approach to concurrency and garbage collection to
 improve performance.
\end_layout

\begin_layout Section
Co-design
\end_layout

\begin_layout Standard
Designing Pony has involved a tight feedback loop between the type system
 and the runtime.
 We began with runtime requirements, such as no-stop-the-world garbage collectio
n, an efficient work-stealing scheduler, and a lock-free runtime implementation.
 These requirements informed the design of the type system, necessitating
 a data-race free type system with strong aliasing guarantees.
 The existence of a data-race free type system allowed further refinement
 of the runtime, enabling features such as zero-copy message passing across
 per-actor heaps, a more efficient underlying memory allocator, and a zero-copy
 asynchronous I/O model.
\end_layout

\begin_layout Standard
This co-design process has continued as both the type system and the runtime
 have developed, and has been one of the most rewarding aspects of this
 work.
 In the language of participatory design 
\begin_inset CommandInset citation
LatexCommand cite
key "spinuzzi2005methodology"

\end_inset

, neither the type system nor the runtime is an isolated system.
\end_layout

\begin_layout Section
Content and Contribution
\end_layout

\begin_layout Standard
This is an overview of the content of this thesis and the contributions
 made.
\end_layout

\begin_layout Paragraph
Chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Language-Design-Decisions"

\end_inset


\end_layout

\begin_layout Standard
This chapter explains the design decisions made during the development of
 Pony.
 We discuss the decision to build a single model for concurrent and distributed
 execution based on the 
\emph on
introduction requirement 
\emph default

\begin_inset CommandInset citation
LatexCommand cite
key "agha1986actors"

\end_inset

.
 We examine the tools for reasoning and correctness provided by Pony, specifical
ly the use of the novel data-race free type system described in chapter
 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Reference-Capabilities"

\end_inset

, logically atomic behaviours, capabilities-security, and causal messaging.
 We also present some of the decisions made in the interest of performance,
 such as modelling behaviours as methods, exceptions as partial functions,
 the use of a single compilation unit, and maintaining C ABI compatibility.
 Finally, we introduce the development philosophy that has guided us, 
\begin_inset Quotes eld
\end_inset

get-stuff-done
\begin_inset Quotes erd
\end_inset

, with apologies to Richard Gabriel.
\end_layout

\begin_layout Paragraph
Chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Syntax-and-Operational"

\end_inset


\end_layout

\begin_layout Standard
This chapter provides a syntax and operational semantics for Pony, in the
 form of a small-step operational semantics for both concurrent and distributed
 execution.
 A distinction is drawn in the semantics between environments where causal
 order is cheaply guaranteed (i.e.
 shared memory concurrent systems) and environments where only pairwise
 FIFO ordering can be cheaply guaranteed (i.e.
 distributed systems).
\end_layout

\begin_layout Standard

\emph on
Contribution: 
\emph default
a unified actor-model operational semantics for concurrent and distributed
 execution.
\end_layout

\begin_layout Paragraph
Chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Reference-Capabilities"

\end_inset


\end_layout

\begin_layout Standard
In this chapter, we develop the concept of 
\emph on
reference capabilities
\emph default
, a novel approach to static data-race freedom based on a matrix of 
\emph on
deny properties
\emph default
.
 The concepts of 
\emph on
aliased and unaliased types
\emph default
, 
\emph on
viewpoint adaptation
\emph default
, 
\emph on
safe-to-write
\emph default
, 
\emph on
capability recovery
\emph default
, and 
\emph on
capability compatibility
\emph default
 are introduced.
 The type system is explained both formally and informally, including descriptio
ns of well-formedness and consistent heap visibility, requiring an interesting
 treatment of 
\emph on
temporary 
\emph default
(i.e.
 unnamed) values, and a proof of soundness is provided.
\end_layout

\begin_layout Standard

\emph on
Contribution: 
\emph default
a novel type system for data-race freedom based on 
\emph on
reference capabilities
\emph default
, wherein concepts such as isolation and immutability are derived rather
 than fundamental, the use of 
\emph on
aliased and unaliased types
\emph default
, and the formalisation and proof of soundness.
\end_layout

\begin_layout Paragraph
Chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Actor-Collection"

\end_inset


\end_layout

\begin_layout Standard
This chapter details 
\emph on
MAC
\emph default
: message-based actor collection, a high-performance no-stop-the-world protocol
 for garbage collecting actors.
 The operational semantics from chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Syntax-and-Operational"

\end_inset

 is extended to express a formal model of 
\emph on
MAC
\emph default
.
 Completeness and robustness are discussed, as well as modifications that
 would allow 
\emph on
MAC
\emph default
 to collect distributed actors.
\end_layout

\begin_layout Standard

\emph on
Contribution: 
\emph default
a novel no-stop-the-world garbage collection algorithm for actors and its
 formalisation.
\end_layout

\begin_layout Paragraph
Chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Object-Collection"

\end_inset


\end_layout

\begin_layout Standard
In this chapter, the 
\emph on
MAC
\emph default
 algorithm from chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Actor-Collection"

\end_inset

 is used as a basis for 
\emph on
ORCA
\emph default
: ownership and reference counting for actors, a no-stop-the-world garbage
 collection protocol for passive objects that allows actors to communicate
 using zero-copy message passing for both mutable and immutable messages.
 The formal model in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Actor-Collection"

\end_inset

 is extended to cover passive object collection, and completeness, robustness,
 and distribution are discussed.
\end_layout

\begin_layout Standard

\emph on
Contribution:
\emph default
 a novel no-stop-the-world garbage collection algorithm for zero-copy message
 passing and its formalisation.
\end_layout

\begin_layout Paragraph
Chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Evaluation-and-Further"

\end_inset


\end_layout

\begin_layout Standard
This chapter concludes the thesis, and provides a brief summary of some
 of the opportunities for further work.
\end_layout

\begin_layout Paragraph
Appendix 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Runtime-Implementation"

\end_inset


\end_layout

\begin_layout Standard
This chapter offers a detailed description and explanation of the implementation
 of the runtime library.
 Topics covered include the memory allocator, size-classed per-actor heaps,
 message queues, actors, the tracing garbage collector, the cross-actor
 garbage collector, the actor garbage collector and cycle detector, finalisation
, the work-stealing scheduler, and asynchronous I/O.
\end_layout

\begin_layout Standard

\emph on
Contribution:
\emph default
 a complete runtime implementation.
\end_layout

\end_body
\end_document