Discourje: Runtime Verification of Communication Protocols in Clojure
277
A. as a testing/debugging tool for concurrent programs in development, to reliably find/diagnose communication-related concurrency bugs;
B. as a fail-safe mechanism for concurrent programs in production, to prevent
propagation of spurious results caused by concurrency bugs to end-users (i.e.,
it is better to throw a runtime error, cf. ArrayIndexOutOfBoundsException.)
A key factor that determines Discourje’s fitness for purpose is overhead. We
therefore conducted two kinds of benchmarks: microbenchmarks to study the
scalability of Discourje and whole-program benchmarks to study the slowdown
it inflicts relative to unmonitored code.
We used two different hardware configurations to run our benchmarks: vm2
is an instance of the TACAS’20 Artifact Evaluation Virtual Machine for VirtualBox, configured with 2 virtual cores and 8 GB of virtual memory; lisa is
a high-end machine with 16 physical cores (Intel Xeon 6130 processor; hyperthreading disabled) and 96 GB of physical memory (far more than needed for
our benchmarks). We hosted vm2 on a machine with 4 physical cores (Intel Core
i7-8569U; hyper-threading enabled) and 16 GB of physical memory.
Microbenchmarks. In the microbenchmarks, we studied Discourje’s scalability under extreme circumstances where threads perform only sends/receives and
no real computations; this is the worst-case scenario for the lock-free algorithm
to synchronize monitor access, as it gives rise to maximal thread contention.
We considered three specifications to investigate the core features/operators
offered by the Discourje DSL in isolation, using our built-in common patterns
(Fig. 7): ring for sequential composition, one-one-one (OOO) for alternative
composition, and one-all-one (OAO) for parallel composition. Each pattern was
recursively repeated (i.e., wrapped in (fix fix fix :X [... (fix fix fix :X)]). For Ring and
OAO, a round consists of 1000 repetitions; for OOO, a round consists of 1000·n
repetitions, where n is the number of worker threads.
For each implementation I ∈ {Ring, OOO, OAO} with n ∈ {2, 4, 6, 8, 10, 12,
14, 16} worker threads,
5 we recorded the mean round latency μ
I
n in eight hours
of execution on lisa, the standard deviation σ
I
n , and the coefficient of variation
c
I
n =
μ
I
n
σ I
n
. We found c
I
n ≤ 6% for all I and n, except c
OOO
6
= 14% and c
OOO
8
= 8%.
As a measure of scalability, we computed normalized means |μ
I
n | =
μ
I
n
0.5·n·μ I
2
:
this metric is a dimensionless number that indicates the extent to which implementations scale linearly in the number of worker threads, relative to n = 2. For
instance, if |μ
I
16 | = 1, I with 16 workers threads is exactly 8× as slow as I with 2
worker threads; this is reasonable, because the worker threads perform 8× more
sends and receives in each round (due to the adversarial microbenchmark conditions, the sends and receives are effectively linearized by the monitor, which
can check and update at most one channel action at a time).
The normalized means are shown in Fig. 13; our raw data (including standard
deviations) are included in our artifact. We summarize the findings:
5 For Ring, the total number of threads is n; for OOO and OAO, the total number of
threads is n+1 (the master thread).
277
A. as a testing/debugging tool for concurrent programs in development, to reliably find/diagnose communication-related concurrency bugs;
B. as a fail-safe mechanism for concurrent programs in production, to prevent
propagation of spurious results caused by concurrency bugs to end-users (i.e.,
it is better to throw a runtime error, cf. ArrayIndexOutOfBoundsException.)
A key factor that determines Discourje’s fitness for purpose is overhead. We
therefore conducted two kinds of benchmarks: microbenchmarks to study the
scalability of Discourje and whole-program benchmarks to study the slowdown
it inflicts relative to unmonitored code.
We used two different hardware configurations to run our benchmarks: vm2
is an instance of the TACAS’20 Artifact Evaluation Virtual Machine for VirtualBox, configured with 2 virtual cores and 8 GB of virtual memory; lisa is
a high-end machine with 16 physical cores (Intel Xeon 6130 processor; hyperthreading disabled) and 96 GB of physical memory (far more than needed for
our benchmarks). We hosted vm2 on a machine with 4 physical cores (Intel Core
i7-8569U; hyper-threading enabled) and 16 GB of physical memory.
Microbenchmarks. In the microbenchmarks, we studied Discourje’s scalability under extreme circumstances where threads perform only sends/receives and
no real computations; this is the worst-case scenario for the lock-free algorithm
to synchronize monitor access, as it gives rise to maximal thread contention.
We considered three specifications to investigate the core features/operators
offered by the Discourje DSL in isolation, using our built-in common patterns
(Fig. 7): ring for sequential composition, one-one-one (OOO) for alternative
composition, and one-all-one (OAO) for parallel composition. Each pattern was
recursively repeated (i.e., wrapped in (fix fix fix :X [... (fix fix fix :X)]). For Ring and
OAO, a round consists of 1000 repetitions; for OOO, a round consists of 1000·n
repetitions, where n is the number of worker threads.
For each implementation I ∈ {Ring, OOO, OAO} with n ∈ {2, 4, 6, 8, 10, 12,
14, 16} worker threads,
5 we recorded the mean round latency μ
I
n in eight hours
of execution on lisa, the standard deviation σ
I
n , and the coefficient of variation
c
I
n =
μ
I
n
σ I
n
. We found c
I
n ≤ 6% for all I and n, except c
OOO
6
= 14% and c
OOO
8
= 8%.
As a measure of scalability, we computed normalized means |μ
I
n | =
μ
I
n
0.5·n·μ I
2
:
this metric is a dimensionless number that indicates the extent to which implementations scale linearly in the number of worker threads, relative to n = 2. For
instance, if |μ
I
16 | = 1, I with 16 workers threads is exactly 8× as slow as I with 2
worker threads; this is reasonable, because the worker threads perform 8× more
sends and receives in each round (due to the adversarial microbenchmark conditions, the sends and receives are effectively linearized by the monitor, which
can check and update at most one channel action at a time).
The normalized means are shown in Fig. 13; our raw data (including standard
deviations) are included in our artifact. We summarize the findings:
5 For Ring, the total number of threads is n; for OOO and OAO, the total number of
threads is n+1 (the master thread).