{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T21:32:12Z","timestamp":1648762332913},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2011,11,23]],"date-time":"2011-11-23T00:00:00Z","timestamp":1322006400000},"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":[[2011,12]]},"DOI":"10.1007\/s10703-011-0131-3","type":"journal-article","created":{"date-parts":[[2011,11,22]],"date-time":"2011-11-22T15:50:44Z","timestamp":1321977044000},"page":"297-331","source":"Crossref","is-referenced-by-count":0,"title":["Verification of STM on relaxed memory models"],"prefix":"10.1007","volume":"39","author":[{"given":"Rachid","family":"Guerraoui","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vasu","family":"Singh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,11,23]]},"reference":[{"key":"131_CR1","unstructured":"Adve SV, Gharachorloo K (1996) Shared memory consistency models: A tutorial. IEEE Comput 66\u201376"},{"key":"131_CR2","doi-asserted-by":"crossref","first-page":"484","DOI":"10.1007\/978-3-540-27813-9_42","volume-title":"International conference on computer aided verification","author":"T Andrews","year":"2004","unstructured":"Andrews T, Qadeer S, Rajamani SK, Rehof J, Xie Y (2004) Zing: A model checker for concurrent software. In: International conference on computer aided verification. Springer, Berlin, pp 484\u2013487"},{"key":"131_CR3","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/1375581.1375591","volume-title":"ACM SIGPLAN conference on programming language design and implementation","author":"HJ Boehm","year":"2008","unstructured":"Boehm HJ, Adve SV (2008) Foundations of the C++ concurrency memory model. In: ACM SIGPLAN conference on programming language design and implementation. ACM, New York, pp 68\u201378"},{"key":"131_CR4","first-page":"392","volume-title":"ACM SIGPLAN symposium on principles of programming languages","author":"G Boudol","year":"2009","unstructured":"Boudol G, Petri G (2009) Relaxed memory models: An operational approach. In: ACM SIGPLAN symposium on principles of programming languages, pp 392\u2013403"},{"key":"131_CR5","doi-asserted-by":"crossref","first-page":"489","DOI":"10.1007\/11817963_45","volume-title":"International conference on computer aided verification","author":"S Burckhardt","year":"2006","unstructured":"Burckhardt S, Alur R, Martin MMK (2006) Bounded model checking of concurrent data types on relaxed memory models: A case study. In: International conference on computer aided verification. Springer, Berlin, pp 489\u2013502"},{"key":"131_CR6","first-page":"12","volume-title":"ACM SIGPLAN conference on programming language design and implementation","author":"S Burckhardt","year":"2007","unstructured":"Burckhardt S, Alur R, Martin MMK (2007) CheckFence: Checking consistency of concurrent data types on relaxed memory models. In: ACM SIGPLAN conference on programming language design and implementation. ACM, New York, pp 12\u201321"},{"key":"131_CR7","unstructured":"Burckhardt S, Musuvathi M, Singh V (2008) Verifying compiler transformations for concurrent programs. Technical Report MSR-TR-2008-171, Microsoft Research"},{"key":"131_CR8","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/978-3-540-70545-1_13","volume-title":"International conference on computer aided verification","author":"A Cohen","year":"2008","unstructured":"Cohen A, Pnueli A, Zuck LD (2008) Mechanical verification of transactional memories with non-transactional memory accesses. In: International conference on computer aided verification. Springer, Berlin, pp 121\u2013134"},{"key":"131_CR9","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1007\/11817963_44","volume-title":"International conference on computer aided verification","author":"R Colvin","year":"2006","unstructured":"Colvin R, Groves L, Luchangco V, Moir M (2006) Formal verification of a lazy concurrent list-based set algorithm. In: International conference on computer aided verification. Springer, Berlin, pp 475\u2013488"},{"key":"131_CR10","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/11817963_5","volume-title":"International conference on computer aided verification","author":"M Wulf De","year":"2006","unstructured":"De Wulf M, Doyen L, Henzinger TA, Raskin J-F (2006) Antichains: A new algorithm for checking universality of finite automata. In: International conference on computer aided verification. Springer, Berlin, pp 17\u201330"},{"key":"131_CR11","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1007\/11864219_14","volume-title":"International symposium on distributed computing","author":"D Dice","year":"2006","unstructured":"Dice D, Shalev O, Shavit N (2006) Transactional locking II. In: International symposium on distributed computing. Springer, Berlin, pp 194\u2013208"},{"key":"131_CR12","first-page":"27","volume-title":"ACM SIGPLAN conference on programming language design and implementation","author":"T Elmas","year":"2005","unstructured":"Elmas T, Tasiran S, Qadeer S (2005) VYRD: Verifying concurrent programs by runtime refinement-violation detection. In: ACM SIGPLAN conference on programming language design and implementation, pp 27\u201337"},{"key":"131_CR13","first-page":"245","volume-title":"ACM SIGPLAN conference on programming language design and implementation","author":"T Elmas","year":"2007","unstructured":"Elmas T, Qadeer S, Tasiran S (2007) Goldilocks: A race and transaction-aware Java runtime. In: ACM SIGPLAN conference on programming language design and implementation, pp 245\u2013255"},{"key":"131_CR14","first-page":"285","volume-title":"International conference on supercomputing","author":"X Fang","year":"2003","unstructured":"Fang X, Lee J, Midkiff SP (2003) Automatic fence insertion for shared memory multiprocessing. In: International conference on supercomputing, pp 285\u2013294"},{"key":"131_CR15","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1145\/964001.964023","volume-title":"ACM SIGPLAN symposium on principles of programming languages","author":"C Flanagan","year":"2004","unstructured":"Flanagan C, Freund SN (2004) Atomizer: A dynamic atomicity checker for multithreaded programs. In: ACM SIGPLAN symposium on principles of programming languages, pp 256\u2013267"},{"key":"131_CR16","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1145\/1542476.1542490","volume-title":"ACM SIGPLAN conference on programming language design and implementation","author":"C Flanagan","year":"2009","unstructured":"Flanagan C, Freund SN (2009) FastTrack: Efficient and precise dynamic race detection. In: ACM SIGPLAN conference on programming language design and implementation, pp 121\u2013133"},{"key":"131_CR17","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/1375581.1375618","volume-title":"ACM SIGPLAN conference on programming language design and implementation","author":"C Flanagan","year":"2008","unstructured":"Flanagan C, Freund SN, Yi J (2008) Velodrome: A sound and complete dynamic atomicity checker for multithreaded programs. In: ACM SIGPLAN conference on programming language design and implementation, pp 293\u2013303"},{"key":"131_CR18","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/978-3-540-27813-9_31","volume-title":"International conference on computer aided verification","author":"G Gopalakrishnan","year":"2004","unstructured":"Gopalakrishnan G, Yang Y, Sivaraj H (2004) QB or Not QB: An efficient execution verification tool for memory orderings. In: International conference on computer aided verification. Springer, Berlin, pp 401\u2013413"},{"key":"131_CR19","doi-asserted-by":"crossref","first-page":"372","DOI":"10.1145\/1375581.1375626","volume-title":"ACM SIGPLAN conference on programming language design and implementation","author":"R Guerraoui","year":"2008","unstructured":"Guerraoui R, Henzinger TA, Jobstmann B, Singh V (2008) Model checking transactional memories. In: ACM SIGPLAN conference on programming language design and implementation. ACM, New York, pp 372\u2013382"},{"key":"131_CR20","first-page":"21","volume-title":"International conference on concurrency theory","author":"R Guerraoui","year":"2008","unstructured":"Guerraoui R, Henzinger TA, Singh V (2008) Nondeterminism and completeness in model checking transactional memories. In: International conference on concurrency theory. Springer, Berlin, pp 21\u201335"},{"key":"131_CR21","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/978-3-642-02658-4_26","volume-title":"International conference on computer aided verification","author":"R Guerraoui","year":"2009","unstructured":"Guerraoui R, Henzinger TA, Singh V (2009) Software transactional memory on relaxed memory models. In: International conference on computer aided verification. Springer, Berlin, pp 321\u2013336"},{"key":"131_CR22","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1145\/1345206.1345233","volume-title":"ACM SIGPLAN symposium on principles and practice of parallel programming","author":"R Guerraoui","year":"2008","unstructured":"Guerraoui R, Kapa\u0142ka M (2008) On the correctness of transactional memory. In: ACM SIGPLAN symposium on principles and practice of parallel programming. ACM, New York, pp 175\u2013184"},{"key":"131_CR23","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1109\/ISCA.1993.698569","volume-title":"International symposium on computer architecture","author":"M Herlihy","year":"1993","unstructured":"Herlihy M, Moss JEB (1993) Transactional memory: Architectural support for lock-free data structures. In: International symposium on computer architecture. ACM, New York, pp 289\u2013300"},{"key":"131_CR24","first-page":"92","volume-title":"ACM SIGACT-SIGOPS symposium on principles of distributed computing","author":"M Herlihy","year":"2003","unstructured":"Herlihy M, Luchangco V, Moir M, Scherer WN (2003) Software transactional memory for dynamic-sized data structures. In: ACM SIGACT-SIGOPS symposium on principles of distributed computing. ACM, New York, pp 92\u2013101"},{"key":"131_CR25","doi-asserted-by":"crossref","unstructured":"Holzmann GJ (1997) The model checker SPIN. IEEE Trans Softw Eng 279\u2013295","DOI":"10.1109\/32.588521"},{"key":"131_CR26","doi-asserted-by":"crossref","unstructured":"Lamport L (1979) How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans Comput 690\u2013691","DOI":"10.1109\/TC.1979.1675439"},{"key":"131_CR27","doi-asserted-by":"crossref","unstructured":"Lee J, Padua DA (2001) Hiding relaxed memory consistency with a compiler. IEEE Trans Comput 824\u2013833","DOI":"10.1109\/12.947002"},{"key":"131_CR28","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1145\/1152154.1152177","volume-title":"International conference on parallel architectures and compilation techniques","author":"C Manovit","year":"2006","unstructured":"Manovit C, Hangal S, Chafi H, McDonald A, Kozyrakis C, Olukotun K (2006) Testing implementations of transactional memory. In: International conference on parallel architectures and compilation techniques, pp 134\u2013143"},{"key":"131_CR29","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1145\/1040305.1040336","volume-title":"ACM SIGPLAN symposium on principles of programming languages","author":"J Manson","year":"2005","unstructured":"Manson J, Pugh W, Adve SV (2005) The Java memory model. In: ACM SIGPLAN symposium on principles of programming languages. ACM, New York, pp 378\u2013391"},{"key":"131_CR30","first-page":"267","volume-title":"USENIX symposium on operating systems design and implementation","author":"M Musuvathi","year":"2008","unstructured":"Musuvathi M, Qadeer S, Ball T, Basler G, Nainar PA, Neamtiu I (2008) Finding and reproducing heisenbugs in concurrent programs. In: USENIX symposium on operating systems design and implementation, pp 267\u2013280"},{"key":"131_CR31","doi-asserted-by":"crossref","unstructured":"Papadimitriou CH (1979) The serializability of concurrent database updates. J ACM 26(4)","DOI":"10.1145\/322154.322158"},{"key":"131_CR32","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"International conference on tools and algorithms for the construction and analysis of systems","author":"S Qadeer","year":"2005","unstructured":"Qadeer S, Rehof J (2005) Context-bounded model checking of concurrent software. In: International conference on tools and algorithms for the construction and analysis of systems, pp 93\u2013107"},{"key":"131_CR33","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1145\/996841.996845","volume-title":"ACM SIGPLAN conference on programming language design and implementation","author":"S Qadeer","year":"2004","unstructured":"Qadeer S, Wu D (2004) KISS: Keep it simple and sequential. In: ACM SIGPLAN conference on programming language design and implementation, pp 14\u201324"},{"key":"131_CR34","first-page":"187","volume-title":"ACM SIGPLAN symposium on principles and practice of parallel programming","author":"B Saha","year":"2006","unstructured":"Saha B, Adl-Tabatabai A, Hudson RL, Minh CC, Hertzberg B (2006) McRT-STM: A high performance software transactional memory system for a multi-core runtime. In: ACM SIGPLAN symposium on principles and practice of parallel programming. ACM, New York, pp 187\u2013197"},{"key":"131_CR35","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1145\/1229428.1229469","volume-title":"ACM SIGPLAN symposium on principles and practice of parallel programming","author":"VA Saraswat","year":"2007","unstructured":"Saraswat VA, Jagadeesan R, Michael M, von Praun C (2007) A theory of memory models. In: ACM SIGPLAN symposium on principles and practice of parallel programming. ACM, New York, pp 161\u2013172"},{"key":"131_CR36","first-page":"379","volume-title":"ACM SIGPLAN symposium on principles of programming languages","author":"S Sarkar","year":"2009","unstructured":"Sarkar S, Sewell P, Zappa Nardelli F, Owens S, Ridge T, Braibant T, Myreen MO, Alglave J (2009) The semantics of x86-CC multiprocessor machine code. In: ACM SIGPLAN symposium on principles of programming languages, pp 379\u2013391"},{"key":"131_CR37","volume-title":"ACM SIGPLAN workshop on transactional computing","author":"ML Scott","year":"2006","unstructured":"Scott ML (2006) Sequential specification of transactional memory semantics. In: ACM SIGPLAN workshop on transactional computing"},{"key":"131_CR38","first-page":"204","volume-title":"ACM SIGACT-SIGOPS symposium on principles of distributed computing","author":"N Shavit","year":"1995","unstructured":"Shavit N, Touitou D (1995) Software transactional memory. In: ACM SIGACT-SIGOPS symposium on principles of distributed computing. ACM, New York, pp 204\u2013213"},{"key":"131_CR39","volume-title":"Alpha architecture reference manual","author":"RL Sites","year":"2002","unstructured":"Sites RL (ed) (2002) Alpha architecture reference manual. Digital Press, Newton"},{"key":"131_CR40","unstructured":"Tasiran S (2008) A compositional method for verifying software transactional memory implementations. Technical Report MSR-TR-2008-56, Microsoft Research"},{"key":"131_CR41","first-page":"129","volume-title":"ACM SIGPLAN symposium on principles and practice of parallel programming","author":"V Vafeiadis","year":"2006","unstructured":"Vafeiadis V, Herlihy M, Hoare T, Shapiro M (2006) Proving correctness of highly-concurrent linearisable objects. In: ACM SIGPLAN symposium on principles and practice of parallel programming, pp 129\u2013136"},{"key":"131_CR42","volume-title":"The SPARC architecture manual (version\u00a09)","year":"1994","unstructured":"Weaver D, Germond T (eds) (1994) The SPARC architecture manual (version\u00a09). Prentice-Hall Inc, Englewood Cliffs"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0131-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-011-0131-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0131-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,17]],"date-time":"2021-12-17T16:44:39Z","timestamp":1639759479000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-011-0131-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,11,23]]},"references-count":42,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2011,12]]}},"alternative-id":["131"],"URL":"https:\/\/doi.org\/10.1007\/s10703-011-0131-3","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,11,23]]}}}