Discourje: Runtime Verification of Communication Protocols in Clojure
279
Whole-program benchmarks. In our whole-program benchmarks, we studied
Discourje’s possible slowdown in five real(istic)/existing concurrent programs:
– Chess: Simulates a game of chess between two player threads.
– Conjugate Gradient (CG-n): Computes an estimate of the largest eigenvalue of a symmetric positive definite sparse matrix with a random pattern
of nonzeros, using the conjugate gradient algorithm, with n worker threads.
– Fourier Transform (FT-n): Computes the solution of a partial differential
equation, using the forward and inverse Fast Fourier Transform algorithm,
with 2·n worker threads.
– Integer Sort (IS-n): Computes a sorted list of uniformly distributed integer
keys, using histogram-based integer sorting, with n worker threads.
– Multi-Grid (MG-n): Computes an approximate solution u to the discrete
Poisson problem ∇
2
u = v, using the V-cycle multigrid algorithm, with 4·n
worker threads.
For Chess, we used Clojure code similar to threads Alice and Bob in Tic-Tac-Toe
(Fig. 3), combined with invocations of the open source chess engine Stockfish
10 (https://stockfishchess.org) to compute moves. For CG, FT, IS, and MG,
we adapted existing Java implementations from the NAS Parallel Benchmarks
(NPB) [23] suite, which consists of computational fluid dynamics kernels, by
taking advantage of our Java interoperability wrapper (Sect. 4) to replace the
monitor-based synchronization used in the original versions.
We also wrote specifications for these implementations in the Discourje DSL.
For Chess, the specification is the same as the Tic-Tac-Toe specification (Sect. 2);
for CG, FT, IS, and MG, the specifications consist of recursively repeated choices
among various instances of the one-all-one pattern (each of which involves different subsets of worker threads and message types); the key difference between
the specifications, then, is the frequency in which repetitions occur.
We recorded execution times of each of the implementations without and
with monitoring enabled, using existing/standardized workloads. For Chess, the
workload is controlled by the total amount of time each player has to compute
its moves during the entire game; we used the four smallest such workloads
supported by the open source chess server Lichess (https://lichess.org), namely
{15, 30, 45, 60} seconds, and we limited games to a maximum of 40 turns per
player (UltraBullet chess).
6 For CG, FT, IS, and MG, the workload is controlled
by the input size; we used the standardized inputs that are predefined by NPB.
We ran Chess on vm2; we ran CG-n, FT-n, IS-n, and MG-n on vm2 for
n = 2 and on lisa for n ∈ {2, 4, 6, 8, 10, 12, 14, 16}. We repeated each of the
runs 50 times to smooth out variability; the resulting coefficients of variation are
below 5% for CG, FT, IS, and MG, and between 19%–22% for Chess (because
moves are not computed deterministically, which affects the number of turns per
game). As a measure of slowdown, we computed normalized means of execution
times with monitoring, μ w , against those without monitoring, μ wo (i.e.,
μw
μwo ): this
6 We allow concurrent “ponder” computations during opponents’ turns.
279
Whole-program benchmarks. In our whole-program benchmarks, we studied
Discourje’s possible slowdown in five real(istic)/existing concurrent programs:
– Chess: Simulates a game of chess between two player threads.
– Conjugate Gradient (CG-n): Computes an estimate of the largest eigenvalue of a symmetric positive definite sparse matrix with a random pattern
of nonzeros, using the conjugate gradient algorithm, with n worker threads.
– Fourier Transform (FT-n): Computes the solution of a partial differential
equation, using the forward and inverse Fast Fourier Transform algorithm,
with 2·n worker threads.
– Integer Sort (IS-n): Computes a sorted list of uniformly distributed integer
keys, using histogram-based integer sorting, with n worker threads.
– Multi-Grid (MG-n): Computes an approximate solution u to the discrete
Poisson problem ∇
2
u = v, using the V-cycle multigrid algorithm, with 4·n
worker threads.
For Chess, we used Clojure code similar to threads Alice and Bob in Tic-Tac-Toe
(Fig. 3), combined with invocations of the open source chess engine Stockfish
10 (https://stockfishchess.org) to compute moves. For CG, FT, IS, and MG,
we adapted existing Java implementations from the NAS Parallel Benchmarks
(NPB) [23] suite, which consists of computational fluid dynamics kernels, by
taking advantage of our Java interoperability wrapper (Sect. 4) to replace the
monitor-based synchronization used in the original versions.
We also wrote specifications for these implementations in the Discourje DSL.
For Chess, the specification is the same as the Tic-Tac-Toe specification (Sect. 2);
for CG, FT, IS, and MG, the specifications consist of recursively repeated choices
among various instances of the one-all-one pattern (each of which involves different subsets of worker threads and message types); the key difference between
the specifications, then, is the frequency in which repetitions occur.
We recorded execution times of each of the implementations without and
with monitoring enabled, using existing/standardized workloads. For Chess, the
workload is controlled by the total amount of time each player has to compute
its moves during the entire game; we used the four smallest such workloads
supported by the open source chess server Lichess (https://lichess.org), namely
{15, 30, 45, 60} seconds, and we limited games to a maximum of 40 turns per
player (UltraBullet chess).
6 For CG, FT, IS, and MG, the workload is controlled
by the input size; we used the standardized inputs that are predefined by NPB.
We ran Chess on vm2; we ran CG-n, FT-n, IS-n, and MG-n on vm2 for
n = 2 and on lisa for n ∈ {2, 4, 6, 8, 10, 12, 14, 16}. We repeated each of the
runs 50 times to smooth out variability; the resulting coefficients of variation are
below 5% for CG, FT, IS, and MG, and between 19%–22% for Chess (because
moves are not computed deterministically, which affects the number of turns per
game). As a measure of slowdown, we computed normalized means of execution
times with monitoring, μ w , against those without monitoring, μ wo (i.e.,
μw
μwo ): this
6 We allow concurrent “ponder” computations during opponents’ turns.