DeNovo
A hardware/software co-designed cache-coherence protocol that exploits a disciplined parallel programming model (Deterministic Parallel Java) — structured parallel control, data-race freedom, and deterministic semantics — to simplify the memory hierarchy. By assuming race-free code the protocol eliminates transient coherence states (model checking finds 15x fewer reachable states than a conventional MESI protocol) and guarantees sequential consistency for data-race-free programs, while improving cache hit rates, network traffic, performance, and energy.
Properties
Property vector author-extrapolated — set only where the model’s definition pins the cell down (unknown cells are omitted); cells citing a specific source are marked.
- Other local transformations
- yes Inverse roach motel Poetzl & Kroening 2015
- Reasoning guarantees
- yes External DRF
- yes Coherence
- yes In-order execution
- yes No out-of-thin-air
- Atomicity guarantees
- yes Multicopy atomic
Ordering relationships
- Equivalent to
- Sequential Consistency (SC) — The paper states DeNovo provides sequential consistency for data-race-free programs, so on the race-free fragment it admits exactly the SC outcomes. Unlike DRFx it assumes race-freedom is supplied by the disciplined language (Deterministic Parallel Java) rather than detected at runtime, and defines no behaviour for racy programs.
References
- Byn Choi, Rakesh Komuravelli, Hyojin Sung, Robert Smolinski, Nima Honarmand, Sarita V. Adve, Vikram S. Adve, Nicholas P. Carter, Ching-Tsun Chou. DeNovo: Rethinking the Memory Hierarchy for Disciplined Parallelism. PACT 2011, 2011. doi:10.1109/PACT.2011.21
- Daniel Poetzl, Daniel Kroening. Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models. arXiv:1510.07171, 2015. arxiv.org/abs/1510.07171