objectgc.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:Object-Collection"

\end_inset

Object Collection
\end_layout

\begin_layout Standard
As discussed in chapters 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Syntax-and-Operational"

\end_inset

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

\end_inset

, Pony, like many actor-model languages, has non-actor entities, in the
 form of passive (synchronous) objects, and such objects can be passed between
 actors in messages.
 In order to pass such messages by reference, in order to have zero-copy
 message passing, objects that have been passed or shared between actors
 must be garbage collected, and this garbage collection must be more efficient
 than copying objects in messages.
 Garbage collecting such objects in an actor-model language faces similar
 problems to garbage collecting actors themselves.
 The inability to examine the global state of the program without pausing
 the program results in existing approaches to object garbage collection
 suffering performance problems, particularly when stop-the-world pauses
 cause the program to become unresponsive.
\end_layout

\begin_layout Standard
Existing approaches to reducing stop-the-world pauses in garbage collection
 
\begin_inset CommandInset citation
LatexCommand cite
key "click2005pauseless,tene2011c4"

\end_inset

 significantly reduce such program pauses.
 However, such general approaches cannot leverage the properties of an actor-mod
el language, particularly the isolation of state within actors.
 As a result, they rely on techniques such as 
\emph on
read barriers
\emph default
, which adversely affect mutator thread performance, in order to reduce
 pause times.
\end_layout

\begin_layout Standard
Erlang achieves fully concurrent passive object garbage collection by copying
 passive objects sent in messages to the 
\emph on
process-local heap
\emph default
 of the destination.
 This comes at a cost: copying the passive objects can be expensive when
 large data structures are passed between actors, both when the message
 is sent (due to the time taken to copy the message) and over time (due
 to the resulting increased memory usage).
 Copying message contents also means that 
\emph on
object identity
\emph default
 must be encoded in the data structure by the programmer, rather than being
 implicitly derived from the object's memory address.
 While this is less important for a functional language such as Erlang,
 it is important for an 
\emph on
object capability
\emph default
 language such as Pony.
\end_layout

\begin_layout Standard
In Pony, a novel technique for passive object collection has been developed
 based on Message-based Actor Collection (
\emph on
MAC
\emph default
), described in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Actor-Collection"

\end_inset

.
 This approach, termed Ownership and Reference Counting for Actors (
\emph on
ORCA
\emph default
) extends 
\emph on
MAC
\emph default
 to allow synchronous objects allocated by some actor 
\begin_inset Formula $\alpha$
\end_inset

 and subsequently shared with other actors to be efficiently and safely
 garbage collected by the allocating actor 
\begin_inset Formula $\alpha$
\end_inset

 without requiring any synchronisation mechanism other than message passing.
 This combines 
\emph on
actor-local heaps
\emph default
 with an 
\emph on
ownership
\emph default
 model wherein an actor 
\begin_inset Formula $\alpha$
\end_inset

 may be able to reach an object 
\begin_inset Formula $\omega$
\end_inset

 in the heap of another actor 
\begin_inset Formula $\alpha'$
\end_inset

, but the allocating actor 
\begin_inset Formula $\alpha'$
\end_inset

 (i.e.
 the owner) remains responsible for garbage collecting 
\begin_inset Formula $\omega$
\end_inset

.
\end_layout

\begin_layout Section
Background on Actor-Model Object GC
\end_layout

\begin_layout Standard
Existing approaches to collecting passive objects in actor-model languages
 and libraries fall into four basic categories:
\end_layout

\begin_layout Enumerate

\emph on
Manual actor termination with global heap tracing.

\emph default
 This approach relies on the programmer manually terminating actors and
 leverages an existing garbage collection mechanism, such as is present
 on the JVM or the CLR, as is done in Scala 
\begin_inset CommandInset citation
LatexCommand cite
key "haller2009scala"

\end_inset

, Akka, Kilim 
\begin_inset CommandInset citation
LatexCommand cite
key "srinivasan2008kilim"

\end_inset

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

\end_inset

, and SALSA 2.0 
\begin_inset CommandInset citation
LatexCommand cite
key "varela2001programming"

\end_inset

.
 Garbage collection in such systems does not leverage actor isolation, but
 can leverage existing well-known garbage collection techniques for non-actor
 languages.
\end_layout

\begin_layout Enumerate

\emph on
Manual actor termination with local heap tracing.
 
\emph default
This approach also relies on the programmer manually terminating actors,
 but the tracing mechanism takes advantage of actor isolation to provide
 local heaps.
 To preserve heap locality, messages are copied into the heap of the receiving
 actor.
 This approach is taken by BEAM-based languages such as Erlang 
\begin_inset CommandInset citation
LatexCommand cite
key "armstrong2007history"

\end_inset

 and Elixir.
 By accepting the costs of message copying, this technique allows garbage
 collection to be fully concurrent.
\end_layout

\begin_layout Enumerate

\emph on
Actor graph transformation with global heap tracing
\emph default
.
 By transforming the actor graph into a passive object graph and using a
 tracing collector for both actors and objects 
\begin_inset CommandInset citation
LatexCommand cite
key "vardhan2002using,wang2010actor"

\end_inset

, this approach allows actors themselves to be garbage collected.
 ActorFoundry uses this technique.
 While this approach requires significant stop-the-world pauses, it is also
 the first approach to allow actors themselves to be garbage collected.
\end_layout

\begin_layout Enumerate

\emph on
Snapshots and reference listing with global heap tracing
\emph default
.
 This technique, used in SALSA 1.0 
\begin_inset CommandInset citation
LatexCommand cite
key "wang2006distributed,wang2006non,wang2013conservative"

\end_inset

, is able to collect both local and distributed actors.
 While the approach is heavyweight and was removed in SALSA 2.0, it provided
 a mechanism for collecting actors that did not rely on transforming the
 actor graph to a passive object graph.
 This approach uses an existing garbage collecting runtime, in this case
 the JVM, to collect passive objects.
\end_layout

\begin_layout Standard
The purpose of 
\emph on
ORCA 
\emph default
is to provide an approach that combines garbage collected actors with local
 heap tracing while not requiring messages to be copied to the destination
 heap.
\end_layout

\begin_layout Section
Ownership and Reference Counting for Actors Algorithm
\end_layout

\begin_layout Standard

\emph on
ORCA
\emph default
 extends 
\emph on
MAC
\emph default
 by tracking object references in external maps as well as actor references.
 Through message receipt, actors may acquire references to objects allocated
 by other actors, which we term 
\emph on
foreign objects
\emph default
, and during execution they may release those references.
 Therefore, to keep track of this, they acquire and release reference counts.
 Importantly, such reference counts are not dependent on the shape of the
 heap, but instead change only when messages are sent and received.
\end_layout

\begin_layout Standard
To do so, the operational semantics are altered to perform reference count
 adjustments for passive objects as well as for actor references when sending
 and receiving messages.
 Similarly, actors can acquire and release reference counts for objects
 owned by other actors.
 To account for that,
\emph on
 INC 
\emph default
and 
\emph on
DEC
\emph default
 messages are changed to carry a map of address to reference count (that
 is, an 
\begin_inset Formula $\mathit{ExMap}$
\end_inset

) instead of a scalar reference count.
\end_layout

\begin_layout Subsection
Local Heap Tracing
\end_layout

\begin_layout Standard
The model for 
\emph on
ORCA
\emph default
 does not require a specific method of tracing a local heap.
 In Pony, a mark-and-don't-sweep collector is used, as described in section
 
\begin_inset CommandInset ref
LatexCommand ref
reference "sec:Actor-GC"

\end_inset

.
 However, alternate mechanisms for collecting a local heap, such as an increment
al garbage collector, or even a concurrent collector that examines a single
 actor's local state and local heap at any given time, could be used.
\end_layout

\begin_layout Standard
The operational semantics accounts for this with a high level description
 of when objects are unreachable by an actor 
\begin_inset Formula $\alpha$
\end_inset

.
 If such objects are owned by 
\begin_inset Formula $\alpha$
\end_inset

, they may be collected if they have a local reference count of zero (or
 have never had a local reference count).
 If such objects are owned by some other actor, the foreign reference count
 held by 
\begin_inset Formula $\alpha$
\end_inset

 can be released.
\end_layout

\begin_layout Subsection
Cyclic Passive Object Garbage
\end_layout

\begin_layout Standard
Importantly, 
\emph on
ORCA
\emph default
 does not require a cycle detector to collect passive objects.
 This is because of the 
\emph on
ownership
\emph default
 model, wherein only actors hold reference counts for passive objects.
 The topology of an object graph, that is, the number of paths by which
 an object is reachable, does not affect the local or foreign reference
 count for an object.
 As such, a cyclic graph of passive objects does not result in reference
 counts that will never reach zero.
\end_layout

\begin_layout Subsection
Local Heap Collection
\end_layout

\begin_layout Standard
The 
\emph on
ownership
\emph default
 model results in local heaps that are independently traceable and collectable,
 without synchronisation.
 Effectively, passive objects for which the owning (i.e.
 allocating) actor maintains a positive local reference count are added
 to the reachable set, preventing premature collection.
\end_layout

\begin_layout Standard
This local heap collection takes place without synchronisation, even though
 the algorithm uses message passing to increment and decrement deferred
 distributed weighted reference counts.
 Importantly, none of the 
\emph on
ORCA 
\emph default
messages requires a reply, so there is never a situation in which an actor
 
\begin_inset Formula $\alpha$
\end_inset

 must wait for another actor 
\begin_inset Formula $\alpha'$
\end_inset

 to make progress before 
\begin_inset Formula $\alpha$
\end_inset

 can itself make progress.
\end_layout

\begin_layout Section
Formal Model
\end_layout

\begin_layout Standard
The formal model for 
\emph on
ORCA
\emph default
 is expressed as an extension of the model for message-based actor collection
 (
\emph on
MAC
\emph default
) presented in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Actor-Collection"

\end_inset

.
 Where a rule or a definition is not changed, it is used unmodified.
\end_layout

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

\begin_layout Plain Layout
\align center
\begin_inset Formula $\begin{array}{rclcl}
\mu & \in & \mathit{Message} & = & {\color{gray}(\mathit{MethodID\times\overline{Value}})}\\
 &  &  & | & INC(\mathit{ExMap})\,|\,DEC(\mathit{ExMap})\\
 &  &  & | & {\color{gray}BLK(\mathit{ActorAddr},\mathit{RefCount},\mathit{ExMap})}\\
 &  &  & | & {\color{gray}UNB(\mathit{ActorAddr})}\\
 &  &  & | & {\color{gray}CNF(\mathit{Token})\,|\,ACK(\mathit{ActorAddr},\mathit{Token})}
\end{array}$
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset Caption Standard

\begin_layout Plain Layout
\begin_inset CommandInset label
LatexCommand label
name "fig:Runtime-entities-for-object-GC"

\end_inset


\begin_inset Argument 1
status open

\begin_layout Plain Layout
Runtime entities for object GC
\end_layout

\end_inset

Runtime entities for object GC.
 Elements that are unchanged are greyed out.
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
The only change in the runtime entities is a modification in the information
 carried by 
\emph on
INC 
\emph default
and 
\emph on
DEC
\emph default
 messages.
 Instead of a scalar reference count, those messages now carry a mapping
 of address to reference count.
 This allows a single message to communicate reference count changes for
 a collection of objects allocated by some actor, and possibly the actor
 itself.
\end_layout

\begin_layout Subsection
\begin_inset CommandInset label
LatexCommand label
name "subsec:Reachability-1"

\end_inset

Reachability
\end_layout

\begin_layout Standard
The rules for reachability remain unchanged from those delineated for 
\emph on
MAC
\emph default
 in section 
\begin_inset CommandInset ref
LatexCommand ref
reference "subsec:Reachability"

\end_inset

.
 Because 
\emph on
MAC
\emph default
 must find actor references anywhere in a passive object graph, the same
 rules can be used to allow 
\emph on
ORCA
\emph default
 to find passive object references in the same graph.
 Just as 
\emph on
MAC
\emph default
 does not have to determine global liveness for actor collection, 
\emph on
ORCA 
\emph default
does not need to determine global liveness for object collection.
\end_layout

\begin_layout Subsection
Reference Count Invariant
\end_layout

\begin_layout Standard
The reference count invariant for passive objects takes the same form as
 the invariant for actors, and so can be stated for both as:
\end_layout

\begin_layout Standard
\begin_inset Formula 
\[
\mathit{LRC}(\iota)+\mathit{INC}(\iota)-\mathit{DEC}(\iota)=\mathit{AMC}(\iota)+\mathit{FRC}(\iota)
\]

\end_inset


\end_layout

\begin_layout Standard
This invariant is evaluated in the context of some heap 
\begin_inset Formula $\chi$
\end_inset

.
 The reference count components for passive objects are effectively the
 same as for actors, but use the external map exclusively for tracking reference
 counts, without using the owning actor's local reference count.
\end_layout

\begin_layout Definition
Reference count invariant components
\end_layout

\begin_layout Definition
\begin_inset Formula $\begin{array}{lcl}
\mathit{LRC}(\omega) & = & \chi(\mathcal{O}(\omega))\downarrow_{8}(\omega)\\
\mathit{INC}(\omega) & = & \sum_{i=1}^{|Q(\chi,\mathcal{O}(\omega))|}\begin{cases}
\rho & \mathit{if}\,Q(\chi,\mathcal{O}(\omega))_{i}=\mathit{INC}(\xi)\wedge\xi(\omega)=\rho\\
0 & \mathit{otherwise}
\end{cases}\\
\mathit{DEC}(\omega) & = & \sum_{i=1}^{|Q(\chi,\mathcal{O}(\omega))|}\begin{cases}
\rho & \mathit{if}\,Q(\chi,\mathcal{O}(\omega))_{i}=\mathit{DEC}(\xi)\wedge\xi(\omega)=\rho\\
0 & \mathit{otherwise}
\end{cases}\\
\mathit{AMC}(\omega) & = & \sum_{\alpha\in\mathit{dom}(\chi)}\sum_{i=1}^{|Q(\chi,\alpha)|}\begin{cases}
1 & \mathit{if}\,\omega\in\mathit{Reach}(\chi,\alpha,Q(\chi,\alpha)_{i})\\
0 & \mathit{otherwise}
\end{cases}\\
\mathit{FRC}(\omega) & = & \sum_{\alpha\neq\mathcal{O}(\omega)}\chi(\alpha)\downarrow_{8}(\omega)
\end{array}$
\end_inset


\end_layout

\begin_layout Standard
The reference count invariant is maintained in the same way for passive
 objects as for actors.
\end_layout

\begin_layout Standard
The reachability reference count invariant for objects differs from the
 actor reachability reference count invariant in several ways.
 When determining which queues should be examined, the owning actor 
\begin_inset Formula $\alpha=\mathcal{O}(\omega)$
\end_inset

 is considered.
 Rather than an object 
\begin_inset Formula $\omega$
\end_inset

 tracking its own local reference count, the owning actor 
\begin_inset Formula $\alpha$
\end_inset

 for 
\begin_inset Formula $\omega$
\end_inset

 tracks the local reference count for 
\begin_inset Formula $\omega$
\end_inset

 in the external map of 
\begin_inset Formula $\alpha$
\end_inset

.
 When examining 
\emph on
INC 
\emph default
and 
\emph on
DEC
\emph default
 messages, external sets are examined rather than a scalar reference count
 value.
\end_layout

\begin_layout Definition
\begin_inset CommandInset label
LatexCommand label
name "Reachability-invariant"

\end_inset

Reachability invariant
\end_layout

\begin_layout Definition
\begin_inset Formula $\forall\alpha,\omega.[\alpha\neq\mathcal{O}(\omega)\wedge\omega\in\mathit{Reach}(\chi,\alpha,\mathtt{ref})\Rightarrow\chi(\mathcal{O}(\omega))\downarrow_{8}(\omega)>0\wedge\chi(\alpha)\downarrow_{8}(\omega)>0]$
\end_inset


\end_layout

\begin_layout Subsection
Sending a Reference
\end_layout

\begin_layout Standard
When a sending a message that can reach some object 
\begin_inset Formula $\omega$
\end_inset

, 
\emph on
ORCA
\emph default
 must perform a reference count adjustment.
 This is accounted for by changing the definition of 
\begin_inset Formula $\mathit{Send}$
\end_inset

 when a passive object is being sent (previously defined in definition 
\begin_inset CommandInset ref
LatexCommand ref
reference "Sending-a-reference"

\end_inset

) to perform reference a reference count adjustment, as defined by 
\begin_inset Formula $\mathit{Adj}$
\end_inset

 in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Auxiliary-definitions-for-object-gc"

\end_inset

.
\end_layout

\begin_layout Definition
\begin_inset CommandInset label
LatexCommand label
name "def:Sending-a-reference-1"

\end_inset

Sending a reference
\end_layout

\begin_layout Definition
\begin_inset Formula $\begin{array}{lcl}
\mathit{Send}(\chi,\alpha,\omega) & = & \mathit{Adj}(\chi,\alpha,\omega,1)\end{array}$
\end_inset


\end_layout

\begin_layout Standard
Note that 
\begin_inset Formula $\mathit{Adj}$
\end_inset

 is defined such that if 
\begin_inset Formula $\alpha$
\end_inset

 is the owner of 
\begin_inset Formula $\omega$
\end_inset

, then 
\begin_inset Formula $\alpha$
\end_inset

 adds 
\begin_inset Formula $n$
\end_inset

 (here, 
\begin_inset Formula $-1$
\end_inset

 ) to its local reference count for 
\begin_inset Formula $\omega$
\end_inset

.
 On the other hand, if 
\begin_inset Formula $\alpha$
\end_inset

 is not the owner of 
\begin_inset Formula $\omega$
\end_inset

, then 
\begin_inset Formula $\alpha$
\end_inset

 subtracts 
\begin_inset Formula $n$
\end_inset

 from its foreign reference count for 
\begin_inset Formula $\omega$
\end_inset

.
\end_layout

\begin_layout Subsection
Receiving a Reference
\end_layout

\begin_layout Standard
As with sending a reference to an object, when receiving a reference to
 some object 
\begin_inset Formula $\omega$
\end_inset

, 
\emph on
ORCA
\emph default
 must also perform a reference count adjustment.
 The definition of 
\begin_inset Formula $\mathit{Recv}$
\end_inset

, previously defined in definition 
\begin_inset CommandInset ref
LatexCommand ref
reference "Receiving-a-reference"

\end_inset

, is altered in the same way as 
\begin_inset Formula $\mathit{Send}$
\end_inset

, performing a reference count adjustment for passive objects.
\end_layout

\begin_layout Definition
\begin_inset CommandInset label
LatexCommand label
name "def:Receiving-a-reference-1"

\end_inset

Receiving a reference
\end_layout

\begin_layout Definition
\begin_inset Formula $\begin{array}{lcl}
\mathit{Recv}(\chi,\alpha,\omega) & = & \mathit{Adj}(\chi,\alpha,\omega,-1)\end{array}$
\end_inset


\end_layout

\begin_layout Subsection
Actor Local Execution
\end_layout

\begin_layout Standard
The operational semantics in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:opsem-for-object-GC"

\end_inset

 extends the semantics presented in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:opsem-for-actor-GC"

\end_inset

.
 Rules from figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:opsem-for-actor-GC"

\end_inset

 that are not listed remain unchanged from 
\emph on
MAC.
\end_layout

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

\begin_layout Plain Layout
\align center
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
makebox[
\backslash
textwidth][c]{
\end_layout

\end_inset


\begin_inset Formula $\begin{array}{ccc}
\dfrac{\begin{array}{c}
\neg\chi(\alpha)\downarrow_{9}\quad\mathit{INC}(\xi)\cdot\overline{\mu}=\chi(\alpha)\downarrow_{3}\\
\chi'=\mathit{Adj}(\chi,\alpha,\xi)
\end{array}}{\chi,\alpha,\varepsilon\rightsquigarrow\chi'[\alpha\mapsto\overline{\mu}],\alpha,\varepsilon}\;\textrm{\textsc{Inc}} &  & \dfrac{\begin{array}{c}
\neg\chi(\alpha)\downarrow_{9}\quad\mathit{DEC}(\xi)\cdot\overline{\mu}=\chi(\alpha)\downarrow_{3}\\
\chi'=\mathit{Adj}(\chi,\alpha,-\xi)
\end{array}}{\chi,\alpha,\varepsilon\rightsquigarrow\chi'[\alpha\mapsto\overline{\mu}],\alpha,\varepsilon}\;\textrm{\textsc{Dec}}\\
\\
\dfrac{\begin{array}{c}
\neg\chi(\alpha)\downarrow_{9}\quad\alpha\neq\alpha'\\
\iota s\subseteq\mathit{dom}(\chi(\alpha)\downarrow_{8})\\
\forall\iota\in\iota s.[\mathcal{O}(\iota)=\alpha'\wedge\chi(\alpha)\downarrow_{8}(\iota)>0]\\
\xi=[\iota\mapsto n\,|\,\iota\in\iota s]\\
\chi'=\mathit{Adj}(\chi[\alpha,\alpha'++\mathit{INC}(\xi)],\alpha,-\xi)
\end{array}}{\chi,\alpha\cdot\overline{\varphi},\mathtt{e}\rightsquigarrow\chi',\alpha\cdot\overline{\varphi},\mathtt{e}}\;\textrm{\textsc{Acquire}} &  & \dfrac{\begin{array}{c}
\neg\chi(\alpha)\downarrow_{9}\quad\alpha\neq\alpha'\\
\iota s\subseteq\mathit{dom}(\chi(\alpha)\downarrow_{8})\backslash\mathit{Reach}(\chi,\alpha,\mathtt{ref})\\
\forall\iota\in\iota s.[\mathcal{O}(\iota)=\alpha'\wedge\chi(\alpha)\downarrow_{8}(\iota)>0]\\
\xi=[\iota\mapsto\chi(\alpha)\downarrow_{8}(\iota)\,|\,\iota\in\iota s]\\
\chi'=\mathit{Rel}(\chi[\alpha,\alpha'++\mathit{DEC}(\xi)],\alpha,\iota s)
\end{array}}{\chi,\alpha,\varepsilon\rightsquigarrow\chi',\alpha,\varepsilon}\;\textrm{\textsc{Release}}
\end{array}$
\end_inset


\begin_inset ERT
status open

\begin_layout Plain Layout

}
\end_layout

\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset VSpace bigskip
\end_inset


\end_layout

\begin_layout Plain Layout
\align center
\begin_inset Formula $\dfrac{\begin{array}{c}
\omega\in\mathit{dom}(\chi)\quad\omega\notin\mathit{Reach}(\chi,\alpha,\mathtt{ref})\\
\mathcal{O}(\omega)=\alpha\quad\chi(\alpha)\downarrow_{8}(\omega)\not>0
\end{array}}{\chi,\alpha\cdot\overline{\varphi},\mathtt{e}\rightsquigarrow\chi\backslash\omega,\alpha\cdot\overline{\varphi},\mathtt{e}}\;\textrm{\textsc{Collect}}$
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset Caption Standard

\begin_layout Plain Layout
\begin_inset CommandInset label
LatexCommand label
name "fig:opsem-for-object-GC"

\end_inset

Operational semantics of object GC
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

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

\begin_layout Plain Layout
\align center
\begin_inset Formula $\begin{array}{lcl}
\mathit{Adj}(\chi,\alpha,\xi) & = & \mathit{Adj}(\mathit{Adj}(\chi,\alpha,\iota,\xi(\iota)),\alpha,\xi\backslash\iota)\,\mathit{where}\,\iota\in\mathit{dom}(\xi)\\
\mathit{Adj}(\chi,\alpha,\emptyset) & = & \chi\\
\mathit{Adj}(\chi,\alpha,\omega,n) & = & \chi[\alpha\mapsto(\chi(\alpha)\downarrow_{1}...\chi(\alpha)\downarrow_{7},\\
 &  & \quad\chi(\alpha)\downarrow_{8}[\omega\mapsto(\chi(\alpha)\downarrow_{8}(\omega)-n)],\chi(\alpha)\downarrow_{9})]\\
 &  & \quad\mathit{if}\,\alpha\neq\mathcal{O}(\omega)\wedge\chi(\alpha)\downarrow_{8}(\omega)>n\\
\mathit{Adj}(\chi,\alpha,\omega,n) & = & \chi[\alpha\mapsto(\chi(\alpha)\downarrow_{1}...\chi(\alpha)\downarrow_{7},\\
 &  & \quad\chi(\alpha)\downarrow_{8}[\omega\mapsto(\chi(\alpha)\downarrow_{8}(\iota)+n)],\chi(\alpha)\downarrow_{9})]\\
 &  & \quad\mathit{if}\,\alpha=\mathcal{O}(\omega)\\
-\xi & = & [\iota\mapsto-\rho\,|\,\xi(\iota)=\rho]\\
\chi(\alpha)\downarrow_{8}(\omega)\not>0 & \mathit{iff} & \omega\notin\mathit{dom}(\chi(\alpha)\downarrow_{8})\vee\chi(\alpha)\downarrow_{8}(\omega)=0
\end{array}$
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset Caption Standard

\begin_layout Plain Layout
\begin_inset CommandInset label
LatexCommand label
name "fig:Auxiliary-definitions-for-object-gc"

\end_inset

Auxiliary definitions for object GC
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
The 
\noun on
Inc
\noun default
 and 
\noun on
Dec 
\noun default
rules are modified such that the message carries an 
\begin_inset Formula $\mathit{ExMap}$
\end_inset

, a mapping of address to reference count, rather than a scalar value.
 This allows an 
\emph on
INC 
\emph default
or 
\emph on
DEC 
\emph default
message to carry reference count adjustment information for a collection
 of addresses.
 In practice, this is some set of passive objects all owned by the same
 actor 
\begin_inset Formula $\alpha$
\end_inset

, and possibly 
\begin_inset Formula $\alpha$
\end_inset

 itself.
 Passive objects owned by other actors, and indeed other actors themselves,
 will not appear in 
\emph on
INC
\emph default
 or 
\emph on
DEC
\emph default
 messages delivered to 
\begin_inset Formula $\alpha$
\end_inset

, as they are not owned by 
\begin_inset Formula $\alpha$
\end_inset

.
\end_layout

\begin_layout Standard
Note that both 
\noun on
Inc
\noun default
 and 
\noun on
Dec
\noun default
 require the actor to 
\noun on
Unblock
\noun default
 if they are blocked.
 This is to ensure that an actor 
\begin_inset Formula $\alpha$
\end_inset

 does not send a 
\emph on
MAC
\emph default
\noun on
 
\emph on
\noun default
ACK
\emph default
 message to the cycle detector when in fact the cycle detector's view of
 the reference count of 
\begin_inset Formula $\alpha$
\end_inset

 is out of date.
 This requirement can be optimised away by keeping a per-actor flag indicating
 when the actor has altered its reference count due to an 
\emph on
INC 
\emph default
or 
\emph on
DEC
\emph default
 while blocked.
 When this flag is set, 
\emph on
ACK
\emph default
 messages are suppressed, and the flag is unset when the actor unblocks.
\end_layout

\begin_layout Standard
The 
\noun on
Acquire 
\noun default
and 
\noun on
Release 
\noun default
rules are modified to allow the executing actor to acquire and release reference
 counts for passive objects as well as actors.
 Each rule allows generating a single message (
\emph on
INC
\emph default
 and 
\emph on
DEC
\emph default
, respectively) to a single destination.
 As such, only the destination actor and passive objects owned by the destinatio
n actor are considered.
 As with 
\emph on
MAC
\emph default
, the executing actor must hold a foreign reference count of 1 or more for
 an address in order to acquire more reference count weight, and must both
 hold a foreign reference count weight and not be able to reach the address
 in order to release that weight.
\end_layout

\begin_layout Standard
Note that 
\noun on
Acquire
\noun default
 uses 
\begin_inset Formula $-\xi$
\end_inset

 rather than 
\begin_inset Formula $\xi$
\end_inset

, as 
\begin_inset Formula $\alpha$
\end_inset

 wishes to add to, rather than subtract from, its foreign reference counts
 for 
\begin_inset Formula $\iota s$
\end_inset

.
 Since 
\begin_inset Formula $\mathit{Adj}$
\end_inset

 is defined in terms of sending and receiving, it must be reversed for 
\noun on
Acquire.
\end_layout

\begin_layout Standard
The 
\noun on
Collect
\noun default
 rule allows for removal of a passive object 
\begin_inset Formula $\omega$
\end_inset

 from the heap when 
\begin_inset Formula $\omega$
\end_inset

 is not reachable from the owning actor and the owning actor holds no local
 reference count weight for 
\begin_inset Formula $\omega$
\end_inset

.
 This allows local heap collection by the owning actor using any mechanism
 for local heap tracing.
\end_layout

\begin_layout Standard
Note that in the definition of 
\begin_inset Formula $\mathit{Adj}$
\end_inset

 in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Auxiliary-definitions-for-object-gc"

\end_inset

, although the choice of 
\begin_inset Formula $\iota$
\end_inset

 in the first case is arbitrary, the definition is deterministic.
 The order in which adjustments to addresses in 
\begin_inset Formula $\xi$
\end_inset

 are applied does not affect the result.
\end_layout

\begin_layout Section
Completeness
\end_layout

\begin_layout Standard
The presented object garbage collection semantics allow the 
\noun on
Collect
\noun default
 rule to be executed non-deterministically.
 This models real world garbage collection scenarios, wherein there can
 be many heuristics to determine at what point garbage collection should
 occur.
 As such, it is possible for a program to run to completion (i.e.
 achieve actor quiescence) without collecting any passive object garbage.
 Indeed, some small real world programs written in Pony do exactly this.
\end_layout

\begin_layout Standard
However, these semantics allow all globally unreachable passive objects
 to be collected, while not strictly requiring that such collection takes
 place.
 Objects that are not sent in messages are collectable via 
\noun on
Collect
\noun default
, and objects that have been sent in messages will eventually be collectable
 after receiving actors either no longer reference the object and send a
 
\emph on
DEC
\emph default
 message via 
\noun on
Release
\noun default
, or are themselves collected (as in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:opsem-cycle-detection"

\end_inset

), which also generates a 
\emph on
DEC
\emph default
 message.
\end_layout

\begin_layout Section
Robustness
\end_layout

\begin_layout Standard
The semantics for 
\emph on
ORCA
\emph default
 are sound and do not have exceptional conditions.
 However, as with 
\emph on
MAC
\emph default
, 
\emph on
ORCA
\emph default
 is robust even when failure is introduced.
\end_layout

\begin_layout Standard
The robustness conditions are similar to those for 
\emph on
MAC
\emph default
, described in section 
\begin_inset CommandInset ref
LatexCommand ref
reference "sec:Robustness"

\end_inset

.
 The failure of a some actor 
\begin_inset Formula $\alpha$
\end_inset

 will cause objects 
\begin_inset Formula $\alpha$
\end_inset

 has allocated to never be collected, even if they become globally unreachable.
 Similarly, any objects for which 
\begin_inset Formula $\alpha$
\end_inset

 held a foreign reference count will not be collected by their owners, as
 
\begin_inset Formula $\alpha$
\end_inset

 will never send 
\emph on
DEC
\emph default
 messages for those objects.
 However, again similar to 
\emph on
MAC
\emph default
, such failures impact completeness, but do not result in objects being
 prematurely collected.
\end_layout

\begin_layout Standard
The impact of individual message failure depends on the message type.
 For 
\emph on
APP
\emph default
 and 
\emph on
DEC
\emph default
 messages, an object 
\begin_inset Formula $\omega$
\end_inset

 contained in such a messages will never be collected, as the implicit reference
 to 
\begin_inset Formula $\omega$
\end_inset

 in 
\emph on
APP
\emph default
, or the explicit reference count in 
\emph on
DEC
\emph default
, will be lost.
 However, a lost 
\emph on
INC
\emph default
 message can result in premature object collection, making 
\emph on
ORCA
\emph default
 unsound in the face of individual message loss.
\end_layout

\begin_layout Standard
However, the mediating factors described in section 
\begin_inset CommandInset ref
LatexCommand ref
reference "sec:Robustness"

\end_inset

 remain true for 
\emph on
ORCA
\emph default
: due to the actor-model requirement of guaranteed delivery, individual
 message failure can be treated as actor failure, reducing the soundness
 failure to a completeness failure.
 In Pony, individual actors and messages in the concurrent setting (or on
 a single node in the distributed setting) do not fail, removing even the
 completeness impact.
\end_layout

\begin_layout Standard
Interestingly, another possible failure mode is integer overflow in reference
 counts.
 In the formal model, unbounded integers are used, and this problem does
 not occur.
 In the implementation, bounded integers are used, and it might be possible
 to overflow a reference count, for example if the owner 
\begin_inset Formula $\alpha$
\end_inset

 of 
\begin_inset Formula $\omega$
\end_inset

 sends 
\begin_inset Formula $\omega$
\end_inset

 to some other actor 
\begin_inset Formula $\alpha'$
\end_inset

 
\begin_inset Formula $2^{64}$
\end_inset

 times without 
\begin_inset Formula $\alpha'$
\end_inset

 performing a 
\noun on
Release
\noun default
 for 
\begin_inset Formula $\omega$
\end_inset

.
 In this circumstance, the implementation should treat the reference count
 of 
\begin_inset Formula $\omega$
\end_inset

 as infinite, preserving robustness, but not completeness.
\end_layout

\begin_layout Section
Distributed Object GC
\end_layout

\begin_layout Standard
The reduction in the ordering guarantee from causal order in the concurrent
 setting to pairwise FIFO order in the distributed setting would initially
 appear to make 
\emph on
ORCA
\emph default
 as described unsound.
 However, the data-race free type system described in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Reference-Capabilities"

\end_inset

 combined with the necessity for copying objects when they are sent between
 distributed nodes (generally by serialising the object over a network,
 as distributed nodes do not share memory between nodes) means that 
\emph on
ORCA
\emph default
 remains sound in the distributed setting.
 As with distributed actor collection, it is important to note that distributed
 object collection has not yet been implemented in the runtime.
 As such, this section represents a sketch of a possible implementation,
 rather than a description of completed work.
\end_layout

\begin_layout Subsection
Locally Fulfilled Object Capabilities
\end_layout

\begin_layout Standard

\noun on
WF-Async
\noun default
 in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Well-formed-programs"

\end_inset

 requires that behaviour arguments are 
\begin_inset Formula $\mathit{Sendable}$
\end_inset

, i.e.
 
\begin_inset Formula $\mathtt{iso}$
\end_inset

, 
\begin_inset Formula $\mathtt{val}$
\end_inset

, or 
\begin_inset Formula $\mathtt{tag}$
\end_inset

.
 Each of these cases will be examined.
\end_layout

\begin_layout Standard
When an actor 
\begin_inset Formula $\alpha_{1}$
\end_inset

 on node 
\begin_inset Formula $\mathcal{N}_{1}$
\end_inset

 sends an 
\begin_inset Formula $\mathtt{iso}$
\end_inset

 reference to object 
\begin_inset Formula $\omega$
\end_inset

 to another actor 
\begin_inset Formula $\alpha_{2}$
\end_inset

 on node 
\begin_inset Formula $\mathcal{N}_{2}$
\end_inset

, the deny properties of 
\begin_inset Formula $\mathtt{iso}$
\end_inset

 guarantee that no actor other than 
\begin_inset Formula $\alpha_{2}$
\end_inset

 can read from or write to 
\begin_inset Formula $\omega$
\end_inset

.
 As a result, the deserialised copy of 
\begin_inset Formula $\omega$
\end_inset

 on 
\begin_inset Formula $\mathcal{N}_{2}$
\end_inset

 is the authoritative representation of 
\begin_inset Formula $\omega$
\end_inset

.
 As such, if 
\begin_inset Formula $\omega$
\end_inset

 becomes unreachable on 
\begin_inset Formula $\mathcal{N}_{2}$
\end_inset

, without accounting for reachability on any other node, it is safe for
 
\begin_inset Formula $\alpha_{2}$
\end_inset

 to collect 
\begin_inset Formula $\omega$
\end_inset

.
 References on other nodes may survive, but they will be 
\begin_inset Formula $\mathtt{tag}$
\end_inset

 references, so the collection of 
\begin_inset Formula $\omega$
\end_inset

 is sound.
\end_layout

\begin_layout Standard
When an actor 
\begin_inset Formula $\alpha_{1}$
\end_inset

 on node 
\begin_inset Formula $\mathcal{N}_{1}$
\end_inset

 sends a 
\begin_inset Formula $\mathtt{val}$
\end_inset

 reference to object 
\begin_inset Formula $\omega$
\end_inset

 to another actor 
\begin_inset Formula $\alpha_{2}$
\end_inset

 on node 
\begin_inset Formula $\mathcal{N}_{2}$
\end_inset

, the deny properties of 
\begin_inset Formula $\mathtt{val}$
\end_inset

 guarantee that no actor can write to 
\begin_inset Formula $\omega$
\end_inset

.
 As such, any copy of 
\begin_inset Formula $\omega$
\end_inset

 on any node is an authoritative representation of 
\begin_inset Formula $\omega$
\end_inset

.
 As such, if 
\begin_inset Formula $\omega$
\end_inset

 becomes unreachable on any node, without accounting for reachability on
 any other node, it is safe for 
\begin_inset Formula $\omega$
\end_inset

 to be collected on that node.
 References on other nodes may survive, and will remain authoritative.
\end_layout

\begin_layout Standard
Finally, when an actor 
\begin_inset Formula $\alpha_{1}$
\end_inset

 on node 
\begin_inset Formula $\mathcal{N}_{1}$
\end_inset

 sends a 
\begin_inset Formula $\mathtt{tag}$
\end_inset

 reference to object 
\begin_inset Formula $\omega$
\end_inset

 to another actor 
\begin_inset Formula $\alpha_{2}$
\end_inset

 on node 
\begin_inset Formula $\mathcal{N}_{2}$
\end_inset

, that reference cannot be used to read from or write to 
\begin_inset Formula $\omega$
\end_inset

.
 The fields of 
\begin_inset Formula $\omega$
\end_inset

 need not be serialised when sending such a reference.
 If 
\begin_inset Formula $\omega$
\end_inset

 becomes unreachable on 
\begin_inset Formula $\mathcal{N}_{2}$
\end_inset

, without accounting for reachability on any other node, it is safe for
 
\begin_inset Formula $\omega$
\end_inset

 to be collected on 
\begin_inset Formula $\mathcal{N}_{2}$
\end_inset

.
 References on other nodes may survive, and, if they allow reading from
 or writing to 
\begin_inset Formula $\omega$
\end_inset

, will remain authoritative.
\end_layout

\begin_layout Standard
The combination of the introduction requirement and deny properties results
 in a distributed system wherein object references are always able to fulfil
 their interfaces (i.e.
 provide capabilities allowed by the type system) locally, without communication
 with other nodes.
 Asynchronous messages to actors, i.e.
 behaviour invocations, may result in communication with other nodes, but
 synchronous calls to actors or objects, i.e.
 function invocations, will not.
\end_layout

\begin_layout Subsection
Distributed Object Identity
\end_layout

\begin_layout Standard
An object's identity in the concurrent setting, or on a single node in the
 distributed setting, is the object's address in the heap.
 However, when an actor 
\begin_inset Formula $\alpha_{1}$
\end_inset

 on node 
\begin_inset Formula $\mathcal{N}_{1}$
\end_inset

 sends a reference to some object 
\begin_inset Formula $\omega$
\end_inset

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

 on node 
\begin_inset Formula $\mathcal{N}_{2}$
\end_inset

, it is not feasible to require that 
\begin_inset Formula $\alpha_{2}$
\end_inset

 instantiate 
\begin_inset Formula $\omega$
\end_inset

 on 
\begin_inset Formula $\mathcal{N}_{2}$
\end_inset

 with the same heap address that 
\begin_inset Formula $\omega$
\end_inset

 has on 
\begin_inset Formula $\mathcal{N}_{1}$
\end_inset

.
 The language must either accept that an object loses its identity when
 sent in a message to an actor that happens to be executing on another node,
 which would break the equivalence of the concurrent and distributed operational
 semantics, or some mechanism for mapping the identity of 
\begin_inset Formula $\omega$
\end_inset

 on 
\begin_inset Formula $\mathcal{N}_{1}$
\end_inset

 to its identity on 
\begin_inset Formula $\mathcal{N}_{2}$
\end_inset

 must be provided.
\end_layout

\begin_layout Standard
It is important that such a mechanism not introduce a new garbage collection
 problem in the form of garbage collecting assigned global identities.
 For example, if 
\begin_inset Formula $\mathcal{N}_{2}$
\end_inset

 were to provide a local mapping of 
\begin_inset Formula $\mathcal{N}_{1}$
\end_inset

 heap addresses to 
\begin_inset Formula $\mathcal{N}_{2}$
\end_inset

 heap addresses, 
\begin_inset Formula $\mathcal{N}_{2}$
\end_inset

 would need to inform all nodes in the distributed system when any address
 on 
\begin_inset Formula $\mathcal{N}_{2}$
\end_inset

 that had been sent to any node was garbage collected, in order to prevent
 out-of-date mappings resulting in a new object at address 
\begin_inset Formula $\omega$
\end_inset

 on 
\begin_inset Formula $\mathcal{N}_{1}$
\end_inset

 having the same identity as the previous object at address 
\begin_inset Formula $\omega$
\end_inset

 on 
\begin_inset Formula $\mathcal{N}_{1}$
\end_inset

 that had been sent to 
\begin_inset Formula $\mathcal{N}_{2}$
\end_inset

.
\end_layout

\begin_layout Standard
Similarly, any system of non-random identities must cope with namespace
 issues (
\begin_inset Formula $\mathcal{N}_{1}$
\end_inset

 must not assign an identity that 
\begin_inset Formula $\mathcal{N}_{2}$
\end_inset

 might assign).
 Assigning namespaces is complex in a distributed system due to network
 splits and joins.
 That is, if 
\begin_inset Formula $\mathcal{N}_{1}$
\end_inset

 and 
\begin_inset Formula $\mathcal{N}_{2}$
\end_inset

 each take on the namespace assignment role after a network split, if the
 network split is healed, 
\begin_inset Formula $\mathcal{N}_{1}$
\end_inset

 and 
\begin_inset Formula $\mathcal{N}_{2}$
\end_inset

 may have assigned the same namespace to different nodes.
\end_layout

\begin_layout Standard
One possible approach is to assign a sufficiently long and sufficiently
 random identifier to any object sent to another node.
 This provides a probabilistic approach to distributed object identity that
 requires no garbage collection.
 The probability of a distributed object identity collision can be approximated
 by treating the distributed system as if it were executing a birthday attack
 on itself, which gives a probability 
\begin_inset Formula $p$
\end_inset

 for a number of distributed objects 
\begin_inset Formula $n$
\end_inset

 with a random identifier length of 
\begin_inset Formula $k$
\end_inset

 bits as 
\begin_inset Formula $p(n,k)=1-e^{-n(n-1)/2^{k+1}}$
\end_inset

.
 For example, if the acceptable risk of an object identity collision is
 
\begin_inset Formula $p=10^{-12}$
\end_inset

, a 128-bit object identity allows approximately 
\begin_inset Formula $2^{45}$
\end_inset

 objects to be created, or a 256-bit object identity allows approximately
 
\begin_inset Formula $2^{109}$
\end_inset

 objects to be created.
\end_layout

\begin_layout Standard
To reduce the computational overhead of calculating such random numbers
 for every object sent to another node, each node 
\begin_inset Formula $\mathcal{N}$
\end_inset

 can create a random identity for itself, 
\begin_inset Formula $\mathcal{N}_{id}$
\end_inset

, when the node joins the distributed system, and use a monotonic counter
 
\begin_inset Formula $c$
\end_inset

 to assign object identities of the form 
\begin_inset Formula $\mathcal{N}_{id}\cdot c$
\end_inset

.
 For the same 
\begin_inset Formula $p=10^{-12}$
\end_inset

 risk, a 128-bit node identifier and a 64-bit monotonic counter allows approxima
tely 
\begin_inset Formula $2^{45}$
\end_inset

 nodes and 
\begin_inset Formula $2^{64}$
\end_inset

 objects per node.
\end_layout

\begin_layout Section
Using 
\emph on
ORCA
\emph default
 in Other Actor-Model Languages
\end_layout

\begin_layout Standard
As an extension of 
\emph on
MAC
\emph default
, using 
\emph on
ORCA
\emph default
 in another actor-model language would be possible with the same caveats
 described in section 
\begin_inset CommandInset ref
LatexCommand ref
reference "sec:Using-MAC-in"

\end_inset

.
 Additionally, 
\emph on
ORCA
\emph default
 requires that the 
\emph on
introduction requirement
\emph default
 
\begin_inset CommandInset citation
LatexCommand cite
key "agha1986actors"

\end_inset

 of the actor model, described in section 
\begin_inset CommandInset ref
LatexCommand ref
reference "sec:Single-Model-for"

\end_inset

, not be violated.
 If the introduction requirement were to be violated, then it would be possible
 for some actor 
\begin_inset Formula $\alpha$
\end_inset

 to be able to reach some object 
\begin_inset Formula $\omega$
\end_inset

 allocated by some other actor 
\begin_inset Formula $\alpha'$
\end_inset

 without 
\begin_inset Formula $\alpha$
\end_inset

 having either created 
\begin_inset Formula $\omega$
\end_inset

 or received 
\begin_inset Formula $\omega$
\end_inset

 in a message.
 As a result, 
\begin_inset Formula $\alpha$
\end_inset

 might not hold a positive foreign reference count for 
\begin_inset Formula $\omega$
\end_inset

, and 
\begin_inset Formula $\alpha'$
\end_inset

 might prematurely collect 
\begin_inset Formula $\omega$
\end_inset

.
\end_layout

\begin_layout Standard
The BEAM runtime, being built specifically for as an actor-model runtime,
 does not violate the introduction requirement, and so languages built on
 top of it, such as Erlang and Elixir, could use 
\emph on
ORCA
\emph default
, again with the same caveats regarding causality and non-atomic behaviours
 as for 
\emph on
MAC
\emph default
.
 On the other hand, Akka, being built on JVM languages that allow non-actor
 concurrency, does not enforce the introduction requirement, and so 
\emph on
ORCA
\emph default
 would be unsound.
\end_layout

\end_body
\end_document