opsem.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
\noindent
\begin_inset CommandInset label
LatexCommand label
name "chap:Syntax-and-Operational"

\end_inset

Syntax and Operational Semantics
\end_layout

\begin_layout Standard
The syntax and operational semantics of Pony is presented here as a small-step
 operational semantics that expresses a simplified subset of the full Pony
 language.
 Additional features in the full language can be encoded in this subset,
 including control structures, exception handling, algebraic data types
 (tuples, unions, and intersections), machine word types, singleton types,
 C ABI compatible structures, single-assignment fields and variables, embedded
 fields, nominal and structural subtyping via traits and interfaces, object
 literals, lambdas, partial application, pattern matching, case functions,
 and generic types and methods.
 Various forms of syntactic sugar are also used in the full language to
 allow for more succinct code.
\end_layout

\begin_layout Standard
The syntax and formalisation of inheritance, union types, tuples, and intersecti
on types appears in Steed 
\begin_inset CommandInset citation
LatexCommand cite
key "steed2016"

\end_inset

.
 The syntax and formalisation of generics, value-dependent types, and compile-ti
me expressions appears in Cheeseman 
\begin_inset CommandInset citation
LatexCommand cite
key "cheeseman2016"

\end_inset

.
 The operational semantics presented here differs from previous work 
\begin_inset CommandInset citation
LatexCommand cite
key "clebsch2015deny"

\end_inset

, particularly in the treatment of message sends and in providing a distributed
 semantics.
\end_layout

\begin_layout Section
Syntax
\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}{rcccl}
\mathtt{P} & \in & \mathit{Program} & ::= & \mathtt{\overline{CT}\,\overline{AT}}\\
\mathtt{CT} & \in & \mathit{ClassDef} & ::= & \mathtt{class\,C\,\overline{F}\,\overline{K}\,\overline{M}}\\
\mathtt{AT} & \in & \mathit{ActorDef} & ::= & \mathtt{actor\,A\,\overline{F}\,\overline{K}\,\overline{M}\,\overline{B}}\\
\mathtt{S} & \in & \mathit{TypeID} & ::= & \mathtt{A\,|\,C}\\
\mathtt{T} & \in & \mathit{Type} & ::= & \mathtt{S\,\kappa}\\
\mathtt{ET} & \in & ExtType & ::= & \mathtt{T\,|\,S\,\kappa\circ}\\
\mathtt{F} & \in & \mathit{Field} & ::= & \mathtt{var\,f:T}\\
\mathtt{K} & \in & \mathit{Ctor} & ::= & \mathtt{new\,k(\overline{x}:\overline{T})\Rightarrow e}\\
\mathtt{M} & \in & \mathit{Func} & ::= & \mathtt{fun\,\kappa\,m(\overline{x}:\overline{T}):ET\Rightarrow e}\\
\mathtt{B} & \in & \mathit{Behv} & ::= & \mathtt{be\,b(\overline{x}:\overline{T})\Rightarrow e}\\
\mathtt{n} & \in & \mathit{MethodID} & ::= & \mathtt{k\,|\,m\,|\,b}\\
\mathtt{\kappa} & \in & \mathit{Cap} & ::= & \mathtt{iso\,|\,trn\,|\,ref\,|\,val\,|\,box\,|\,tag}\\
\mathtt{e} & \in & \mathit{Expr} & ::= & \mathtt{this\,|\,x\,|\,var\,x:T\,|\,x=e\,|\,e;e\,|\,e.f}\\
 &  &  & | & \mathtt{e.f=e\,|\,consume\,x\,|\,recover\,e}\\
 &  &  & | & \mathtt{e.m(\overline{e})\,|\,e.b(\overline{e})\,|\,S.k(\overline{e})}\\
\mathtt{E[\cdot]} & \in & \mathit{ExprHole} & ::= & \mathtt{x=E[\cdot]\,|\,E[\cdot];e\,|\,(E[\cdot])\,|\,E[\cdot].f}\\
 &  &  & | & \mathtt{e.f=E[\cdot]\,|\,E[\cdot].f=z\,|\,E[\cdot].n(\overline{z})}\\
 &  &  & | & \mathtt{e.n(\overline{z},E[\cdot],\overline{e})\,|\,recover\,E[\cdot]}
\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:Syntax"

\end_inset

Syntax
\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}{rclcccl}
\mathtt{C} & \in & \mathit{ClassID} &  & \mathtt{k} & \in & \mathit{CtorID}\\
\mathtt{A} & \in & \mathit{ActorID} &  & \mathtt{m} & \in & \mathit{FuncID}\\
\mathtt{f} & \in & \mathit{FieldID} &  & \mathtt{b} & \in & \mathit{BehvID}\\
\mathtt{this,x} & \in & \mathit{SourceID} &  & \mathtt{n} & \in & \mathit{CtorID\cup BehvID}\\
\mathtt{t} & \in & \mathit{TempID} &  & \mathtt{y,z} & \in & \mathit{LocalID}
\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:Identifiers"

\end_inset

Identifiers
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
The syntax is presented in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Syntax"

\end_inset

.
 Actors have a type, in the mould of active objects, and are introduced
 with the keyword 
\begin_inset Formula $\mathtt{actor}$
\end_inset

.
 These can have both synchronous methods (
\emph on
functions
\emph default
, introduced through the keyword 
\begin_inset Formula $\mathtt{fun}$
\end_inset

) and asynchronous methods (
\emph on
behaviours
\emph default
, introduced through the keyword 
\begin_inset Formula $\mathtt{be}$
\end_inset

) as well as named constructors (introduced through the keyword 
\begin_inset Formula $\mathtt{new}$
\end_inset

).
\end_layout

\begin_layout Standard
Passive objects (introduced through the keyword 
\begin_inset Formula $\mathtt{class}$
\end_inset

) have only synchronous methods (functions) and constructors.
 The term 
\emph on
method
\emph default
 is used to refer to constructors, functions, and behaviours.
\end_layout

\begin_layout Standard
The novel element of the syntax is the inclusion of
\emph on
 reference capability annotations
\emph default
 
\begin_inset Formula $\kappa$
\end_inset

 on types and functions, where:
\end_layout

\begin_layout Standard
\begin_inset Formula $\kappa\in\{\mathtt{iso,trn,ref,val,box,tag}\}$
\end_inset


\end_layout

\begin_layout Standard
These reference capabilities are the foundation of the Pony type system.
\end_layout

\begin_layout Standard
Types consist of a class or actor identifier 
\begin_inset Formula $\mathtt{S}$
\end_inset

 followed by a reference capability 
\begin_inset Formula $\kappa$
\end_inset

.
 In addition, extended types 
\begin_inset Formula $\mathtt{ET}$
\end_inset

 can be 
\emph on
unaliased
\emph default
, 
\begin_inset Formula $\circ$
\end_inset

.
 An 
\emph on
unaliased type
\emph default
 is created with constructors and destructive reads.
 This is described in detail in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Reference-Capabilities"

\end_inset

.
\end_layout

\begin_layout Standard
The over-bar notation indicates a sequence of elements such as 
\begin_inset Formula $\mathtt{\overline{F}}$
\end_inset

, with the convention that the 
\begin_inset Formula $n^{th}$
\end_inset

 element is referred to as 
\begin_inset Formula $\mathtt{F_{n}}$
\end_inset

.
 Similarly, 
\begin_inset Formula $\mathtt{\overline{x}:\overline{T}}$
\end_inset

 indicates a pairwise sequence of identifiers and types.
 To reduce notation, a 
\emph on
fixed
\emph default
 program 
\begin_inset Formula $\mathtt{P}$
\end_inset

 is assumed.
\end_layout

\begin_layout Section
Operational Semantics
\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}{rclcl}
\chi & \in & \mathit{Heap} & = & \mathit{Addr\rightarrow(Actor\vee Object)}\\
\sigma & \in & \mathit{Stack} & = & \mathit{ActorAddr\cdot\overline{Frame}}\\
\varphi & \in & \mathit{Frame} & = & \mathit{MethodID\times(LocalID\rightarrow Value)}\\
 &  &  & \times & \mathit{ExprHole}\\
 &  & \mathit{LocalID} & = & \mathit{SourceID}\cup\mathit{TempID}\\
v & \in & \mathit{Value} & = & \mathit{Addr\cup\{null\}}\\
\iota & \in & \mathit{Addr} & = & \mathit{ActorAddr\cup ObjectAddr}\\
\alpha & \in & \mathit{ActorAddr}\\
\omega & \in & \mathit{ObjectAddr}\\
 &  & \mathit{Actor} & = & \mathit{ActorID\times(FieldID\rightarrow Value)}\\
 &  &  & \times & \mathit{\overline{Message}}\times Stack\times Expr\\
 &  &  & \times & (\mathit{ActorID}\rightarrow\overline{Message})\\
 &  & \mathit{Object} & = & \mathit{ClassID\times(FieldID\rightarrow Value)}\\
\mu & \in & \mathit{Message} & = & \mathit{MethodID\times\overline{Value}}
\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"

\end_inset

Runtime entities
\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 ERT
status open

\begin_layout Plain Layout


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

\end_inset


\begin_inset Formula $\begin{array}{ccc}
\dfrac{\chi,\sigma\cdot\varphi,\mathtt{e}\rightsquigarrow\chi',\sigma\cdot\varphi',\mathtt{e'}}{\chi,\sigma\cdot\varphi,\mathtt{E[e]}\rightsquigarrow\chi',\sigma\cdot\varphi',\mathtt{E[e']}}\;\textrm{\textsc{ExprHole}} &  & \dfrac{\mathtt{t}\notin\varphi\quad\iota=\varphi(\mathtt{z})\quad\varphi'=\varphi[\mathtt{t}\mapsto\chi(\iota,\mathtt{f})]}{\chi,\sigma\cdot\varphi,\mathtt{z.f}\rightsquigarrow\chi,\sigma\cdot\varphi',\mathtt{t}}\;\textrm{\textsc{Fld}}\\
\\
\dfrac{\mathtt{x}\notin\varphi\quad\varphi'=\varphi[\mathtt{x}\mapsto\mathit{null}]}{\chi,\sigma\cdot\varphi,\mathtt{var\,x:ET}\rightsquigarrow\chi,\sigma\cdot\varphi',\mathit{null}}\;\textrm{\textsc{DeclLocal}} &  & \dfrac{}{\chi,\sigma,\mathtt{z}\mathtt{;e}\rightsquigarrow\chi,\sigma,\mathtt{e}}\;\textrm{\textsc{Seq}}\\
\\
\dfrac{\mathtt{t}\notin\varphi\quad\varphi'=\varphi[\mathtt{x}\mapsto\varphi(\mathtt{z}),\mathtt{t}\mapsto\varphi(\mathtt{x})]}{\chi,\sigma\cdot\varphi,\mathtt{x=z}\rightsquigarrow\chi,\sigma\cdot\varphi',\mathtt{t}}\;\textrm{\textsc{AsnLocal}} &  & \dfrac{\begin{array}{c}
\mathtt{t}\notin\varphi\quad\iota=\varphi(\mathtt{z})\quad\varphi'=\varphi[\mathtt{t}\mapsto\chi(\iota,\mathtt{f})]\\
\chi'=\chi[\varphi(\mathtt{z}),\mathtt{f}\mapsto\varphi(\mathtt{y})]
\end{array}}{\chi,\sigma\cdot\varphi,\mathtt{z.f=y}\rightsquigarrow\chi',\sigma\cdot\varphi',\mathtt{t}}\;\textrm{\textsc{AsnFld}}\\
\\
\dfrac{\begin{array}{c}
\iota=\varphi(\mathtt{z})\quad\mathcal{M}(\chi(\iota)\downarrow_{1},\mathtt{m})=\mathtt{(\_,\overline{x}:\_,e,\_)}\\
\varphi'=(\mathtt{m},[\mathtt{this}\mapsto\iota,\mathtt{\overline{x}}\mapsto\varphi(\mathtt{\overline{y}})],\mathtt{E[\cdot]})
\end{array}}{\chi,\sigma\cdot\varphi,\mathtt{E[z.m(\overline{y})}]\rightsquigarrow\chi,\sigma\cdot\varphi\cdot\varphi',\mathtt{e}}\;\textrm{\textsc{Sync}} &  & \dfrac{\begin{array}{c}
\mathtt{t}\notin\varphi\quad\iota=\varphi'(\mathtt{z})\\
\varphi'\downarrow_{3}=\mathtt{E[\cdot]}\quad\varphi''=\varphi[\mathtt{t}\mapsto\iota]
\end{array}}{\chi,\sigma\cdot\varphi\cdot\varphi',\mathtt{z}\rightsquigarrow\chi,\sigma\cdot\varphi'',\mathtt{E[t]}}\;\textrm{\textsc{Return}}\\
\\
\dfrac{\begin{array}{c}
\alpha'=\varphi(\mathtt{z})\\
\chi'=\chi[\alpha'++(\mathtt{b},\varphi(\mathtt{\overline{y}})]
\end{array}}{\chi,\alpha\cdot\overline{\varphi}\cdot\varphi,\mathtt{z.b(\overline{y})}\rightsquigarrow\chi',\alpha\cdot\overline{\varphi}\cdot\varphi,\mathtt{z}}\;\textrm{\textsc{Async}} &  & \dfrac{\begin{array}{c}
\mathtt{A}=\chi(\alpha)\downarrow_{1}\quad(\mathtt{n},\overline{v})\cdot\overline{\mu}=\chi(\alpha)\downarrow_{3}\\
\mathcal{M}(\mathtt{A,n})=\mathtt{(\_,\overline{x}:\_,e,\_)}\\
\varphi=(\mathtt{n},[\mathtt{this}\mapsto\alpha,\mathtt{\overline{x}}\mapsto\overline{v}],\cdot)
\end{array}}{\chi,\alpha,\varepsilon\rightsquigarrow\chi[\alpha\mapsto\overline{\mu}],\alpha\cdot\varphi,\mathtt{e}}\;\textrm{\textsc{Behave}}\\
\\
\dfrac{\begin{array}{c}
(\omega,\chi')=\mathit{New}(\chi,\mathtt{C})\\
\mathcal{M}(\mathtt{C,k})=\mathtt{(\_,\overline{x}:\_,e,\_)}\\
\varphi'=(\mathtt{k},[\mathtt{this}\mapsto\omega,\mathtt{\overline{x}}\mapsto\varphi(\mathtt{\overline{y}})],\mathtt{E[\cdot]})
\end{array}}{\chi,\sigma\cdot\varphi,\mathtt{E[C.k(\overline{y})]}\rightsquigarrow\chi',\sigma\cdot\varphi\cdot\varphi',\mathtt{e}}\;\textrm{\textsc{Ctor}} &  & \dfrac{\begin{array}{c}
(\alpha,\chi')=\mathit{New}(\chi,\mathtt{A},\mathtt{k},\varphi(\overline{\mathtt{y}}))\\
\mathtt{t}\notin\varphi\quad\varphi'=\varphi[\mathtt{t}\mapsto\alpha]
\end{array}}{\chi,\sigma\cdot\varphi,\mathtt{A.k(\overline{y})}\rightsquigarrow\chi',\sigma\cdot\varphi',\mathtt{t}}\;\textrm{\textsc{Ator}}\\
\\
\dfrac{\mathtt{t}\notin\varphi\quad\varphi'=\varphi[\mathtt{t}\mapsto\varphi(\mathtt{x})]\backslash\mathtt{x}}{\chi,\sigma\cdot\varphi,\mathtt{consume\,x}\rightsquigarrow\chi,\sigma\cdot\varphi',\mathtt{t}}\;\textrm{\textsc{Consume}} &  & \dfrac{\mathtt{t}\notin\varphi\quad\varphi'=\varphi[\mathtt{t}\mapsto\varphi(\mathtt{z})]}{\chi,\sigma,\mathtt{recover\,z}\rightsquigarrow\chi,\sigma,\mathtt{t}}\;\textrm{\textsc{Recover}}
\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 Caption Standard

\begin_layout Plain Layout
\begin_inset CommandInset label
LatexCommand label
name "fig:Local-execution"

\end_inset

Local execution
\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}{c}
\dfrac{\chi,\chi(\alpha)\downarrow_{4},\chi(\alpha)\downarrow_{5}\rightsquigarrow\chi',\sigma,\mathtt{e}}{\chi\rightarrow\chi'[\alpha\mapsto(\sigma,\mathtt{e})]}\;\textrm{\textsc{Global}}\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:Global-execution."

\end_inset

Global execution
\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 Itemize
\begin_inset Formula $\varphi(\mathtt{x})=\varphi\downarrow_{2}(\mathtt{x})\downarrow_{1}$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\varphi[\mathtt{x}\mapsto v]=(\varphi\downarrow_{1},\varphi\downarrow_{2}[\mathtt{x}\mapsto v],\varphi\downarrow_{3})$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\varphi\backslash\mathtt{x}=(\varphi\downarrow_{1},[\mathtt{z}\mapsto v\,|\,\varphi(\mathtt{z})=v\wedge\mathtt{z}\neq\mathtt{x}],\varphi\downarrow_{3})$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\chi(\iota,\mathtt{f})=\chi(\iota)\downarrow_{2}(\mathtt{f})$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\chi[\omega,\mathtt{f}\mapsto v]=\chi[\omega\mapsto(\chi(\omega)\downarrow_{1},\chi(\omega)\downarrow_{2}[\mathtt{f}\mapsto v]]$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\chi[\alpha,\mathtt{f}\mapsto v]=\chi[\alpha\mapsto(\chi(\alpha)\downarrow_{1},\chi(\alpha)\downarrow_{2}[\mathtt{f}\mapsto v],\chi(\alpha)\downarrow_{3}...\chi(\alpha)\downarrow_{5})]$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\chi[\alpha\mapsto(\sigma,\mathtt{e})]=\chi[\alpha\mapsto(\chi(\alpha)\downarrow_{1}...\chi(\alpha)\downarrow_{3},\sigma,\mathtt{e})]$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\chi[\alpha++\mu]=\chi[\alpha\mapsto(\chi(\alpha)\downarrow_{1},\chi(\alpha)\downarrow_{2},\chi(\alpha)\downarrow_{3}\cdot\mu,\chi(\alpha)\downarrow_{4},\chi(\alpha)\downarrow_{5})]$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\chi[\alpha\mapsto\overline{\mu}]=\chi[\alpha\mapsto(\chi(\alpha)\downarrow_{1},\chi(\alpha)\downarrow_{2},\overline{\mu},\chi(\alpha)\downarrow_{4},\chi(\alpha)\downarrow_{5})]$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\mathit{New}(\chi,\mathtt{C})=(\omega,\chi')\,\mathit{where}\,\omega\not\in\mathit{dom}(\chi)\wedge\chi'=\chi[\omega\mapsto(\mathtt{C},{\cal F}s(\mathtt{C})\mapsto\mathit{null})]$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\mathit{New}(\chi,\mathtt{A},\mathtt{k},\overline{v})=(\alpha,\chi')\,\mathit{where}$
\end_inset


\begin_inset Newline newline
\end_inset


\begin_inset Formula $\alpha\not\in\mathit{dom}(\chi)\wedge\chi'=\chi[\alpha\mapsto(\mathtt{A},{\cal F}s(\mathtt{A})\mapsto\mathit{null},(\mathtt{k},\overline{v}),\alpha,\varepsilon,[])]$
\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"

\end_inset

Auxiliary definitions
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
The operational semantics has the shape 
\begin_inset Formula $\chi\rightarrow\chi'$
\end_inset

, where 
\begin_inset Formula $\chi,\chi'$
\end_inset

 are heaps mapping object addresses 
\begin_inset Formula $\omega$
\end_inset

 to their class identifier and their fields, and actor addresses 
\begin_inset Formula $\alpha$
\end_inset

 to their actor identifier, their fields, their message queue, their stack,
 and the next expression to execute.
 These runtime entities are defined in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Runtime-entities"

\end_inset

.
 Some shorthand notation is used for clarity, as defined in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Auxiliary-definitions"

\end_inset

.
\end_layout

\begin_layout Standard
Note that 
\emph on
null
\emph default
 is used to indicate an undefined field or variable in the operational semantics.
 However, the full language does not permit the use of undefined fields
 or variables, or the construction of a partially defined object (one where
 some subset of fields remains undefined).
 Thus there is no 
\emph on
null
\emph default
, in the sense of a bottom value that can inhabit any type, in the full
 language.
\end_layout

\begin_layout Standard
The symbol 
\begin_inset Formula $\mathtt{x}$
\end_inset

 is used to indicate a source identifier, 
\begin_inset Formula $\mathtt{t}$
\end_inset

 to indicate a temporary identifier, and 
\begin_inset Formula $\mathtt{y}$
\end_inset

 and 
\begin_inset Formula $\mathtt{z}$
\end_inset

 to indicate identifiers which may be either.
 Temporary identifiers are used in the semantics instead of values in order
 to associate a type, including a reference capability, with intermediate
 expression results.
 Importantly, temporary identifiers are accounted for in well-formedness.
\end_layout

\begin_layout Standard
A call stack consists of an actor address 
\begin_inset Formula $\alpha$
\end_inset

 followed by a sequence of frames 
\begin_inset Formula $\varphi$
\end_inset

.
 A frame consists of the method identifier, a mapping of its parameters
 to values, and an expression hole.
 The latter is the continuation of the caller and will be executed by the
 previous frame when the current activation terminates.
\end_layout

\begin_layout Standard
The auxiliary judgement 
\begin_inset Formula $\chi,\sigma,\mathtt{e}\rightsquigarrow\chi',\sigma',\mathtt{e'}$
\end_inset

 expresses local execution within a 
\emph on
single
\emph default
 actor.
 
\begin_inset Formula $\mathcal{M}$
\end_inset

 and 
\begin_inset Formula $\mathcal{F}$
\end_inset

 return method and field declarations, as defined in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Lookup-functions"

\end_inset

.
\end_layout

\begin_layout Subsection
Notation
\end_layout

\begin_layout Standard
To simplify the presentation, some notation conventions are followed.
 The use of 
\begin_inset Formula $\overline{x}$
\end_inset

 indicates a sequence of 
\begin_inset Formula $x$
\end_inset

, whereas 
\begin_inset Formula $xs$
\end_inset

 indicates a set of 
\begin_inset Formula $x$
\end_inset

.
 The projection 
\begin_inset Formula $x\downarrow_{k}$
\end_inset

 is used to express the 
\begin_inset Formula $k^{th}$
\end_inset

 element of the tuple 
\begin_inset Formula $x$
\end_inset

.
 The use of 
\begin_inset Formula $x\downarrow_{k}...x\downarrow_{k+n}$
\end_inset

 refers to a sequence of the 
\begin_inset Formula $k^{th}$
\end_inset

 through 
\begin_inset Formula $k+n^{th}$
\end_inset

 elements of the tuple 
\begin_inset Formula $x$
\end_inset

.
\end_layout

\begin_layout Subsection
Concurrent Execution
\end_layout

\begin_layout Standard
Local execution is defined in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Local-execution"

\end_inset

.
 These rules define local execution within an actor.
 
\noun on
ExprHole 
\noun default
allows execution to propagate to the context, and also determines the order
 of evaluation for complex expressions.
 
\noun on
Fld,
\noun default
 
\noun on
DeclLocal
\noun default
, and
\noun on
 Seq 
\noun default
are as expected.
\end_layout

\begin_layout Standard

\noun on
AsnLocal
\noun default
 and 
\noun on
AsnFld
\noun default
 combine assignment with a destructive read, returning the previous value
 of the left-hand side.
 The resulting value is 
\emph on
unaliased
\emph default
: while there may be other paths pointing to the value in the program, this
 one no longer does.
 In effect, one alias to the value has been discarded.
 The existence of unaliased values is used in the type system, where 
\noun on
T-AsnLocal
\noun default
 and 
\noun on
T-AsnField
\noun default
 both return an 
\emph on
unaliased type
\emph default
, as explained in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Reference-Capabilities"

\end_inset

.
\end_layout

\begin_layout Standard

\noun on
Sync
\noun default
 and 
\noun on
Return
\noun default
 describe synchronous method call and return.
 In 
\noun on
Sync
\noun default
, method 
\begin_inset Formula $\mathtt{m}$
\end_inset

 is called on object or actor 
\begin_inset Formula $\iota$
\end_inset

.
 The method parameters 
\begin_inset Formula $\mathtt{\overline{x}}$
\end_inset

 and the method body 
\family typewriter

\begin_inset Formula $\mathtt{e}$
\end_inset


\family default
 are looked up using the method 
\begin_inset Formula $\mathtt{m}$
\end_inset

 and the type 
\begin_inset Formula $\mathtt{S}$
\end_inset

 of 
\begin_inset Formula $\iota$
\end_inset

 from the heap.
 A new frame is pushed on to the stack, consisting of 
\begin_inset Formula $\mathtt{m}$
\end_inset

, the address of the receiver, the values of the arguments, and the continuation.
 In 
\noun on
Return
\noun default
, the topmost frame is popped from the stack and execution continues.
\end_layout

\begin_layout Standard

\noun on
Async
\noun default
 and 
\noun on
Behave
\noun default
 describe asynchronous method calls and execution.
 In 
\noun on
Async
\noun default
, a message consisting of the behaviour identifier 
\begin_inset Formula $\mathtt{b}$
\end_inset

 and the arguments is appended to the receiver's message queue.
 In 
\noun on
Behave
\noun default
, an actor with an empty call stack and a non-empty message queue removes
 the oldest message from the queue, and pushes a new frame on the stack.
\end_layout

\begin_layout Standard

\noun on
Ctor
\noun default
 and 
\noun on
Ator
\noun default
 describe the construction of new objects and actors.
 In 
\noun on
Ctor
\noun default
, a new address 
\begin_inset Formula $\omega$
\end_inset

 is allocated on the heap and the fields are initialised to 
\emph on
null
\emph default
.
 A new frame is pushed on the stack in the same way as for 
\noun on
Sync
\noun default
.
 In 
\noun on
Ator
\noun default
, instead of pushing a new frame on the stack, the new actor's queue is
 initialised with a constructor message containing the constructor identifier
 
\begin_inset Formula $\mathtt{k}$
\end_inset

 and the arguments.
 The first local execution rule for a new actor will be 
\noun on
Behave
\noun default
, which will execute the body of the constructor 
\begin_inset Formula $\mathtt{k}$
\end_inset

.
\end_layout

\begin_layout Standard

\noun on
Recover
\noun default
 and 
\noun on
Consume
\noun default
 are effectively no-ops in the operational semantics, but have an impact
 in the type system, where 
\noun on
T-Recover
\noun default
 and 
\noun on
T-Consume
\noun default
 affect the reference capability of the result of the expression.
\end_layout

\begin_layout Standard
Global execution is defined in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Global-execution."

\end_inset

.

\noun on
 Global 
\noun default
says that if an actor can execute, then its stack and next expression to
 execute will be updated.
\end_layout

\begin_layout Subsection
Distributed Execution
\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}{rclcl}
 &  & \mathit{Actor} & = & {\color{gray}\mathit{ActorID\times(FieldID\rightarrow Value)}}\\
 &  &  & {\color{gray}\times} & {\color{gray}\mathit{\overline{Message}}\times Stack\times Expr}\\
 &  &  & \times & (\mathit{ActorID}\rightarrow\overline{Message})
\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-1"

\end_inset


\begin_inset Argument 1
status open

\begin_layout Plain Layout
Distributed runtime entities
\end_layout

\end_inset

Distributed runtime entities.
 Elements that are unchanged are greyed out.
\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}{c}
\dfrac{\begin{array}{c}
\alpha'=\varphi(\mathtt{z})\\
\chi'=\chi[\alpha,\alpha'++(\mathtt{b},\varphi(\mathtt{\overline{y}})]
\end{array}}{\chi,\alpha\cdot\overline{\varphi}\cdot\varphi,\mathtt{z.b(\overline{y})}\rightsquigarrow\chi',\alpha\cdot\overline{\varphi}\cdot\varphi,\mathtt{z}}\;\textrm{\textsc{Async}}\\
\\
\dfrac{\exists\alpha'.\chi(\alpha')\downarrow_{6}(\alpha)=\mu\cdot\overline{\mu}}{\chi\rightarrow\chi[\alpha',\alpha\mapsto\overline{\mu}][\alpha++\mu]}\;\textrm{\textsc{Deliver}}
\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:Distributed-execution"

\end_inset

Distributed execution
\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 Itemize
\begin_inset Formula $\chi[\alpha,\alpha'++\mu]=\chi[\alpha\mapsto(\chi(\alpha)\downarrow_{1}...\chi(\alpha)\downarrow_{5},\chi(\alpha)\downarrow_{6}[\alpha'\mapsto\chi(\alpha)\downarrow_{6}(\alpha')\cdot\mu])$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $\chi[\alpha,\alpha'\mapsto\mu]=\chi[\alpha\mapsto(\chi(\alpha)\downarrow_{1}...\chi(\alpha)\downarrow_{5},\chi(\alpha)\downarrow_{6}[\alpha'\mapsto\overline{\mu}])$
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset Caption Standard

\begin_layout Plain Layout
\begin_inset CommandInset label
LatexCommand label
name "fig:Distributed-execution-1"

\end_inset

Auxiliary definitions for distributed execution
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
In the distributed setting, atomic delivery of messages is not feasible.
 To account for this, the definition of an actor is extended in figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Runtime-entities-1"

\end_inset

 to include a logical pairwise (actor-to-actor) FIFO queue of messages sent
 by this actor that have not yet been delivered.
\end_layout

\begin_layout Standard
In figure 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Distributed-execution"

\end_inset

, the 
\noun on
Async
\noun default
 rule is changed to place the newly created message into the pairwise FIFO
 queue of undelivered messages between the sender and the receiver, rather
 than directly into the message queue of the receiver.
 The new
\noun on
 Deliver 
\noun default
rule moves a message from a pairwise FIFO queue to the receiver's message
 queue.
\end_layout

\begin_layout Standard
The purpose of the separate pairwise FIFO queues is to model an arbitrary
 delay between some actor 
\begin_inset Formula $\alpha$
\end_inset

 sending a message and the delivery of that message to the destination actor
 
\begin_inset Formula $\alpha'$
\end_inset

.
 On a single node, 
\noun on
Async 
\noun default
atomically enqueues the message in the receiver's message queue.
 This guarantees message causality on a single node.
\end_layout

\begin_layout Standard
However, in the distributed context, the message produced by 
\noun on
Async 
\noun default
is not placed in the receiver's queue until some future execution of 
\noun on
Deliver
\noun default
.
 This models arbitrary delay, including network delays, and breaks causality.
 Pairwise FIFO ordering is maintained, but it is possible for a third actor
 to appear to violate causality.
 Distributed causality can be built on top of this model using tree-structured
 networks, which will be addressed in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Evaluation-and-Further"

\end_inset

.
\end_layout

\begin_layout Standard
In order to consider all messages bound for some actor 
\begin_inset Formula $\alpha$
\end_inset

, 
\begin_inset Formula $Q(\chi,\alpha)$
\end_inset

 is defined to be the concatenation of all message queues that will be delivered
 to 
\begin_inset Formula $\alpha$
\end_inset

, including the already enqueued messages and the FIFO queue from all other
 actors that have not yet been enqueued for 
\begin_inset Formula $\alpha$
\end_inset

.
\end_layout

\begin_layout Definition
Queues for 
\begin_inset Formula $\alpha$
\end_inset


\end_layout

\begin_layout Definition
\begin_inset Formula $Q(\chi,\alpha)=\{\chi(\alpha)\downarrow_{3}\}\cup\{\overline{\mu}\,|\,\alpha'\in\mathit{dom}(\chi)\wedge\overline{\mu}=\chi(\alpha')\downarrow_{6}(\alpha)\}$
\end_inset


\end_layout

\begin_layout Definition
\begin_inset Formula $\begin{array}{ccc}
Q(\chi,\alpha) & = & Q(\chi,\alpha,\{\alpha'\,|\,\alpha'\in\mathit{dom}(\chi)\}\\
Q(\chi,\alpha,\{\alpha'\}\cup\alpha s) & = & Q(\chi,\alpha,\alpha')\cdot Q(\chi,\alpha,\alpha s)\\
Q(\chi,\alpha,\emptyset) & = & \emptyset\\
Q(\chi,\alpha,\alpha') & = & \begin{cases}
\chi(\alpha)\downarrow_{3} & \mathit{if}\,\alpha=\alpha'\\
\chi(\alpha')\downarrow_{6}(\alpha) & \mathit{otherwise}
\end{cases}
\end{array}$
\end_inset


\end_layout

\begin_layout Standard
In the concurrent setting, where enqueuing messages is atomic, only the
 actor's message queue will contain messages.
 However, in the distributed setting, where causality is not enforced, the
 FIFO queues may also contain messages.
 The concatenation produced by 
\begin_inset Formula $Q(\chi,\alpha)$
\end_inset

 is non-deterministic, as the evaluation of 
\begin_inset Formula $\alpha'\in\mathit{dom}(\chi)$
\end_inset

 is unordered.
\end_layout

\begin_layout Standard
Note that, unlike 
\noun on
Async, Ator 
\noun default
does not enqueue the constructor message.
 Instead, the new actor is created with a single message in its queue, as
 if 
\noun on
Deliver
\noun default
 had already taken place.
 This is to avoid a situation in a distributed context where a message could
 arrive before the actor had been constructed, while still allowing asynchronous
 construction of actors in both concurrent and distributed settings.
\end_layout

\begin_layout Section
Lookup Functions
\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}{c}
\dfrac{\begin{array}{c}
\mathtt{P=\overline{CT}\,\overline{AT}}\\
\mathtt{class\,C\,\mathtt{\overline{F}\,\overline{K}\,\overline{M}}\in\overline{CT}}
\end{array}}{\begin{array}{c}
\mathcal{P}(\mathtt{C})=\mathtt{\overline{F}\,\overline{K}\,\overline{M}\,\varepsilon}\\
\mathtt{C\in P}
\end{array}}\\
\\
\dfrac{\begin{array}{c}
\mathtt{P=\overline{CT}\,\overline{AT}}\\
\mathtt{actor\,A\,\mathtt{\overline{F}\,\overline{K}\,\overline{M}\,\overline{B}}\in\overline{AT}}
\end{array}}{\begin{array}{c}
\mathcal{P}(\mathtt{A})=\mathtt{\overline{F}\,\overline{K}\,\overline{M}\,\overline{B}}\\
\mathtt{A\in P}
\end{array}}\\
\\
\dfrac{\mathcal{P}(\mathtt{S})=\mathtt{\overline{F}\,\overline{K}\,\overline{M}\,\overline{B}}}{\mathcal{F}s(\mathtt{S})=\mathtt{\{f\,|\,var\,f:T\in\overline{F}\}}}\\
\\
\dfrac{\mathcal{P}(\mathtt{S})=\mathtt{\overline{F}\,\overline{K}\,\overline{M}\,\overline{B}}\quad\mathtt{var\,f:T\in\overline{F}}}{\mathcal{F}(\mathtt{S,f})=\mathtt{T}}\\
\\
\dfrac{\mathcal{P}(\mathtt{C})=\mathtt{\overline{F}\,\overline{K}\,\overline{M}}\quad\mathtt{(new\,k(\overline{x}:\overline{T})\Rightarrow e)}\in\mathtt{\overline{K}}}{\mathcal{M}(\mathtt{C,k})=\mathtt{(C\,ref,\overline{x}:\overline{T},e,C\,ref\circ)}}\\
\\
\dfrac{\mathcal{P}(\mathtt{A})=\mathtt{\overline{F}\,\overline{K}\,\overline{M}\,\overline{B}}\quad\mathtt{(new\,k(\overline{x}:\overline{T})\Rightarrow e)}\in\mathtt{\overline{K}}}{\mathcal{M}(\mathtt{A,k})=\mathtt{(A\,ref,\overline{x}:\overline{T},e,A\,tag)}}\\
\\
\dfrac{\mathcal{P}(\mathtt{S})=\mathtt{\overline{F}\,\overline{K}\,\overline{M}\,\overline{B}}\quad\mathtt{(fun\,\kappa\,m(\overline{x}:\overline{T}):ET\Rightarrow e)}\in\mathtt{\overline{M}}}{\mathcal{M}(\mathtt{S,m})=\mathtt{(S\,\kappa,\overline{x}:\overline{T},e,ET)}}\\
\\
\dfrac{\mathcal{P}(\mathtt{A})=\mathtt{\overline{F}\,\overline{K}\,\overline{M}\,\overline{B}}\quad\mathtt{(be\,b(\overline{x}:\overline{T})\Rightarrow e)}\in\mathtt{\overline{B}}}{\mathcal{M}(\mathtt{A,b})=\mathtt{(A\,ref,\overline{x}:\overline{T},e,A\,tag)}}
\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:Lookup-functions"

\end_inset

Lookup functions
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
Lookup functions are defined in fig.
 
\begin_inset CommandInset ref
LatexCommand ref
reference "fig:Lookup-functions"

\end_inset

.
 Function 
\begin_inset Formula $\mathcal{P}$
\end_inset

 returns a type definition for a class identifier 
\begin_inset Formula $\mathtt{C}$
\end_inset

 or actor identifier 
\begin_inset Formula $\mathtt{A}$
\end_inset

.
 This contains the fields 
\begin_inset Formula $\mathtt{\overline{F}}$
\end_inset

, constructors 
\begin_inset Formula $\mathtt{\overline{K}}$
\end_inset

, functions 
\begin_inset Formula $\mathtt{\overline{M}}$
\end_inset

, and behaviours 
\begin_inset Formula $\mathtt{\overline{B}}$
\end_inset

 defined for that type.
 Since classes have no asynchronous behaviour, the last entry in 
\begin_inset Formula $\mathcal{P}(\mathtt{C})$
\end_inset

 is empty, i.e.
 
\begin_inset Formula $\varepsilon$
\end_inset

.
 
\end_layout

\begin_layout Standard
Function 
\begin_inset Formula $\mathcal{F}s$
\end_inset

 returns the identifiers of all fields defined in a type 
\begin_inset Formula $\mathtt{S}$
\end_inset

, and function 
\begin_inset Formula $\mathcal{F}$
\end_inset

 returns the type of field 
\begin_inset Formula $\mathtt{f}$
\end_inset

 in 
\begin_inset Formula $\mathtt{S}$
\end_inset

.
 Function 
\begin_inset Formula $\mathcal{M}$
\end_inset

 returns method information for some method in 
\begin_inset Formula $\mathtt{S}$
\end_inset

.
 This is overloaded on both the method identifier and the type identifier
 in order to handle class constructors, actor constructors, synchronous
 methods (functions) and asynchronous methods (behaviours).
 The result is a tuple of: the receiver type, the names and types of the
 parameters, the body of the method, and the return type.
\end_layout

\begin_layout Standard
The lookup functions mention both types and 
\emph on
reference capabilities
\emph default
, such as 
\begin_inset Formula $\mathtt{ref}$
\end_inset

, 
\begin_inset Formula $\mathtt{ref\circ}$
\end_inset

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

.
 These will be explained in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Reference-Capabilities"

\end_inset

.
\end_layout

\begin_layout Section
Actor model implementation
\end_layout

\begin_layout Standard
This operational semantics is intended to conform to the design decisions
 in chapter 
\begin_inset CommandInset ref
LatexCommand ref
reference "chap:Language-Design-Decisions"

\end_inset

.
 Actors as active objects, single node causality, and distributed pairwise
 FIFO message ordering are directly provided by the operational semantics.
\end_layout

\begin_layout Standard
However, many of the design goals cannot be provided for with the semantics
 alone.
 For example, logically atomic behaviours rely on the operational semantics
 to order messages and run behaviours to completion without interleaving
 other messages or allowing the message queue to be examined, but this is
 insufficient.
 Without a type system that can enforce that communication between actors
 happens only via message passing, it remains possible for two actors to
 exchange information by modifying fields of the same object, resulting
 in behaviours that are no longer logically atomic.
\end_layout

\end_body
\end_document