{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T18:19:24Z","timestamp":1784830764951,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642288685","type":"print"},{"value":"9783642288692","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28869-2_2","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T20:44:36Z","timestamp":1332449076000},"page":"26-46","source":"Crossref","is-referenced-by-count":43,"title":["What\u2019s Decidable about Weak Memory Models?"],"prefix":"10.1007","author":[{"given":"Mohamed Faouzi","family":"Atig","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ahmed","family":"Bouajjani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sebastian","family":"Burckhardt","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Madanlal","family":"Musuvathi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems. In: LICS, pp. 313\u2013321 (1996)","DOI":"10.1109\/LICS.1996.561359"},{"issue":"12","key":"2_CR2","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"S. Adve","year":"1996","unstructured":"Adve, S., Gharachorloo, K.: Shared memory consistency models: a tutorial. Computer\u00a029(12), 66\u201376 (1996)","journal-title":"Computer"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: POPL, pp. 7\u201318. ACM (2010)","DOI":"10.1145\/1707801.1706303"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-22110-1_9","volume-title":"Computer Aided Verification","author":"M.F. Atig","year":"2011","unstructured":"Atig, M.F., Bouajjani, A., Parlato, G.: Getting Rid of Store-Buffers in TSO Analysis. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 99\u2013115. Springer, Heidelberg (2011)"},{"key":"2_CR5","unstructured":"Boehm, H.: WG21\/N2176 memory model rationales (March 2007), http:\/\/open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2007\/n2176.html#dependencies"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Boehm, H., Adve, S.: Foundations of the C++ concurrency memory model. In: PLDI, pp. 68\u201378 (2008)","DOI":"10.1145\/1379022.1375591"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-642-22012-8_34","volume-title":"Automata, Languages and Programming","author":"A. Bouajjani","year":"2011","unstructured":"Bouajjani, A., Meyer, R., M\u00f6hlmann, E.: Deciding Robustness against Total Store Ordering. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol.\u00a06756, pp. 428\u2013440. Springer, Heidelberg (2011)"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Alur, R., Martin, M.: CheckFence: Checking consistency of concurrent data types on relaxed memory models. In: PLDI, pp. 12\u201321 (2007)","DOI":"10.1145\/1273442.1250737"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-70545-1_12","volume-title":"Computer Aided Verification","author":"S. Burckhardt","year":"2008","unstructured":"Burckhardt, S., Musuvathi, M.: Effective Program Verification for Relaxed Memory Models. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 107\u2013120. Springer, Heidelberg (2008); 2008 Extended Version as Tech Report MSR-TR-2008-12, Microsoft Research"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-11970-5_7","volume-title":"Compiler Construction","author":"S. Burckhardt","year":"2010","unstructured":"Burckhardt, S., Musuvathi, M., Singh, V.: Verifying Local Transformations on Relaxed Memory Models. In: Gupta, R. (ed.) CC 2010. LNCS, vol.\u00a06011, pp. 104\u2013123. Springer, Heidelberg (2010)"},{"key":"2_CR11","unstructured":"Burnim, J., Sen, K., Stergiou, C.: Testing concurrent programs on relaxed memory models. Tech. Rep. UCB\/EECS-2010-32, EECS Department, University of California, Berkeley (March 2010), http:\/\/www.eecs.berkeley.edu\/Pubs\/TechRpts\/2010\/EECS-2010-32.html"},{"key":"2_CR12","unstructured":"Chen, C., Chen, W., Sreedhar, V., Barik, R., Sarkar, V., Gao, G.: Establishing causality as a desideratum for memory models and transformations of parallel programs. Tech. rep., University of Delaware (2010)"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Gharachorloo, K., Gupta, A., Hennessy, J.: Performance evaluation of memory consistency models for shared-memory multiprocessors. In: ASPLOS 1991, pp. 245\u2013257 (1991)","DOI":"10.1145\/106974.106997"},{"key":"2_CR14","unstructured":"Kuperstein, M., Vechev, M., Yahav, E.: Automatic inference of memory fences. In: FMCAD, pp. 111\u2013119 (October 2010)"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Kuperstein, M., Vechev, M., Yahav, E.: Partial-coherence abstractions for relaxed memory models. In: PLDI, San Jose, CA (June 2011)","DOI":"10.1145\/1993498.1993521"},{"issue":"9","key":"2_CR16","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"C-28","author":"L. Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comp.\u00a0C-28(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Comp."},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-642-22306-8_10","volume-title":"Model Checking Software","author":"A. Linden","year":"2011","unstructured":"Linden, A., Wolper, P.: A Verification-Based Approach to Memory Fence Insertion in Relaxed Memory Systems. In: Groce, A., Musuvathi, M. (eds.) SPIN 2011. LNCS, vol.\u00a06823, pp. 144\u2013160. Springer, Heidelberg (2011)"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-642-14295-6_26","volume-title":"Computer Aided Verification","author":"S. Mador-Haim","year":"2010","unstructured":"Mador-Haim, S., Alur, R., Martin, M.M.K.: Generating Litmus Tests for Contrasting Memory Consistency Models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 273\u2013287. Springer, Heidelberg (2010)"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.: The java memory model. In: POPL, pp. 378\u2013391 (2005)","DOI":"10.1145\/1047659.1040336"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-642-14107-2_23","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"S. Owens","year":"2010","unstructured":"Owens, S.: Reasoning about the Implementation of Concurrency Abstractions on x86-TSO. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol.\u00a06183, pp. 478\u2013503. Springer, Heidelberg (2010)"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-642-03359-9_27","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Owens","year":"2009","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A Better x86 Memory Model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 391\u2013407. Springer, Heidelberg (2009)"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: PLDI, San Jose, CA (June 2011)","DOI":"10.1145\/1993498.1993520"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Sevcik, J.: Safe optimisations for shared-memory concurrent programs. In: PLDI, pp. 306\u2013316 (2011)","DOI":"10.1145\/1993316.1993534"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Sevcik, J., Vafeiadis, V., Nardelli, F.Z., Jagannathan, S., Sewell, P.: Relaxed-memory concurrency and verified compilation. In: POPL, pp. 43\u201354 (2011)","DOI":"10.1145\/1925844.1926393"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Sewell, P., Sarkar, S., Owens, S., Nardelli, F., Myreen, M.: x86-TSO: A rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun. ACM\u00a053 (2010)","DOI":"10.1145\/1785414.1785443"},{"issue":"5-6","key":"2_CR26","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1002\/cpe.837","volume":"17","author":"Y. Yang","year":"2005","unstructured":"Yang, Y., Gopalakrishnan, G., Lindstrom, G.: UMM: an operational memory model specification framework with integrated model checking capability. Concurrency and Computation: Practice and Experience\u00a017(5-6), 465\u2013487 (2005)","journal-title":"Concurrency and Computation: Practice and Experience"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28869-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,23]],"date-time":"2025-03-23T18:48:43Z","timestamp":1742755723000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28869-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288685","9783642288692"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28869-2_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}