Sharding

Proofs are independent, so a large suite parallelises cleanly. On one machine, parallelism (plugin config) already runs several at once. Sharding goes further by splitting the work across separate machines.

Across machines

Give each machine a shard index out of a total, and bmc4j runs only that machine’s share:

./gradlew test -Dbmc.shard.count=4 -Dbmc.shard.index=1

By default each proof is assigned to a shard by its name. To keep one heavy proof or class on a fixed shard, pin it with @Shard(2) on the method or the class.

Splitting one big proof

A proof that uses domain splitting can itself be the long pole, because all its slices would otherwise run on the single shard it landed on. Add @ShardSlices and its slices spread across the shards instead, so a proof tiled into many slices finishes in parallel rather than back to back.