  Collective communication algorithms are an important component of distributed
computation. Indeed, in the case of deep-learning, collective communication is
the Amdahl's bottleneck of data-parallel training.
  This paper introduces SCCL (for Synthesized Collective Communication
Library), a systematic approach to synthesize collective communication
algorithms that are explicitly tailored to a particular hardware topology. SCCL
synthesizes algorithms along the Pareto-frontier spanning from latency-optimal
to bandwidth-optimal implementations of a collective. The paper demonstrates
how to encode SCCL's synthesis as a quantifier-free SMT formula which can be
discharged to a theorem prover. We further demonstrate how to scale our
synthesis by exploiting symmetries in topologies and collectives.
  We synthesize and introduce novel latency and bandwidth optimal algorithms
not seen in the literature on two popular hardware topologies. We also show how
SCCL efficiently lowers algorithms to implementations on two hardware
architectures (NVIDIA and AMD) and demonstrate competitive performance with
hand optimized collective communication libraries.
