DeNovoSync
An extension of the DeNovo coherence protocol that lifts DeNovo's restriction to structured synchronization and supports arbitrary synchronization — including non-blocking algorithms — without writer-initiated invalidations. It relies on reader-initiated self-invalidation combined with synchronization read registration and hardware backoff, and adopts the standard data-race-free memory model of C++/Java, which defines sequentially consistent semantics for data-race-free programs; sequential consistency is used as the correctness criterion for synchronization accesses. It thereby guarantees sequential consistency for data-race-free programs while broadening the synchronization constructs DeNovo can support.
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 & Adve (DeNovoSync, ASPLOS 2015) adopt the standard C++/Java data-race-free memory model, which defines sequentially consistent semantics for data-race-free programs (SC is used as the correctness criterion for synchronization accesses), so on the race-free fragment it admits exactly the SC outcomes. It extends DeNovo to arbitrary synchronization while keeping this SC-for-DRF contract.
References
- Hyojin Sung, Sarita V. Adve. DeNovoSync: Efficient Support for Arbitrary Synchronization without Writer-Initiated Invalidations. ASPLOS 2015, 2015. doi:10.1145/2775054.2694356
- Daniel Poetzl, Daniel Kroening. Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models. arXiv:1510.07171, 2015. arxiv.org/abs/1510.07171