Exploiting the commutativity lattice

Speculative execution is a promising approach for exploiting parallelism in many programs, but it requires efficient schemes for detecting conflicts between concurrently executing threads. Prior work has argued that checking semantic commutativity of method invocations is the right way to detect conflicts for complex data structures such as kd-trees. Several ad hoc ways of checking commutativity have been proposed in the literature, but there is no systematic approach for producing implementations.

In this paper, we describe a novel framework for reasoning about commutativity conditions: the commutativity lattice. We show how commutativity specifications from this lattice can be systematically implemented in one of three different schemes: abstract locking, forward gatekeeping and general gatekeeping. We also discuss a disciplined approach to exploiting the lattice to find different implementations that trade off precision in conflict detection for performance. Finally, we show that our novel conflict detection schemes are practical and can deliver speedup on three real-world applications.