  Distributive laws are important for algebraic reasoning in arithmetic and
logic. They are equally important for algebraic reasoning about concurrent
programs. In existing theories such as Concurrent Kleene Algebra, only partial
correctness is handled, and many of its distributive laws are weak, in the
sense that they are only refinements in one direction, rather than equalities.
The focus of this paper is on strengthening our theory to support the proof of
strong distributive laws that are equalities, and in doing so come up with laws
that are quite general. Our concurrent refinement algebra supports total
correctness by allowing both finite and infinite behaviours. It supports the
rely/guarantee approach of Jones by encoding rely and guarantee conditions as
rely and guarantee commands. The strong distributive laws may then be used to
distribute rely and guarantee commands over sequential compositions and into
(and out of) iterations. For handling data refinement of concurrent programs,
strong distributive laws are essential.
