{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T23:08:37Z","timestamp":1740179317734,"version":"3.37.3"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","funder":[{"name":"Swiss National Science Foundation","award":["197065"]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"Many separation logics support fractional permissions to distinguish between read and write access to a heap location, for instance, to allow concurrent reads while enforcing exclusive writes. Fractional permissions extend to composite assertions such as (co)inductive predicates and magic wands by allowing those to be multiplied by a fraction. Typical separation logic proofs require that this multiplication has three key properties: it needs to distribute over assertions, it should permit fractions to be factored out from assertions, and two fractions of the same assertion should be combinable into one larger fraction.<\/jats:p>\n Existing formal semantics incorporating fractional assertions into a separation logic define multiplication semantically (via models), resulting in a semantics in which distributivity and combinability do not hold for key resource assertions such as magic wands, and fractions cannot be factored out from a separating conjunction. By contrast, existing automatic separation logic verifiers define multiplication syntactically, resulting in a different semantics for which it is unknown whether distributivity and combinability hold for all assertions.<\/jats:p>\n In this paper, we present a novel semantics for separation logic assertions that allows states to hold more than a full permission to a heap location during the evaluation of an assertion. By reimposing upper bounds on the permissions held per location at statement boundaries, we retain key properties of separation logic, in particular, the frame rule. Our assertion semantics unifies semantic and syntactic multiplication and thereby reconciles the discrepancy between separation logic theory and tools and enjoys distributivity, factorisability, and combinability. We have formalised our semantics and proved its properties in Isabelle\/HOL.<\/jats:p>","DOI":"10.1145\/3563326","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"1066-1092","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Fractional resources in unbounded separation logic"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2719-4856","authenticated-orcid":false,"given":"Thibault","family":"Dardinier","sequence":"first","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7001-2566","authenticated-orcid":false,"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5554-9381","authenticated-orcid":false,"given":"Alexander J.","family":"Summers","sequence":"additional","affiliation":[{"name":"University of British Columbia, Canada"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"volume-title":"Concurrent Separation Logic for Pipelined Parallelization","author":"Bell Christian J.","key":"e_1_2_1_4_1","unstructured":"Christian J. Bell , Andrew W. Appel , and David Walker . 2010. Concurrent Separation Logic for Pipelined Parallelization . In Static Analysis, Radhia Cousot and Matthieu Martel (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 151\u2013166. isbn:978-3-642-15769-1 Christian J. Bell, Andrew W. Appel, and David Walker. 2010. Concurrent Separation Logic for Pipelined Parallelization. In Static Analysis, Radhia Cousot and Matthieu Martel (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 151\u2013166. isbn:978-3-642-15769-1"},{"key":"e_1_2_1_5_1","first-page":"06410","volume-title":"The VerCors Tool for Verification of Concurrent Programs. In FM 2014: Formal Methods, Cliff Jones, Pekka Pihlajasaari, and Jun Sun (Eds.). Springer International Publishing, Cham. 127\u2013131","author":"Blom Stefan","year":"2014","unstructured":"Stefan Blom and Marieke Huisman . 2014 . The VerCors Tool for Verification of Concurrent Programs. In FM 2014: Formal Methods, Cliff Jones, Pekka Pihlajasaari, and Jun Sun (Eds.). Springer International Publishing, Cham. 127\u2013131 . isbn:978-3-319- 06410 - 06419 Stefan Blom and Marieke Huisman. 2014. The VerCors Tool for Verification of Concurrent Programs. In FM 2014: Formal Methods, Cliff Jones, Pekka Pihlajasaari, and Jun Sun (Eds.). Springer International Publishing, Cham. 127\u2013131. isbn:978-3-319-06410-9"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0372-3"},{"key":"e_1_2_1_7_1","volume-title":"Parkinson","author":"Bornat Richard","year":"2005","unstructured":"Richard Bornat , Cristiano Calcagno , Peter W. O\u2019Hearn , and Matthew J . Parkinson . 2005 . Permission accounting in separation logic. In Principle of Programming Languages (POPL), Jens Palsberg and Mart\u00edn Abadi (Eds.). ACM , 259\u2013270. Richard Bornat, Cristiano Calcagno, Peter W. O\u2019Hearn, and Matthew J. Parkinson. 2005. Permission accounting in separation logic. In Principle of Programming Languages (POPL), Jens Palsberg and Mart\u00edn Abadi (Eds.). ACM, 259\u2013270."},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"John Boyland. 2003. Checking Interference with Fractional Permissions. In Static Analysis (SAS) Radhia Cousot (Ed.). 55\u201372. \t\t\t\t John Boyland. 2003. Checking Interference with Fractional Permissions. In Static Analysis (SAS) Radhia Cousot (Ed.). 55\u201372.","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1749608.1749611"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"James Brotherston Diana Costa Aquinas Hobor and John Wickerson. 2020. Reasoning over Permissions Regions in Concurrent Separation Logic. In Computer Aided Verification (CAV) Shuvendu K. Lahiri and Chao Wang (Eds.). \t\t\t\t James Brotherston Diana Costa Aquinas Hobor and John Wickerson. 2020. Reasoning over Permissions Regions in Concurrent Separation Logic. In Computer Aided Verification (CAV) Shuvendu K. Lahiri and Chao Wang (Eds.).","DOI":"10.1007\/978-3-030-53291-8_13"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Cristiano Calcagno Peter W. O\u2019Hearn and Hongseok Yang. 2007. Local action and abstract separation logic. In Logic in Computer Science (LICS). 366\u2013375. \t\t\t\t Cristiano Calcagno Peter W. O\u2019Hearn and Hongseok Yang. 2007. Local action and abstract separation logic. In Logic in Computer Science (LICS). 366\u2013375.","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_2_1_12_1","volume-title":"Appel","author":"Cao Qinxiang","year":"2019","unstructured":"Qinxiang Cao , Shengyi Wang , Aquinas Hobor , and Andrew W . Appel . 2019 . Proof Pearl : Magic Wand as Frame . arxiv:cs.PL\/1909.08789. Qinxiang Cao, Shengyi Wang, Aquinas Hobor, and Andrew W. Appel. 2019. Proof Pearl: Magic Wand as Frame. arxiv:cs.PL\/1909.08789."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328469"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1979.82.43"},{"key":"e_1_2_1_15_1","unstructured":"Thibault Dardinier. 2022. Unbounded Separation Logic. Archive of Formal Proofs September issn:2150-914x https:\/\/isa-afp.org\/entries\/Separation_Logic_Unbounded.html \t\t\t\t Thibault Dardinier. 2022. Unbounded Separation Logic. Archive of Formal Proofs September issn:2150-914x https:\/\/isa-afp.org\/entries\/Separation_Logic_Unbounded.html"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7072457"},{"key":"e_1_2_1_17_1","volume-title":"Summers","author":"Dardinier Thibault","year":"2022","unstructured":"Thibault Dardinier , Gaurav Parthasarathy , No\u00e9 Weeks , Peter M\u00fcller , and Alexander J . Summers . 2022 . Sound Automation of Magic Wands. In Computer Aided Verification, Sharon Shoham and Yakir Vizel (Eds.). Springer International Publishing , Cham. 130\u2013151. isbn:978-3-031-13188-2 Thibault Dardinier, Gaurav Parthasarathy, No\u00e9 Weeks, Peter M\u00fcller, and Alexander J. Summers. 2022. Sound Automation of Magic Wands. In Computer Aided Verification, Sharon Shoham and Yakir Vizel (Eds.). Springer International Publishing, Cham. 130\u2013151. isbn:978-3-031-13188-2"},{"key":"e_1_2_1_18_1","volume-title":"Appel","author":"Dockins Robert","year":"2009","unstructured":"Robert Dockins , Aquinas Hobor , and Andrew W . Appel . 2009 . A Fresh Look at Separation Algebras and Share Accounting. In Programming Languages and Systems, Zhenjiang Hu (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg. 161\u2013177. isbn:978-3-642-10672-9 Robert Dockins, Aquinas Hobor, and Andrew W. Appel. 2009. A Fresh Look at Separation Algebras and Share Accounting. In Programming Languages and Systems, Zhenjiang Hu (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 161\u2013177. isbn:978-3-642-10672-9"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2009.8.4.a3"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(2:2)2012"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926417"},{"volume-title":"Sound, Predictable, Fast Verifier for C and Java. In NASA Formal Methods (NFM), Mihaela Gheorghiu Bobaru, Klaus Havelund, Gerard J","author":"Jacobs Bart","key":"e_1_2_1_22_1","unstructured":"Bart Jacobs , Jan Smans , Pieter Philippaerts , Fr\u00e9d\u00e9ric Vogels , Willem Penninckx , and Frank Piessens . 2011. VeriFast : A Powerful , Sound, Predictable, Fast Verifier for C and Java. In NASA Formal Methods (NFM), Mihaela Gheorghiu Bobaru, Klaus Havelund, Gerard J . Holzmann, and Rajeev Joshi (Eds.) (Lecture Notes in Computer Science, Vol . 6617). Springer , 41\u201355. Bart Jacobs, Jan Smans, Pieter Philippaerts, Fr\u00e9d\u00e9ric Vogels, Willem Penninckx, and Frank Piessens. 2011. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In NASA Formal Methods (NFM), Mihaela Gheorghiu Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi (Eds.) (Lecture Notes in Computer Science, Vol. 6617). Springer, 41\u201355."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1924520.1924524"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181195.1181213"},{"key":"e_1_2_1_26_1","volume-title":"Logical Reasoning for Disjoint Permissions. In European Symposium on Programming (ESOP), Amal Ahmed (Ed.).","author":"Le Xuan-Bach","year":"2018","unstructured":"Xuan-Bach Le and Aquinas Hobor . 2018 . Logical Reasoning for Disjoint Permissions. In European Symposium on Programming (ESOP), Amal Ahmed (Ed.). Xuan-Bach Le and Aquinas Hobor. 2018. Logical Reasoning for Disjoint Permissions. In European Symposium on Programming (ESOP), Amal Ahmed (Ed.)."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03829-7_7"},{"key":"e_1_2_1_28_1","volume-title":"Deadlock-free Channels and Locks. In European Symposium on Programming (ESOP), A. D. Gordon (Ed.) (Lecture Notes in Computer Science","volume":"426","author":"Leino K. Rustan M.","year":"2010","unstructured":"K. Rustan M. Leino , Peter M\u00fcller , and Jan Smans . 2010 . Deadlock-free Channels and Locks. In European Symposium on Programming (ESOP), A. D. Gordon (Ed.) (Lecture Notes in Computer Science , Vol. 6012). Springer, 407\u2013 426 . http:\/\/www.springerlink.com K. Rustan M. Leino, Peter M\u00fcller, and Jan Smans. 2010. Deadlock-free Channels and Locks. In European Symposium on Programming (ESOP), A. D. Gordon (Ed.) (Lecture Notes in Computer Science, Vol. 6012). Springer, 407\u2013426. http:\/\/www.springerlink.com"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929553.1929559"},{"key":"e_1_2_1_30_1","volume-title":"Summers","author":"M\u00fcller Peter","year":"2016","unstructured":"Peter M\u00fcller , Malte Schwerhoff , and Alexander J . Summers . 2016 . Viper : A Verification Infrastructure for Permission-Based Reasoning. In Verification, Model Checking, and Abstract Interpretation (VMCAI), B. Jobstmann and K. R. M. Leino (Eds.) (Lecture Notes in Computer Science , Vol. 9583). Springer, 41\u2013 62 . Peter M\u00fcller, Malte Schwerhoff, and Alexander J. Summers. 2016. Viper: A Verification Infrastructure for Permission-Based Reasoning. In Verification, Model Checking, and Abstract Interpretation (VMCAI), B. Jobstmann and K. R. M. Leino (Eds.) (Lecture Notes in Computer Science, Vol. 9583). Springer, 41\u201362."},{"volume-title":"a proof assistant for higher-order logic. 2283","author":"Nipkow Tobias","key":"e_1_2_1_31_1","unstructured":"Tobias Nipkow , Lawrence C Paulson , and Markus Wenzel . 2002. Isabelle\/HOL : a proof assistant for higher-order logic. 2283 , Springer Science & Business Media . Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. 2002. Isabelle\/HOL: a proof assistant for higher-order logic. 2283, Springer Science & Business Media."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/982962.964024"},{"volume-title":"Principle of Programming Languages (POPL)","author":"Parkinson Matthew","key":"e_1_2_1_34_1","unstructured":"Matthew Parkinson and Gavin Bierman . 2005. Separation logic and abstraction . In Principle of Programming Languages (POPL) , J. Palsberg and M. Abadi (Eds.). ACM , 247\u2013258. Matthew Parkinson and Gavin Bierman. 2005. Separation logic and abstraction. In Principle of Programming Languages (POPL), J. Palsberg and M. Abadi (Eds.). ACM, 247\u2013258."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_7"},{"key":"e_1_2_1_36_1","volume-title":"Separation Logic: A Logic for Shared Mutable Data Structures. In Logic in Computer Science (LICS)","author":"Reynolds John C.","year":"2002","unstructured":"John C. Reynolds . 2002 . Separation Logic: A Logic for Shared Mutable Data Structures. In Logic in Computer Science (LICS) . IEEE , 55\u201374. John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In Logic in Computer Science (LICS). IEEE, 55\u201374."},{"key":"e_1_2_1_37_1","volume-title":"European Conference on Object-Oriented Programming (ECOOP), J. T. Boyland (Ed.) (LIPIcs","volume":"638","author":"Schwerhoff Malte","unstructured":"Malte Schwerhoff and Alexander J. Summers . 2015. Lightweight Support for Magic Wands in an Automatic Verifier . In European Conference on Object-Oriented Programming (ECOOP), J. T. Boyland (Ed.) (LIPIcs , Vol. 37). Schloss Dagstuhl, 614\u2013 638 . Malte Schwerhoff and Alexander J. Summers. 2015. Lightweight Support for Magic Wands in an Automatic Verifier. In European Conference on Object-Oriented Programming (ECOOP), J. T. Boyland (Ed.) (LIPIcs, Vol. 37). Schloss Dagstuhl, 614\u2013638."},{"key":"e_1_2_1_38_1","volume-title":"Summers and Peter M\u00fcller","author":"Alexander","year":"2018","unstructured":"Alexander J. Summers and Peter M\u00fcller . 2018 . Automating Deductive Verification for Weak-Memory Programs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (Lecture Notes in Computer Science). Springer , 190\u2013209. Alexander J. Summers and Peter M\u00fcller. 2018. Automating Deductive Verification for Weak-Memory Programs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (Lecture Notes in Computer Science). Springer, 190\u2013209."},{"volume-title":"Impredicative Concurrent Abstract Predicates","author":"Svendsen Kasper","key":"e_1_2_1_39_1","unstructured":"Kasper Svendsen and Lars Birkedal . 2014. Impredicative Concurrent Abstract Predicates . In Programming Languages and Systems, Zhong Shao (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 149\u2013168. isbn:978-3-642-54833-8 Kasper Svendsen and Lars Birkedal. 2014. Impredicative Concurrent Abstract Predicates. In Programming Languages and Systems, Zhong Shao (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 149\u2013168. isbn:978-3-642-54833-8"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_1_41_1","volume-title":"Tools and Experiments - Theory Workshop (VS-Theory).","author":"Tuerk Thomas","year":"2010","unstructured":"Thomas Tuerk . 2010 . Local reasoning about while-loops. In Verified Software: Theories , Tools and Experiments - Theory Workshop (VS-Theory). Thomas Tuerk. 2010. Local reasoning about while-loops. In Verified Software: Theories, Tools and Experiments - Theory Workshop (VS-Theory)."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.029"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_15"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563326","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,2]],"date-time":"2023-01-02T11:00:33Z","timestamp":1672657233000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563326"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":42,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563326"],"URL":"https:\/\/doi.org\/10.1145\/3563326","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}