{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:00:32Z","timestamp":1779087632820,"version":"3.51.4"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2015,9,24]],"date-time":"2015-09-24T00:00:00Z","timestamp":1443052800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"DFG project R2M2: Robustness against Relaxed Memory Models"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2015,12,8]]},"abstract":"<jats:p>To improve the performance of the memory system, multiprocessors implement weak memory consistency models. Weak memory models admit different views of the processes on their load and store instructions, thus allowing for computations that are not sequentially consistent. Program analyses have to take into account the memory model of the targeted hardware. This is challenging because numerous memory models have been developed, and every memory model requires its own analysis.<\/jats:p>\n          <jats:p>In this article, we study a prominent approach to program analysis: testing. The testing problem takes as input sequences of operations, one for each process in the concurrent program. The task is to check whether these sequences can be interleaved to an execution of the entire program that respects the constraints of a memory model under consideration. We determine the complexity of the testing problem for most of the known memory models. Moreover, we study the impact on the complexity of parameters, such as the number of concurrent processes, the length of their executions, and the number of shared variables.<\/jats:p>\n          <jats:p>\n            What differentiates our contribution from related results is a uniform approach that avoids considering each memory model on its own. We build upon work of Steinke and Nutt. They showed that the existing memory models form a hierarchy where one model is called weaker than another one if it includes the latter\u2019s behavior. Using the Steinke-Nutt hierarchy, we develop three general concepts that allow us to quickly determine the complexity of a testing problem. First, we generalize the technique of problem reductions from complexity theory. So-called range reductions propagate hardness results between memory models, and we apply them to establish\n            <jats:bold>NP<\/jats:bold>\n            lower bounds for the stronger memory models. Second, for the weaker models, we present polynomial-time testing algorithms that are inspired by determinization algorithms for automata. Finally, we describe a single SAT encoding of the testing problem that works for all memory models in the Steinke-Nutt hierarchy to prove their membership in\n            <jats:bold>NP<\/jats:bold>\n            . Our results are general enough to carry over to future weak memory models. Moreover, they show that SAT solvers are adequate tools for testing.\n          <\/jats:p>","DOI":"10.1145\/2753761","type":"journal-article","created":{"date-parts":[[2015,9,29]],"date-time":"2015-09-29T19:22:29Z","timestamp":1443554549000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Memory-Model-Aware Testing"],"prefix":"10.1145","volume":"14","author":[{"given":"Florian","family":"Furbach","sequence":"first","affiliation":[{"name":"TU Kaiserslautern"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roland","family":"Meyer","sequence":"additional","affiliation":[{"name":"TU Kaiserslautern"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Klaus","family":"Schneider","sequence":"additional","affiliation":[{"name":"TU Kaiserslautern"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maximilian","family":"Senftleben","sequence":"additional","affiliation":[{"name":"TU Kaiserslautern"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,9,24]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_15"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.546611"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/165231.165264"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0161-5"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the (EC)2 Workshop.","author":"Alglave J.","year":"2013","unstructured":"J. Alglave. 2013. Weakness is a virtue. In Proceedings of the (EC)2 Workshop."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_33"},{"key":"e_1_2_1_8_1","volume-title":"Computer Aided Verification. Lecture Notes in Computer Science","volume":"8044","author":"Alglave J.","unstructured":"J. Alglave, D. Kroening, and M. Tautschnig. 2013. Partial orders for efficient bounded model checking of concurrent software. In Computer Aided Verification. Lecture Notes in Computer Science, Vol. 8044. Springer, 141--157."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032311"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706303"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_2"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032314"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_29"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/2027223.2027267"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_12"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987389.1987393"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. 127--139","author":"Calin G.","unstructured":"G. Calin, E. Derevenetc, R. Majumdar, and R. Meyer. 2013. A theory of partitioned global address spaces. In Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. 127--139."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2005.86"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734089"},{"key":"e_1_2_1_20_1","volume-title":"Lecture Notes in Computer Science","volume":"8573","author":"Derevenetc E.","unstructured":"E. Derevenetc and R. Meyer. 2014. Robustness against power is PSpace-complete. In Automata, Languages, and Programming. Lecture Notes in Computer Science, Vol. 8573. Springer, 158--170."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926443"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_14"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2014.27"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794279614"},{"key":"e_1_2_1_26_1","volume-title":"Technical Report BU-CS-92-004. Boston University.","author":"Heddaya A.","year":"1992","unstructured":"A. Heddaya and H. Sinha. 1992. Coherence, Non-Coherence and Local Consistency in Distributed Shared Memory for Parallel Computing. Technical Report BU-CS-92-004. Boston University."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/861856"},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the 10th International Conference on Distributed Computing Systems. IEEE","author":"Hutto P. W.","unstructured":"P. W. Hutto and M. Ahamad. 1990. Slow memory: Weakening consistency to enhance concurrency in distributed shared memories. In Proceedings of the 10th International Conference on Distributed Computing Systems. IEEE, Los Alamitos, CA, 302--309."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.16"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","unstructured":"M. Kuperstein M. T. Vechev and E. Yahav. 2011. Partial coherence abstractions for relaxed memory models. In PLDI. ACM 187--198. 10.1145\/1993498.1993521","DOI":"10.1145\/1993498.1993521"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the International Conference on Advances in Computer Science and Electronics Engineering.","author":"Lawrence R.","year":"1998","unstructured":"R. Lawrence. 1998. A survey of cache coherence mechanisms in shared memory multiprocessors. In Proceedings of the International Conference on Advances in Computer Science and Electronics Engineering."},{"key":"e_1_2_1_33_1","volume-title":"PRAM: A Scalable Shared Memory. Technical Report CS-TR-180-88","author":"Lipton R. J.","year":"1988","unstructured":"R. J. Lipton and J. S. Sandberg. 1988. PRAM: A Scalable Shared Memory. Technical Report CS-TR-180-88. Princeton University."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254115"},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the Automated Formal Methods Workshop (AFM\u201906)","author":"Loewenstein P.","unstructured":"P. Loewenstein, S. Chaudhry, R. Cypher, and C. Manovit. 2006. Multiprocessor memory model verification. In Proceedings of the Automated Formal Methods Workshop (AFM\u201906)."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/160551.160553"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017460.1017464"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","unstructured":"D. Weaver and T. Germond (Eds.). 1994. The SPARC Architecture Manual\u2014Version 9. Prentice Hall.","DOI":"10.5555\/174556"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2753761","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2753761","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:16:39Z","timestamp":1750227399000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2753761"}},"subtitle":["A Unified Complexity Analysis"],"short-title":[],"issued":{"date-parts":[[2015,9,24]]},"references-count":36,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,12,8]]}},"alternative-id":["10.1145\/2753761"],"URL":"https:\/\/doi.org\/10.1145\/2753761","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,9,24]]},"assertion":[{"value":"2014-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-03-01","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-09-24","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}