Discourje: Runtime Verification of Communication Protocols in Clojure
275
S
S
S
monitor
spec spec spec
moni moni moni
Fig. 11. DSL workflow
I
I
instr.
API
Fig. 12. API workflow
Inclusion relation. Finally, we define a relation to decide if the behavior of an
implementation I is included in the behavior of a specification S.
First, let † range over functions from heap locations to sender–receiver pairs;
informally, † establishes a correspondence between channel references in the implementation (characterized by their heap locations) and channel references in
the specification (characterized by the roles that use them as sender/receiver).
Next, let → I ⊆ →. We call → I an execution of I if it satisfies these conditions:
– (I, ∅, ∅)
α
− → I ( ˆ
I
, E
, H
);
– if ( ˆ
I, E, H)
α
− → I ( ˆ
I
, E
, H
), then ( ˆ
I
, E
, H
)
α
− → I ( ˆ
I
, E
, H
) or ˆ
I
is a value;
– if ( ˆ
I, E, H)
α1
−→ I ( ˆ
I
1 , E
1 , H
1 ) and ( ˆ
I, E, H)
α2
−→ I ( ˆ
I
2 , E
2 , H
2 ), then α 1 = α 2
and ( ˆ
I
1 , E
1 , H
1 ) = ( ˆ
I
2 , E
2 , H
2 ).
Finally, a (†, → I )-simulation R is a binary relation such that if ( ˆ
I, E, H)
α
− → I
( ˆ
I
, E
, H
) and ( ˆ
I, E, H) R S, then for some S
:
– if α ∈ {!v, ,?v, ,#} for some , v, then S
α[†()//]
−−−−−→ S
and ( ˆ
I
, E
, H
) R S
;
– if α = τ , then ( ˆ
I
, E
, H
) R S.
In words, ( ˆ
I, E, H) R S iff whenever ˆ
I can reduce to ˆ
I
, S can reduce accordingly
to S
(and ˆ
I
and S
are again related by R), up to τ -reductions (R is weak [24]).
Implementation I is safe relative to specification S, denoted as I S, if for
every execution → I of I, there is a (†, → I )-simulation R such that (I, ∅, ∅) R S.
4 Implementation
The DSL. The DSL consists of: Clojure macros to write specifications (cf.
syntax of the specification calculus; Sect. 3); Clojure data structures to represent
specifications as state machines (cf. operational semantics of the specification
calculus); Clojure functions to instantiate these data structures and construct
monitors. The workflow is shown in Fig. 11: first, the programmer writes a
specification S using the macros; then, at run-time, function spec spec spec is applied to S
to expand and evaluate the macros to a data structure S; then, function moni moni moni
is applied to S to construct a monitor.
Essentially, the monitor provides two operations, depicted as “lollipops” in
Fig. 11: checking if a given channel action α is allowed by S (formally: S
α
− →
S
for some S
), and subsequently updating S to its successor. In this way,
effectively, the monitor incrementally builds a formal simulation to ensure safety
(Sect. 3, page 275). We note that checking/updating is protected by lock-free
synchronization (compare-and-set): an α reduction happens only if it was already
checked if α is allowed, and the state has not yet been updated after that check.
275
S
S
S
monitor
spec spec spec
moni moni moni
Fig. 11. DSL workflow
I
I
instr.
API
Fig. 12. API workflow
Inclusion relation. Finally, we define a relation to decide if the behavior of an
implementation I is included in the behavior of a specification S.
First, let † range over functions from heap locations to sender–receiver pairs;
informally, † establishes a correspondence between channel references in the implementation (characterized by their heap locations) and channel references in
the specification (characterized by the roles that use them as sender/receiver).
Next, let → I ⊆ →. We call → I an execution of I if it satisfies these conditions:
– (I, ∅, ∅)
α
− → I ( ˆ
I
, E
, H
);
– if ( ˆ
I, E, H)
α
− → I ( ˆ
I
, E
, H
), then ( ˆ
I
, E
, H
)
α
− → I ( ˆ
I
, E
, H
) or ˆ
I
is a value;
– if ( ˆ
I, E, H)
α1
−→ I ( ˆ
I
1 , E
1 , H
1 ) and ( ˆ
I, E, H)
α2
−→ I ( ˆ
I
2 , E
2 , H
2 ), then α 1 = α 2
and ( ˆ
I
1 , E
1 , H
1 ) = ( ˆ
I
2 , E
2 , H
2 ).
Finally, a (†, → I )-simulation R is a binary relation such that if ( ˆ
I, E, H)
α
− → I
( ˆ
I
, E
, H
) and ( ˆ
I, E, H) R S, then for some S
:
– if α ∈ {!v, ,?v, ,#} for some , v, then S
α[†()//]
−−−−−→ S
and ( ˆ
I
, E
, H
) R S
;
– if α = τ , then ( ˆ
I
, E
, H
) R S.
In words, ( ˆ
I, E, H) R S iff whenever ˆ
I can reduce to ˆ
I
, S can reduce accordingly
to S
(and ˆ
I
and S
are again related by R), up to τ -reductions (R is weak [24]).
Implementation I is safe relative to specification S, denoted as I S, if for
every execution → I of I, there is a (†, → I )-simulation R such that (I, ∅, ∅) R S.
4 Implementation
The DSL. The DSL consists of: Clojure macros to write specifications (cf.
syntax of the specification calculus; Sect. 3); Clojure data structures to represent
specifications as state machines (cf. operational semantics of the specification
calculus); Clojure functions to instantiate these data structures and construct
monitors. The workflow is shown in Fig. 11: first, the programmer writes a
specification S using the macros; then, at run-time, function spec spec spec is applied to S
to expand and evaluate the macros to a data structure S; then, function moni moni moni
is applied to S to construct a monitor.
Essentially, the monitor provides two operations, depicted as “lollipops” in
Fig. 11: checking if a given channel action α is allowed by S (formally: S
α
− →
S
for some S
), and subsequently updating S to its successor. In this way,
effectively, the monitor incrementally builds a formal simulation to ensure safety
(Sect. 3, page 275). We note that checking/updating is protected by lock-free
synchronization (compare-and-set): an α reduction happens only if it was already
checked if α is allowed, and the state has not yet been updated after that check.