{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T22:30:57Z","timestamp":1742941857704,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030549961"},{"type":"electronic","value":"9783030549978"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-54997-8_22","type":"book-chapter","created":{"date-parts":[[2020,8,10]],"date-time":"2020-08-10T20:11:50Z","timestamp":1597090310000},"page":"342-357","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Weakening Correctness and Linearizability for Concurrent Objects on Multicore Processors"],"prefix":"10.1007","author":[{"given":"Graeme","family":"Smith","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lindsay","family":"Groves","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,8,11]]},"reference":[{"key":"22_CR1","doi-asserted-by":"publisher","unstructured":"Back, R.-J.R.: Refinement calculus, part II: Parallel and reactive programs. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1989. LNCS, vol. 430, pp. 67\u201393. Springer, Heidelberg (1990). \nhttps:\/\/doi.org\/10.1007\/3-540-52559-9_61","DOI":"10.1007\/3-540-52559-9_61"},{"key":"22_CR2","doi-asserted-by":"publisher","unstructured":"Back, R.-J.R., von Wright, J.: Trace refinement of action systems. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 367\u2013384. Springer, Heidelberg (1994). \nhttps:\/\/doi.org\/10.1007\/978-3-540-48654-1_28","DOI":"10.1007\/978-3-540-48654-1_28"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: POPL, pp. 55\u201366. ACM (2011)","DOI":"10.1145\/1925844.1926394"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-642-28869-2_5","volume-title":"Programming Languages and Systems","author":"S Burckhardt","year":"2012","unstructured":"Burckhardt, S., Gotsman, A., Musuvathi, M., Yang, H.: Concurrent library correctness on the TSO memory model. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 87\u2013107. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-28869-2_5"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Chase, D., Lev, Y.: Dynamic circular work-stealing deque. In: SPAA 2005, pp. 21\u201328. ACM Press (2005)","DOI":"10.1145\/1073970.1073974"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-319-95582-7_14","volume-title":"Formal Methods","author":"RJ Colvin","year":"2018","unstructured":"Colvin, R.J., Smith, G.: A wide-spectrum language for verification of programs on weak memory models. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 240\u2013257. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-95582-7_14"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-319-19249-9_12","volume-title":"FM 2015: Formal Methods","author":"J Derrick","year":"2015","unstructured":"Derrick, J., Smith, G.: A framework for correctness criteria on weak memory models. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 178\u2013194. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-19249-9_12"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-319-10181-1_21","volume-title":"Integrated Formal Methods","author":"J Derrick","year":"2014","unstructured":"Derrick, J., Smith, G., Dongol, B.: Verifying linearizability on TSO architectures. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 341\u2013356. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-10181-1_21"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-319-41591-8_4","volume-title":"Software Engineering and Formal Methods","author":"S Doherty","year":"2016","unstructured":"Doherty, S., Derrick, J.: Linearizability and causality. In: De Nicola, R., K\u00fchn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 45\u201360. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-41591-8_4"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-319-47846-3_17","volume-title":"Formal Methods and Software Engineering","author":"B Dongol","year":"2016","unstructured":"Dongol, B., Groves, L.: Contextual trace refinement for concurrent objects: safety and progress. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 261\u2013278. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-47846-3_17"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-319-73721-8_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Dongol","year":"2018","unstructured":"Dongol, B., Jagadeesan, R., Riely, J., Armstrong, A.: On abstraction and compositionality for weak-memory linearisability. VMCAI 2018. LNCS, vol. 10747, pp. 183\u2013204. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-73721-8_9"},{"issue":"51\u201352","key":"22_CR12","doi-asserted-by":"publisher","first-page":"4379","DOI":"10.1016\/j.tcs.2010.09.021","volume":"411","author":"I Filipovi\u0107","year":"2010","unstructured":"Filipovi\u0107, I., O\u2019Hearn, P.W., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. Theor. Comput. Sci. 411(51\u201352), 4379\u20134398 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"Flur, S., et al.: Modelling the ARMv8 architecture, operationally: concurrency and ISA. In: Bodik, R., Majumdar, R. (eds.) POPL 2016, pp. 608\u2013621. ACM (2016)","DOI":"10.1145\/2914770.2837615"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-33651-5_3","volume-title":"Distributed Computing","author":"A Gotsman","year":"2012","unstructured":"Gotsman, A., Musuvathi, M., Yang, H.: Show no weakness: sequentially consistent specifications of TSO libraries. In: Aguilera, M.K. (ed.) DISC 2012. LNCS, vol. 7611, pp. 31\u201345. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-33651-5_3"},{"key":"22_CR15","volume-title":"The Art of Multiprocessor Programming","author":"M Herlihy","year":"2008","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann, San Francisco (2008)"},{"issue":"3","key":"22_CR16","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"L\u00ea, N.M., Pop, A., Cohen, A., Zappa Nardelli, F.: Correct and efficient work-stealing for weak memory models. In: PPoPP 2013, pp. 69\u201380. ACM (2013)","DOI":"10.1145\/2517327.2442524"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Moir, M., Shavit, N.: Concurrent Data Structures. Handbook of Data Structures and Applications, pp. 47:1\u201347:30 (2004)","DOI":"10.1201\/9781420035179.ch47"},{"key":"22_CR19","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). \nhttps:\/\/doi.org\/10.1007\/978-3-642-03359-9_27"},{"issue":"POPL","key":"22_CR20","doi-asserted-by":"publisher","first-page":"19:1","DOI":"10.1145\/3158107","volume":"2","author":"C Pulte","year":"2018","unstructured":"Pulte, C., Flur, S., Deacon, W., French, J., Sarkar, S., Sewell, P.: Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8. Proc. ACM Program. Lang. 2(POPL), 19:1\u201319:29 (2018)","journal-title":"Proc. ACM Program. Lang."},{"issue":"POPL","key":"22_CR21","doi-asserted-by":"publisher","first-page":"68:1","DOI":"10.1145\/3290381","volume":"3","author":"A Raad","year":"2019","unstructured":"Raad, A., Doko, M., Ro\u017ei\u0107, L., Lahav, O., Vafeiadis, V.: On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models. Proc. ACM Program. Lang. 3(POPL), 68:1\u201368:31 (2019)","journal-title":"Proc. ACM Program. Lang."},{"issue":"6","key":"22_CR22","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1145\/1993316.1993520","volume":"46","author":"S Sarkar","year":"2011","unstructured":"Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. SIGPLAN Not. 46(6), 175\u2013186 (2011)","journal-title":"SIGPLAN Not."},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Smith, G., Winter, K., Colvin, R.J.: Correctness of concurrent objects under weak memory models. In: Derrick, J., Dongol, B., Reeves, S. (eds.) Refine 2018, EPTCS, vol. 282, pp. 53\u201367. Open Publishing Association (2018)","DOI":"10.4204\/EPTCS.282.5"},{"key":"22_CR24","unstructured":"Smith, G., Winter, K., Colvin, R.J.: A sound and complete definition of linearizability on weak memory models. CoRR, abs\/1802.04954v2 (2019)"},{"key":"22_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-319-03077-7_21","volume-title":"Hardware and Software: Verification and Testing","author":"O Travkin","year":"2013","unstructured":"Travkin, O., M\u00fctze, A., Wehrheim, H.: SPIN as a linearizability checker under weak memory models. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 311\u2013326. Springer, Cham (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-319-03077-7_21"}],"container-title":["Lecture Notes in Computer Science","Formal Methods. FM 2019 International Workshops"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-54997-8_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,10]],"date-time":"2020-08-10T20:16:54Z","timestamp":1597090614000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-54997-8_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030549961","9783030549978"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-54997-8_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"11 August 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/formalmethods2019.inesctec.pt\/?page_id=84","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"129","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"44","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"34% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5,5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}