True concurrency semantics for a linear logic programming language with broadcast communication

Abstract

We define a true concurrency semantics for LO, a reactive programming language characterized by dynamically reconfigurable agents (processes), with interagent communication implemented as broadcasting and logical operators corresponding to Linear Logic connectives. Our semantic model is given by the well-known Chemical Abstract Machine formalism, where concurrent events happen in the form of chemical-like reactions. Our approach consists of mapping LO computations into CHAM computations and is easily generalizable to CHAM-related models like CHARMs, rewriting logics etc. We propose two mappings from LO to CHAMs, both making use of the “membrane” mechanism of the CHAM, but differing in the choice of active elements: in one case, the messages are passive and the agents are the active entities which perform read and write operations; by contrast, in the second case, the agents are passive with respect to communication and the messages themselves move around the solution to deliver their content to each agent. The results in the paper show the effectiveness of the CHAM and related formalisms as abstract frameworks for modeling the implementation of practical languages on parallel architectures. Furthermore, they provide insight on the two following issues: (i) the amount of synchronization needed to add broadcasting to one-to-one communication primitives; (ii) the problem of parallel searching for Linear Logic proofs.