A concurrent constraint programming interpretation of access permissions

DOI10.1017/S1471068418000017zbMATH Open1478.68056arXiv1802.04695OpenAlexW2963666856WikidataQ130039380 ScholiaQ130039380MaRDI QIDQ4644356FDOQ4644356

Authors: Carlos Olarte, Elaine Pimentel, Camilo Rueda 

Publication date: 31 May 2018

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

Abstract: A recent trend in object oriented (OO) 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 (lcc). 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 lcc 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 lcc 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 lcc model, observing the flow of APs and quickly finding inconsistencies of the APs vis-a-vis the implementation. The latter is an automatic theorem prover based on ILL. This paper is under consideration for publication in Theory and Practice of Logic Programming (TPLP).

Full work available at URL: https://arxiv.org/abs/1802.04695

Recommendations

• Automatic inference of access permissions
• Linear concurrent constraint programming: Operational and phase semantics
• Dynamic Access Control in a Concurrent Object Calculus
• Concurrent object-oriented programs: from specification to code.
• A type checking algorithm for concurrent object protocols

zbMATH Keywords

linear logicconcurrent constraint programmingfocusingaccess permissions

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Cites Work

• Decision problems for propositional linear logic
• Truly concurrent constraint programming
• Title not available (Why is that?)
• Linear logic
• Linear concurrent constraint programming: Operational and phase semantics
• Models and emerging trends of concurrent constraint programming
• On the complexity of linear authorization logics
• Observational equivalences for linear logic concurrent constraint languages
• Title not available (Why is that?)
• Logic Programming with Focusing Proofs in Linear Logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• A type system for borrowing permissions
• On concurrent behaviors and focusing in linear logic

Cited In (9)

• Access control in a core calculus of dependency
• Structural lock correlation with ownership types
• A focused linear logical framework and its application to metatheory of object logics
• Hybrid linear logic, revisited
• Access permission contracts for scripting languages
• Alcove
• Permission to speak: a logic for access control and conformance
• Dynamic Access Control in a Concurrent Object Calculus
• Automatic inference of access permissions

Uses Software

• Rodin
• Mezzo
• Featherweight Java

This page was built for publication: A concurrent constraint programming interpretation of access permissions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4644356)