{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:02:14Z","timestamp":1767927734839,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642287282","type":"print"},{"value":"9783642287299","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28729-9_12","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T20:47:40Z","timestamp":1332449260000},"page":"180-194","source":"Crossref","is-referenced-by-count":8,"title":["Brookes Is Relaxed, Almost!"],"prefix":"10.1007","author":[{"given":"Radha","family":"Jagadeesan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gustavo","family":"Petri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James","family":"Riely","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/1787234.1787255","volume":"53","author":"S.V. Adve","year":"2010","unstructured":"Adve, S.V., Boehm, H.-J.: Memory models: a case for rethinking parallel languages and hardware. Commun. ACM\u00a053, 90\u2013101 (2010) ISSN 0001-0782","journal-title":"Commun. ACM"},{"issue":"12","key":"12_CR2","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"S.V. Adve","year":"1996","unstructured":"Adve, S.V., Gharachorloo, K.: Shared memory consistency models: A tutorial. Computer\u00a029(12), 66\u201376 (1996)","journal-title":"Computer"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Adve, S.V., Hill, M.D.: Weak ordering - a new definition. In: ISCA, pp. 2\u201314 (1990)","DOI":"10.1145\/325096.325100"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Boudol, G., Petri, G.: Relaxed memory models: an operational approach. In: POPL, pp. 392\u2013403 (2009)","DOI":"10.1145\/1594834.1480930"},{"issue":"1-3","key":"12_CR5","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/j.tcs.2006.12.034","volume":"375","author":"S. Brookes","year":"2007","unstructured":"Brookes, S.: A semantics for concurrent separation logic. Theor. Comput. Sci.\u00a0375(1-3), 227\u2013270 (2007)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"12_CR6","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1006\/inco.1996.0056","volume":"127","author":"S. Brookes","year":"1996","unstructured":"Brookes, S.: Full abstraction for a shared-variable parallel language. Inf. Comput.\u00a0127(2), 145\u2013163 (1996)","journal-title":"Inf. Comput."},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-642-11957-6_17","volume-title":"Programming Languages and Systems","author":"R. Jagadeesan","year":"2010","unstructured":"Jagadeesan, R., Pitcher, C., Riely, J.: Generative Operational Semantics for Relaxed Memory Models. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 307\u2013326. Springer, Heidelberg (2010)"},{"issue":"9","key":"12_CR8","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L. Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess program. IEEE Trans. Comput.\u00a028(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Comput."},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The java memory model. In: POPL, pp. 378\u2013391 (2005)","DOI":"10.1145\/1047659.1040336"},{"issue":"1-3","key":"12_CR10","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"P.W. O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci.\u00a0375(1-3), 271\u2013307 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR11","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":"12_CR12","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bornat, R., O\u2019Hearn, P.W.: Modular verification of a non-blocking stack. In: POPL, pp. 297\u2013302 (2007)","DOI":"10.1145\/1190215.1190261"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Sevc\u00edk, J., Vafeiadis, V., Nardelli, F.Z., Jagannathan, S., Sewell, P.: Relaxed-memory concurrency and verified compilation. In: POPL, pp. 43\u201354 (2011)","DOI":"10.1145\/1925844.1926393"},{"issue":"7","key":"12_CR15","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/1785414.1785443","volume":"53","author":"P. Sewell","year":"2010","unstructured":"Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-TSO: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun. ACM\u00a053(7), 89\u201397 (2010)","journal-title":"Commun. ACM"},{"key":"12_CR16","unstructured":"Inc. CORPORATE.\u00a0SPARC. The SPARC Architecture Manual (version 9). Prentice-Hall, Inc., Upper Saddle River (1994)"},{"key":"12_CR17","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1145\/1925844.1926415","volume":"46","author":"A.J. Turon","year":"2011","unstructured":"Turon, A.J., Wand, M.: A separation logic for refining concurrent objects. SIGPLAN Not.\u00a046, 247\u2013258 (2011) ISSN 0362-1340","journal-title":"SIGPLAN Not."},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"V. Vafeiadis","year":"2007","unstructured":"Vafeiadis, V., Parkinson, M.J.: A Marriage of Rely\/Guarantee and Separation Logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 256\u2013271. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computational Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28729-9_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,23]],"date-time":"2025-03-23T18:49:17Z","timestamp":1742755757000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28729-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642287282","9783642287299"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28729-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}