The Scalable Commutativity Rule: Designing Scalable Software for Multicore Processors
📜 Abstract
What fundamental opportunities for scalability are latent in interfaces, such as system call APIs? Can scalability opportunities be identified even before any implementation exists, simply by considering interface specifications? To answer these questions this paper introduces the following rule: Whenever interface operations commute, they can be implemented in a way that scales. This rule aids developers in building more scalable software starting from interface design and carrying on through implementation, testing, and evaluation. To help developers apply the rule, a new tool named COMMUTER accepts high-level interface models and generates tests of operations that commute and hence could scale. Using these tests, COMMUTER can evaluate the scalability of an implementation. We apply COMMUTER to 18 POSIX calls and use the results to guide the implementation of a new research operating system kernel called sv6. Linux scales for 68% of the 13,664 tests generated by COMMUTER for these calls, and COMMUTER finds many problems that have been observed to limit application scalability. sv6 scales for 99% of the tests.
✨ Summary
Summary
The paper introduces the scalable commutativity rule: when interface operations commute—meaning their execution order is not distinguishable through the interface—there exists an implementation whose memory accesses are conflict-free in that situation. The authors define SIM commutativity, a state-dependent, interface-based, and monotonic form of commutativity suitable for complex system interfaces, and provide a constructive proof of the rule.
The paper also presents COMMUTER, a toolchain consisting of symbolic interface analysis, test generation, and dynamic memory-access tracing. Applied to 18 POSIX calls, COMMUTER generated 13,664 tests. Linux 3.8 was conflict-free for 9,389 tests, while the authors’ sv6 research kernel was conflict-free for 13,528 tests. The resulting designs used techniques including per-core allocation, radix arrays, deferred reclamation, scalable reference counting, optimistic checks, RCU, and weaker interface ordering. Microbenchmarks and a mail-server workload showed that modified, more-commutative interfaces scaled substantially better than standard POSIX interfaces on an 80-core system.
The work received the SOSP ’13 Best Paper award and was subsequently disseminated in an ACM Transactions on Computer Systems extended version and a 2017 Communications of the ACM article. (usenix.org) The project also led to continued public tooling and systems research around COMMUTER, sv6, and interface-level multicore scalability. (pdos.csail.mit.edu) A later paper identified a flaw in the original proof and supplied a revised, mechanically verified Coq proof, demonstrating direct follow-on research on the paper’s formal foundations. (arxiv.org) Subsequent systems papers continue to cite the scalable commutativity rule when discussing kernel bottlenecks and scalable system design, although the available evidence does not establish broad industrial adoption as a standard engineering methodology. (usenix.org)