{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:23:41Z","timestamp":1779074621581,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642288685","type":"print"},{"value":"9783642288692","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28869-2_5","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T20:44:36Z","timestamp":1332449076000},"page":"87-107","source":"Crossref","is-referenced-by-count":47,"title":["Concurrent Library Correctness on the TSO Memory Model"],"prefix":"10.1007","author":[{"given":"Sebastian","family":"Burckhardt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexey","family":"Gotsman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Madanlal","family":"Musuvathi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Alglave, J., Fox, A., Ishtiaq, S., Myreen, M.O., Sarkar, S., Sewell, P., Zappa Nardelli, F.: The semantics of Power and ARM multiprocessor machine code. In: DAMP (2009)","DOI":"10.1145\/1629635.1629638"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: POPL (2011)","DOI":"10.1145\/1926385.1926394"},{"key":"5_CR3","unstructured":"Bovet, D., Cesati, M.: Understanding the Linux Kernel, 3rd edn. O\u2019Reilly (2005)"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: A complete and automatic linearizability checker. In: PLDI (2010)","DOI":"10.1145\/1806596.1806634"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Gotsman, A., Musuvathi, M., Yang, H.: Concurrent library correctness on the TSO memory model, extended version (2012), \n                  \n                    http:\/\/www.software.imdea.org\/~gotsman","DOI":"10.1007\/978-3-642-28869-2_5"},{"key":"5_CR6","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":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/978-3-642-14052-5_28","volume-title":"Interactive Theorem Proving","author":"E. Cohen","year":"2010","unstructured":"Cohen, E., Schirmer, B.: From Total Store Order to Sequential Consistency: A Practical Reduction Theorem. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 403\u2013418. Springer, Heidelberg (2010)"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-642-00590-9_19","volume-title":"Programming Languages and Systems","author":"I. Filipovi\u0107","year":"2009","unstructured":"Filipovi\u0107, I., O\u2019Hearn, P., Rinetzky, N., Yang, H.: Abstraction for Concurrent Objects. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol.\u00a05502, pp. 252\u2013266. Springer, Heidelberg (2009)"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Yang, H.: Linearizability with ownership transfer. Draft (2011), \n                  \n                    http:\/\/www.software.imdea.org\/~gotsman","DOI":"10.1007\/978-3-642-32940-1_19"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-642-22012-8_36","volume-title":"Automata, Languages and Programming","author":"A. Gotsman","year":"2011","unstructured":"Gotsman, A., Yang, H.: Liveness-Preserving Atomicity Abstraction. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol.\u00a06756, pp. 453\u2013465. Springer, Heidelberg (2011)"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. TOPLAS\u00a012 (1990)","DOI":"10.1145\/78969.78972"},{"key":"5_CR12","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":"5_CR13","unstructured":"Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: OSDI (2008)"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-642-14107-2_23","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"S. Owens","year":"2010","unstructured":"Owens, S.: Reasoning about the Implementation of Concurrency Abstractions on x86-TSO. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol.\u00a06183, pp. 478\u2013503. Springer, Heidelberg (2010)"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-642-03359-9_27","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Owens","year":"2009","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A Better x86 Memory Model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 391\u2013407. Springer, Heidelberg (2009)"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-15057-9_4","volume-title":"Verified Software: Theories, Tools, Experiments","author":"T. Ridge","year":"2010","unstructured":"Ridge, T.: A Rely-Guarantee Proof System for x86-TSO. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol.\u00a06217, pp. 55\u201370. Springer, Heidelberg (2010)"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: PLDI (2011)","DOI":"10.1145\/1993498.1993520"},{"key":"5_CR18","unstructured":"Vafeiadis, V.: Modular fine-grained concurrency verification. PhD Thesis. Technical Report UCAM-CL-TR-726, University of Cambridge (2008)"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-642-14295-6_40","volume-title":"Computer Aided Verification","author":"V. Vafeiadis","year":"2010","unstructured":"Vafeiadis, V.: Automatically Proving Linearizability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 450\u2013464. Springer, Heidelberg (2010)"},{"key":"5_CR20","unstructured":"Wehrman, I., Berdine, J.: A proposal for weak-memory local reasoning. In: LOLA (2011)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28869-2_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:13:44Z","timestamp":1620126824000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28869-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288685","9783642288692"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28869-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}