A simple actor definition
This article offers a definition and construction methodology for the Actor Model to provide a simple common vocabulary useful for software specification and implementation. Defining an actor implies defining a protocol (what it does) and an implementation (how it does it). A stopwatch actor is provided as an illustrative example.
Introduction
Building correct software requires two distinct steps: writing a specification that defines what the system must do, and providing an implementation that tells the computer how to do it [1]. An implementation ultimately consists of instructions executable by a specific machine — the kernel language [2].
Bridging this gap involves human programming, compilation, and increasingly, AI assistance. Yet the industry lacks consensus on how to specify and program computers, with little agreement even on notation [3].
This fragmentation stems partly from evolving software requirements, especially the need for coordination in massively concurrent systems. The Actor Model addresses this by aligning with modern hardware properties while remaining expressive enough for high-level specification [4].
This work attempts to capture the essence of the Actor Model and provide a framework for modeling software.
Objective
- Provide a definition for an actor.
- Provide an illustrative example.
- Provide a method to build new actors.
Context
The following resources were used:
- Writing by progressive refinements
- Type Theory
- Laws for communicating parallel processes [5]
- Actor model of computation: Scalable robust information systems [4]
Machines
Computing today relies on a network of heterogeneous machines. Each of these machines has its own memory, computation and communication capabilities. Some of them are linked in some ways, e.g., TCP/IP or Email.
Actor system
An actor system is an abstraction used to model computing carried out by a network of machines.
Each actor is an abstraction representing some aspects of a machine. Communication between machines is abstracted by giving actors the capability to send and receive messages.
A message is the analogue of a letter: it has the address of an actor and an arbitrary payload. After being sent, a message may or may not be received. Nothing guarantees that a message will reach the designated actor. Even if it does, the actor may crash before being able to send a reply, if any.
Actor
An actor is an abstract representation of a machine. It has a canonical address, a state and a script:
Actor :≡ Address × State × Script
To build an actor, it is enough to provide an initial state, a script and have the guarantee that there is a machine it is the abstraction of. Only the canonical address is returned by the constructor as the only way to interact with an actor is to send/receive messages to/from it. In other words:
Actor#mk : Script State ⇝ Actor :≡
script state ↦
address :≡ Address#mk()
actor :≡ <address, state, script>
script is executing on some machine starting from state.
For all messages of the form <address, _>,
send(m) works as expected.
address
Address
An actor has a canonical address.
An address is an abstract representation of whatever address the associated machine
may have, for instance an IP address or an email address in the sense that it can be
used to send data to the actor. In addition, an address cannot be arbitrarily
created, fabricated, guessed, or forged. The expression Address#mk() is the address
constructor.
State
An actor has a state.
A state is an instance of some type that acts as an abstract representation of the associated machine's memory.
Script
An actor has a script.
A script is an abstract representation of whatever programming language is used to define the behaviour of its associated machine. It may use the following instructions:
- ■ - self - send(m) - receive() - become(script [state])
In addition to the usual instruction set.
The exact Script language is not specified here. We attempt to make our intent clear using a pseudo-language even if formalisation attempts have been made, e.g., ActorScript [6].
■
■ means that the current script stops, "killing" the current machine, i.e., freeing all resources (e.g., CPU, Memory).
self
self refers to the current canonical actor address.
Message
A message is the analogue of an envelope: it is formed by an actor address and an arbitrary payload.
Payload : Type Message :≡ Address × Payload
send
Given m : Message :≡ <address, payload>, then send(m) instructs the underlying
infrastructure to transport payload to address. This operation is asynchronous and
non-blocking.
send(m) :≡ <address, payload> ≡ m Network#dispatch(address, payload) ∅ send(address payload) :≡ send(<address, payload>)
Network#dispatch abstracts the act of placing the message into the communication medium (e.g., the network stack). It returns immediately, allowing the sender to continue execution without waiting for acknowledgment or delivery.
Crucially, send(m) provides no guarantees at the sender level:
- It does not verify if address exists.
- It does not verify if address is currently reachable.
- It does not wait for the payload to be placed in the recipient's mailbox.
If the recipient exists and the network succeeds, the payload is eventually written to
the recipient's I/O subsystem, becoming available for a future receive operation.
receive
receive is a language construct that allows the current actor to pattern match against message payloads not already processed.
If a payload p triggers the execution of one of the receive branches, i.e., <cond(p),
script>, then script is executed; else receive blocks until a new message is
received. (TODO timeout).
For instance:
receive
<from, n> when n > 0 ↦ send(from "${n} > 0")
"stop" ↦ ■
means that if a message m is of the form <from, n> where n > 0, then a string is
replied to the sender. If "stop" is received, then the actor dies.
become
Given script : Script, then after become(state script), the current actor executes script from state.
For instance:
french :≡
receive
<from, "hello"> ↦ send(from "Bonjour")
become(french)
italian :≡
receive
<from, "hello"> ↦ send(from "Buongiorno")
become(italian)
receive
"french" ↦ become(french)
"italian" ↦ become(italian)
The previous example means that the current actor will reply "Bonjour" to "hello" after receiving "french" and "Buongiorno" after receiving "italian".
Example
In order to use the previous definitions, let's define a stopwatch using the actor model.
Oscillator
We model an oscillator by an actor built using the expression:
Oscillator#mk(). We assume that the definition of this expression is given. It acts
as a black box; we only know the protocol it is supposed to fulfil, namely:
oscillator :≡ Oscillator#mk()is an oscillator that starts emitting ticks every second starting as soon as it is created.Given an actor
α, thenoscillator#subscribe(α)will subscribeαto the ticks ofoscillator. It means thatαwill receive a message<oscillator, "tick">after each emission.
oscillator#unsubscribe(α)is the reciprocal operation.
Stopwatch
Since the definition of a stopwatch is not given, we provide it ourselves. First, we describe the protocol, in other words what it does:
A stopwatch is an actor that implements the following protocol: it starts counting elapsed seconds as soon as it is created. Then, it replies
<stopwatch, seconds>to a message<actor, "read">.seconds : ℕandactoris an actor address.
Now, we can define how it does it by defining a constructor. To build an actor, we
need to define a state and a script. So, we define a constructor Stopwatch#mk() that builds
an actor that implements the desired behaviour as follows:
script :≡
n : Nat ↦
seconds :≡ n
oscillator :≡ Oscillator#mk()
oscillator#subscribe(self)
next :≡
seconds ↦
receive
<oscillator, "tick"> ↦
become(next seconds+1)
<actor, "read"> ↦
send(actor <self, seconds>)
become(next seconds)
next(seconds)
Stopwatch#mk() :≡ Actor#mk(script 0)
Usage
So, an actor executing the following script:
stopwatch :≡ Stopwatch#mk()
send(stopwatch <self, "read">)
receive
<stopwatch, sec> ↦ "#{sec} seconds elapsed."
would start a stopwatch then ask the stopwatch for the number of elapsed seconds.
Protocol
A protocol describes message sequences and expected replies.
TODO: look at session types.
Actor construction
As seen in the example, defining an actor starts with what it should do. This definition takes the form of a protocol it must implement. Then, a constructor for that type of actor must be defined. It defines how the actor implements its protocol. The how is certainly better expressed using an executable programming language instead of a pseudo-language. A higher-level language seems to be necessary to express the what in any meaningful manner. In other words:
ActorConstruction :≡ 1. What: define the protocol. 2. How: define an implementation that satisfies the protocol. 3. Experiment: provide at least a few tests.
Result
An actor definition has been provided together with a method to define different kinds of actors. An illustrative example has been provided in the form of a stopwatch actor.