Discourje: Runtime Verification of Communication Protocols in Clojure
269
parenthesized prefix notation. Clojure offers asynchronous channel-based programming abstractions through core library clojure.core.async [16]. In the annual Clojure survey [15], Clojure programmers indicate “ease of development” is
more important than “runtime performance”; this makes Clojure an interesting
target for runtime verification (viz. overheads).
To introduce the core features of Clojure relevant to this paper, Fig. 3 shows a
channel-based concurrent Tic-Tac-Toe program in Clojure,
3 while Fig. 4 summarizes the meaning of every primitive (“;;” indicates comments). Lines 1–9 define
constants (blank, cross, nought, initial-grid) and functions (get-blank, add,
not-final?) to represent Tic-Tac-Toe concepts. Lines 11-12 define two channels
(a->b and b->a) that implement the infrastructure through which players Alice
and Bob communicate. Channels in Clojure are bounded: sends/receives block
until a channel is not full/empty. Lines 14–24 and 25–35 define threads that implement Alice and Bob. Both players execute a loop, starting with a blank grid.
In each iteration, Alice first gets the index of some blank space on the grid, then
plays a cross in that space, then sends a message to Bob to communicate the
index, then awaits a message from Bob, and then updates the grid accordingly;
Bob acts symmetrically. After every grid update, Alice or Bob checks if it has
reached a final configuration; if so, the loop is exited and channels are closed.
Every Clojure data structure, including the vector that implements the grid,
is persistent, and therefore, effectively immutable. This means that every operation on an existing data structure leaves it intact, and instead, it returns a new
data structure. Thus, Alice and Bob initially share the same initial grid, but
because it cannot be modified in-place, modifications need to be explicitly communicated. Persistence of Clojure data structures is also why we can guarantee
freedom from data races in pure Clojure (= Clojure without Java objects): if
users communicate only Clojure data through channels, race freedom is guaranteed (if Java objects are communicated, the user is responsible to avoid races).
Basic Discourje: Tic-Tac-Toe. A basic Discourje specification of the TicTac-Toe protocol for Alice and Bob is shown in Fig. 5. We typeset Discourje
“keywords” (which are actually just Clojure functions and macros) bold violet
bold violet
bold violet.
Lines 1–2 define two roles (role role role) to represent Alice and Bob. Lines 4–6 define
an auxiliary specification, inserted twice into the main specification (ins ins ins); it
states that the channels between Alice and Bob are closed (-## -## -##), in parallel (par par par).
Lines 7–13 define the main specification; it states that recursively (fix fix fix), first a
message of type Long (the index of a grid) is communicated from Alice to Bob
(--> --> -->), and then from Bob to Alice, unless the channels are closed (the game is
done). Square brackets are used to build lists of sub-specifications (sequencing).
The Tic-Tac-Toe protocol depends on value-dependent control flow, as Alice
and Bob close the channels only once the grid has reached a final configuration.
This is a non-protocol-related property that no existing MPST tool supports.
3 Tic-Tac-Toe is a two-player game played on a 3x3 grid. Players take turns to fill the
initially blank spaces of the grid with crosses (“X”) and noughts (“O”). The first
player to fill three adjacent spaces, in any direction, with the same symbol wins.
269
parenthesized prefix notation. Clojure offers asynchronous channel-based programming abstractions through core library clojure.core.async [16]. In the annual Clojure survey [15], Clojure programmers indicate “ease of development” is
more important than “runtime performance”; this makes Clojure an interesting
target for runtime verification (viz. overheads).
To introduce the core features of Clojure relevant to this paper, Fig. 3 shows a
channel-based concurrent Tic-Tac-Toe program in Clojure,
3 while Fig. 4 summarizes the meaning of every primitive (“;;” indicates comments). Lines 1–9 define
constants (blank, cross, nought, initial-grid) and functions (get-blank, add,
not-final?) to represent Tic-Tac-Toe concepts. Lines 11-12 define two channels
(a->b and b->a) that implement the infrastructure through which players Alice
and Bob communicate. Channels in Clojure are bounded: sends/receives block
until a channel is not full/empty. Lines 14–24 and 25–35 define threads that implement Alice and Bob. Both players execute a loop, starting with a blank grid.
In each iteration, Alice first gets the index of some blank space on the grid, then
plays a cross in that space, then sends a message to Bob to communicate the
index, then awaits a message from Bob, and then updates the grid accordingly;
Bob acts symmetrically. After every grid update, Alice or Bob checks if it has
reached a final configuration; if so, the loop is exited and channels are closed.
Every Clojure data structure, including the vector that implements the grid,
is persistent, and therefore, effectively immutable. This means that every operation on an existing data structure leaves it intact, and instead, it returns a new
data structure. Thus, Alice and Bob initially share the same initial grid, but
because it cannot be modified in-place, modifications need to be explicitly communicated. Persistence of Clojure data structures is also why we can guarantee
freedom from data races in pure Clojure (= Clojure without Java objects): if
users communicate only Clojure data through channels, race freedom is guaranteed (if Java objects are communicated, the user is responsible to avoid races).
Basic Discourje: Tic-Tac-Toe. A basic Discourje specification of the TicTac-Toe protocol for Alice and Bob is shown in Fig. 5. We typeset Discourje
“keywords” (which are actually just Clojure functions and macros) bold violet
bold violet
bold violet.
Lines 1–2 define two roles (role role role) to represent Alice and Bob. Lines 4–6 define
an auxiliary specification, inserted twice into the main specification (ins ins ins); it
states that the channels between Alice and Bob are closed (-## -## -##), in parallel (par par par).
Lines 7–13 define the main specification; it states that recursively (fix fix fix), first a
message of type Long (the index of a grid) is communicated from Alice to Bob
(--> --> -->), and then from Bob to Alice, unless the channels are closed (the game is
done). Square brackets are used to build lists of sub-specifications (sequencing).
The Tic-Tac-Toe protocol depends on value-dependent control flow, as Alice
and Bob close the channels only once the grid has reached a final configuration.
This is a non-protocol-related property that no existing MPST tool supports.
3 Tic-Tac-Toe is a two-player game played on a 3x3 grid. Players take turns to fill the
initially blank spaces of the grid with crosses (“X”) and noughts (“O”). The first
player to fill three adjacent spaces, in any direction, with the same symbol wins.