{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T01:29:35Z","timestamp":1743125375832,"version":"3.40.3"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319189406"},{"type":"electronic","value":"9783319189413"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-18941-3_3","type":"book-chapter","created":{"date-parts":[[2015,5,6]],"date-time":"2015-05-06T15:14:47Z","timestamp":1430925287000},"page":"97-145","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Modeling of Architectures"],"prefix":"10.1007","author":[{"given":"Jade","family":"Alglave","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,5,7]]},"reference":[{"key":"3_CR1","unstructured":"Alglave, J.: A shared memory poetics. Ph.D. thesis, Universit\u00e9 Paris 7 (2010)"},{"issue":"2","key":"3_CR2","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/s10703-012-0161-5","volume":"41","author":"J Alglave","year":"2012","unstructured":"Alglave, J.: A formal hierarchy of weak memory models. Formal Methods Syst. Des. 41(2), 178\u2013210 (2012)","journal-title":"Formal Methods Syst. Des."},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Alglave, J., Batty, M., Donaldson, A.F., Gopalakrishnan, G., Ketema, J., Poetzl, D., Sorensen, T., Wickerson, J.: GPU concurrency: weak behaviours and programming assumptions. In: ASPLOS (2015)","DOI":"10.1145\/2694344.2694391"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-642-25318-8_21","volume-title":"Programming Languages and Systems","author":"J Alglave","year":"2011","unstructured":"Alglave, J., Kroening, D., Lugton, J., Nimal, V., Tautschnig, M.: Soundness of data flow analyses for weak memory models. In: Yang, H. (ed.) APLAS 2011. LNCS, vol. 7078, pp. 272\u2013288. Springer, Heidelberg (2011)"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data-mining for weak memory. TOPLAS 36(2) (2014)","DOI":"10.1145\/2627752"},{"key":"3_CR6","unstructured":"The Beatles: The Continuing Story of Bungalow Bill. In: White Album (1968)"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Hower, D.R., Hechtman, B.A., Beckmann, B.M., Gaster, B.R., Hill, M.D., Reinhardt, S.K., Wood, D.A.: Heterogeneous-race-free memory models. In: ASPLOS 14 (2014)","DOI":"10.1145\/2541940.2541981"},{"issue":"9","key":"3_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 programs. IEEE Trans. Comput. 28(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Comput."},{"key":"3_CR9","unstructured":"Roxy Music: Re-Make Re-Model. In: Roxy Music (1972)"},{"key":"3_CR10","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. 5674, pp. 391\u2013407. Springer, Heidelberg (2009)"},{"key":"3_CR11","unstructured":"SPARC International Inc.: The SPARC Architecture Manual Version 9 (1994)"},{"key":"3_CR12","unstructured":"Sparks: Here Kitty. In: Hello Young Lovers (2006)"},{"key":"3_CR13","unstructured":"T-Rex: Jeepster. In: Electric Warrior (1971)"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Balabonski, T., Chakraborty, S., Morisset, R., Nardelli, F.Z.: Common compiler optimisations are invalid in the C11 memory model and what we can do about it. In: POPL (2015)","DOI":"10.1145\/2676726.2676995"},{"key":"3_CR15","unstructured":"Sonic Youth: Kool Thing. In: Goo (1990)"},{"key":"3_CR16","unstructured":"Led Zeppelin: Black Dog. In: Led Zeppelin IV (1971)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Multicore Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-18941-3_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T01:16:07Z","timestamp":1676942167000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-18941-3_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319189406","9783319189413"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-18941-3_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"7 May 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}