Name
Title | ||
|---|---|---|
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 executions. 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 annotated 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 linear logic. Properties include deadlock detection, program correctness (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. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1145/2370776.2370802 | PPDP |
Keywords | Field | DocType |
ap annotated program,analysis approach,lcc agent,unsystematic use,program correctness,linear concurrent constraint approach,concurrent code,automatic verification,complexity analysis,access permission,concurrent execution,ap specification,use access permissions,linear logic,verification | Logical consequence,Programming language,Object-oriented programming,Computer science,Correctness,Decidability,Theoretical computer science,Concurrent constraint logic programming,Mathematical proof,Linear logic,Deadlock prevention algorithms | Conference |
Citations | PageRank | References |
1 | 0.34 | 15 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Carlos Olarte | 1 | 151 | 19.14 |
| Elaine Pimentel | 2 | 119 | 14.78 |
| Camilo Rueda | 3 | 243 | 41.36 |
| Nestor Cataño | 4 | 57 | 4.77 |