{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,30]],"date-time":"2025-12-30T23:36:22Z","timestamp":1767137782610,"version":"build-2238731810"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319051185","type":"print"},{"value":"9783319051192","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-05119-2_15","type":"book-chapter","created":{"date-parts":[[2014,3,7]],"date-time":"2014-03-07T04:36:28Z","timestamp":1394166988000},"page":"254-272","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Studying Operational Models of Relaxed Concurrency"],"prefix":"10.1007","author":[{"given":"Gustavo","family":"Petri","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,3,8]]},"reference":[{"key":"15_CR1","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"SV Adve","year":"1996","unstructured":"Adve, S.V., Gharachorloo, K.: Shared memory consistency models: a tutorial. Computer 29, 66\u201376 (1996)","journal-title":"Computer"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Adve, S.V., Hill, M.D.: Weak ordering \u2013 a new definition. In: ISCA, pp. 2\u201314. ACM, New York (1990)","DOI":"10.1145\/325096.325100"},{"key":"15_CR3","unstructured":"Alglave, J.: A shared memory poetics. Ph.D. thesis, Universit\u00e9 Paris 7 (2010)"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: POPL \u201910, pp. 7\u201318 (2010)","DOI":"10.1145\/1707801.1706303"},{"key":"15_CR5","series-title":"LNCS","first-page":"26","volume-title":"ESOP 2012","author":"MF Atig","year":"2012","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: What\u2019s decidable about weak memory models? In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 26\u201346. Springer, Heidelberg (2012)"},{"issue":"1","key":"15_CR6","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1145\/322108.322122","volume":"26","author":"G Berry","year":"1979","unstructured":"Berry, G., L\u00e9vy, J.-J.: Minimal and optimal computations of recursive programs. J. ACM 26(1), 148\u2013175 (1979)","journal-title":"J. ACM"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Boudol, G., Petri, G.: Relaxed memory models: an operational approach. In: POPL, pp. 392\u2013403. ACM, New York (2009)","DOI":"10.1145\/1594834.1480930"},{"key":"15_CR8","series-title":"LNCS","first-page":"165","volume-title":"ESOP 2010","author":"G Boudol","year":"2010","unstructured":"Boudol, G., Petri, G.: A theory of speculative computation. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 165\u2013184. Springer, Heidelberg (2010)"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations. In: PLDI, pp. 237\u2013247. ACM, New York (1993)","DOI":"10.1145\/173262.155113"},{"key":"15_CR10","series-title":"LNCS","first-page":"307","volume-title":"ESOP 2010","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. 6012, pp. 307\u2013326. Springer, Heidelberg (2010)"},{"issue":"9","key":"15_CR11","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 progranm. IEEE Trans. Comput. 28(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Comput."},{"key":"15_CR12","first-page":"159","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"J-J L\u00e9vy","year":"1980","unstructured":"L\u00e9vy, J.-J.: Optimal reductions in the lambda calculus. In: Seldin, J.P., Hindley, J.R. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 159\u2013191. Academic Press, London (1980)"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: POPL \u201905, pp. 378\u2013391. ACM, New York (2005)","DOI":"10.1145\/1047659.1040336"},{"key":"15_CR14","series-title":"LNCS","first-page":"391","volume-title":"TPHOLs 2009","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. 5674, pp. 391\u2013407. Springer, Heidelberg (2009)"},{"key":"15_CR15","unstructured":"Petri, G.: Operational semantics of relaxed memory models. Ph.D. thesis, Nice (2010). http:\/\/www.cs.purdue.edu\/homes\/gpetri\/publis\/thesisPetri.pdf"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Petri, G.: Studying operational models of relaxed concurrency (extended version) (2013). http:\/\/www.cs.purdue.edu\/homes\/gpetri\/publis\/opsem-long.pdf","DOI":"10.1007\/978-3-319-14128-2_15"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Saraswat, V.A., Jagadeesan, R., Michael, M.M., von Praun, C.: A theory of memory models. In: PPOPP, pp. 161\u2013172 (2007)","DOI":"10.1145\/1229428.1229469"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Sewell, P., Nardelli, F.Z., Owens, S., Ridge, T., Braibant, T., Myreen, M.O., Alglave, J.: The semantics of x86-CC multiprocessor machine code. In: POPL, pp. 379\u2013391. ACM, New York (2009)","DOI":"10.1145\/1594834.1480929"},{"issue":"7","key":"15_CR19","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. CACM 53(7), 89\u201397 (2010)","journal-title":"CACM"},{"key":"15_CR20","unstructured":"CORPORATE SPARC Inc.: The SPARC Architecture Manual (version 9). Prentice-Hall Inc., Upper Saddle River (1994)"}],"container-title":["Lecture Notes in Computer Science","Trustworthy Global Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-05119-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,22]],"date-time":"2023-12-22T00:11:44Z","timestamp":1703203904000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-05119-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319051185","9783319051192"],"references-count":20,"aliases":["10.1007\/978-3-319-14128-2_15"],"URL":"https:\/\/doi.org\/10.1007\/978-3-319-05119-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"8 March 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}