{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T06:48:09Z","timestamp":1693637289710},"reference-count":32,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2018,4,10]],"date-time":"2018-04-10T00:00:00Z","timestamp":1523318400000},"content-version":"unspecified","delay-in-days":40,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2018,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A recent trend in object-oriented programming languages is the use of access permissions (APs) as an abstraction for controlling concurrent executions of programs. The use of AP source code annotations defines a protocol specifying how object references can access the mutable state of objects. Although the use of APs simplifies the task of writing concurrent code, an unsystematic use of them can lead to subtle problems. This paper presents a declarative interpretation of APs as linear concurrent constraint programs (<jats:monospace>lcc<\/jats:monospace>). We represent APs as constraints (i.e., formulas in logic) in an underlying constraint system whose entailment relation models the transformation rules of APs. Moreover, we use processes in<jats:monospace>lcc<\/jats:monospace>to model the dependencies imposed by APs, thus allowing the faithful representation of their flow in the program. We verify relevant properties about AP programs by taking advantage of the interpretation of<jats:monospace>lcc<\/jats:monospace>processes as formulas in Girard's intuitionistic linear logic (ILL). Properties include deadlock detection, program correctness (whether programs adhere to their AP specifications or not), and the ability of methods to run concurrently. By relying on a focusing discipline for ILL, we provide a complexity measure for proofs of the above-mentioned properties. The effectiveness of our verification techniques is demonstrated by implementing the Alcove tool that includes an animator and a verifier. The former executes the<jats:monospace>lcc<\/jats:monospace>model, observing the flow of APs, and quickly finding inconsistencies of the APs vis-\u00e0-vis the implementation. The latter is an automatic theorem prover based on ILL.<\/jats:p>","DOI":"10.1017\/s1471068418000017","type":"journal-article","created":{"date-parts":[[2018,4,10]],"date-time":"2018-04-10T10:28:50Z","timestamp":1523356130000},"page":"252-295","source":"Crossref","is-referenced-by-count":1,"title":["A concurrent constraint programming interpretation of access permissions"],"prefix":"10.1017","volume":"18","author":[{"given":"CARLOS","family":"OLARTE","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ELAINE","family":"PIMENTEL","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"CAMILO","family":"RUEDA","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2018,4,10]]},"reference":[{"key":"S1471068418000017_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/265943.265954"},{"key":"S1471068418000017_ref29","first-page":"933","volume-title":"OOPSLA Companion","author":"Stork","year":"2009"},{"key":"S1471068418000017_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/2543920"},{"key":"S1471068418000017_ref10","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000123"},{"key":"S1471068418000017_ref22","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1016\/j.tcs.2016.08.026","article-title":"On concurrent behaviors and focusing in linear logic","volume":"685","author":"Olarte","year":"2017","journal-title":"Theoretical Computer Science"},{"key":"S1471068418000017_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-013-9145-3"},{"key":"S1471068418000017_ref25","first-page":"173","article-title":"Programming with permissions in mezzo","volume":"48","author":"Pottier","year":"2013","journal-title":"Special Interest Group on Programming Languages Notices"},{"key":"S1471068418000017_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503505"},{"key":"S1471068418000017_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(92)90075-B"},{"key":"S1471068418000017_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0145-y"},{"key":"S1471068418000017_ref2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"S1471068418000017_ref3","doi-asserted-by":"crossref","unstructured":"Beckman N. E. , Bierhoff K. and Aldrich J. 2008. Verifying correct usage of atomic blocks and typestate. In OOPSLA, G. E. Harris , Ed. ACM, 227\u2013244.","DOI":"10.1145\/1449764.1449783"},{"key":"S1471068418000017_ref4","doi-asserted-by":"crossref","unstructured":"Bierhoff K. and Aldrich J. 2007. Modular typestate checking of aliased objects. In OOPSLA, R. P. Gabriel , D. F. Bacon , C. V. Lopes and G. L. S. Jr., Eds. ACM, 301\u2013320.","DOI":"10.1145\/1297027.1297050"},{"key":"S1471068418000017_ref5","doi-asserted-by":"crossref","unstructured":"Boyland J. 2003. Checking interference with fractional permissions. In SAS, R. Cousot , Ed. Lecture Notes in Computer Science, vol. 2694. Springer, 55\u201372.","DOI":"10.1007\/3-540-44898-5_4"},{"key":"S1471068418000017_ref8","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.3002"},{"key":"S1471068418000017_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S1471068418000017_ref17","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139021326"},{"key":"S1471068418000017_ref12","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1145\/1069774.1069790","volume-title":"PPDP","author":"Jagadeesan","year":"2005"},{"key":"S1471068418000017_ref13","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1145\/286936.286953","volume-title":"OOPSLA","author":"Leino","year":"1998"},{"key":"S1471068418000017_ref14","first-page":"2","volume-title":"VMCAI","author":"Leino","year":"2010"},{"key":"S1471068418000017_ref16","first-page":"57","volume-title":"PPDP","author":"Martinez","year":"2010"},{"key":"S1471068418000017_ref18","first-page":"810","volume-title":"Logic Programming, Proc. of the 5th International Conference and Symposium","author":"Nadathur","year":"1988"},{"key":"S1471068418000017_ref20","first-page":"145","article-title":"Temporal concurrent constraint programming: Denotation, logic and applications","volume":"9","author":"Nielsen","year":"2002","journal-title":"Nordic Journal of Computing"},{"key":"S1471068418000017_ref21","doi-asserted-by":"crossref","unstructured":"Nigam V. 2012. On the complexity of linear authorization logics. In LICS. IEEE, 511\u2013520.","DOI":"10.1109\/LICS.2012.61"},{"key":"S1471068418000017_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/2370776.2370802"},{"key":"S1471068418000017_ref26","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2086.001.0001","volume-title":"Concurrent Constraint Programming","author":"Saraswat","year":"1993"},{"key":"S1471068418000017_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96733"},{"key":"S1471068418000017_ref28","first-page":"333","volume-title":"POPL","author":"Saraswat","year":"1991"},{"key":"S1471068418000017_ref31","first-page":"713","volume-title":"OOPSLA","author":"Sunshine","year":"2011"},{"key":"S1471068418000017_ref32","unstructured":"Ullrich S. A. 2016. Simple Verification of Rust Programs via Functional Purification. Master's Thesis, Karlsruher Institut f\u00fcr Technologie (KIT)."},{"key":"S1471068418000017_ref19","doi-asserted-by":"crossref","first-page":"557","DOI":"10.1145\/2103656.2103722","volume-title":"POPL","author":"Naden","year":"2012"},{"key":"S1471068418000017_ref6","first-page":"2","volume-title":"ECOOP","author":"Boyland","year":"2001"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068418000017","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T00:46:39Z","timestamp":1693615599000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068418000017\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,3]]},"references-count":32,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,3]]}},"alternative-id":["S1471068418000017"],"URL":"https:\/\/doi.org\/10.1017\/s1471068418000017","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,3]]}}}