architecture.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
\begin_inset CommandInset label
LatexCommand label
name "chap:Language-Design-Decisions"

\end_inset

Language Design Decisions
\end_layout

\begin_layout Standard
Pony is a language predicated on the idea that a sufficiently powerful static
 type system can be leveraged to write a faster runtime.
 In particular, such a type system could make guarantees that result in
 eliminating many dynamic checks, not just related to dynamically checking
 data types, but also eliminating checks that would otherwise be required
 for safe concurrency, garbage collection, and security.
\end_layout

\begin_layout Section
\begin_inset CommandInset label
LatexCommand label
name "sec:Single-Model-for"

\end_inset

Single Model for Concurrent and Distributed Execution
\end_layout

\begin_layout Standard
One of the driving principles behind the design of Pony has been the desire
 for a single model for both concurrent and distributed execution, as described
 in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Syntax-and-Operational"

\end_inset

.
 As a result, the communication mechanism between units of execution cannot
 rely on shared mutable state, since such shared memory is not available
 in a distributed setting.
 In addition, the communication mechanism cannot be synchronous, as relying
 on synchronous communication in a distributed context can introduce severe
 performance problems.
 These are also important considerations when ensuring that maximum use
 is made of the hardware available on a single node.
 For example, synchronous messaging can introduce deadlocks and priority
 inversion, and shared mutable state can cause data races and put a heavy
 load on cache coherency hardware.
\end_layout

\begin_layout Standard
This is a different approach than languages such as C/C++, C#, Java, Javascript,
 Python, and other languages that treat both concurrency and distribution
 as library-level rather than language-level features.
 Such languages are in some sense sequential-first.
 Pony instead takes a concurrent-first approach that is more in the style
 of Erlang, in which concurrency and distribution are language-level features
 that inform the design of the sequential portion of the language.
 As such, problems endemic to sequential-first languages when concurrency
 is introduced, such as non-composable concurrent libraries, garbage collectors
 that must cope with shared mutable state, deadlocking, and data-races,
 are avoided by design.
\end_layout

\begin_layout Standard
Like Erlang, Pony uses asynchronous message passing for communicating between
 units of execution.
 This decision, combined with a desire to provide dynamic topology and object
 capabilities, lead to the decision to use actors as the unit of execution.
 The actor model has been implemented in many ways, but at its core it has
 three fundamental requirements 
\begin_inset CommandInset citation
LatexCommand cite
key "agha1986actors,agha1987concurrent"

\end_inset

:
\end_layout

\begin_layout Enumerate
An actor can send messages to other actors or itself.
\end_layout

\begin_layout Enumerate
An actor can create new actors.
\end_layout

\begin_layout Enumerate
An actor can choose the way in which it will respond to the next message
 it receives.
\end_layout

\begin_layout Standard
These requirements are intentionally weak.
 For example, while the model does require that messages are eventually
 delivered, it does not require a delivery order.
 Similarly, while the third requirement allows actors to encode state, the
 model does not require an implementation to encode state in any particular
 way.
 For example, encoding state via recursion or via mutating object fields
 are both allowable strategies.
\end_layout

\begin_layout Standard
On the other hand, there are subtle implications of these three requirements.
 For example, since an actor can send a message to itself, and message delivery
 is guaranteed, messages must be buffered, as otherwise an actor would deadlock
 when attempting to send itself a message.
 Interestingly, while real world constraints limit the size of a message
 buffer, the model implicitly requires that buffer space is logically unbounded:
 any upper bound devolves to the possibility that an actor will be blocked
 if it tries to send a message to itself, because its message buffer is
 full and it cannot clear it.
 That is, the actor can neither enqueue the message and continue execution,
 nor can it dequeue messages to create space, as the actor must not interleave
 message handling executions.
\end_layout

\begin_layout Standard
Another subtle implication is that there can be no shared mutable state
 across actors.
 This follows from the requirement that an actor 
\begin_inset Formula $\alpha$
\end_inset

 can only send a message to another actor 
\begin_inset Formula $\alpha'$
\end_inset

 in response to some message 
\begin_inset Formula $m$
\end_inset

 if:
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\alpha'$
\end_inset

 was known to 
\begin_inset Formula $\alpha$
\end_inset

 before 
\begin_inset Formula $m$
\end_inset

 was received, or
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\alpha'$
\end_inset

 is contained in 
\begin_inset Formula $m$
\end_inset

, or
\end_layout

\begin_layout Enumerate
\begin_inset Formula $\alpha$
\end_inset

 created 
\begin_inset Formula $\alpha'$
\end_inset

 while handling 
\begin_inset Formula $m$
\end_inset

.
\end_layout

\begin_layout Standard
This is the 
\emph on
introduction requirement
\emph default
, as detailed in Gul Agha's Ph.D.
 thesis 
\begin_inset CommandInset citation
LatexCommand cite
key "agha1986actors"

\end_inset

: an actor 
\begin_inset Formula $\alpha$
\end_inset

 can only send a message to another actor 
\begin_inset Formula $\alpha'$
\end_inset

 if they have been properly introduced.
 Shared mutable state would allow an actor to send messages without prior
 introduction: namely, 
\begin_inset Formula $\alpha$
\end_inset

 could read the address of 
\begin_inset Formula $\alpha'$
\end_inset

 from some shared variable that a third-party actor modified, without 
\begin_inset Formula $\alpha$
\end_inset

 either receiving 
\begin_inset Formula $\alpha'$
\end_inset

 in a message or creating 
\begin_inset Formula $\alpha'$
\end_inset

.
\end_layout

\begin_layout Standard
The implementation of the actor model in Pony is intended to satisfy all
 of these aspects of the actor model, including the more subtle implications.
\end_layout

\begin_layout Section
Tools for Correctness and Reasoning
\end_layout

\begin_layout Standard
Pony makes additional guarantees that extend the fundamental requirements
 of the actor model:
\end_layout

\begin_layout Enumerate
Both mutable and immutable state are supported, both within an actor and
 in messages between actors, as described in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Reference-Capabilities"

\end_inset

.
\end_layout

\begin_layout Enumerate
Data-race freedom, including mutable state isolation, is guaranteed statically,
 as described in section 
\begin_inset CommandInset ref
LatexCommand ref
reference "subsec:Static-Data-Race-Freedom"

\end_inset

 and chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Reference-Capabilities"

\end_inset

.
\end_layout

\begin_layout Enumerate
Message handling is 
\emph on
logically atomic
\emph default
, as described in section 
\begin_inset CommandInset ref
LatexCommand ref
reference "subsec:Logically-Atomic-Behaviours"

\end_inset

 and chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Reference-Capabilities"

\end_inset

.
\end_layout

\begin_layout Enumerate
The language is 
\emph on
capabilities secure
\emph default
, as described in section 
\begin_inset CommandInset ref
LatexCommand ref
reference "subsec:Capabilities-Security"

\end_inset

 and chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Reference-Capabilities"

\end_inset

.
\end_layout

\begin_layout Enumerate
Within a node, message delivery is 
\emph on
causal
\emph default
, and across nodes, message delivery is pairwise FIFO ordered, and can be
 made optionally 
\emph on
causal
\emph default
, as described in section 
\begin_inset CommandInset ref
LatexCommand ref
reference "subsec:Causal-Messaging"

\end_inset

 and chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Syntax-and-Operational"

\end_inset

.
\end_layout

\begin_layout Enumerate
Both actors and objects are garbage collected without requiring coordination
 outside of the underlying message passing system, as described in section
 
\begin_inset CommandInset ref
LatexCommand ref
reference "subsec:Message-based-Garbage-Collection"

\end_inset

 and chapters 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Actor-Collection"

\end_inset

 and 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Object-Collection"

\end_inset

.
\end_layout

\begin_layout Enumerate
Within a node, messages are 
\emph on
zero-copy
\emph default
, as described in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Object-Collection"

\end_inset

.
\end_layout

\begin_layout Standard
Each of these guarantees is made possible due to the interaction between
 the type system and the runtime.
 In some cases this interaction is obvious, such as the semantics of the
 language providing no global variables, which is important for capabilities
 security, and in other cases it is more subtle, such as data-race freedom
 being important for logically atomic message handling, which is in turn
 important for both causal messaging and garbage collection.
\end_layout

\begin_layout Standard
It is important to note that, while Pony makes some guarantees that are
 useful for ensuring correctness and reasoning about programs, Pony is not
 a tool for formal verification, nor is the implementation of the runtime
 itself formally verified.
 It would be extremely interesting to apply techniques used in formal verificati
on tools, such as Dafny and F*, to allow Pony to function as its own proof
 assistant, and to implement a formally verified runtime (perhaps using
 an extended Pony that provides for formal verification), but that must
 be left for future work.
\end_layout

\begin_layout Subsection
\begin_inset CommandInset label
LatexCommand label
name "subsec:Static-Data-Race-Freedom"

\end_inset

Static Data-Race Freedom
\end_layout

\begin_layout Standard
If the type system can statically ensure data-race freedom, the runtime
 and every program written in the language need not contain dynamic locking
 mechanisms.
 This is a significant performance gain, and the impact is felt not just
 in computational performance, but, as we will see later, also in parallel
 scalability and garbage collection.
\end_layout

\begin_layout Standard
To ensure data-race free concurrent execution, it is sufficient to enforce
 a single principle: if a unit of execution (whether it is a thread, a process,
 or any other implementation) can write to a data structure, no other unit
 of execution can read from that data structure.
 This has a natural corollary: if a unit of execution can read from a data
 structure, no other unit of execution can write to that data structure.
\end_layout

\begin_layout Standard
Enforcing this property on individual memory locations, as opposed to complete
 data structures, is insufficient, as it could result in the data structure
 as a whole being inconsistent, even though the individual reads and writes
 were safe.
 For example, a data structure comprised of a linked list and a count of
 the number of nodes in the list cannot be safely updated by controlling
 access to individual memory locations: either the count or the list itself
 would have to be changed first, resulting in a period where the count does
 not accurately reflect the number of nodes in the list.
\end_layout

\begin_layout Standard
As a result, in order to enforce this property dynamically, access to a
 data structure must be controlled with some form of runtime locking mechanism.
 For example, the counted linked list could also include a mutex that must
 be acquired in order to read from or write to the data structure.
 However, this does not address safe access to the contents of the list
 nodes.
 If two units of execution each read the first element of the list, two
 threads now have access to the same contained data.
 In order to make the list as a whole data-race safe, every data element
 that could be put in the list must also be protected by a mutex.
 This problem is recursive: the data elements themselves may contain references
 to data structures that must also be lockable.
\end_layout

\begin_layout Standard
This is the fine-grained locking problem.
 There are many approaches to mitigating this problem, particularly in database
 research.
 The most common approach is to rely on a programer's domain knowledge to
 correctly guess what the minimum level of locking is to ensure correct
 behaviour.
 However, all of these approaches are domain specific, are subject to programmin
g errors, and rely on locking mechanisms that are expensive on shared memory
 systems and prohibitive in distributed systems.
\end_layout

\begin_layout Standard
A type system that allows only immutable data types solves the data-race
 problem by disallowing all mutation.
 This is an approach favoured by functional programming languages.
 Since no unit of execution can write to the data structure, it is trivial
 to guarantee without dynamic checks that the program is data-race free.
 However, some algorithms are faster to compute or easier to implement over
 mutable data structures than immutable ones.
 As such, a type system that can express data-race free mutable data types
 might offer advantages over a type system that can express only immutable
 data types.
\end_layout

\begin_layout Standard
Purely static data-race free mutability has been expressed several ways,
 including via ownership types, fractional permissions, and uniqueness and
 immutability type systems.
 In Pony, the type system incorporates 
\emph on
deny capabilities
\emph default
, expressed as 
\emph on
reference 
\emph default
capabilities
\emph on
.
 
\emph default
Deny capabilities are a form of uniqueness and immutability type system
 influenced by both 
\emph on
object capabilities 
\begin_inset CommandInset citation
LatexCommand cite
key "miller2003capability"

\end_inset


\emph default
 and 
\emph on
deny guarantee reasoning
\emph default
 
\begin_inset CommandInset citation
LatexCommand cite
key "dodds2009deny"

\end_inset

.
\end_layout

\begin_layout Standard
Deny capabilities describe what other aliases are 
\emph on
denied
\emph default
 by the existence of a reference.
 Furthermore, they distinguish between what is denied 
\emph on
locally 
\emph default
(i.e.
 aliases reachable via the same actor) and what is denied 
\emph on
globally
\emph default
 (i.e.
 aliases reachable via other actors).
 The result is a matrix of 
\emph on
deny properties
\emph default
, with notions such as isolation, mutability, and immutability all being
 derived from these deny properties.
 What aliases to the object are allowed to do is explicit rather than implied,
 whereas what the reference is allowed to do is derived.
\end_layout

\begin_layout Standard
Importantly, reference capabilities obey simple type checking rules that
 allow for reasoning about data-race freedom to be done locally, both by
 the programmer and by the compiler, rather than requiring global knowledge
 about a program.
 That is, the existence of some reference capability in some lexical scope
 explicitly indicates that:
\end_layout

\begin_layout Enumerate
No other alias to that object can exist that violates that reference capability'
s deny properties.
\end_layout

\begin_layout Enumerate
No other alias to that object can exist whose deny properties would be violated
 by that reference capability.
\end_layout

\begin_layout Standard
Such reasoning is both local (i.e.
 can be done without reference to implementation details outside of the
 function being reasoned about) and modular (i.e.
 reasoning about a function once is sufficient regardless of the context
 in which that function is used), even in the presence of type variables,
 i.e.
 generic types.
 The Pony type system accomplishes this through a combination of 
\emph on
viewpoint adaptation
\emph default
 
\begin_inset CommandInset citation
LatexCommand cite
key "cunningham2008universe"

\end_inset

, which determines a reference capability for a path based on all elements
 of that path, rather than simply the reference capability of the final
 element of the path, a separate and more liberal treatment of the types
 of temporary values (that is, the result of an expression which is then
 used in another expression, without establishing a path to the value by
 assigning it to a field or a stack variable), and 
\emph on
aliased and unaliased
\emph default
 types, which provide a way to refer to the alias of a reference capability
 (the type that results when a new path to a reference capability is created)
 and the unalias of a reference capability (the type that results when a
 path to a reference capability is removed, either through destructive read
 or by explicitly removing a variable in the lexical scope).
\end_layout

\begin_layout Subsection
\begin_inset CommandInset label
LatexCommand label
name "subsec:Logically-Atomic-Behaviours"

\end_inset

Logically Atomic Behaviours
\end_layout

\begin_layout Standard
The code that an actor executes upon receipt of some message 
\begin_inset Formula $m$
\end_inset

 is termed a 
\emph on
behaviour
\emph default
.
 In Pony, every behaviour on every actor is 
\emph on
logically atomic
\emph default
.
\end_layout

\begin_layout Standard
When a behaviour begins execution, it has a set of object and reference
 capabilities defined by the actor's state and the contents of the message
 
\begin_inset Formula $m$
\end_inset

 that has been received.
 In Pony, an actor's state is represented as fields of the actor, and the
 contents of the message 
\begin_inset Formula $m$
\end_inset

 are represented as arguments to the behaviour, in much the same way as
 an object-oriented method call has a receiver and a set of arguments.
 This initial state of capabilities is the total set of capabilities that
 the behaviour will have.
 No new capabilities that are not present when the behaviour begins executing
 can be acquired.
 Note that the behaviour may still create new actors and objects, but these
 new actors and objects do not represent an expansion of the set of capabilities
: they must be created with the capabilities that were initially available.
\end_layout

\begin_layout Standard
As a result, a behaviour cannot witness heap mutation that the behaviour
 does not itself perform.
 This is a result of combining the reference capability type system, which
 statically guarantees that if an actor can read from a memory address then
 no other actor can write to it, with the guarantee that the initial set
 of capabilities available to a behaviour cannot be expanded.
\end_layout

\begin_layout Standard
It is interesting to note that, while the set of capabilities cannot be
 expanded, it is possible for it to be contracted.
 Specifically, a capability that allows mutation of an address can be 
\emph on
sent
\emph default
 to another actor, and the data-race free type system guarantees that the
 sending actor retains neither the ability to read from nor write to that
 address.
 As a result, it is possible for a behaviour to have the capability to read
 or write some memory address, to give up that capability, and for the contents
 of that address to be mutated by some other actor while the original behaviour
 is still executing.
 However, in this case, the behaviour will not be able to expand its set
 of capabilities to once again include the capability to read from that
 memory address.
 As a result, the behaviour will not be able to witness the heap mutation.
\end_layout

\begin_layout Subsubsection
Reasoning About Atomic Behaviours
\end_layout

\begin_layout Standard
Requiring logically atomic behaviours is a powerful tool for reasoning about
 actors.
 Each behaviour can be considered as a separate sequential program, with
 a separate heap, that operates on some set of preexisting state (fields
 of the actor) and a set of input values (behaviour arguments).
 The resulting program will produce output in four forms:
\end_layout

\begin_layout Enumerate
Sending a finite number of messages to other actors or itself.
\end_layout

\begin_layout Enumerate
The creation of a finite number of new actors.
\end_layout

\begin_layout Enumerate
Changes to the executing actor's state that will be propagated to the next
 behaviour on that actor.
\end_layout

\begin_layout Enumerate
Side effects in the form of output to some device, for example a file system,
 network, display, etc.
\end_layout

\begin_layout Standard
Note that these possible outputs correspond to the fundamental requirements
 of the actor model, with the addition of device output.
\end_layout

\begin_layout Standard
Reasoning about individual behaviours as separate sequential programs removes
 the need to consider concurrency within a behaviour.
 This significantly simplifies the reasoning process.
 However, it does not remove the need to consider concurrency in a program
 as a whole.
 While interleaved concurrent reads and writes to memory locations no longer
 must be considered, message ordering remains non-deterministic where a
 causal relationship is not present, which can introduce program executions
 that exhibit race conditions at the logical level while still being data-race
 free.
\end_layout

\begin_layout Subsubsection
Asynchronous Function Results
\end_layout

\begin_layout Standard
There are three primary techniques for returning asynchronous results from
 asynchronous functions.
 The first is blocking futures, where an asynchronous function returns a
 value that may not yet be the result, but will be populated with the result
 in the future.
 The caller can then choose to block execution at some point until the result
 has been populated.
 The second is non-blocking futures, also referred to as asynchronous await.
 This approach captures the stack as a continuation that will be executed
 when the asynchronous result is available, and allows the caller to continue
 handling other messages in the meantime.
 The third is promises, which are similar to non-blocking futures, but instead
 of capturing the stack as a continuation, closures are explicitly specified.
 Promises allow more than one receiver of an asynchronous result, and also
 allow exceptional behaviour to be propagated in the form of separate closures
 for successful and unsuccessful execution.
\end_layout

\begin_layout Standard
These approaches are closely related, and each can be used, with some effort,
 to implement the others.
 Pony uses promises rather than blocking or non-blocking futures.
 This decision is motivated by reasoning rather than performance: logically
 atomic behaviours require asynchronous results to be returned via promises
 rather than futures in order to avoid expanding the available set of capabiliti
es during execution of a behaviour.
\end_layout

\begin_layout Standard
Arguably, logically atomic behaviours could be considered an implicit requiremen
t of the actor model.
 Specifically, the 
\emph on
introduction requirement
\emph default
 that implies that there can be no shared mutable state could be read to
 also imply that a memory location that is not readable when a behaviour
 begins executing must not become readable during execution.
 This is because a newly readable memory location could contain an actor
 address previously unknown to the actor executing the behaviour.
\end_layout

\begin_layout Standard
On the other hand, if the event of a previously unreadable memory location
 becoming readable is considered to be a new message 
\begin_inset Formula $m'$
\end_inset

, with the response to 
\begin_inset Formula $m$
\end_inset

 being considered finished and any remaining code to execute being considered
 a response to 
\begin_inset Formula $m'$
\end_inset

, then the introduction requirement is not violated.
 Such an approach treats messages as more abstract than actual messages
 in a mail queue: any expansion of the set of capabilities is treated as
 the logical arrival of a new message.
 This would allow, for example, blocking futures, which prevent shared mutable
 state but allow expanding the set of capabilities.
\end_layout

\begin_layout Standard
Awaiting an asynchronous result, i.e.
 using a non-blocking future, pauses a behaviour until an asynchronous result
 is returned, but allows the actor to continue receiving messages and executing
 their associated behaviours in the meantime.
 Effectively, the behaviour stack is captured as a continuation and resumed
 when the asynchronous result becomes available.
 This approach also results in non-atomic behaviours, as the actor may have
 been given new capabilities by intervening messages, resulting in the continuat
ion being executed with a larger set of capabilities than existed when 
\begin_inset Formula $m$
\end_inset

 initially arrived.
\end_layout

\begin_layout Standard
Both blocking and non-blocking futures can be encoded with logically atomic
 behaviours, either with or without promises, but doing so can result in
 code that is difficult to understand.
 A non-blocking future (asynchronous await) can be encoded as a closure
 that will be executed upon receipt of a message containing the expected
 result.
 This is continuation-passing style for asynchronous messages.
 Encoding a blocking future involves combining continuation-passing style
 with a queue to store messages that arrive before the message containing
 the expected result.
 The processing of these queued messages is delayed until after the expected
 result is received and the associated closure executed.
 In both cases, the programmer writes code to explicitly do what a compiler
 transformation would implicitly do.
\end_layout

\begin_layout Standard
Using promises, which are implemented in Pony as part of the standard library
 rather than as a language feature, preserves the introduction requirement
 without requiring the fulfilment of a future to be treated as a equivalent
 to a new message.
 The semantics of both blocking and non-blocking futures are still possible
 to achieve, but the underlying complexity of these approaches is directly
 exposed to the programmer.
\end_layout

\begin_layout Subsection
\begin_inset CommandInset label
LatexCommand label
name "subsec:Capabilities-Security"

\end_inset

Capabilities Security
\end_layout

\begin_layout Standard
A capability is an unforgeable token that both designates an object and
 provides access to that object.
 Capabilities security uses the possession of such tokens to control access
 to resources.
 Capabilities have a long history, stretching from operating system research
 (such as KeyKOS 
\begin_inset CommandInset citation
LatexCommand cite
key "hardy1985keykos"

\end_inset

, EROS
\begin_inset CommandInset citation
LatexCommand cite
key "shapiro2002eros"

\end_inset

, Coyotos 
\begin_inset CommandInset citation
LatexCommand cite
key "shapiro2007coyotos"

\end_inset

, and seL4 
\begin_inset CommandInset citation
LatexCommand cite
key "klein2009sel4"

\end_inset

) to programming languages (such as Joule 
\begin_inset CommandInset citation
LatexCommand cite
key "tribble1995joule"

\end_inset

, E 
\begin_inset CommandInset citation
LatexCommand cite
key "miller2005concurrency"

\end_inset

, AmbientTalk 
\begin_inset CommandInset citation
LatexCommand cite
key "van2007ambienttalk"

\end_inset

, Caja 
\begin_inset CommandInset citation
LatexCommand cite
key "miller2008safe"

\end_inset

, and BitC 
\begin_inset CommandInset citation
LatexCommand cite
key "shapiro2008bitc"

\end_inset

).
\end_layout

\begin_layout Standard
Capabilities are usually compared with access control list systems, where
 some arbiter that holds a mapping of roles to permissions must be traversed
 in order to gain access to a resource.
 While the two approaches are both security mechanisms, capabilities security
 is a more interesting match for a programming language, as a language can
 express unforgeable tokens easily and naturally.
\end_layout

\begin_layout Standard
Pony uses the 
\emph on
object capability
\emph default
 
\begin_inset CommandInset citation
LatexCommand cite
key "miller2003capability"

\end_inset

 model to express capabilities security.
 This was an easy choice, as in the absence of hardware support for capability-b
ased addressing, the object capability model is the most efficient way to
 implement capabilities security.
 The alternative would be using a C-list, which is a protected data structure
 that maps a process identifier and integer handle to a capability.
 In operating systems such as KeyKOS, the C-list is maintained by the kernel.
 The use of a C-list to express capabilities at the language level without
 an object model is simply too expensive; it would require a mapping of
 actor identifier and integer handle to capabilities, plus a mechanism for
 delegating capabilities to other actors.
 In contrast, the object capability model requires no runtime mechanism.
\end_layout

\begin_layout Standard
Adopting the object capability model had several follow-on effects.
 Most importantly, it required Pony to express 
\emph on
identity
\emph default
 as a first-class concept.
 An object's identity serves as the unforgeable token.
 In a memory safe language, such a mapping of identity to capability is
 a natural fit, as object identities cannot be manufactured or forged.
 The lack of mechanisms such as pointer arithmetic to manipulate identities
 allows those identities to be issuable only via controlled mechanisms.
 In Pony's case, this is via constructors.
\end_layout

\begin_layout Standard
The object capability model in Pony is designed to take advantage of type
 safety as well as memory safety.
 For example, a type with a private constructor is a capability that can
 only be constructed from within a certain package, providing a lexical
 bounds on capability creation.
\end_layout

\begin_layout Subsection
\begin_inset CommandInset label
LatexCommand label
name "subsec:Causal-Messaging"

\end_inset

Causal Messaging
\end_layout

\begin_layout Standard
The actor model requires that messages are delivered, but makes no requirement
 as to the order of delivery.
 Many implementations of the actor model effectively provide pairwise FIFO
 ordering of messages between actors, because the implementation of a message
 queue, even in a distributed setting, can make this relatively inexpensive
 to provide.
\end_layout

\begin_layout Standard
In addition, some implementations of the actor model provide 
\emph on
causal messaging
\emph default
 between actors running on the same physical hardware (node), again due
 to the availability of an inexpensive implementation.
 Here, causal messaging refers to a message order guarantee wherein an 
\emph on
effect
\emph default
 (a message) does not get delivered until after all of its 
\emph on
causes
\emph default
, where the causes of a message are every message that the sending actor
 has previously sent or received.
 Such causality is transitive.
\end_layout

\begin_layout Standard
Pony also provides
\emph on
 
\emph default
causal messaging between actors running on the same node.
 In addition, it was originally believed that message-based garbage collection
 would require causal messaging across nodes in the distributed setting.
 To address this, 
\emph on
tree-structured networks
\emph default
 were used to guarantee causality with no space overhead, but with 
\begin_inset Formula $O(\mathit{log}\,n)$
\end_inset

 latency overhead due to messages traversing the tree.
 This is a significant improvement compared to other causal messaging techniques
, but still represents both a latency cost and a possible message bottleneck.
\end_layout

\begin_layout Standard
To address these problems, the garbage collection algorithm was extended
 to work with only pairwise FIFO ordering, which can be implemented in a
 distributed setting with no overhead, eliminating the additional latency
 and the possible bottlenecks for system-level messages.
\end_layout

\begin_layout Standard
However, distributed message causality can be useful at the application
 level.
 Using multiple tree-structured networks (overlaid on the actual underlying
 network), it is possible to build any number of 
\emph on
causality bubbles
\emph default
, over which messaging, whether on a single node or across nodes, maintain
 causality.
 These causality bubbles can each have a different topology over the same
 nodes.
 As a result, the 
\begin_inset Formula $O(\mathit{log}\,n)$
\end_inset

 latency cost is still born, but bottlenecks are reduced because each bubble
 has a different tree-structure.
\end_layout

\begin_layout Standard
It is interesting to note that logically atomic behaviours, and thus deny
 capabilities for data-race freedom, play an important part in causal messaging.
 The ability to expand a capability set to examine some modified memory
 location during the execution of 
\begin_inset Formula $m$
\end_inset

, and therefore treating the modified memory location as a new message 
\begin_inset Formula $m'$
\end_inset

, effectively allows an actor to reorder its message queue.
 Such reordering can lead to causality violations.
 Any data race can cause such a violation by propagating information outside
 of message passing system, but it is also possible to have causality violations
 when data-race freedom is preserved if behaviours are not logically atomic.
\end_layout

\begin_layout Standard
For example, suppose actor 
\begin_inset Formula $\alpha_{1}$
\end_inset

 sends messages 
\begin_inset Formula $m_{1}$
\end_inset

 and 
\begin_inset Formula $m_{2}$
\end_inset

, in that order, to actor 
\begin_inset Formula $\alpha_{2}$
\end_inset

.
 In this case, 
\begin_inset Formula $m_{1}$
\end_inset

 is a cause of 
\begin_inset Formula $m_{2}$
\end_inset

.
 Now suppose that while handling 
\begin_inset Formula $m_{1}$
\end_inset

, 
\begin_inset Formula $\alpha_{2}$
\end_inset

 sends message 
\begin_inset Formula $m_{3}$
\end_inset

 to 
\begin_inset Formula $\alpha_{1}$
\end_inset

 and receives the result as a blocking future, such that 
\begin_inset Formula $\alpha_{2}$
\end_inset

 will treat the result generated by 
\begin_inset Formula $\alpha_{1}$
\end_inset

 as a new message 
\begin_inset Formula $m_{1}'$
\end_inset

, handling it as a continuation of 
\begin_inset Formula $m_{1}$
\end_inset

 and, importantly, 
\emph on
before
\emph default
 handling 
\begin_inset Formula $m_{2}$
\end_inset

.
 When 
\begin_inset Formula $\alpha_{1}$
\end_inset

 then receives 
\begin_inset Formula $m_{3}$
\end_inset

 and generates a result, it populates the future that 
\begin_inset Formula $\alpha_{2}$
\end_inset

 has blocked on.
 This result is a message 
\begin_inset Formula $m_{4}$
\end_inset

, and its causes are 
\begin_inset Formula $m_{1}$
\end_inset

, 
\begin_inset Formula $m_{2}$
\end_inset

 (the messages 
\begin_inset Formula $\alpha_{1}$
\end_inset

 has previously sent) and 
\begin_inset Formula $m_{3}$
\end_inset

 (the messages 
\begin_inset Formula $\alpha_{1}$
\end_inset

 has previously received).
 Now 
\begin_inset Formula $\alpha_{2}$
\end_inset

 unblocks, as the future has been fulfilled, and handles the result 
\begin_inset Formula $m_{4}$
\end_inset

.
 At this point, 
\begin_inset Formula $\alpha_{2}$
\end_inset

 has handled 
\begin_inset Formula $m_{1}$
\end_inset

, is handling 
\begin_inset Formula $m_{4}$
\end_inset

 next, and will handle 
\begin_inset Formula $m_{2}$
\end_inset

 in the future, resulting in a causality violation: 
\begin_inset Formula $\alpha_{2}$
\end_inset

 handles the effect 
\begin_inset Formula $m_{4}$
\end_inset

 before the cause 
\begin_inset Formula $m_{2}$
\end_inset

.
\end_layout

\begin_layout Subsection
\begin_inset CommandInset label
LatexCommand label
name "subsec:Message-based-Garbage-Collection"

\end_inset

Message-based Garbage Collection
\end_layout

\begin_layout Standard
Pony's garbage collector uses the underlying message-passing architecture
 as its only form of concurrent coordination.
 This is important for performance, but it is also important for correctness
 and reasoning.
\end_layout

\begin_layout Standard
Most implementations of the actor model require actors to be 
\emph on
explicitly terminated
\emph default
.
 That is, the programmer must manually manage actor lifetime, and send an
 actor that is no longer required a message requesting termination.
 This is effectively equivalent to manual memory management, with all of
 the attendant pitfalls.
 An actor that is prematurely collected may result in messages being ignored,
 or delivered to the wrong actor, or cause the program to terminate.
 An actor that is never collected will continue to consume memory and possibly
 CPU time.
\end_layout

\begin_layout Standard
Message-based garbage collection in Pony allows both actors and passive
 objects to be garbage collected, in both the concurrent and the distributed
 setting.
 As a result, the programmer not only need not manually manage actors, but
 also need not write code to defend against the possibility of a message
 being sent to a prematurely terminated actor.
 This both reduces the burden on the programmer and also allows for truly
 composable actor model subsystems, since the details of actor lifetime
 management do not have to be communicated between layers or components.
\end_layout

\begin_layout Standard
The same protocol that is used to garbage collect actors is also used to
 determine quiescence amongst scheduler threads on a single node and amongst
 nodes in a distributed environment.
 As a result, programs themselves also need not be explicitly terminated.
 Instead, a program terminates when there is no more work to be done and
 no more work can be created, without explicitly exiting a top level function
 or any other such explicit mechanism.
 As a result, no unit of execution is the leader, in the sense that no unit
 of execution can terminate and result in the termination of a program that
 may or may not have finished processing all pending and future work.
\end_layout

\begin_layout Standard
Message-based garbage collection relies on both the data-race free type
 system and causal messaging.
 Static data-race freedom allows coordination-free traversal of of data
 structures, both when sending and receiving messages and when collecting
 an individual actor's heap.
 Without static data-race freedom guarantees, the protocol would be both
 significantly more complicated and require runtime thread coordination,
 which is problematic when scaling over a large number of cores on a single
 node, and even more problematic in a distributed environment.
\end_layout

\begin_layout Standard
Causal messaging is used on a single node to enable the protocol to function
 without requiring acknowledgement messages when message-based reference
 counts are changed.
 Without causal messaging, such acknowledgement messages would effectively
 constitute a form of coordination, and would exhibit similar scaling problems.
\end_layout

\begin_layout Section
Performance
\end_layout

\begin_layout Standard
In co-designing the type system and the runtime, one of the motivations
 has been the idea that an advanced type system can be a tool for performance
 as well as for correctness.
 Some aspects of this are already well known, such as simplifying runtime
 virtual dispatch, eliding error checking and handling in the presence of
 an invalid type assumption, or using a type system that ensures data-race
 freedom to write concurrent programs without locks.
\end_layout

\begin_layout Standard
There are other design decisions, however, which impact performance in a
 way that may not be immediately obvious.
\end_layout

\begin_layout Subsection
Behaviours as Methods
\end_layout

\begin_layout Standard
In many actor model languages, receiving a message involves an explicit
 expression in the source code.
 In Pony, behaviours are instead written as methods on an actor type.
 As a result, Pony messages behave as asynchronous function calls: they
 are statically typed, and can interact fully with subtyping.
 For example, it is possible for an actor behaviour to be a subtype of a
 synchronous function.
\end_layout

\begin_layout Standard
This approach disallows receiving a new message while handling the current
 message.
 This is important for maintaining logically atomic behaviours, as it disallows
 expanding the available capability set with the arguments to a future message.
 In addition, pattern matching on the queue to select a specific message
 is also effectively disallowed, which is important for maintaining message
 causality.
\end_layout

\begin_layout Standard
Defining behaviours as methods has important performance implications as
 well.
 An obvious benefit is that strongly typed messages have similar performance
 benefits to strongly typed functions.
 Runtime type checking of arguments is not required, and machine words need
 not be boxed or otherwise distinguished at runtime from object references.
\end_layout

\begin_layout Standard
In addition, the lack of an explicit source statement to receive a message
 removes the need to capture a stack in order to suspend the execution of
 an actor while awaiting message delivery.
 Removing the need to capture the stack significantly simplifies the runtime.
 Not only does it avoid the need for user-space stack swapping or copying,
 but it also allows the runtime to use standard operating system stacks
 for scheduler threads.
 This allows the foreign function interface (FFI) to conform to the local
 platform's C ABI, allowing Pony to call code written in any language that
 can expose a conforming interface, without any overhead.
 No marshalling or other preparation is required.
 When link-time optimisation information is available, the Pony compiler
 can even inline FFI calls in Pony programs.
\end_layout

\begin_layout Standard
Disallowing pattern matching on an actor's message queue not only maintains
 message causality, it also allows an efficient lock-free unbounded intrusive
 queue to be used in the runtime.
 The queue can perform integral memory management without needing to garbage
 collect queue entries, which is important for coordination-free garbage
 collection.
\end_layout

\begin_layout Subsection
Exceptions as Partial Functions
\end_layout

\begin_layout Standard
Exception handling is a complex topic, both for reasons of type safety,
 particularly in the presence of checked exceptions, and for performance.
 The approach adopted by Pony is somewhat different from existing exception
 handling mechanisms, in that exceptions that unwind the stack can be raised,
 but these exceptions do not carry information.
 That is, there is no type or value associated with an exception.
 Effectively, a function that can raise an exception represents a partial
 function, one for which not every value in the domain produces a value
 in the range.
\end_layout

\begin_layout Standard
This approach allows Pony to have fully checked exceptions without the associate
d problems of function type signature expansion or issues with modularity.
 A Pony exception still represents a non-local return, but since it carries
 no information, the possibility of a non-local return can be indicated
 with a single bit of information (i.e.
 annotation as a partial function) rather than requiring all possible non-local
 return types to be enumerated.
 This also addresses the modularity problem: a change in a callee's exception
 raising behaviour (assuming the callee was already a partial function)
 does not impact the caller.
\end_layout

\begin_layout Standard
At runtime, this has a noticeable performance impact.
 In most languages, an exception results in a two-phase stack unwinding
 process.
 The first phase the locates a landing pad (a destination for the non-local
 return) in the stack that is capable of handling an exception of the type
 being raised.
 The second phase iterates through the stack frames that will be discarded,
 running any finalisation code, for example 
\begin_inset Formula $\mathtt{finally}$
\end_inset

 blocks in Java or destructors for objects on the stack in C++, and then
 continues execution at the landing pad.
 Some languages, such as Java, compound the resulting performance issues
 by carrying a backtrace in the exception information, which must be built
 before unwinding since frames will be discarded during the unwinding process.
\end_layout

\begin_layout Standard
In contrast, Pony effectively has a one-phase unwind process.
 The stack is searched for a landing pad, without having to determine if
 the landing pad is capable of handling the exception, since the exception
 has no value and can be handled by any landing pad.
 Once the landing pad is found, execution immediately continues at the landing
 pad, without the need to walk the stack or reify a backtrace.
\end_layout

\begin_layout Standard
Including exceptions in the language at all was also a performance decision.
 In the absence of exceptions, methods could return union types that include
 error values (an approach that is also used in the Pony standard library
 when a reason for failure must be propagated up the stack).
 However, this would require machine-word return values to be boxed in order
 to be able to distinguish them from types representing errors, which is
 a significant performance penalty.
 In addition, the return value would have to be checked by the caller, which
 has a runtime cost.
 Exceptions allow for code that does not normally fail to elide the cost
 of checking the return value, improving performance when no error occurs,
 at the expense of an increased cost (due to stack unwinding) when an error
 does happen.
\end_layout

\begin_layout Subsection
\begin_inset CommandInset label
LatexCommand label
name "subsec:Single-Compilation-Unit"

\end_inset

Single Compilation Unit
\end_layout

\begin_layout Standard
Many ahead-of-time compiled languages provide 
\emph on
separate
\emph default
 or even 
\emph on
independent
\emph default
 compilation.
 In contrast, even though the Pony type system allows type checking to be
 both local and modular, the compiler treats a program as a single compilation
 unit.
 Compiler passes before code generation are separate, but code generation
 occurs for the entire program at once.
\end_layout

\begin_layout Standard
Performance oriented compilers, such as C and C++, have been moving towards
 this approach with 
\emph on
link-time optimisation
\emph default
, wherein object files include the compiler's internal program representation
 (such as GIMPLE or LLVM IR) and the linker can then perform inter-procedural
 optimisations across object files.
\end_layout

\begin_layout Standard
Pony leverages the single compilation unit approach not just for inter-procedura
l optimisation, but also to perform reachability analysis, which is used
 for dead code elimination, generic type and method instantiation, to enable
 
\emph on
selector colouring
\emph default
 
\begin_inset CommandInset citation
LatexCommand cite
key "vitek1996compact"

\end_inset

 for virtual dispatch, and to reify structural types for runtime pattern-matchin
g on type.
\end_layout

\begin_layout Standard
Reachability analysis in Pony is performed by tracing the program from the
 entry point and finding all types and methods that are instantiated in
 the program.
 When a method receiver is a trait, an interface, or a union type, the method
 is instantiated on all subtypes of the receiving type.
 This process simultaneously performs dead code elimination.
\end_layout

\begin_layout Standard
Type and method reifications account for the full type of all type arguments,
 including reference capabilities and viewpoint adaptation, to allow the
 most specific possible code to be generated, including elements not present
 in the source, such as code generation to support garbage collection.
 During this process, all subtyping information required at runtime is reified,
 which allows both nominal and structural subtyping to be determined at
 compile time and stored in the type descriptors.
\end_layout

\begin_layout Standard
Precomputing subtyping information allows a selector colouring algorithm
 to be used to calculate method indices for virtual dispatch.
 This algorithm is similar to register colouring.
 It assigns an integer index to each method based on a matrix of types and
 the methods that are instantiated on those types.
 As a result, at runtime, virtual dispatch is always a single integer lookup
 in an array, without requiring thunking or other methods of selecting the
 correct vtable.
\end_layout

\begin_layout Standard
Since this approach precomputes both nominal and structural subtyping, there
 is no additional runtime cost when using structural types as compared to
 nominal types.
 Effectively, during reachability, structural types are reified as anonymous
 nominal types.
\end_layout

\begin_layout Standard
The downside of using a single compilation unit is that it prevents incremental
 compilation.
 This results in longer compilation times when making small edits to programs,
 since the entire program must be recompiled.
 In addition, it prevents constructing a REPL for the language, as adding
 code to a running program is not possible.
 This will be addressed in future work.
\end_layout

\begin_layout Subsection
C ABI Compatibility
\end_layout

\begin_layout Standard
The runtime is designed so that the 
\emph on
foreign function interface
\emph default
 does not require marshalling or unmarshalling of arguments, nor any stack
 manipulation.
 The underlying scheduler threads use standard kernel threads on every platform,
 and do not require the stack to be copied or modified.
 The use of logically atomic behaviours allows this to be done efficiently,
 as each behaviour runs to completion on a single scheduler thread, using
 the stack in the usual manner.
\end_layout

\begin_layout Standard
As a result, FFI calls can be made without any cost other than the function
 prologue and epilogue of the target function, i.e.
 the same cost paid in C, C++ or Fortran.
 A Pony program can link to a static or dynamic library written in any language,
 which allows Pony programs to leverage existing software.
 For example, the standard library uses both OpenSSL (for SSL, TLS and cryptogra
phic functions) and PCRE2 (for Perl compatible regular expressions).
\end_layout

\begin_layout Standard
If the target library provides link time optimisation information, a Pony
 program can inline functions from the library, providing a significant
 performance improvement.
\end_layout

\begin_layout Standard
In order to provide more complete FFI compatibility, Pony has a separate
 object type called a 
\begin_inset Formula $\mathtt{struct}$
\end_inset

 that is ABI compatible with a C 
\begin_inset Formula $\mathtt{struct}$
\end_inset

.
 As a result, it has no object header, and so a Pony 
\begin_inset Formula $\mathtt{struct}$
\end_inset

 cannot be a subtype of any other type, since it would not be able to disambigua
te the type at runtime.
 Their use is confined solely to FFI interoperability.
\end_layout

\begin_layout Section
\begin_inset CommandInset label
LatexCommand label
name "sec:Code-Example"

\end_inset

Code Example
\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

use "time"
\end_layout

\begin_layout Plain Layout

\end_layout

\begin_layout Plain Layout

class TimerPrint is TimerNotify
\end_layout

\begin_layout Plain Layout

  let _env: Env
\end_layout

\begin_layout Plain Layout

  var _count: U64 = 0
\end_layout

\begin_layout Plain Layout

\end_layout

\begin_layout Plain Layout

  new iso create(env: Env) =>
\end_layout

\begin_layout Plain Layout

    _env = env
\end_layout

\begin_layout Plain Layout

\end_layout

\begin_layout Plain Layout

  fun ref apply(timer: Timer, count: U64): Bool =>
\end_layout

\begin_layout Plain Layout

    _count = _count + count
\end_layout

\begin_layout Plain Layout

    _env.out.print("timer: " + _count.string())
\end_layout

\begin_layout Plain Layout

    _count < 10
\end_layout

\begin_layout Plain Layout

\end_layout

\begin_layout Plain Layout

  fun ref cancel(timer: Timer box) =>
\end_layout

\begin_layout Plain Layout

    _env.out.print("timer cancelled")
\end_layout

\begin_layout Plain Layout

\end_layout

\begin_layout Plain Layout

actor Main
\end_layout

\begin_layout Plain Layout

  new create(env: Env) =>
\end_layout

\begin_layout Plain Layout

    let timers = Timers
\end_layout

\begin_layout Plain Layout

\end_layout

\begin_layout Plain Layout

    let t1 = Timer(TimerPrint(env), 500000000, 500000000) // 500 ms
\end_layout

\begin_layout Plain Layout

    let t1' = t1
\end_layout

\begin_layout Plain Layout

    timers(consume t1)
\end_layout

\begin_layout Plain Layout

    timers.cancel(t1')
\end_layout

\begin_layout Plain Layout

\end_layout

\begin_layout Plain Layout

    let t2 = Timer(TimerPrint(env), 500000000, 500000000) // 500 ms
\end_layout

\begin_layout Plain Layout

    timers(consume t2)
\end_layout

\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset Caption Standard

\begin_layout Plain Layout
\begin_inset CommandInset label
LatexCommand label
name "fig:A-code-example"

\end_inset

A program illustrating the use of asynchronous timers.
\end_layout

\end_inset


\end_layout

\begin_layout Plain Layout

\end_layout

\end_inset


\end_layout

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

\begin_layout Verbatim

$ ./timers.exe
\end_layout

\begin_layout Verbatim

timer cancelled
\end_layout

\begin_layout Verbatim

timer: 1
\end_layout

\begin_layout Verbatim

timer: 2
\end_layout

\begin_layout Verbatim

timer: 3
\end_layout

\begin_layout Verbatim

timer: 4
\end_layout

\begin_layout Verbatim

timer: 5
\end_layout

\begin_layout Verbatim

timer: 6
\end_layout

\begin_layout Verbatim

timer: 7
\end_layout

\begin_layout Verbatim

timer: 8
\end_layout

\begin_layout Verbatim

timer: 9
\end_layout

\begin_layout Verbatim

timer: 10
\end_layout

\begin_layout Verbatim

timer cancelled
\end_layout

\begin_layout Plain Layout
\begin_inset Caption Standard

\begin_layout Plain Layout
\begin_inset CommandInset label
LatexCommand label
name "fig:The-output-of"

\end_inset

The output of the program in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:A-code-example"

\end_inset

.
\end_layout

\end_inset


\end_layout

\begin_layout Plain Layout

\end_layout

\end_inset

Figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:A-code-example"

\end_inset

 contains a complete example program that is included with the compiler.
 It is an illustration of how to use asynchronous timers.
 The program first creates an actor that handles timers.
 Then, it sets a timer and immediately cancels it.
 Then, it sets a timer without cancelling it.
 The program produces the output in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:The-output-of"

\end_inset

.
 This brief example illustrates a number of core concepts in Pony, including
 asynchronous message passing, causality, the use of reference capabilities,
 passing isolated mutable state, sharing globally immutable state, actor
 and object garbage collection, and program quiescence.
\end_layout

\begin_layout Standard
One line 1, the 
\family typewriter
time
\family default
 package is imported into the current module's namespace.
 It is also possible to import a package using an enclosing identifier to
 avoid namespace collisions.
 On line 3, a new type 
\family typewriter
TimerPrint
\family default
 is defined, and it specifies that it implements the 
\family typewriter
TimerNotify
\family default
 trait.
 On line 4, 
\family typewriter
TimerPrint
\family default
 is given a single-assignment private field 
\family typewriter
_env
\family default
 of type 
\family typewriter
Env
\family default
, which is an immutable environment that gives the program access to its
 command line arguments, environment variables, and the console via actors
 associated with 
\family typewriter
stdout
\family default
, 
\family typewriter
stderr
\family default
, and 
\family typewriter
stdin
\family default
.
 On line 5, a multiple-assignment field 
\family typewriter
_count
\family default
 of type 
\family typewriter
U64
\family default
, an unsigned 64-bit integer, is declared, and is initialised to 
\family typewriter
0 
\family default
in all constructors.
\end_layout

\begin_layout Standard
On line 6, 
\family typewriter
TimerPrint
\family default
 is given a constructor named 
\family typewriter
create
\family default
, which is the default constructor used if no named constructor is specified
 when instantiating a type.
 Here, 
\family typewriter
TimerPrint.create
\family default
 takes a single argument 
\family typewriter
env
\family default
 of type 
\family typewriter
Env
\family default
.
 This constructor has the 
\family typewriter
iso
\family default
 reference capability, as described in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Reference-Capabilities"

\end_inset

.
 This means the constructed object is mutable, but isolated, i.e.
 externally unique.
 In order for this to hold, all arguments to the constructor must themselves
 be either 
\family typewriter
iso
\family default
 or 
\family typewriter
val
\family default
, i.e.
 globally immutable (also described in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Reference-Capabilities"

\end_inset

).
 In this case, 
\family typewriter
Env
\family default
 is defined has having a default reference capability of 
\family typewriter
val
\family default
, so this constructor is valid.
\end_layout

\begin_layout Standard
On line 7, the single-assignment field 
\family typewriter
_env
\family default
 is initialised.
 At this point, 
\family typewriter
_env
\family default
 cannot be assigned again, and this is enforced statically.
 Pony constructors are required to initialise all fields of the instantiated
 type, and 
\family typewriter
this
\family default
 in a constructor has the reference capability 
\family typewriter
tag
\family default
, as described in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Reference-Capabilities"

\end_inset

, until it is fully initialised.
 Note that 
\family typewriter
_count
\family default
 is not explicitly initialised in the body of 
\family typewriter
create
\family default
, as it is initialised where it is defined.
\end_layout

\begin_layout Standard
On line 10, 
\family typewriter
TimerPrint
\family default
 is given an 
\family typewriter
apply
\family default
 method, which is the default method if an object is invoked without a method
 being specified.
 This is called from the 
\family typewriter
time 
\family default
package when the associated timer fires.
 It takes two arguments: the 
\family typewriter
Timer
\family default
 that is firing, and the number of times the 
\family typewriter
Timer
\family default
 has fired since the notifier was last informed.
 The default reference capability for 
\family typewriter
Timer
\family default
 is defined in the 
\family typewriter
time
\family default
 package as 
\family typewriter
ref
\family default
, i.e.
 mutable but not isolated, as described in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Reference-Capabilities"

\end_inset

.
 This allows the 
\family typewriter
TimerPrint
\family default
 notifier to mutate the 
\family typewriter
Timer
\family default
 when a notification occurs, perhaps by changing its expiry time.
 In this case, the body of 
\family typewriter
TimerPrint.apply
\family default
 advances the notifier's 
\family typewriter
_count
\family default
, prints to the console by sending a message to 
\family typewriter
_env.out
\family default
 (an actor with access to 
\family typewriter
stdout
\family default
), and then returns 
\family typewriter
true
\family default
 if the total 
\family typewriter
_count
\family default
 is less than ten, or 
\family typewriter
false
\family default
 otherwise.
 In the 
\family typewriter
time
\family default
 package, a timer is cancelled if the notifier for the timer returns 
\family typewriter
false
\family default
.
\end_layout

\begin_layout Standard
Note that the message sent to 
\family typewriter
_env.out
\family default
 on line 12 contains a globally immutable 
\family typewriter
String
\family default
.
 It would be safe for the notifier to keep a referenec to the 
\family typewriter
String
\family default
 being sent, but in this case it does not.
\end_layout

\begin_layout Standard
On line 15, 
\family typewriter
TimerPrint
\family default
 is given a 
\family typewriter
cancel
\family default
 method, which is called from the 
\family typewriter
time
\family default
 package when the associated timer is cancelled.
 It takes a single argument of type 
\family typewriter
Timer box
\family default
, i.e.
 a locally immutable 
\family typewriter
Timer
\family default
, as described in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Reference-Capabilities"

\end_inset

.
 A 
\family typewriter
box
\family default
 reference allows 
\family typewriter
TimerPrint.cancel
\family default
 to read from the 
\family typewriter
Timer
\family default
, but neither mutate it nor pass it in a message.
 In this case, the 
\family typewriter
cancel
\family default
 method simply prints a notification to the console, by again sending a
 message to 
\family typewriter
_env.out
\family default
 containing a globally immutable 
\family typewriter
String
\family default
.
\end_layout

\begin_layout Standard
On line 18, the program's 
\family typewriter
Main
\family default
 actor is defined.
 A Pony program begins with its 
\family typewriter
Main
\family default
 actor being constructed using the 
\family typewriter
create
\family default
 constructor, which is defined here on line 19.
 The 
\family typewriter
Main.create
\family default
 constructor always takes a single argument, which is an immutable environment
 
\family typewriter
Env
\family default
.
 This program begins by creating a 
\family typewriter
Timers
\family default
 actor on line 20, which is a hierarchical timing wheel actor defined in
 the 
\family typewriter
time
\family default
 package.
 The local variable 
\family typewriter
timer
\family default
 is of type 
\family typewriter
Timer tag
\family default
, as an actor is viewed as an opaque type from other actors, as described
 in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Reference-Capabilities"

\end_inset

.
\end_layout

\begin_layout Standard
On line 22, a 
\family typewriter
Timer
\family default
 is created, using the default 
\family typewriter
Timer.create
\family default
 constructor.
 Its first argument is a 
\family typewriter
TimerNotify
\family default
, created with 
\family typewriter
TimerNotify.create
\family default
 and passed 
\family typewriter
env
\family default
 as an argument.
 It is safe to share the reference to 
\family typewriter
env
\family default
 as it is a 
\family typewriter
val
\family default
 reference, i.e.
 globally immutable, and as such its use cannot result in a data-race.
 The resulting notifier is of type 
\family typewriter
TimerNotify iso
\family default
, that is, it is isolated.
 The other two arguments to the 
\family typewriter
Timer
\family default
 constructor are integers, which type inference will discover are of type
 
\family typewriter
U64
\family default
.
 All basic machine-word types, i.e.
 booleans, integers, and floating point number, are treated as 
\family typewriter
val
\family default
, so here the 
\family typewriter
Timer
\family default
 constructor takes only 
\family typewriter
iso
\family default
 and 
\family typewriter
val
\family default
 arguments.
 As a result, the type of 
\family typewriter
t1
\family default
 when it is assigned on line 22, is 
\family typewriter
Timer iso
\family default
, that is, an isolated 
\family typewriter
Timer
\family default
, with a 500 millisecond initial firing time that repeatedly fires every
 500 milliseconds after that.
\end_layout

\begin_layout Standard
On line 23, an alias of 
\family typewriter
t1
\family default
, here called 
\family typewriter
t1'
\family default
, is created.
 However, as described in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Reference-Capabilities"

\end_inset

, an alias of an 
\family typewriter
iso
\family default
 reference is a 
\family typewriter
tag
\family default
 reference.
 To maintain isolation, an alias to an isolated reference must be opaque,
 i.e.
 allow neither reading from nor writing to the reference object.
\end_layout

\begin_layout Standard
On line 24, 
\family typewriter
t1
\family default
 is 
\family typewriter
consume
\family default
'd from the current lexical scope, making it unavailable in that scope.
 This results in an 
\emph on
unaliased
\emph default
 type, that is, a type for which one alias has been removed, again as described
 in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Reference-Capabilities"

\end_inset

.
 This allows the object formerly referenced by 
\family typewriter
t1
\family default
 to be safely sent in a message to the 
\family typewriter
Timers
\family default
 actor that was created on line 20.
 Line 24 implicitly calls 
\family typewriter
Timers.apply
\family default
, which in this case is a 
\emph on
behaviour
\emph default
, that is, an asynchronous method call, as described in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Syntax-and-Operational"

\end_inset

.
 This in turn uses the garabage collection protocol described in chapter
 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Object-Collection"

\end_inset

 to ensure that the 
\family typewriter
Timer
\family default
 can eventually be collected without requiring a stop-the-world step.
\end_layout

\begin_layout Standard
Then, on line 25, the 
\family typewriter
timer
\family default
 actor is sent another message, this time 
\family typewriter
Timers.cancel
\family default
.
 The argument is 
\family typewriter
t1'
\family default
, which is a 
\family typewriter
tag
\family default
 alias to the same 
\family typewriter
Timer
\family default
 that was set on line 24.
 By keeping a 
\family typewriter
tag
\family default
 alias to the 
\family typewriter
Timer
\family default
, the 
\family typewriter
Main
\family default
 actor can refer to it by its identity when cancelling it.
 The 
\family typewriter
tag
\family default
 reference to the 
\family typewriter
Timer
\family default
 is a capability that allows cancelling the possessor to cancel it, with
 no risk of name collision.
 Because messages are causally ordered, the 
\family typewriter
Timers
\family default
 actor will receive the creation of the 
\family typewriter
Timer
\family default
 before the cancellation, so the cancellation cannot be lost.
\end_layout

\begin_layout Standard
On line 27, the 
\family typewriter
Main
\family default
 actor creates another 
\family typewriter
Timer
\family default
, in the same manner as previously, and on line 28, that timer is sent to
 the 
\family typewriter
Timers
\family default
 actor.
 At this point, the 
\family typewriter
Main
\family default
 actor's constructor completes, but, unlike the 
\family typewriter
main
\family default
 function in a C or C++ program, the program does not terminate.
 This is because the 
\family typewriter
Timers
\family default
 actor still has pending work, and so the program has not yet reached quiescence
, as described in section 
\begin_inset CommandInset ref
LatexCommand ref
reference "sec:Completeness"

\end_inset

.
 However, the actor garbage collection protocol described in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Actor-Collection"

\end_inset

 may at this point collect the 
\family typewriter
Main
\family default
 actor, as it is not executing and has no pending work, i.e.
 it is 
\emph on
blocked
\emph default
 as described in section 
\begin_inset CommandInset ref
LatexCommand ref
reference "subsec:Cycle-Detection"

\end_inset

, and cannot receive work in the future, as no other actor has a reference
 to it, i.e.
 it is 
\emph on
dead
\emph default
 as described in section 
\begin_inset CommandInset ref
LatexCommand ref
reference "subsec:Dead-Actors"

\end_inset

.
\end_layout

\begin_layout Standard
Concurrently with the execution of 
\family typewriter
Main
\family default
's constructor, the 
\family typewriter
Timers
\family default
 actor will begin handling its own messages, as shown in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Syntax-and-Operational"

\end_inset

.
 Specifically, it will set the first 
\family typewriter
Timer
\family default
, including making a system call to set up an operating system timer, then
 cancel the first 
\family typewriter
Timer
\family default
, and then set the second 
\family typewriter
Timer
\family default
.
 Interleaved with these messages will be messages from the asynchronous
 I/O layer in the runtime, as described in section 
\begin_inset CommandInset ref
LatexCommand ref
reference "sec:Asynchronous-I/O"

\end_inset

, indicating that the operating system timer has fired.
 When those occur, the 
\family typewriter
Timers
\family default
 actor examines its hierarchical timing wheel, as implemented in the 
\family typewriter
time
\family default
 package, and fires the 
\family typewriter
Timer
\family default
 objects it holds as appropriate.
\end_layout

\begin_layout Standard
In this case, the 
\family typewriter
TimerPrint
\family default
 notifier for the first 
\family typewriter
Timer
\family default
 is called with 
\family typewriter
cancel
\family default
 first, before any timers have fired.
 Then, the second 
\family typewriter
Timer
\family default
 fires ten times, after which it returns 
\family typewriter
false
\family default
 and the 
\family typewriter
Timers
\family default
 actor cancels it.
 At this point, the 
\family typewriter
Timers
\family default
 actor has no pending 
\family typewriter
Timer
\family default
 objects, and so cancels its operating system timer.
\end_layout

\begin_layout Standard
This results in the 
\family typewriter
Timers
\family default
 actor becoming 
\emph on
blocked
\emph default
, as it is not executing and has no pending work.
 Since the only actor that may have a reference to it, the 
\family typewriter
Main
\family default
 actor, is also
\emph on
 blocked
\emph default
, and the asynchronous I/O layer will not generate new work for it, the
 
\family typewriter
Timers
\family default
 actor is also 
\emph on
dead
\emph default
, and eligible for garbage collection.
 At this point, all actors are 
\emph on
dead
\emph default
 and the program has reached quiescence, as described in section 
\begin_inset CommandInset ref
LatexCommand ref
reference "subsec:Quiescence"

\end_inset

, and terminates.
\end_layout

\begin_layout Section
Philosophy
\end_layout

\begin_layout Standard
In the spirit of Richard Gabriel, the Pony philosophy is neither "the-right-thin
g" nor "worse-is-better".
 It is "get-stuff-done".
 
\end_layout

\begin_layout Itemize
Correctness.
 Incorrectness is simply not allowed.
 
\emph on
It's pointless to try to get stuff done if you can't guarantee the result
 is correct.
 
\end_layout

\begin_layout Itemize
Performance.
 Runtime speed is more important than everything except correctness.
 If performance must be sacrificed for correctness, try to come up with
 a new way to do things.
 
\emph on
The faster the program can get stuff done, the better.
 This is more important than anything except a correct result.
 
\end_layout

\begin_layout Itemize
Simplicity.
 Simplicity can be sacrificed for performance.
 It is more important for the interface to be simple than the implementation.
 
\emph on
The faster the programmer can get stuff done, the better.
 It's ok to make things a bit harder on the programmer to improve performance,
 but it's more important to make things easier on the programmer than it
 is to make things easier on the language/runtime.
 
\end_layout

\begin_layout Itemize
Consistency.
 Consistency can be sacrificed for simplicity or performance.
 
\emph on
Don't let excessive consistency get in the way of getting stuff done.
 
\end_layout

\begin_layout Itemize
Completeness.
 It's nice to cover as many things as possible, but completeness can be
 sacrificed for anything else.
 
\emph on
It's better to get some stuff done now than wait until everything can get
 done later.
 
\end_layout

\begin_layout Standard
The "get-stuff-done" approach has the same attitude towards correctness
 and simplicity as "the-right-thing", but the same attitude towards consistency
 and completeness as "worse-is-better".
 It also adds performance as a new principle, treating it as the second
 most important thing, after correctness.
\end_layout

\begin_layout Standard
As with any self-professed philosophy, this one should be taken with a grain
 of salt.
 It has helped guide the development of Pony, but it is the map, not the
 territory.
\end_layout

\end_body
\end_document