Discourje: Runtime Verification of Communication Protocols in Clojure
271
1 (def def def alice (role role role "alice")) ;; roles
2 (def def def bob
(role role role "bob"))
3
4 (def def def ttt-close (dsl dsl dsl ;; auxiliary spec
5
(par par par (-## -## -## alice bob)
6
(-## -## -## bob alice))))
7 (def def def ttt (dsl dsl dsl ;; main spec
8
(fix fix fix :X
9
[(--> --> --> alice bob Long)
10
(alt alt alt (ins ins ins ttt-close)
11
[(--> --> --> bob alice Long)
12
(alt alt alt (ins ins ins ttt-close)
13
(fix fix fix :X))])])))
Fig. 5. Discourje specification of Tic-Tac-Toe
10 (def def def m (moni moni moni (spec spec spec ttt)))
11 (def def def a->b (chan chan chan 1 alice bob m)) (def def def b<-a a->b)
12 (def def def b->a (chan chan chan 1 bob alice m)) (def def def a<-b b->a)
Fig. 6. Changes to Fig. 3 to monitor Alice and Bob against the specification in Fig. 5
To monitor the implementations of Alice and Bob against this specification,
first, we need to load library discourje.core.async instead of clojure.core.async
(implicitly loaded in Fig. 3). All other code modifications are shown in Fig. 6: on
line 10, the specification is evaluated to an internal form (spec spec spec) and wrapped in
a new monitor (moni moni moni), while on lines 11–12, we associate the intended sender, receiver, and monitor with the channels. No other changes are needed: notably, the
code for Alice (Fig. 3, lines 14–24) and Bob (lines 25–35) is unaffected; Discourje
is non-invasive to start using. Running the monitor alongside the implementation guarantees safety: if a non-compliant channel action were to be attempted,
the monitor prevents it from happening and throws an exception.
The implementation in Fig 3 can indeed violate the specification in Fig. 5:
the specification states channels are allowed to be closed only after (the receive of) the previous communication is done, but in the implementation, Alice
or Bob could attempt to close already before. In our artifact, we have a solution where we mix channels with barrier synchronization from the standard
java.util.concurrent library (readily usable in Clojure), to let Alice and Bob
first await each other and then close. Thus, channel-based programming abstractions monitored through Discourje can be mixed seamlessly with other concurrency libraries, which happens regularly in message passing programs [46,48].
Advanced Discourje: common patterns. Discourje specifications of common patterns of communication are shown in Fig. 7; they make use of Discourje’s
role indexing and finite repetition (rep rep rep) features.
Imagine we have a sequence of worker threads, organized in a pipeline (i.e.,
the i-th worker receives from its predecessor, i−1, and sends to it successor,
i+1). Lines 1–2 define the specification of a communication from a worker to its
successor. Intuitively, succ is a function that maps three parameters to a specification. For instance, (ins ins ins succ bob 5 Turn) inserts (--> --> --> (bob 5) (bob 6) Turn),
where (bob 5) and (bob 6) are indexed roles. We note that every role created
with role role role allows indexing (with arbitrary types), and that specifications can be
271
1 (def def def alice (role role role "alice")) ;; roles
2 (def def def bob
(role role role "bob"))
3
4 (def def def ttt-close (dsl dsl dsl ;; auxiliary spec
5
(par par par (-## -## -## alice bob)
6
(-## -## -## bob alice))))
7 (def def def ttt (dsl dsl dsl ;; main spec
8
(fix fix fix :X
9
[(--> --> --> alice bob Long)
10
(alt alt alt (ins ins ins ttt-close)
11
[(--> --> --> bob alice Long)
12
(alt alt alt (ins ins ins ttt-close)
13
(fix fix fix :X))])])))
Fig. 5. Discourje specification of Tic-Tac-Toe
10 (def def def m (moni moni moni (spec spec spec ttt)))
11 (def def def a->b (chan chan chan 1 alice bob m)) (def def def b<-a a->b)
12 (def def def b->a (chan chan chan 1 bob alice m)) (def def def a<-b b->a)
Fig. 6. Changes to Fig. 3 to monitor Alice and Bob against the specification in Fig. 5
To monitor the implementations of Alice and Bob against this specification,
first, we need to load library discourje.core.async instead of clojure.core.async
(implicitly loaded in Fig. 3). All other code modifications are shown in Fig. 6: on
line 10, the specification is evaluated to an internal form (spec spec spec) and wrapped in
a new monitor (moni moni moni), while on lines 11–12, we associate the intended sender, receiver, and monitor with the channels. No other changes are needed: notably, the
code for Alice (Fig. 3, lines 14–24) and Bob (lines 25–35) is unaffected; Discourje
is non-invasive to start using. Running the monitor alongside the implementation guarantees safety: if a non-compliant channel action were to be attempted,
the monitor prevents it from happening and throws an exception.
The implementation in Fig 3 can indeed violate the specification in Fig. 5:
the specification states channels are allowed to be closed only after (the receive of) the previous communication is done, but in the implementation, Alice
or Bob could attempt to close already before. In our artifact, we have a solution where we mix channels with barrier synchronization from the standard
java.util.concurrent library (readily usable in Clojure), to let Alice and Bob
first await each other and then close. Thus, channel-based programming abstractions monitored through Discourje can be mixed seamlessly with other concurrency libraries, which happens regularly in message passing programs [46,48].
Advanced Discourje: common patterns. Discourje specifications of common patterns of communication are shown in Fig. 7; they make use of Discourje’s
role indexing and finite repetition (rep rep rep) features.
Imagine we have a sequence of worker threads, organized in a pipeline (i.e.,
the i-th worker receives from its predecessor, i−1, and sends to it successor,
i+1). Lines 1–2 define the specification of a communication from a worker to its
successor. Intuitively, succ is a function that maps three parameters to a specification. For instance, (ins ins ins succ bob 5 Turn) inserts (--> --> --> (bob 5) (bob 6) Turn),
where (bob 5) and (bob 6) are indexed roles. We note that every role created
with role role role allows indexing (with arbitrary types), and that specifications can be