Discourje: Runtime Verification of Communication Protocols in Clojure
267
S
Glob
S
Loc
1
S
Loc
2
S
Loc
3
I1
I2
I3
projection
(compile-time)
type checking
(compile-time)
spec.
impl.
Fig. 1. MPST
S
I1
I2
I3
monitoring
(run-time)
spec.
impl.
Fig. 2. This paper
theory guarantees that static well-typedness of threads at compile-time implies
dynamic safety of their channel actions at run-time. Originally [27], I was a
dialect of pi-calculus, S was a calculus of behavioral types, and was defined
through formal typing rules, but more recently, practical implementations were
developed as well [14,28,29,37,38,44], where I is an existing general-purpose language (GPL; Erlang, F#, Go, Java, Scala), S is a new domain-specific language
(DSL; Scribble), and encodes behavioral types in S as non-behavioral types
in I (e.g., through custom communication API generation [29]). These works
highlight two key strengths of the MPST methodology, namely it supports:
#1 fully automated verification of concrete programs (vs. abstract models);
#2 user-friendly programming language-based notation to write specifications of
protocols (vs. dynamic logic or temporal logic).
Problem. One of the key open problems of MPST concerns expressiveness. For
instance, suppose we need to write a program in which messages are repeatedly
communicated from threads I 1 and I 2 to thread I 3 , non-deterministically ordered
(i.e., standard producers–consumer); this protocol is not supported by MPST.
We identify two reasons why expressiveness is limited.
First, MPST were originally developed for distributed computing (service
choreographies [10,11]); accordingly, decoupled verification of roles (per-service
type-checking) has always been a key requirement [14]. This is reflected in the
MPST workflow (Fig. 1): first, the programmer writes a global protocol specification; then, an MPST tool projects it onto every role to infer local protocol specifications; then, the implemented threads are type-checked. However, role-based
decomposition of global behavior into equivalent local behaviors often cannot be
done statically (e.g., [12]), so expressiveness is limited by “projectability”.
Second, MPST prescribes static type-checking, which limits expressiveness,
because: (a) type-checking is sound, but not complete, so the static MPST approach rejects implementations that are conservatively ill-typed but actually
safe; (b) protocols whose execution relies on value-dependent control flow are
supported only in limited circumstances. To alleviate (b), value-dependent type
constructors can be added to S [20,47], but this raises practical issues (i.e.,
dependent types are only scarcely supported by mainstream GPLs).
267
S
Glob
S
Loc
1
S
Loc
2
S
Loc
3
I1
I2
I3
projection
(compile-time)
type checking
(compile-time)
spec.
impl.
Fig. 1. MPST
S
I1
I2
I3
monitoring
(run-time)
spec.
impl.
Fig. 2. This paper
theory guarantees that static well-typedness of threads at compile-time implies
dynamic safety of their channel actions at run-time. Originally [27], I was a
dialect of pi-calculus, S was a calculus of behavioral types, and was defined
through formal typing rules, but more recently, practical implementations were
developed as well [14,28,29,37,38,44], where I is an existing general-purpose language (GPL; Erlang, F#, Go, Java, Scala), S is a new domain-specific language
(DSL; Scribble), and encodes behavioral types in S as non-behavioral types
in I (e.g., through custom communication API generation [29]). These works
highlight two key strengths of the MPST methodology, namely it supports:
#1 fully automated verification of concrete programs (vs. abstract models);
#2 user-friendly programming language-based notation to write specifications of
protocols (vs. dynamic logic or temporal logic).
Problem. One of the key open problems of MPST concerns expressiveness. For
instance, suppose we need to write a program in which messages are repeatedly
communicated from threads I 1 and I 2 to thread I 3 , non-deterministically ordered
(i.e., standard producers–consumer); this protocol is not supported by MPST.
We identify two reasons why expressiveness is limited.
First, MPST were originally developed for distributed computing (service
choreographies [10,11]); accordingly, decoupled verification of roles (per-service
type-checking) has always been a key requirement [14]. This is reflected in the
MPST workflow (Fig. 1): first, the programmer writes a global protocol specification; then, an MPST tool projects it onto every role to infer local protocol specifications; then, the implemented threads are type-checked. However, role-based
decomposition of global behavior into equivalent local behaviors often cannot be
done statically (e.g., [12]), so expressiveness is limited by “projectability”.
Second, MPST prescribes static type-checking, which limits expressiveness,
because: (a) type-checking is sound, but not complete, so the static MPST approach rejects implementations that are conservatively ill-typed but actually
safe; (b) protocols whose execution relies on value-dependent control flow are
supported only in limited circumstances. To alleviate (b), value-dependent type
constructors can be added to S [20,47], but this raises practical issues (i.e.,
dependent types are only scarcely supported by mainstream GPLs).