{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:09:02Z","timestamp":1774987742481,"version":"3.50.1"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,6,27]],"date-time":"2012-06-27T00:00:00Z","timestamp":1340755200000},"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,10]]},"DOI":"10.1007\/s10703-012-0161-5","type":"journal-article","created":{"date-parts":[[2012,6,27]],"date-time":"2012-06-27T09:55:46Z","timestamp":1340790946000},"page":"178-210","source":"Crossref","is-referenced-by-count":52,"title":["A formal hierarchy of weak memory models"],"prefix":"10.1007","volume":"41","author":[{"given":"Jade","family":"Alglave","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,6,27]]},"reference":[{"key":"161_CR1","unstructured":"Sparc Architecture Manual (1992 and 1994) Versions 8 and 9"},{"key":"161_CR2","unstructured":"Power\u00a0ISA (2009) Version 2.06"},{"key":"161_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":"161_CR4","unstructured":"Adve SV (1993) Designing memory consistency models for shared-memory multiprocessors. PhD thesis, 1993"},{"key":"161_CR5","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. IEEE Comput 29:66\u201376","journal-title":"IEEE Comput"},{"key":"161_CR6","author":"SV Adve","year":"2012","unstructured":"Adve SV, Boehm H-J (2012) Memory models: a case for rethinking parallel languages and hardware. Commun ACM. doi: 10.1145\/1787234.1787255","journal-title":"Commun ACM"},{"key":"161_CR7","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":"161_CR8","unstructured":"Alglave J (2010) A shared memory poetics. PhD thesis, Universit\u00e9 Paris 7 and INRIA. http:\/\/moscova.inria.fr\/~alglave\/these"},{"key":"161_CR9","volume-title":"APLAS 11","author":"J Alglave","year":"2011","unstructured":"Alglave J, Kroening D, Lugton J, Nimal V, Tautschnig M (2011) Soundness of data flow analyses on weak memory models In: APLAS 11"},{"key":"161_CR10","volume-title":"CAV","author":"J Alglave","year":"2011","unstructured":"Alglave J, Maranget L (2011) Stability in weak memory models. In: CAV"},{"key":"161_CR11","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":"161_CR12","volume-title":"TACAS","author":"J Alglave","year":"2011","unstructured":"Alglave J, Maranget L, Sarkar S, Sewell P (2011) Litmus: running tests against hardware. In: TACAS"},{"key":"161_CR13","unstructured":"Alpha Architecture Reference Manual, 4th edn (2002)"},{"key":"161_CR14","volume-title":"ISCA","author":"Arvind","year":"2006","unstructured":"Arvind, Maessen J-W (2006) Memory model = instruction reordering + store atomicity. In: ISCA"},{"key":"161_CR15","unstructured":"Bertot Y, Casteran P (2004) Coq\u2019Art, EATCS texts in theoretical computer science. Springer, Berlin"},{"key":"161_CR16","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":"161_CR17","volume-title":"POPL","author":"G Boudol","year":"2009","unstructured":"Boudol G, Petri G (2009) Relaxed memory models: an operational approach. In: POPL"},{"key":"161_CR18","volume-title":"CAV","author":"S Burckhardt","year":"2008","unstructured":"Burckhardt S, Musuvathi M (2008) Effective program verification for relaxed memory models. In: CAV"},{"key":"161_CR19","volume-title":"CC","author":"S Burckhardt","year":"2010","unstructured":"Burckhardt S, Musuvathi M, Singh V (2010) Verifying local transformations of concurrent programs. In: CC"},{"key":"161_CR20","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":"161_CR21","volume-title":"Reasoning about parallel architectures","author":"WW Collier","year":"1992","unstructured":"Collier WW (1992) Reasoning about parallel architectures. Prentice Hall, New York"},{"key":"161_CR22","doi-asserted-by":"crossref","unstructured":"Dubois M, Scheurich C (1990) Memory access dependencies in shared-memory multiprocessors. IEEE Trans Softw Eng 16(6). doi: 10.1109\/32.55094","DOI":"10.1109\/32.55094"},{"key":"161_CR23","volume-title":"ESOP","author":"R Ferreira","year":"2010","unstructured":"Ferreira R, Feng X, Shao Z (2010) Parameterized memory models and concurrent separation logic. In: ESOP"},{"key":"161_CR24","unstructured":"Gharachorloo K (1995) Memory consistency models for shared-memory multiprocessors. WRL Res Rep 95(9). doi: 10.1.1.37.3026"},{"key":"161_CR25","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":"161_CR26","unstructured":"Higham L, Kawash J, Verwaal N (1998) Weak memory consistency models part I: definitions and comparisons. Technical report 98\/612\/03, Department of Computer Science, The University of Calgary"},{"key":"161_CR27","unstructured":"Intel 64 Architecture Memory Ordering White Paper, August 2007"},{"key":"161_CR28","unstructured":"Intel 64 and IA-32 Architectures Software Developer\u2019s Manual, vol 3A, October 2011"},{"key":"161_CR29","unstructured":"A Formal Specification of Intel Itanium Processor Family Memory Ordering, October 2002. Intel Document 251429-001"},{"issue":"7","key":"161_CR30","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":"161_CR31","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":"161_CR32","volume-title":"POPL","author":"J Manson","year":"2005","unstructured":"Manson J, Pugh W, Adve SV (2005) The Java memory model. In: POPL"},{"key":"161_CR33","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":"161_CR34","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":"161_CR35","volume-title":"PLDI 11","author":"S Sarkar","year":"2011","unstructured":"Sarkar S, Sewell P, Alglave J, Maranget L, Williams D (2011) Understanding power multiprocessors. In: PLDI 11"},{"key":"161_CR36","unstructured":"Sparc Architecture Manual Version 8 (1992)"},{"key":"161_CR37","unstructured":"Sparc Architecture Manual Version 9 (1994)"},{"key":"161_CR38","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"},{"key":"161_CR39","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":"161_CR40","volume-title":"EC2 09","author":"F Zappa Nardelli","year":"2009","unstructured":"Zappa Nardelli F, Sewell P, Sevcik J, Sarkar S, Owens S, Maranget L, Batty M, Alglave J (2009) Relaxed memory models must be rigorous. In: EC2 09"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0161-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-012-0161-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0161-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T18:05:52Z","timestamp":1559239552000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-012-0161-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,27]]},"references-count":40,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,10]]}},"alternative-id":["161"],"URL":"https:\/\/doi.org\/10.1007\/s10703-012-0161-5","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,6,27]]}}}