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.
Type de document :
Article dans une revue
Proceedings of the 14th symposium on Principles and practice of declarative programming, ACM, 2012, pp.207-216. 〈http://dl.acm.org/citation.cfm?doid=2370776.2370802〉. 〈10.1145/2370776.2370802〉
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00748141
Contributeur : Catuscia Palamidessi <>
Soumis le : dimanche 4 novembre 2012 - 23:55:44
Dernière modification le : lundi 13 octobre 2014 - 15:43:25
Document(s) archivé(s) le : samedi 17 décembre 2016 - 07:14:29

Fichier

aeminium-ppdp-pp.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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. 〈http://dl.acm.org/citation.cfm?doid=2370776.2370802〉. 〈10.1145/2370776.2370802〉. 〈hal-00748141〉

Partager

Métriques

Consultations de la notice

94

Téléchargements de fichiers

98