{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T14:18:22Z","timestamp":1778077102148,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642140518","type":"print"},{"value":"9783642140525","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_28","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"403-418","source":"Crossref","is-referenced-by-count":19,"title":["From Total Store Order to Sequential Consistency: A Practical Reduction Theorem"],"prefix":"10.1007","author":[{"given":"Ernie","family":"Cohen","sequence":"first","affiliation":[]},{"given":"Bert","family":"Schirmer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","unstructured":"Advanced Micro Devices (AMD), Inc. AMD64 Architecture Programmer\u2019s Manual: Vol. 1-3, rev. 3.14 (September 2007)"},{"issue":"12","key":"28_CR2","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"S.V. Adve","year":"1996","unstructured":"Adve, S.V., Gharachorloo, K.: Shared memory consistency models: A tutorial. IEEE Computer\u00a029(12), 66\u201376 (1996)","journal-title":"IEEE Computer"},{"key":"28_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-540-74591-4_4","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Aspinall","year":"2007","unstructured":"Aspinall, D., Sevc\u00edk, J.: Formalising Java\u2019s data race free guarantee. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 22\u201337. Springer, Heidelberg (2007)"},{"key":"28_CR4","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":"28_CR5","unstructured":"Cohen, E., Schirmer, N.: A better reduction theorem for store buffers. Technical report (2009), \n                    \n                      http:\/\/arxiv.org\/abs\/0909.4637v1"},{"key":"28_CR6","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"TPHOLs 2009","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., et al.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 1\u201322. Springer, Heidelberg (2009)"},{"key":"28_CR7","first-page":"379","volume-title":"POPL \u201909","author":"S. Sarkar","year":"2009","unstructured":"Sarkar, S., et al.: The semantics of x86 multiprocessor machine code. In: POPL \u201909, January 2009, pp. 379\u2013391. ACM Press, New York (2009)"},{"key":"28_CR8","unstructured":"Intel. Intel 64 architecture memory ordering white paper. SKU 318147-001 (2007)"},{"key":"28_CR9","unstructured":"Intel Corporation. Intel 64 and IA-32 Architectures Software Developer\u2019s Manual: Vol. 1-3b, rev. 29 (March 2009)"},{"key":"28_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"Owens, S.: Reasoning about the implementation of concurrency abstractions on x86-TSO. In: ECOOP 2010 (to appear, 2010)","DOI":"10.1007\/978-3-642-14107-2_23"},{"key":"28_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"TPHOLs 2009","author":"S. Owens","year":"2009","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: TPHOLs 2009. LNCS. Springer, Heidelberg (2009)"},{"key":"28_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-74591-4_21","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Ridge","year":"2007","unstructured":"Ridge, T.: Operational reasoning for concurrent caml programs and weak memory models. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 278\u2013293. Springer, Heidelberg (2007)"},{"key":"28_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-540-70592-5_3","volume-title":"ECOOP 2008 \u2013 Object-Oriented Programming","author":"J. Sevc\u00edk","year":"2008","unstructured":"Sevc\u00edk, J., Aspinall, D.: On validity of program transformations in the Java memory model. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol.\u00a05142, pp. 27\u201351. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T19:54:58Z","timestamp":1558295698000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}