Transformations of CCP programs
Sandro Etalle, Maurizio Gabbrielli, Maria Chiara Meo

TL;DR
This paper presents a transformation system for concurrent constraint programming that optimizes programs while preserving semantics, deadlock behavior, and enabling deadlock-freeness proofs, leading to more efficient and reliable concurrent software.
Contribution
The paper introduces a novel transformation system for CCP that guarantees semantic preservation and deadlock analysis, allowing for program optimization and correctness proofs.
Findings
Transformations preserve input/output semantics.
Optimization includes eliminating communication channels and synchronization.
System aids in proving deadlock freeness.
Abstract
We introduce a transformation system for concurrent constraint programming (CCP). We define suitable applicability conditions for the transformations which guarantee that the input/output CCP semantics is preserved also when distinguishing deadlocked computations from successful ones and when considering intermediate results of (possibly) non-terminating computations. The system allows us to optimize CCP programs while preserving their intended meaning: In addition to the usual benefits that one has for sequential declarative languages, the transformation of concurrent programs can also lead to the elimination of communication channels and of synchronization points, to the transformation of non-deterministic computations into deterministic ones, and to the crucial saving of computational space. Furthermore, since the transformation system preserves the deadlock behavior of programs,…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge
