272
R. Hamers and S.-S. Jongmans
1 (def def def succ (dsl dsl dsl :w :i :t
2
(--> --> --> (:w :i) (:w (inc :i)) t)))
3
4 (def def def pipe (dsl dsl dsl :w :k :t
5
(rep rep rep seq [:i (range (dec :k))]
6
(ins ins ins succ :w :i :t))))
7
8 (def def def ring (dsl dsl dsl :w :k :t
9
[(ins ins ins pipe :w :k :t)
10
(--> --> --> (:w (dec :k)) (:w 0) :t)]))
11 (def def def one-one-one (dsl dsl dsl :m :w :k :t :u
12
(rep rep rep alt [:i (range :k)]
13
[(--> --> --> :m (:w :i) :t)
14
(--> --> --> (:w :i) :m :u)]))
15
16 (def def def one-all-one (dsl dsl dsl :m :w :k :t :u
17
(rep rep rep par [:i (range :k)]
18
[(--> --> --> :m (:w :i) :t)
19
(--> --> --> (:w :i) :m :u)]))
Fig. 7. Discourje specification of common patterns
parametrized by roles (:w), indices (:i), and/or types (:t). We also note that any
Clojure function can be used in specifications (e.g., inc, to manipulate indices).
Lines 4–6 define the specification of a pipeline communication pattern; it
states that specification (ins ins ins succ :w :i :t) is repeated for each value :i from
0 to k-1, and the iterations are composed sequentially (seq). Lines 8–10 extend
the pipeline to a ring, where the last worker also communicates with the first.
Lines 11–14 define the specification of a communication from a “master” to
one of k workers, and back. Similarly, lines 16–19 define the specification of a
communication from a master to all of k workers, and back. In these specifications, loop iterations are composed alternatively (alt) and in parallel (par).
3 Design
Implementation calculus. To formalize our verification problem, we first define a calculus to model Clojure implementations. Let range over heap locations, x over variables, v over values, and I over implementations. The calculus
is generated by the following grammar:
v ::= nil | | fn x I | true | false | 0 | 1 | 2 | ...
I ::= v | I 1 I 2 | x | def x I | let x I 1 I 2 | loop x I 1 I 2 | recur I |
if I 1 I 2 I 3 | I 1 · I 2 | send I 1 I 2 | recv I | close I | chan I | I 1 I 2
Calculus notation corresponds closely with Clojure notation (Fig. 4), with the
exception of application (I 1 I 2 ), sequencing (I 1 · I 2 ), and threading (I 1 I 2 ).
The operational semantics of the calculus is defined in terms of labeled reductions of triples (I, E, H): I is an implementation, E is a global environment (from
variables to values), and H is a heap (from heap locations to channel states).
Channel states are represented as pairs (w, n), where w is a list of values (messages in transit, from left to right), and n the buffer size. Labels, ranged over by
α, are of the form !v (send), ?v (receive), # (close), and τ (anything else; we
verify only channel actions). The reduction rules are shown in Fig. 8.
Rule [I-Ctxt] executes the first step of implementation I in context C: it
first substitutes I for in C (notation: C[I]), and then executes the first step.
R. Hamers and S.-S. Jongmans
1 (def def def succ (dsl dsl dsl :w :i :t
2
(--> --> --> (:w :i) (:w (inc :i)) t)))
3
4 (def def def pipe (dsl dsl dsl :w :k :t
5
(rep rep rep seq [:i (range (dec :k))]
6
(ins ins ins succ :w :i :t))))
7
8 (def def def ring (dsl dsl dsl :w :k :t
9
[(ins ins ins pipe :w :k :t)
10
(--> --> --> (:w (dec :k)) (:w 0) :t)]))
11 (def def def one-one-one (dsl dsl dsl :m :w :k :t :u
12
(rep rep rep alt [:i (range :k)]
13
[(--> --> --> :m (:w :i) :t)
14
(--> --> --> (:w :i) :m :u)]))
15
16 (def def def one-all-one (dsl dsl dsl :m :w :k :t :u
17
(rep rep rep par [:i (range :k)]
18
[(--> --> --> :m (:w :i) :t)
19
(--> --> --> (:w :i) :m :u)]))
Fig. 7. Discourje specification of common patterns
parametrized by roles (:w), indices (:i), and/or types (:t). We also note that any
Clojure function can be used in specifications (e.g., inc, to manipulate indices).
Lines 4–6 define the specification of a pipeline communication pattern; it
states that specification (ins ins ins succ :w :i :t) is repeated for each value :i from
0 to k-1, and the iterations are composed sequentially (seq). Lines 8–10 extend
the pipeline to a ring, where the last worker also communicates with the first.
Lines 11–14 define the specification of a communication from a “master” to
one of k workers, and back. Similarly, lines 16–19 define the specification of a
communication from a master to all of k workers, and back. In these specifications, loop iterations are composed alternatively (alt) and in parallel (par).
3 Design
Implementation calculus. To formalize our verification problem, we first define a calculus to model Clojure implementations. Let range over heap locations, x over variables, v over values, and I over implementations. The calculus
is generated by the following grammar:
v ::= nil | | fn x I | true | false | 0 | 1 | 2 | ...
I ::= v | I 1 I 2 | x | def x I | let x I 1 I 2 | loop x I 1 I 2 | recur I |
if I 1 I 2 I 3 | I 1 · I 2 | send I 1 I 2 | recv I | close I | chan I | I 1 I 2
Calculus notation corresponds closely with Clojure notation (Fig. 4), with the
exception of application (I 1 I 2 ), sequencing (I 1 · I 2 ), and threading (I 1 I 2 ).
The operational semantics of the calculus is defined in terms of labeled reductions of triples (I, E, H): I is an implementation, E is a global environment (from
variables to values), and H is a heap (from heap locations to channel states).
Channel states are represented as pairs (w, n), where w is a list of values (messages in transit, from left to right), and n the buffer size. Labels, ranged over by
α, are of the form !v (send), ?v (receive), # (close), and τ (anything else; we
verify only channel actions). The reduction rules are shown in Fig. 8.
Rule [I-Ctxt] executes the first step of implementation I in context C: it
first substitutes I for in C (notation: C[I]), and then executes the first step.