{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:36:18Z","timestamp":1770284178755,"version":"3.49.0"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,2,3]],"date-time":"2012-02-03T00:00:00Z","timestamp":1328227200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2012,4]]},"DOI":"10.1007\/s10703-011-0135-z","type":"journal-article","created":{"date-parts":[[2012,2,7]],"date-time":"2012-02-07T18:20:12Z","timestamp":1328638812000},"page":"170-205","source":"Crossref","is-referenced-by-count":26,"title":["Fences in weak memory models (extended version)"],"prefix":"10.1007","volume":"40","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","published-online":{"date-parts":[[2012,2,3]]},"reference":[{"key":"135_CR1","unstructured":"A formal specification of Intel Itanium processor family memory ordering, October 2002. Intel Document 251429-001"},{"key":"135_CR2","volume-title":"HLDVT","author":"A Adir","year":"2002","unstructured":"Adir A, Shurek G (2002) Generating concurrent test-programs with collisions for multi-processor verification. In: HLDVT"},{"key":"135_CR3","volume-title":"TPDS","author":"A Adir","year":"2003","unstructured":"Adir A, Attiya H, Shurek G (2003) Information-flow models for shared Memory with an application to the PowerPC architecture. In: TPDS"},{"key":"135_CR4","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"SV Adve","year":"1995","unstructured":"Adve SV, Gharachorloo K (1995) Shared memory consistency models: a tutorial. Computer 29:66\u201376","journal-title":"Computer"},{"key":"135_CR5","volume-title":"SPAA","author":"M Ahamad","year":"1993","unstructured":"Ahamad M, Bazzi RA, John R, Kohli P, Neiger G (1993) The power of processor consistency. In: SPAA"},{"key":"135_CR6","unstructured":"Alglave J A shared memory poetics. PhD thesis, Universit\u00e9 Paris 7 and INRIA, 26 November 2010. http:\/\/diy.inria.fr\/alglave-thesis.pdf"},{"key":"135_CR7","volume-title":"DAMP","author":"J Alglave","year":"2009","unstructured":"Alglave J, Fox A, Ishtiaq S, Myreen MO, Sarkar S, Sewell P, Zappa Nardelli F (2009) The semantics of Power and ARM multiprocessor machine code. In: DAMP"},{"key":"135_CR8","volume-title":"CAV","author":"J Alglave","year":"2010","unstructured":"Alglave J, Maranget L, Sarkar S, Sewell P (2010) Fences in weak memory models. In: CAV"},{"key":"135_CR9","unstructured":"Alpha Architecture Reference Manual, 4th edn (2002)"},{"key":"135_CR10","unstructured":"AMD64 Architecture Programmer\u2019s Manual. Advanced Micro Devices, September 2007. (3 vols)"},{"key":"135_CR11","unstructured":"ARM Architecture Reference Manual (ARMv7-A and ARMv7-R), April 2008"},{"key":"135_CR12","volume-title":"ISCA","author":"Arvind","year":"2006","unstructured":"Arvind, Maessen J-W (2006) Memory model = instruction reordering + store atomicity. In: ISCA. IEEE Comput Soc, Los Alamitos"},{"key":"135_CR13","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 (2004) In: Coq\u2019Art. EATCS texts in theoretical computer science. Springer, Berlin"},{"key":"135_CR14","volume-title":"PLDI","author":"H-J Boehm","year":"2008","unstructured":"Boehm H-J, Adve SV (2008) Foundations of the C++ concurrency memory model. In: PLDI"},{"key":"135_CR15","volume-title":"CAV","author":"S Burckhardt","year":"2008","unstructured":"Burckhardt S, Musuvathi M (2008) Effective program verification for relaxed memory models. In: CAV"},{"key":"135_CR16","volume-title":"SPAA","author":"J Cantin","year":"2003","unstructured":"Cantin J, Lipasti M, Smith J (2003) The complexity of verifying memory coherence. In: SPAA"},{"key":"135_CR17","volume-title":"Reasoning about parallel architectures","author":"WW Collier","year":"1992","unstructured":"Collier WW (1992) Reasoning about parallel architectures. Prentice Hall, New York"},{"key":"135_CR18","volume-title":"ISCA","author":"S Hangal","year":"2004","unstructured":"Hangal S, Vahia D, Manovit C, Lu J-YJ, Narayanan S (2004) TSOTool: a program for verifying memory systems using the memory consistency model. In: ISCA"},{"key":"135_CR19","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":"135_CR20","unstructured":"Intel 64 and IA-32 Architectures Software Developer\u2019s Manual (5 vols). Intel Corporation, March 2010. rev. 34"},{"issue":"7","key":"135_CR21","doi-asserted-by":"crossref","first-page":"779","DOI":"10.1109\/12.599898","volume":"46","author":"L Lamport","year":"1979","unstructured":"Lamport L (1979) How to make a correct multiprocess program execute correctly on a multiprocessor. IEEE Trans Comput 46(7):779\u2013782","journal-title":"IEEE Trans Comput"},{"issue":"3","key":"135_CR22","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1145\/115953.115964","volume":"19","author":"A Landin","year":"1991","unstructured":"Landin A, Hagersten E, Haridi S (1991) Race-free interconnection networks and multiprocessor consistency. Comput Archit News 19(3):106\u2013115","journal-title":"Comput Archit News"},{"key":"135_CR23","volume-title":"POPL","author":"J Manson","year":"2005","unstructured":"Manson J, Pugh W, Adve SV (2005) The Java memory model. In: POPL"},{"key":"135_CR24","volume-title":"TPHOL","author":"S Owens","year":"2009","unstructured":"Owens S, Sarkar S, Sewell P (2009) A better x86 memory model: x86-TSO. In: TPHOL"},{"key":"135_CR25","unstructured":"Power ISA version 2.06, January 2009"},{"key":"135_CR26","volume-title":"POPL","author":"S Sarkar","year":"2009","unstructured":"Sarkar S, Sewell P, Zappa Nardelli F, Owens S, Ridge T, Braibant T, Myreen M, Alglave J (2009) The semantics of x86-CC multiprocessor machine code. In: POPL"},{"key":"135_CR27","volume-title":"PLDI","author":"S Sarkar","year":"2011","unstructured":"Sarkar S, Sewell P, Alglave J, Maranget L, Williams D (2011) Understanding Power multiprocessors. In: PLDI"},{"issue":"7","key":"135_CR28","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1145\/1785414.1785443","volume":"53","author":"P Sewell","year":"2010","unstructured":"Sewell P, Sarkar S, Owens S, Zappa Nardelli F, Myreen MO (2010) x86-TSO: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun ACM 53(7):89\u201397. (Research Highlights)","journal-title":"Commun ACM"},{"issue":"2","key":"135_CR29","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1145\/42190.42277","volume":"10","author":"D Shasha","year":"1988","unstructured":"Shasha D, Snir M (1988) Efficient and correct execution of parallel programs that share memory. ACM Trans Program Lang Syst 10(2):282\u2013312","journal-title":"ACM Trans Program Lang Syst"},{"key":"135_CR30","unstructured":"Sparc Architecture Manual Versions 8 and 9, 1992 and 1994"},{"key":"135_CR31","volume-title":"IPDPS","author":"Y Yang","year":"2004","unstructured":"Yang Y, Gopalakrishnan G, Linstrom G, Slind K (2004) Nemos: a framework for axiomatic and executable specifications of memory consistency models. In: IPDPS"},{"key":"135_CR32","volume-title":"CCPE","author":"Y Yang","year":"2007","unstructured":"Yang Y, Gopalakrishnan G, Lindstrom G (2007) UMM: an operational memory model specification framework with integrated model checking capability. In: CCPE"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0135-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-011-0135-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0135-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:05:52Z","timestamp":1559253952000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-011-0135-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,2,3]]},"references-count":32,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["135"],"URL":"https:\/\/doi.org\/10.1007\/s10703-011-0135-z","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,2,3]]}}}