Verifying sequential consistency with at most π preemptions is polynomial-time for single-writer programs, NP-hard for two-writer programs, and has an ETH-based conditional lower bound for three-writer programs.
Available: https://dl.acm.org/doi/10.1145/3158105
3 Pith papers cite this work. Polarity classification is still indexing.
3
Pith papers citing it
citation-role summary
background 1
citation-polarity summary
years
2026 3verdicts
UNVERDICTED 3roles
background 1polarities
background 1representative citing papers
An ISA-level memory consistency model for tākō is introduced and proven sound by verifying that executions of an implementation model are permitted by the model.
Consistency testing for release-acquire C11 is in P with one writer per location but NP-hard with two writers and ETH-hard for subexponential time with three writers.
citing papers explorer
-
Verifying Sequential Consistency under Bounded Preemptions
Verifying sequential consistency with at most π preemptions is polynomial-time for single-writer programs, NP-hard for two-writer programs, and has an ETH-based conditional lower bound for three-writer programs.
-
t\"{a}k\={o}Formal: Enabling Robust Software for Programmable Memory Hierarchies (Extended Version)
An ISA-level memory consistency model for tākō is introduced and proven sound by verifying that executions of an implementation model are permitted by the model.
-
Complexity of Consistency Testing for the Release-Acquire Semantics
Consistency testing for release-acquire C11 is in P with one writer per location but NP-hard with two writers and ETH-hard for subexponential time with three writers.