@article{POPL2024WeakMemoryTesting,
    author = {Chakraborty, Soham and Krishna, Shankara Narayanan and Mathur, Umang and Pavlogiannis, Andreas},
    title = {How Hard Is Weak-Memory Testing?},
    year = {2024},
    issue_date = {January 2024},
    publisher = {Association for Computing Machinery},
    address = {New York, NY, USA},
    volume = {8},
    number = {POPL},
    url = {https://doi.org/10.1145/3632908},
    doi = {10.1145/3632908},
    abstract = {Weak-memory models are standard formal specifications of concurrency across hardware, programming languages, and distributed systems. A fundamental computational problem is consistency testing: is the observed execution of a concurrent program in alignment with the specification of the underlying system? The problem has been studied extensively across Sequential Consistency (SC) and weak memory, and proven to be NP-complete when some aspect of the input (e.g., number of threads/memory locations) is unbounded. This unboundedness has left a natural question open: are there efficient parameterized algorithms for testing?The main contribution of this paper is a deep hardness result for consistency testing under many popular weak-memory models: the problem remains NP-complete even in its bounded setting, where candidate executions contain a bounded number of threads, memory locations, and values. This hardness spreads across several Release-Acquire variants of C11, a popular variant of its Relaxed fragment, popular Causal Consistency models, and the POWER architecture. To our knowledge, this is the first result that fully exposes the hardness of weak-memory testing and proves that the problem admits no parameterization under standard input parameters. It also yields a computational separation of these models from SC, x86-TSO, PSO, and Relaxed, for which bounded consistency testing is either known (for SC), or shown here (for the rest), to be in polynomial time.},
    journal = {Proc. ACM Program. Lang.},
    month = jan,
    articleno = {66},
    numpages = {32},
    keywords = {concurrency, consistency checking, weak memory models, complexity}
}