DeNovoND
A hardware/software co-designed extension of the DeNovo coherence protocol that adds efficient support for disciplined non-determinism — lock-based synchronization — on top of DeNovo's deterministic core. It combines distributed queue-based locks with access signatures to keep the protocol free of transient coherence states, invalidation traffic, directories, and false sharing, while still guaranteeing sequential consistency for data-race-free programs. It is reported to match or improve on a MESI baseline in performance and energy for non-deterministic (lock-based) workloads.
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) — Sung, Komuravelli & Adve (DeNovoND, ASPLOS 2013) state their disciplined-non-determinism (lock-based) design guarantees sequential consistency, so on the data-race-free fragment it admits exactly the SC outcomes. Like DeNovo it assumes software supplies race-freedom and defines no behaviour for racy programs; the value-add over DeNovo is the coherence design (locks / access signatures), not the consistency class.
References
- Hyojin Sung, Rakesh Komuravelli, Sarita V. Adve. DeNovoND: Efficient Hardware Support for Disciplined Non-Determinism. ASPLOS 2013, 2013. doi:10.1145/2451116.2451119
- Daniel Poetzl, Daniel Kroening. Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models. arXiv:1510.07171, 2015. arxiv.org/abs/1510.07171