{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T12:32:05Z","timestamp":1790944325020,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642221095","type":"print"},{"value":"9783642221101","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22110-1_6","type":"book-chapter","created":{"date-parts":[[2011,7,4]],"date-time":"2011-07-04T09:08:45Z","timestamp":1309770525000},"page":"50-66","source":"Crossref","is-referenced-by-count":34,"title":["Stability in Weak Memory Models"],"prefix":"10.1007","author":[{"given":"Jade","family":"Alglave","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Luc","family":"Maranget","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"Power ISA Version 2.06 (2009)"},{"key":"6_CR2","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"S.V. Adve","year":"1995","unstructured":"Adve, S.V., Gharachorloo, K.: Shared Memory Consistency Models: A Tutorial. IEEE Computer\u00a029, 66\u201376 (1995)","journal-title":"IEEE Computer"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Adve, S.V., Hill, M.D.: Weak Ordering - A New Definition. In: ISCA (1990)","DOI":"10.1145\/325164.325100"},{"key":"6_CR4","unstructured":"Adve, S.V., Boehm, H.-J.: Memory Models: A Case for Rethinking Parallel Languages and Hardware. To appear in CACM"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-14295-6_25","volume-title":"Computer Aided Verification","author":"J. Alglave","year":"2010","unstructured":"Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Fences in weak memory models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 258\u2013272. Springer, Heidelberg (2010)"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-19835-9_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Alglave","year":"2011","unstructured":"Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: litmus: Running tests against hardware. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 41\u201344. Springer, Heidelberg (2011)"},{"key":"6_CR7","unstructured":"Alpha Architecture Reference Manual, 4th edn. (2002)"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Boehm, H.-J.: Reordering Constraints for Pthread-Style Locks. In: PPoPP (2007)","DOI":"10.1145\/1229428.1229470"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Boehm, H.-J.: Threads Cannot Be Implemented As a Library. In: PLDI (2005)","DOI":"10.1145\/1065010.1065042"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Boehm, H.-J., Adve, S.V.: Foundations of the C++ Concurrency Memory Model. In: PLDI (2008)","DOI":"10.1145\/1375581.1375591"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Alur, R., Martin, M.K.: Checkfence: Checking consistency of concurrent data types on relaxed memory models. In: PLDI (2007)","DOI":"10.1145\/1250734.1250737"},{"key":"6_CR12","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)"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Cantin, J., Lipasti, M., Smith, J.: The Complexity of Verifying Memory Coherence. In: SPAA (2003)","DOI":"10.1145\/777412.777457"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Fang, X., Lee, J., Midkiff, S.: Automatic fence insertion for shared memory multiprocessing. In: ICS (2003)","DOI":"10.1145\/782814.782854"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/11813040_32","volume-title":"FM 2006: Formal Methods","author":"T.Q. Huynh","year":"2006","unstructured":"Huynh, T.Q., Roychoudhury, A.: A memory model sensitive checker for C#. In: Misra, J., Nipkow, T., Karakostas, G. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 476\u2013491. Springer, Heidelberg (2006)"},{"key":"6_CR16","unstructured":"Intel 64 and IA-32 Architectures Software Developer\u2019s Manual, vol.\u00a03A, rev.\u00a030 (March 2009)"},{"key":"6_CR17","unstructured":"Kuperstein, M., Vechev, M., Yahav, E.: Automatic inference of memory fences. In: FMCAD (2010)"},{"issue":"7","key":"6_CR18","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1109\/12.599898","volume":"46","author":"L. Lamport","year":"1979","unstructured":"Lamport, L.: How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor. IEEE Trans. Comput.\u00a046(7), 779\u2013782 (1979)","journal-title":"IEEE Trans. Comput."},{"key":"6_CR19","unstructured":"Lea, D.: The JSR-133 Cookbook for Compiler Writers (September 2006), http:\/\/gee.cs.oswego.edu\/dl\/jmm\/cookbook.html"},{"key":"6_CR20","doi-asserted-by":"publisher","first-page":"824","DOI":"10.1109\/12.947002","volume":"50","author":"J. Lee","year":"2001","unstructured":"Lee, J., Padua, D.A.: Hiding relaxed memory consistency with a compiler. IEEE Transactions on Computers\u00a050, 824\u2013833 (2001)","journal-title":"IEEE Transactions on Computers"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The Java Memory Model. In: POPL (2005)","DOI":"10.1145\/1040305.1040336"},{"key":"6_CR22","unstructured":"McKenney, P., Silvera, R.: Example Power Implementation for C\/C++ Memory Model (August 2008), http:\/\/www.rdrop.com\/users\/paulmck\/scalability\/paper\/N2745r.2010.02.19a.html"},{"key":"6_CR23","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":"6_CR24","doi-asserted-by":"crossref","unstructured":"Park, S., Dill, D.: An executable specification, analyzer and verifier for RMO. In: SPAA 1995 (1995)","DOI":"10.1145\/215399.215413"},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-47764-0_1","volume-title":"Static Analysis","author":"M. Rinard","year":"2001","unstructured":"Rinard, M.: Analysis of multithreaded programs. In: Cousot, P. (ed.) SAS 2001. LNCS, vol.\u00a02126, p. 1. Springer, Heidelberg (2001)"},{"key":"6_CR26","unstructured":"Sevcik, J.: Program Transformations in Weak Memory Models. PhD thesis, University of Edinburgh (2008)"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Shasha, D., Snir, M.: Efficient and Correct Execution of Parallel Programs that Share Memory. In: TOPLAS (1988)","DOI":"10.1145\/42190.42277"},{"key":"6_CR28","unstructured":"Sparc Architecture Manual Version 9 (1994)"},{"key":"6_CR29","volume-title":"PPoPP 2005","author":"Z. Sura","year":"2005","unstructured":"Sura, Z., Fang, X., Wong, C.-L., Midkiff, S.P., Lee, J., Padua, D.A.: Compiler techniques for high performance SC Java programs. In: PPoPP 2005. ACM Press, New York (2005)"},{"key":"6_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-540-30482-1_11","volume-title":"Formal Methods and Software Engineering","author":"Y. Yang","year":"2004","unstructured":"Yang, Y., Gopalakrishnan, G.C., Lindstrom, G.: Memory-model-sensitive data race analysis. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 30\u201345. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22110-1_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T13:41:10Z","timestamp":1560346870000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22110-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642221095","9783642221101"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22110-1_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}