{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:57:00Z","timestamp":1774025820687,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642142949","type":"print"},{"value":"9783642142956","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14295-6_25","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T22:36:09Z","timestamp":1278628569000},"page":"258-272","source":"Crossref","is-referenced-by-count":111,"title":["Fences in Weak Memory Models"],"prefix":"10.1007","author":[{"given":"Jade","family":"Alglave","sequence":"first","affiliation":[]},{"given":"Luc","family":"Maranget","sequence":"additional","affiliation":[]},{"given":"Susmit","family":"Sarkar","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"Adir, A., Attiya, H., Shurek, G.: Information-Flow Models for Shared Memory with an Application to the PowerPC Architecture. In: TPDS (2003)","DOI":"10.1109\/TPDS.2003.1199067"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Adir, A., Shurek, G.: Generating Concurrent Test-Programs with Collisions for Multi-Processor Verification. In: HLDVT (2002)","DOI":"10.1109\/HLDVT.2002.1224432"},{"key":"25_CR3","doi-asserted-by":"crossref","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":"25_CR4","doi-asserted-by":"crossref","unstructured":"Ahamad, M., Bazzi, R.A., John, R., Kohli, P., Neiger, G.: The Power of Processor Consistency. In: SPAA (1993)","DOI":"10.1145\/165231.165264"},{"key":"25_CR5","unstructured":"Alpha Architecture Reference Manual, 4th edn. (2002)"},{"key":"25_CR6","unstructured":"ARM Architecture Reference Manual (ARMv7-A and ARMv7-R) (April 2008)"},{"key":"25_CR7","volume-title":"ISCA","author":"Arvind","year":"2006","unstructured":"Arvind, Maessen, J.-W.: Memory Model = Instruction Reordering + Store Atomicity. In: ISCA, IEEE Computer Society, Los Alamitos (2006)"},{"key":"25_CR8","series-title":"EATCS Texts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Coq\u2019Art","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Casteran, P.: Coq\u2019Art. EATCS Texts in Theoretical Computer Science. Springer, Heidelberg (2004)"},{"key":"25_CR9","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":"25_CR10","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":"25_CR11","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":"25_CR12","volume-title":"Reasoning About Parallel Architectures","author":"W.W. Collier","year":"1992","unstructured":"Collier, W.W.: Reasoning About Parallel Architectures. Prentice-Hall, Englewood Cliffs (1992)"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"Dubois, M., Scheurich, C.: Memory Access Dependencies in Shared-Memory Multiprocessors. IEEE Transactions on Software Engineering\u00a016(6) (June 1990)","DOI":"10.1109\/32.55094"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Hangal, S., Vahia, D., Manovit, C., Lu, J.-Y.J., Narayanan, S.: TSOTool: A Program for Verifying Memory Systems Using the Memory Consistency Model. In: ISCA (2004)","DOI":"10.1145\/1028176.1006710"},{"key":"25_CR15","unstructured":"Higham, L., Kawash, J., Verwaal, N.: Weak memory consistency models part I: Definitions and comparisons. Technical Report98\/612\/03, Department of Computer Science, The University of Calgary (January 1998)"},{"key":"25_CR16","unstructured":"A Formal Specification of Intel Itanium Processor Family Memory Ordering . Intel Document 251429-001 (October 2002)"},{"issue":"7","key":"25_CR17","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."},{"issue":"3","key":"25_CR18","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/115953.115964","volume":"19","author":"A. Landin","year":"1991","unstructured":"Landin, A., Hagersten, E., Haridi, S.: Race-free interconnection networks and multiprocessor consistency. SIGARCH Comput. Archit. News\u00a019(3), 106\u2013115 (1991)","journal-title":"SIGARCH Comput. Archit. News"},{"key":"25_CR19","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":"25_CR20","doi-asserted-by":"crossref","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A Better x86 Memory Model: x86-TSO. In: TPHOL (2009)","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"25_CR21","unstructured":"Power isa version 2.06 (2009)"},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Sewell, P., Zappa Nardelli, F., Owens, S., Ridge, T., Braibant, T., Myreen, M., Alglave, J.: The Semantics of x86-CC Multiprocessor Machine Code. In: POPL (2009)","DOI":"10.1145\/1594834.1480929"},{"issue":"2","key":"25_CR23","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1145\/42190.42277","volume":"10","author":"D. Shasha","year":"1988","unstructured":"Shasha, D., Snir, M.: Efficient and Correct Execution of Parallel Programs that Share Memory. ACM Trans. Program. Lang. Syst.\u00a010(2), 282\u2013312 (1988)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"25_CR24","unstructured":"Sparc Architecture Manual Versions 8 and 9 (1992\/1994)"},{"key":"25_CR25","unstructured":"Yang, Y., Gopalakrishnan, G., Lindstrom, G.: UMM: an Operational Memory Model Specification Framework with Integrated Model Checking Capability. In: CCPE (2007)"},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"Yang, Y., Gopalakrishnan, G., Linstrom, G., Slind, K.: Nemos: A Framework for Axiomatic and Executable Specifications of Memory Consistency Models. In: IPDPS (2004)","DOI":"10.1109\/IPDPS.2004.1302944"}],"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-14295-6_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:50:38Z","timestamp":1606186238000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14295-6_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642142949","9783642142956"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14295-6_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}