{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T20:44:15Z","timestamp":1742935455980,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030171834"},{"type":"electronic","value":"9783030171841"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-17184-1_4","type":"book-chapter","created":{"date-parts":[[2019,4,6]],"date-time":"2019-04-06T17:34:04Z","timestamp":1554572044000},"page":"88-116","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Safe Deferred Memory Reclamation with Types"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5796-2150","authenticated-orcid":false,"given":"Ismail","family":"Kuru","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9012-4490","authenticated-orcid":false,"given":"Colin S.","family":"Gordon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,4,6]]},"reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-39799-8_9","volume-title":"Computer Aided Verification","author":"J Alglave","year":"2013","unstructured":"Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of\u00a0concurrent\u00a0software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 141\u2013157. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-39799-8_9"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Alglave, J., Maranget, L., McKenney, P.E., Parri, A., Stern, A.: Frightening small children and disconcerting grown-ups: concurrency in the Linux kernel. In: Proceedings of the Twenty-Third International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2018, pp. 405\u2013418. ACM, New York (2018). \n                      https:\/\/doi.org\/10.1145\/3173162.3177156\n                      \n                    . \n                      http:\/\/doi.acm.org\/10.1145\/3173162.3177156","DOI":"10.1145\/3173162.3177156"},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Arbel, M., Attiya, H.: Concurrent updates with RCU: search tree as an example. In: Proceedings of the 2014 ACM Symposium on Principles of Distributed Computing, PODC 2014, pp. 196\u2013205. ACM, New York (2014). \n                      https:\/\/doi.org\/10.1145\/2611462.2611471\n                      \n                    . \n                      http:\/\/doi.acm.org\/10.1145\/2611462.2611471","DOI":"10.1145\/2611462.2611471"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). \n                      https:\/\/doi.org\/10.1007\/11804192_17"},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Clements, A.T., Kaashoek, M.F., Zeldovich, N.: Scalable address spaces using RCU balanced trees. In: Proceedings of the 17th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2012, London, UK, 3\u20137 March 2012, pp. 199\u2013210 (2012). \n                      https:\/\/doi.org\/10.1145\/2150976.2150998\n                      \n                    . \n                      http:\/\/doi.acm.org\/10.1145\/2150976.2150998","DOI":"10.1145\/2150976.2150998"},{"key":"4_CR6","unstructured":"Cooper, T., Walpole, J.: Relativistic programming in Haskell using types to enforce a critical section discipline (2015). \n                      http:\/\/web.cecs.pdx.edu\/~walpole\/papers\/haskell2015.pdf"},{"issue":"2","key":"4_CR7","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1145\/2506164.2506174","volume":"47","author":"M Desnoyers","year":"2013","unstructured":"Desnoyers, M., McKenney, P.E., Dagenais, M.R.: Multi-core systems modeling forformal verification of parallel algorithms. SIGOPS Oper. Syst. Rev. 47(2), 51\u201365 (2013). \n                      https:\/\/doi.org\/10.1145\/2506164.2506174\n                      \n                    . \n                      http:\/\/doi.acm.org\/10.1145\/2506164.2506174","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"4_CR8","unstructured":"Desnoyers, M., McKenney, P.E., Stern, A., Walpole, J.: User-level implementations of read-copy update. IEEE Trans. Parallel Distrib. Syst. (2009). \/static\/publications\/desnoyers-ieee-urcu-submitted.pdf"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Rome, Italy, 23\u201325 January, 2013, pp. 287\u2013300 (2013). \n                      https:\/\/doi.org\/10.1145\/2429069.2429104\n                      \n                    . \n                      http:\/\/doi.acm.org\/10.1145\/2429069.2429104","DOI":"10.1145\/2429069.2429104"},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"Feng, X.: Local rely-guarantee reasoning. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 315\u2013327. ACM, New York (2009). \n                      https:\/\/doi.org\/10.1145\/1480881.1480922\n                      \n                    . \n                      http:\/\/doi.acm.org\/10.1145\/1480881.1480922","DOI":"10.1145\/1480881.1480922"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-71316-6_13","volume-title":"Programming Languages and Systems","author":"X Feng","year":"2007","unstructured":"Feng, X., Ferreira, R., Shao, Z.: On the relationship between concurrent separation logic and assume-guarantee reasoning. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 173\u2013188. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-71316-6_13"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-642-15375-4_27","volume-title":"CONCUR 2010 - Concurrency Theory","author":"M Fu","year":"2010","unstructured":"Fu, M., Li, Y., Feng, X., Shao, Z., Zhang, Y.: Reasoning about optimistic concurrency using a program logic for history. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 388\u2013402. Springer, Heidelberg (2010). \n                      https:\/\/doi.org\/10.1007\/978-3-642-15375-4_27"},{"key":"4_CR13","doi-asserted-by":"publisher","unstructured":"Gordon, C.S., Ernst, M.D., Grossman, D., Parkinson, M.J.: Verifying invariants of lock-free data structures with rely-guarantee and refinement types. ACM Trans. Program. Lang. Syst. (TOPLAS) 39(3) (2017). \n                      https:\/\/doi.org\/10.1145\/3064850\n                      \n                    . \n                      http:\/\/doi.acm.org\/10.1145\/3064850","DOI":"10.1145\/3064850"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Gordon, C.S., Parkinson, M.J., Parsons, J., Bromfield, A., Duffy, J.: Uniqueness and reference immutability for safe parallelism. In: Proceedings of the 2012 ACM International Conference on Object Oriented Programming, Systems, Languages, and Applications (OOPSLA 2012), Tucson, AZ, USA, October 2012. \n                      https:\/\/doi.org\/10.1145\/2384616.2384619\n                      \n                    . \n                      http:\/\/dl.acm.org\/citation.cfm?id=2384619","DOI":"10.1145\/2384616.2384619"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-642-37036-6_15","volume-title":"Programming Languages and Systems","author":"A Gotsman","year":"2013","unstructured":"Gotsman, A., Rinetzky, N., Yang, H.: Verifying concurrent memory reclamation algorithms with grace. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 249\u2013269. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-37036-6_15"},{"key":"4_CR16","unstructured":"Howard, P.W., Walpole, J.: A relativistic enhancement to software transactional memory. In: Proceedings of the 3rd USENIX Conference on Hot Topic in Parallelism, HotPar 2011, p. 15. USENIX Association, Berkeley (2011). \n                      http:\/\/dl.acm.org\/citation.cfm?id=2001252.2001267"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Sagonas, K.: Stateless model checking of the Linux kernel\u2019s hierarchical read-copy-update (tree RCU). In: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, SPIN 2017, pp. 172\u2013181. ACM, New York (2017). \n                      https:\/\/doi.org\/10.1145\/3092282.3092287\n                      \n                    . \n                      http:\/\/doi.acm.org\/10.1145\/3092282.3092287","DOI":"10.1145\/3092282.3092287"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-662-54434-1_26","volume-title":"Programming Languages and Systems","author":"R Krebbers","year":"2017","unstructured":"Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.-H., Dreyer, D., Birkedal, L.: The essence of higher-order concurrent separation logic. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 696\u2013723. Springer, Heidelberg (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-662-54434-1_26"},{"issue":"3","key":"4_CR19","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1145\/320613.320619","volume":"5","author":"HT Kung","year":"1980","unstructured":"Kung, H.T., Lehman, P.L.: Concurrent manipulation of binary search trees. ACMTrans. Database Syst. 5(3), 354\u2013382 (1980). \n                      https:\/\/doi.org\/10.1145\/320613.320619\n                      \n                    . \n                      http:\/\/doi.acm.org\/10.1145\/320613.320619","journal-title":"ACMTrans. Database Syst."},{"key":"4_CR20","unstructured":"Kuru, I., Gordon, C.S.: Safe deferred memory reclamation with types. CoRR abs\/1811.11853 (2018). \n                      http:\/\/arxiv.org\/abs\/1811.11853"},{"key":"4_CR21","unstructured":"Liang, L., McKenney, P.E., Kroening, D., Melham, T.: Verification of the tree-based hierarchical read-copy update in the Linux kernel. CoRR abs\/1610.03052 (2016). \n                      http:\/\/arxiv.org\/abs\/1610.03052"},{"issue":"5","key":"4_CR22","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1134\/S0361768816050054","volume":"42","author":"MU Mandrykin","year":"2016","unstructured":"Mandrykin, M.U., Khoroshilov, A.V.: Towards deductive verification of C programs with shared data. Program. Comput. Softw. 42(5), 324\u2013332 (2016). \n                      https:\/\/doi.org\/10.1134\/S0361768816050054","journal-title":"Program. Comput. Softw."},{"key":"4_CR23","unstructured":"Mckenney, P.E.: Exploiting deferred destruction: an analysis of read-copy-update techniques in operating system kernels. Ph.D. thesis, Oregon Health & Science University (2004). aAI3139819"},{"key":"4_CR24","unstructured":"McKenney, P.E.: N4037: non-transactional implementation of atomic tree move, May 2014. \n                      http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2014\/n4037.pdf"},{"key":"4_CR25","unstructured":"McKenney, P.E.: Some examples of kernel-hacker informal correctness reasoning. Technical report paulmck.2015.06.17a (2015). \n                      http:\/\/www2.rdrop.com\/users\/paulmck\/techreports\/IntroRCU.2015.06.17a.pdf"},{"key":"4_CR26","unstructured":"Mckenney, P.E.: A tour through RCU\u2019s requirements (2017). \n                      https:\/\/www.kernel.org\/doc\/Documentation\/RCU\/Design\/Requirements\/Requirements.html"},{"key":"4_CR27","unstructured":"Mckenney, P.E., et al.: Read-copy update. In: Ottawa Linux Symposium, pp. 338\u2013367 (2001)"},{"issue":"POPL","key":"4_CR28","first-page":"58:1","volume":"3","author":"R Meyer","year":"2019","unstructured":"Meyer, R., Wolff, S.: Decoupling lock-free data structures from memory reclamation for static analysis. PACMPL 3(POPL), 58:1\u201358:31 (2019). \n                      https:\/\/dl.acm.org\/citation.cfm?id=3290371","journal-title":"PACMPL"},{"issue":"6","key":"4_CR29","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1109\/TPDS.2004.8","volume":"15","author":"MM Michael","year":"2004","unstructured":"Michael, M.M.: Hazard pointers: safe memory reclamation for lock-free objects. IEEE Trans. Parallel Distrib. Syst. 15(6), 491\u2013504 (2004). \n                      https:\/\/doi.org\/10.1109\/TPDS.2004.8","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41\u201362. Springer, Heidelberg (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2"},{"key":"4_CR31","unstructured":"McKenney, P.E., Mathieu Desnoyers, L.J., Triplett, J.: The RCU-barrier menagerie, November 2016. \n                      https:\/\/lwn.net\/Articles\/573497\/"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Tassarotti, J., Dreyer, D., Vafeiadis, V.: Verifying read-copy-update in a logic for weak memory. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, pp. 110\u2013120. ACM, New York (2015). \n                      https:\/\/doi.org\/10.1145\/2737924.2737992\n                      \n                    . \n                      http:\/\/doi.acm.org\/10.1145\/2737924.2737992","DOI":"10.1145\/2737924.2737992"},{"key":"4_CR33","unstructured":"Triplett, J., McKenney, P.E., Walpole, J.: Resizable, scalable, concurrent hash tables via relativistic programming. In: Proceedings of the 2011 USENIX Conference on USENIX Annual Technical Conference, USENIXATC 2011, p. 11. USENIX Association, Berkeley (2011). \n                      http:\/\/dl.acm.org\/citation.cfm?id=2002181.2002192"},{"key":"4_CR34","doi-asserted-by":"publisher","unstructured":"Turon, A., Vafeiadis, V., Dreyer, D.: Gps: Navigating weak memory with ghosts, protocols, and separation. In: Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2014, pp. 691\u2013707. ACM, New York (2014). \n                      https:\/\/doi.org\/10.1145\/2660193.2660243\n                      \n                    . \n                      http:\/\/doi.acm.org\/10.1145\/2660193.2660243","DOI":"10.1145\/2660193.2660243"},{"key":"4_CR35","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.: A marriage of rely\/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256\u2013271. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-74407-8_18"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17184-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T09:21:19Z","timestamp":1558344079000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-17184-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030171834","9783030171841"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17184-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"6 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","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":"8 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/esop","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"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"86","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"33% - 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"}},{"value":"3,2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}}]}}