Skip to Main content Skip to Navigation
Journal articles

A linear concurrent constraint approach for the automatic verification of access permissions

Abstract : A recent trend in object oriented programming languages is the use Access Permissions (AP) as abstraction to control concurrent exe- cutions. AP define a protocol specifying how different references can access the mutable state of objects. Although AP simplify the task of writing concurrent code, an unsystematic use of permissions in the program can lead to subtle problems. This paper presents a Linear Concurrent Constraint (lcc) approach to verify AP an- notated programs. We model AP as constraints (i.e., formulas in logic) in an underlying constraint system, and we use entailment of constraints to faithfully model the flow of AP in the program. We verify relevant properties about programs by taking advantage of the declarative interpretation of lcc agents as formulas in lin- ear logic. Properties include deadlock detection, program correct- ness (whether programs adhere to their AP specifications or not), and the ability of methods to run concurrently. We show that those properties are decidable and we present a complexity analysis of finding such proofs. We implemented our verification and analysis approach as the Alcove tool, which is available on-line.
Document type :
Journal articles
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/hal-00748141
Contributor : Catuscia Palamidessi <>
Submitted on : Sunday, November 4, 2012 - 11:55:44 PM
Last modification on : Monday, October 13, 2014 - 3:43:25 PM
Long-term archiving on: : Saturday, December 17, 2016 - 7:14:29 AM

File

aeminium-ppdp-pp.pdf
Files produced by the author(s)

Identifiers

Citation

Carlos Olarte, Camilo Rueda, Elaine Pimentel, Nestor Cataño. A linear concurrent constraint approach for the automatic verification of access permissions. Proceedings of the 14th symposium on Principles and practice of declarative programming, ACM, 2012, pp.207-216. ⟨10.1145/2370776.2370802⟩. ⟨hal-00748141⟩

Share

Metrics

Record views

160

Files downloads

250