The process of purely event-driven programs

arXiv:1803.11229v1 [cs.PL] 29 Mar 2018

Bas van den Heuvel
10343725 — vdheuvel.bas@gmail.com
Supervisors: Dr. A. Ponse and Dr. ir. B. Diertens

February 4, 2018

1

Introduction

The formal specification of processes can play a crucial role in a wide range of fields, such as
factories, biological systems, railway networks, or software. Such a formalism may help to map
out the details of any process and to discover bugs, such as deadlocks. They can also be used to
validate the behaviour of a system, or even to develop a quick prototype.
Why not apply this notion to the design of a programming language? It is more than common
that, behind the surface of its syntax, a programming language hides the process of its execution.
A programmer can discover this process by reading the sometimes millions of lines of documentation or simply by trial-and-error. The process is also encoded in the toolchain provided with
the language: compilers, virtual machines, interpreters, modules, etc.
In [7] I gave an abstract description of a programming language that is concurrent by nature. By programming state machines that can only communicate through events, one can build
programs without the need of a call stack, and with an immediate possibility to use parallel or
distributed systems.
By using process algebra (in particular ACP: the Algebra of Communicating Processes;
see [4], [2] and [1]) combined with notions from PSF (a Process Specification Formalism; see [8]
and [3]) this paper gives a complete and thorough description of the process of purely event-driven
programs. This specification reveals the concurrent nature of the language as described in [7] in
a formal manner.

2

Purely event-driven programming

The Purely Event-driven Programming (PEP) language is designed for implicit concurrency.
This means that the order in which a program’s components are executed is not relevant for
its result. Many programming languages support concurrent programming, but this needs to be
done explicitly by the programmer. PEP is concurrent by design.
Another aim of PEP is to eliminate the call stack. Programs commonly consist of sequences
of function calls. Such calls take memory space to provide a context, to know where to return
the results to, and to remember where to continue the program after finishing. PEP uses state
machines to get rid of these notions, summarized in [5] as context, coordination and continuation.

1

A state machine always has the same context, namely its own collection of variables. One
method waiting for a called method to finish is called coordination, and remembering where to
continue after a method is finished is called continuation. Both these notions are irrelevant when
two state machines are used side-by-side. A state machine only needs to know the state it is in,
and how to react to its environment. A state never “calls” another state, it merely transitions to
it.
To run a state machine, one instantiates it. This way, a state machine can have multiple
running instances. Such an instance can emit events, i.e. a message that has a string as type and
an optional value. Other instances can be programmed to react to certain event types, or events
from specific instances.
Every state machine has a special state in which it deals with incoming events. This state is
called “listen”, because it polls for events, i.e. it actively consults a queue to see if any events
have come in. Once there is an event, the instance’s reaction settings are checked. If a reaction
is set, the instance transitions to the set state. Otherwise, the whole process starts again.
Because of the independent nature of state machines, they are not responsible for the actual
execution of their program. The language has a central component called Machine Control which
is responsible for starting and running machines and distributing events.
In Appendix D, accompanying a program specification, one can find the code for a sample PEP
program that simulates a very simple computer that reads from a hard drive. However, to fully
understand the PEP language itself, please consult [7], which contains a thorough description of
the language, together with justifications for certain design choices as well as experiments and a
Python simulation.

3

The PEP process

The process of a PEP program is complex. It consists of many concurrent subprocesses that
can communicate in several ways and all have their own specific purpose. First, I will go into
some conventions used in writing the processes. This is followed by the implementation of two
important data structures: queues and lookup tables.
Then, I give a detailed description of the process of a single running instance of a state machine.
The central part that binds a program together is Machine Control. I finish this section by giving
the processes Machine Control consists of.
Because these processes are described as independent subprocesses, it can be difficult to have
an idea as to how the system comes together. Therefore, I have included a schematic view of
Machine Control and one state machine instance in appendix A.

3.1

Conventions

The following specifications are neither strictly ACP nor strictly PSF. Therefore, there have to
be some rules on how to name actions and how to define communications, i.e. conventions. In
order to make the specifications readable for anyone, I list here the conventions used.
• All actions are subscripted by an identifier. This identifier can be anything, from a natural
number to a string, or a combination of the two.

2

• Actions for specific machines are subscripted with the machine’s identifier. For example,
the action for an outgoing event: outid (. . . ).
• If actions apply to some specific internal process, the name of the process is included in the
identifier. For example, the action to dequeue an incoming event: deqin(id) (. . . ).
• Functions on internal data structures never appear outside regular actions. As they return
immediate results on their arguments, they do not need to be subscripted. For example, to
continue a queue after dequeuing: Qid (rest(l)).
• Many processes communicate. Actions that “send” data after processing, i.e. outbound
communication, are seen as the initiator. Therefore, the actions that “receive” data for
processing, i.e. inbound communication, have the same name except with a prime. Both
sides of the communication are subscripted by the same identifier. A few examples:
Description
Emission of an event
Enqueuing of an event

Outbound
Mout
id
Mprog
id

Action
outid (. . . )
enqout(id) (. . . )

Inbound
MCin
Qout
id

Action
out0id (. . . )
enq0out(id) (. . . )

• Many specifications contain conditionals. They consist of some test that can be true or false
and a question mark contained in square brackets, followed by a colon and an arrow. They
are used to distinguish cases that can be determined upon entering the process term. For
example, to check whether an event (s, d, t, a) requires an acknowledgment: [a = >?] : . . .

3.2

The event data type

An event is a tuple (s, d, t, a) in which
•
•
•
•

s is a natural number identifying the sender of the event;
d is the identifier for its destination, or −1 if no destination is given;
t is a string representing the event’s type;
a is a boolean (> for true or ⊥ for false) indicating whether the event requires acknowledgment.

Let T be the set of all event types used in the program to be specified. We define Ev to be
the collection of all possible events.
Ev := {(s, d, t, a) | s ∈ N, d ∈ N ∪ {−1}, t ∈ T, a ∈ {>, ⊥}}

3.3

Queues

A queue is the process of storing data in a fifo (first in; first out) manner. All queues are the
same, except in the type of data they store. Also, every queue should have an identifier so other
processes know which queue they are dealing with. In this specification, all queues deal with the
same type of data: events.
A queue needs an internal list, which we call `. To initialize an empty list, the process can be
started as such: Qid (). The specification contains a few operations on this list which are purely
functional. I.e., they do not alter the list, but they merely return the result of some operation.
The following table describes each operation used on some list ` with some value e.
3

Operation
top(`)
rest(`)
append(`, e)

Description
Returns the first item of the list
Returns a copy of the list without the first item (i.e. without top(`))
Returns a copy of the list in which e is added to the end

A queue can be stopped by communicating a halt action with it. This particular halt action
is subscripted by q(id), because the queues of instances have the same name as their respective
event handlers.
Qid (`) =[` = ?] : qemptyid · Qid (`)
+ [` 6= ?] : deqid (top(`)) · Qid (rest(`))
+ Σe∈Ev enq0id (e) · Qid (append(`, e))
+ halt0q(id)
The interface for a queue with id id is depicted in the following table. Here, e is any event.
Description
If the queue is empty, this action can communicate
Take the first item from the queue
Put an item on the queue
Terminate the queue

3.4

Action
qempty0id
deq0id (e)
enqid (e)
haltq(id)

Lookup tables

A lookup table assigns a value to a certain index. Tables differ only in the data type of their
index and their values. Therefore, in the specification we superscript the process by collections
of possible indices (I) and possible values (V ). A table needs an internal array, which we call tbl.
Again, the operations on this array are purely functional. Their functionality for some table
tbl, index i and value v is depicted in the following table.
Operation
i ∈ tbl
insert or update(tbl, i, v)
remove(tbl, i)

Description
True if there is an entry in the table with index i
Returns a copy of the table. If i ∈
/ tbl, the copy now has v under index i.
If i ∈ tbl, the copy merely has changed v under index i.
Returns a copy of the table without the index i

A table can be stopped by communicating a halt action with it.

999 999 999 999

I,V
Tid
(tbl) =Σi∈I (
I,V
[i ∈ tbl?] : get0id (i, tbl[i]) · Tid
(tbl)
I,V
+ [i ∈
/ tbl?] : not set0 (i) · Tid
(tbl)
I,V
+ Σv∈V set0id (i, v) · Tid
(insert or update(tbl, i, v))
I,V
+ unset0id (i) · Tid
(remove(tbl, i))

) + halt0id
4

The interface for a table with types I and V and id id is depicted in the following table. Here,
i is any index and v is any value.
Description
If i : v is in the table, this action can communicate
If i is not in the table, this action can communicate
Set a value
Remove a value
Terminate the table

3.5

Action
getid (i, v)
not setid (i)
setid (i, v)
unsetid (i)
haltid

State machines

A PEP program actually runs by creating instances of state machines. Therefore, we define state
machines by providing templates. Such a template is subscripted by an identifier. When an
instance is made, Machine Control assigns a unique identifier to it. This section describes how
to formalise such a template for some state machine with name “M”.
To be able to start new instances of a machine, Machine Control needs access to its process
identifier. Therefore, we do not assign unique names for these processes to each machine, but we
use one letter M and superscript it with the state machine’s name. So, for our machine “M”, an
instance with id id would be described by the process M“M”
id .
When an instance emits an event or wants to react to events, we don’t want it to wait for
Machine Control to communicate with it. Therefore, outgoing events are put into a queue and
in
communicated by a separate process (Mout
id ) and incoming events by another (Mid ). In this way,
prog(“M”)
the program process (Mid
) can immediately continue after dealing with events.
The identifiers of the event processes are not superscripted with the machine’s name, because
they are the same for every machine. However, they do contain the instance’s id. The program
process does contain the machine’s name, because it is unique to the machine.
This is not all. A machine needs two lookup tables: one to store how to react to events and
one to keep track of the ids of machines it started. So, the definition of an instance includes two
tables and two event queues. Let V ars“M” be the collection of all variable names used in the
instance’s program. The implicit variable name “ctx” is added in the specification. As it will be
provided by Machine Control, which starts the instance, the id of its context is a parameter for
the process. Let S“M” be the set of all states of “M”.
prog(“M”)

999 999

M“M”
id (ctxid) =(Mid

V ars“M” ∪{“ctx”},N

||Tctx(id)

([“ctx” : ctxid])

{(m,t)|m∈N∪{−1},t∈T},S“M”

||Treactions(id)

([(ctxid, “halt”) : “halt”]))

||Qin(id) ()||Qout(id) ()
in
||Mout
id ||Mid

3.5.1

The program process

As this project is about the process of PEP, I will not go into the details of calculating process
terms for each state. Instead, I will describe what such a process term should look like. Let “M”

5

be some state machine. For every state s of S“M” and every instance with id id of “M” we define
“M”
Sid
to map state names to their corresponding processes.
An instance should always have access to the most recent event it reacted to, to use the
event’s value, or to know what instance (e.g. the event’s sender) to return an event to. Although
this behaviour is not explained in my thesis, it was indeed used in several experiments, such as
Eratosthenes’ Sieve (see [7, Appendix A]). Therefore, I am going to include it in the specification.
“M”
To allow every state access to the latest event, Sid
will take a second argument: a tuple
consisting of the id of the sending instance and the event’s type. This argument will only be
changed in the “listen” state, where event reaction takes place.
Every branch (summand in process jargon) should be followed by the process of another state.
If the original code contains a branch without a state transition, this means there is an implicit
transition to the listen state. In such cases, the branch should be changed to be followed by the
listen state process.
The listen state process is predefined. The process first dequeues an event and then consults
its reaction table in order to decide an action. If the event requires an acknowledgment, an
acknowledgment event is enqueued before transitioning. If there is no event or no reaction the
process tries again.
If the event queue is empty, the listen state can also take an action and then return to the
same state. It makes sure that, just as with enqueuing events instead of communicating directly
with Machine Control, an instance’s program can always perform an action.
Because there can be both a machine reaction and a regular reaction to the same type, a
priority is defined: first machine reactions, then regular ones. In this process, this is implemented
by first trying to get a machine reaction from the table. If there is no such reaction, only the
“not set” action can communicate. After this action, regular reactions can be tried, unless again
only “not set” can communicate.
Because this process is rather complex, I have included a flowchart in Appendix B.
“M”
“M”
(“listen”, (old s, old t))
Sid
(“listen”, (old s, old t)) =qempty0in(id) · Sid

999 999 999 999 999 999 999 999 999
999 999 999 999
999 999
999 999

+ Σ(s,d,t,a)∈Ev deq0in(id) ((s, d, t, a)) · (
Σstate∈S“M” getreactions(id) ((s, t), state) · (
“M”
[a = >?] : enqout(id) ((id, s, t.“ack”, ⊥)) · Sid
(state, (s, t))
“M”
+ [a = ⊥?] : Sid
(state, (s, t))

) + not setreactions(id) ((s, t)) · (
Σstate∈S“M” getreactions(id) ((−1, t), state) · (
“M”
[a = >?] : enqout(id) ((id, s, t.“ack”, ⊥)) · Sid
(state, (s, t))
“M”
+ [a = ⊥?] : Sid
(state, (s, t))

“M”
) + not setreactions(id) ((−1, t)) · Sid
(“listen”, (old s, old t)

)

)

6

The halt state process is also predefined. If an instance is done it should transition to this
state. This state tells Machine Control to remove this instance from its administration. Then, it
tells all its internal component processes to cease as well. This is done through communicating
halt actions subscripted by the id and the name of the process. There should be no particular
order in this, so it is done concurrently.
999 999 999

“M”
Sid
(“halt”, (s, t)) =haltid · (

haltctx(id) ||haltreactions(id)
||haltq(in(id)) ||haltq(out(id))
||haltin(id) ||haltout(id)

)
Other state processes can be anything, as long as every branch continues in another state
process. In this article I do not go into the details of what is possible in a state. However, working
with events is relevant, so I have included the following table to show how to encode event actions
in process terms. The code syntax is from [7].
Description
Code
Transition to another state
“M”
⇒
Sid
(“s”, (s, t))

=> s

Starting a machine instance
m = ctl.start(M, ...)
0
⇒
startid (“M”) · Σn∈N (new idid (n) · setctx(id) (“m”, n))
Register an event reaction
⇒
setreactions(id) ((−1, “t”), “s”)

when "t" => s

Unregister an event reaction
⇒
unsetreactions(id) ((−1, “t”))

ignore when "t"

Register a machine reaction
when m emits "t" => s
Σn∈N (get0ctx(id) (“m”, n) · setreactions(id) ((n, “t”), “s”))
⇒
ignore when m emits "t"
Unregister a machine reaction
Σn∈N (get0ctx(id) (“m”, n) · unsetreactions(id) ((n, “t”))
⇒
Emit an event
enqout(id) ((id, −1, “t”, ⊥))
⇒

emit ("t")

Emit an event with acknowledgment
emit ("t") => s
enqout(id) ((id, −1, “t”, >)) · setreactions(id) ((−1, “t ack”), “s”)
⇒
emit ("t") to m
Emit a directed event
Σn∈N (get0ctx(id) (“m”, n) · enqout(id) ((id, n, “t”, ⊥)))
⇒
Emit a directed event with acknowledgment
emit ("t") to m => s
Σn∈N (get0ctx(id) (“m”, n) · enqout(id) ((id, n, “t”, >)) · setreactions(id) ((n, “t ack”), “s”))
⇒
7

3.5.2

Event handling

The outgoing event handler takes an event from its queue and communicates it with Machine
Control. Since the id of the sender is already known, that event parameter is discarded. A halt
action stops the process.

999 999 999

Mout
id =Σ( ,d,t,a)∈Ev (
deq0out(id) ((id, d, t, a))
· outid (d, t, a)
· Mout
id

) + halt0out(id)
Incoming events are put into a queue by the incoming event handler. From there, a machine
instance’s listen state dequeues the event and decides what to do with it. In this case the
destination is not relevant, so it is disregarded. A halt action stops the process.

999 999 999

Min
id =Σ(s, ,t,a)∈Ev (
distrib0id (s, t, a)
· enqin(id) ((s, −1, t, a))
· Min
id

) + halt0in(id)

3.6

Machine Control

Machine Control is the central unit responsible for starting state machine instances and the
distribution of events. In order to keep track of the ids of instances, it is dependent on a counter
and a list. Because most events need to be distributed to all running instances, distribution
cannot be separated from the process that keeps these ids. This part of Machine Control is the
scheduler (MCsched ).
However, the reception of events is completely independent from this. So, in order to be able
to distribute events whilst receiving events, this is done by a separate process and a queue, as
done in machine instances. This part of Machine Control is the incoming event handler (MCin ).
The process for Machine Control is defined with two parameters: n, a natural number representing the amount of instances it started (i.e. the highest instance id), and `, the set of ids of
running instances.

MC(n, `) =MCsched (n, `)
||QMC ()
||MCin

8

3.6.1

Scheduler

The scheduling process can do a number of things. These things deal with the starting and halting
of instances and the distribution of events. Because halting and starting influence the list of ids `,
and events need to be distributed to all instances in `, they cannot run concurrently. Therefore,
they are represented as a choice.
If a request to start an instance is communicated, the scheduler communicates the new id to
the requesting instance. Then it continues its process with updated n and `, merged with the
new instances’ process.
If a request to halt an instance is communicated, the scheduler enqueues an event announcing
this halt. Then it checks whether all instances have halted (i.e. whether its list is empty). If so,
it tells its event handler and queue to halt and then stops itself. If not, it continues with the id
of the halted instance removed from its list.
If there is an event in Machine Control’s queue, a dequeue action may communicate. After
this, the scheduler proceeds to distribute the received event. If the event has a destination,
it will only be communicated with that destination. Otherwise, the event will be concurrently
communicated with all instances with all running instances (i.e. the ids in `). This ensures that
all running instances receive the event and that this process will not hang trying to communicate
with non-existing instances.
Because this process is rather complex, I have included a flowchart in Appendix C.

999 999 999 999 999 999
999 999
999

MCsched (n, `) =Σid∈` (
ΣM ∈M start0id (M ) · new idid (n + 1) · (
MCsched (n + 1, append(`, n + 1))||MM
n+1 (id)

) + halt0id · enqMC ((id, −1, “halt”, ⊥)) · (
[remove(`, id) = ?] : (haltMC(in) ||haltq(MC) )
+ [remove(`, id) 6= ?] : MCsched (n, remove(`, id))

)

999 999

) + Σ(s,d,t,a)∈Ev deq0MC ((s, d, t, a)) · (
[d = −1?] : ||id∈` distribid (s, t, a) · MCsched (n, `)
+ [d 6= −1?] : distribd (s, t, a) · MCsched (n, `)

)

9

3.6.2

Incoming event handler

This process is pretty simple and requires no explanation.

999 999 999

MCin =Σ(s,d,t,a)∈Ev (
out0s (d, t, a)
· enqMC ((s, d, t, a))
· MCin

) + halt0MC(in)

3.7

The specification of individual programs

With the information in this section, one is able to define all the process specifications necessary
to define the specification for a program. In summary, one needs to prepare the following items:
• Define T to be the set of all event types present in the program. This defines the set of all
possible events Ev as in Section 3.2.
• With Ev defined, define the specification of the queue process as in Section 3.3.
• Define the specification of the lookup table as in Section 3.4.
• Define M to be the set of all state machine types present in the program.
• For each state machine “M” of M:
– Define V ars“M” to be the set of all variable names used in the state machine.
– Define S“M” to be the set of all state names in the machine.
“M”
– For each state s of S“M” , define Sid
(s, e) to be the corresponding process specification,
with any event e as parameter, as in Section 3.5.1.
prog(“M”)

– Assigns the machine’s initial state specification to Mid
– Define

M“M”
id (ctxid)

.

as in Section 3.5.

• Define MC(n, `) as in Section 3.6.
As described in [7, Section 2.2.3], a program is defined by telling Machine Control to start
one specific machine. In the spirit of this definition, the specification of a program will take as
argument the initial machine to instantiate. It starts Machine Control with one initial id of 1,
merged with the initial machine, instantiated with id 1.
[7, Section 2.2.3] also mentions that the context of the first instance is an empty state machine. However, since the context of instances in the specification is only the identifier of another
instance, we can safely choose this to be -1.
The final step is to encapsulate the program in order to force communication to take place.
We have to define the set H of all actions that can only be performed as communication.

10

H :={qemptyid , qempty0id , deqid , deq0id |
id ∈ {t(n) | t ∈ {in, out}, n ∈ N} ∪ {MC}}
∪ {getid , get0id , not setid , not set0id , setid , set0id , unsetid , unset0id |
id ∈ {t(n) | t ∈ {ctx, reactions}, n ∈ N}}
∪ {outid , out0id , distribid , distrib0id , startid , start0id , new idid , new id0id , haltid , halt0id |
id ∈ N}
∪ {haltid , halt0id |
id ∈ {q(t) | t ∈ {in(n), out(n), MC | n ∈ N}}
∪ {ctx(n), reactions(n), in(n), out(n) | n ∈ N}
∪ {MC(in)}}
We also need to define the names of all communicating actions. As mentioned in Section 3.1,
any outbound communicating action a has an inbound counterpart a0 . We define the communication of these actions γ(a, a0 ) to be a00 .

Program(machinetype) = ∂H (MC(1, {1})||Mmachinetype
(−1))
1
To see the steps in this section in action, take a look at Appendix D.

4

Discussion and conclusion

Firstly, although this specification seems to give the complete picture, it remains to test its actual
workings. By implementing individual PEP programs in PSF, it is possible to test the different
aspects of the language such as event emission and reaction, state machine instantiation, and
(cascading) halting. It also enables us to debug the design, to answer several questions. Does the
listen state priority mechanism actually work? Does the design contain a deadlock? How does
this implementation compare to the Python simulation (see [6])?
Secondly, as the attentive reader might have noticed, there is one important aspect of PEP
missing: the ability to attach values to events. Because the language has been designed to keep
one instance’s memory private from other instances, the only way to pass values is through events.
However, the notion of value passing between processes is not as simple as the concept of it in
a theoretical description of a programming language. For a specification, all the details need to
be thought of. What is a value? What data types would be allowed, and how would these data
types be implemented in a specification? Will the amount of data be limited?
All of these important decisions need to be made before it is even possible to specify the passing
of values. Because the usage of values and variables is necessary for programming anyway, this
problem needs to be solved before actually implementing the programming language. Therefore,
it would be good to do another project on this detail of PEP alone.
Thirdly, it would be interesting to study PEP programs using the notion of abstraction, such
as in [4, Chapter 5]. By applying an abstraction operator to the specification of a program, one
can abstract away from internal operations. In this case, it could be used to compress all actions
11

that are concerned with events and state machines to get an external behaviour. This external
behaviour can then be compared to the behaviour of another implementation of the program that
does not use PEP.
Finally, some remarks about the specification itself. During this project I became more and
more convinced that using process algebra to specify the workings of a programming language is
very useful. Working out the formulas makes you work out every detail, revealing properties of
the language that are new to you.
On top of that, an algebraic specification can help to prevent problems during implementation,
one might discover a problem with the language’s design. But after writing a substantial amount
of code, programmers usually tend to patch the mistakes, instead of rewriting everything from
scratch. A process algebra specification reveals such errors prior to implementation, preventing
the source of a compiler or interpreter to be littered with spaghetti code.

References
[1] J.A. Bergstra and J.W. Klop. Process algebra for synchronous communication. Information
and Control, 60(1-3):109–137, 1984.
[2] J.A. Bergstra, A. Ponse, and S.A. Smolka, editors. Handbook of Process Algebra. Elsevier,
Amsterdam, 2001.
[3] B. Diertens. What is PSF? Nov. 23, 2005. url: https://staff.science.uva.nl/b.
diertens/psf/whatispsf.html (visited on 02/02/2018).
[4] W.J. Fokkink. Introduction to Process Algebra. Texts in Theoretical Computer Science, An
EATCS Series. Springer, Berlin, 2000. Available at http://www.cs.vu.nl/~wanf/BOOKS/
procalg.pdf (draft 2nd edition).
[5] G. Hohpe. Programming without a call stack: event-driven architectures. Objekt Spektrum,
2006.
[6] B. van den Heuvel. Purely Event-Driven Programming language Python simulation. Feb. 2,
2018. url: https://github.com/klaplong/pepsim (visited on 02/02/2018).
[7] B. van den Heuvel. “Purely event-driven programming: A programming language design”.
Bachelor Thesis. University of Amsterdam, June 2016. url: https://esc.fnwi.uva.nl/
thesis/centraal/files/f522241892.pdf
[8] S. Mauw and G.J. Veltink, editors. Algebraic Specification of Communication Protocols, volume 36 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press,
1993.

12

13

A

Process overview schema

B

Listen state flowchart

14

15

C

Machine Control schedule state flowchart

D

A program specification example

This example describes how a computer starts two programs A and B. Program B continuously
asks the CPU to give it a cycle (what for is not relevant). Program A asks the CPU to lookup
something on a hard drive. The CPU delegates this request to the hard drive, which tells its
internal head to seek the proper data. Once found, the hard drive sends an interrupt event to the
CPU. The CPU then returns the found data to program A, which then shuts down the computer.
This appendix contains this program in the syntax as in [7] (albeit with some slight alterations)
and then describes how this program would be specified according to this paper. There is also an
implementation for the Python simulator available in [6, harddrive.py].

D.1

Program code

N.B.: Each state contains an argument e, referring to the latest event. This does not appear
in [7]. This is discussed in Section 3.5.1.
N.B.2: In HDHead’s state seek you’ll notice an or-construct. This is also not a part of [7], but
merely a very general way to describe non-deterministic choice. It is not really necessary for this
example to actually write code to move the arm of a hard drive; I just want to demonstrate the
possibility that seeking takes a while.
machine CPU {
hd = null;
prog_a = null;
prog_b = null;
hd_reader = null;
init state setup(e) {
hd = ctl.start(HD, null);
prog_a = ctl.start(ProgA, null);
prog_b = ctl.start(ProgB, null);
when "cycle" => cycle;
when "read" => hd_read;
when "shutdown" => halt;
}
state cycle(e) {
<cycle>;
}
state hd_read(e) {
hd_reader = e.emitter;
emit ("read") to hd;
when hd emits "interrupt" => hd_interrupt;
}
state hd_interrupt(e) {
emit ("return") to hd_reader;
ignore when hd emits "interrupt";
}
}
machine HD {
hd_head = null;
init state setup(e) {
hd_head = ctl.start(HDHead, null);
when ctx emits "read" => seek;
}

16

state seek(e) {
ignore when "ctx" emits "read";
emit ("seek") to hd_head;
when hd_head emits "found_data" => found_data;
}
state found_data(e) {
ignore when hd_head emits "found_data";
when "read" => seek;
emit ("interrupt") to ctx;
}
}
machine HDHead {
init state setup(e) {
when ctx emits "seek" => seek;
}
state seek(e) {
{
emit ("found_data") to ctx;
} or {
=> seek;
}
}
}
machine ProgA {
init state program(e) {
emit ("read") to ctx;
when ctx emits "return" => finish;
}
state finish(e) {
ignore when ctx emits "return";
emit ("shutdown") to ctx;
}
}
machine ProgB {
init state cycle(e) {
emit ("cycle") to ctx => cycle;
}
}
ctl.run(CPU);

17

D.2

Specification

We follow the steps in Section 3.7. First we define the set of all event types by going through the
code and putting all used event types in a set.
T := {“cycle”, “read”, “shutdown”, “interrupt”, “seek”, “found data”, “return”}
This defines the set of all possible events Ev as well as the specifications for the queue and the
lookup table, which can be directly copied. Next, we define the set of all state machine types.
M :={“CPU”, “HD”, “HDHead”, “ProgA”, “ProgB”}
For each machine, we need to define the respective set of variable names and state names.
As each state machine always has a “listen” and a “halt” state, we can define a default set of
states Sdef ault := {“listen”, “halt”}. We also need to define the state process specifications. The
specifications for “listen” and “halt” are omitted because they can be directly copied with the
right machine type as superscript. We also define the machine’s program to equal its initial state
(with empty event parameters).
N.B. Some specifications slightly deviate from the table in Section 3.5.1, for example in
“CPU”
Sid
(“hd read”, (s, t)). This is because the same variable name is used multiple times in a
row, so the id of the relevant instance needs to be looked up just once.
V ars“CPU” :={“hd”, “prog a”, “prog b”, “hd reader”}
S“CPU” :=Sdef ault ∪ {“setup”, “cycle”, “hd read”, “hd interrupt”}
“CPU”
Sid
(“setup”, (s, t)) =startid (“HD”) · Σn∈N (new id0id (n) · setctx(id) (“hd”, n))

· startid (“ProgA”) · Σn∈N (new id0id (n) · setctx(id) (“prog a”, n))
· startid (“ProgB”) · Σn∈N (new id0id (n) · setctx(id) (“prog b”, n))
· setreactions(id) ((−1, “cycle”), “cycle”)
· setreactions(id) ((−1, “read”), “hd read”)
· setreactions(id) ((−1, “shutdown”), “halt”)
“CPU”
· Sid
(“listen”, (s, t))
“CPU”
“CPU”
Sid
(“cycle”, (s, t)) =hcyclei · Sid
(“listen”, (s, t))
“CPU”
Sid
(“hd read”, (s, t)) =setctx(id) (“hd reader”, s)

999

· Σn∈N (get0ctx(id) (“hd”, n) · enqout(id) ((id, n, “read”, ⊥))

“CPU”
Sid
(“hd interrupt”)

prog(“CPU”)

Mid

· setreactions(id) ((n, “interrupt”), “hd interrupt”))

“CPU”
· Sid
(“listen”, (s, t))
=Σn∈N (get0ctx(id) (“hd reader”, n) · enqout(id) ((id, n, “return”, ⊥)))
· Σn∈N (get0ctx(id) (“hd”, n) · unsetreactions(id) ((n, “interrupt”)))
“CPU”
=Sid
(“setup”, (−1, “”))

18

V ars“HD” :={“hd head”}
S“HD” :=Sdef ault ∪ {“setup”, “seek”, “found data”}
S “HD” (“setup”, (s, t)) =startid (“HDHead”) · Σn∈N (new id0id (n) · setctx(id) (“hd head”, n))
· Σn∈N (get0id (“ctx”, n) · setreactions(id) ((n, “read”), “seek”))
“HD”
· Sid
(“listen”, (s, t))

S “HD” (“seek”, (s, t)) =Σn∈N (get0ctx(id) (“ctx”, n) · unsetreactions(id) ((n, “read”)))
999

· Σn∈N (get0ctx(id) (“hd head”, n) · enqout(id) ((id, n, “seek”, ⊥))

999

S “HD” (“found data”, (s, t))

· setreactions(id) ((n, “found data”), “found data”))

“HD”
· Sid
(“listen”, (s, t))
=Σn∈N (get0ctx(id) (“hd head”, n) · unsetreactions(id) ((n, “found data”)))
· Σn∈N (get0ctx(id) (“ctx”, n) · setreactions(id) ((n, “read”), “seek”)

· enqout(id) ((id, n, “interrupt”, ⊥)))

“HD”
Sid
(“listen”, (s, t))
prog(“HD”)

Mid

“HD”
=Sid
(“setup”, (−1, “”))

V ars“HDHead” :=∅
S“HDHead” :=Sdef ault ∪ {“setup”, “seek”}
“HDHead”
Sid
(“setup”, (s, t)) =Σn∈N (get0ctx(id) (“ctx”, n) · setreactions(id) ((n, “seek”), “seek”))
“HDHead”
· Sid
(“listen”, (s, t))

999 999

“HDHead”
Sid
(“seek”, (s, t)) =(

Σn∈N (get0ctx(id) (“ctx”, n) · enqout(id) ((id, n, “found data”, ⊥)))
“HDHead”
· Sid
(“listen”, (s, t))

999

)+(
“HDHead”
Sid
(“seek”, (s, t))

)
prog(“HDHead”)
Mid

“HDHead”
=Sid
(“setup”, (−1, “”))

19

V ars“ProgA” :=∅
S“ProgA” :=Sdef ault ∪ {“program”, “finish”}
999

“ProgA”
Sid
(“program”, (s, t)) =Σn∈N (get0ctx(id) (“ctx”, n) · enqout(id) ((id, n, “read”, ⊥))

999

“ProgA”
Sid
(“finish”, (s, t))

· setreactions(id) ((n, “return”), “finish”))

“ProgA”
· Sid
(“listen”, (s, t))
=Σn∈N (get0ctx(id) (“ctx”, n) ·

unsetreactions(id) ((n, “return”))

· enqout(id) ((id, n, “shutdown”, ⊥)))

“ProgA”
· Sid
(“listen”, (s, t))
prog(“ProgA”)

Mid

“ProgA”
=Sid
(“program”, (−1, “”))

V ars“ProgB” :=∅
S“ProgB” :=Sdef ault ∪ {“cycle”}
999

“ProgB”
Sid
(“cycle”, (s, t)) =Σn∈N (get0ctx(id) (“ctx”, n) · enqout(id) ((id, n, “cycle”, >))

· setreactions(id) ((n, “cycle ack”), “cycle”))

“ProgB”
Sid
(“listen”, (s, t))
prog(“ProgB”)

Mid

“ProgB”
=Sid
(“cycle”, (−1, “”))

These are the ingredients to define the instance process for each state machine. These definitions are mostly the same, so I only give the one for “CPU”.
prog(“CPU”)

999 999

M“CPU”
(ctxid) =(Mid
id

V ars“CPU” ∪{“ctx”},N

||Tctx(id)

([“ctx” : ctxid])

{(m,t)|m∈N∪{−1},t∈T},S“CPU”
||Treactions(id)
([(ctxid, “halt”)

: “halt”]))

||Qin(id) ()||Qout(id) ()
in
||Mout
id ||Mid

Next, we copy the definition for MC(n, `). Finally, we define the program.
harddisk = Program(“CPU”) = ∂H (MC(1, {1})||M“CPU”
(−1))
1

20

