Decomposing Data Structure Commutativity Proofs with $$m\!n$$-Differencing

Commutativity of data structure methods is of ongoing interest in contexts such as parallelizing compilers, transactional memory, speculative execution and software scalability. Despite this interest, we lack effective theories and techniques to aid commutativity verification.