Dynamic Slicing for Concurrent Constraint Languages

Concurrent Constraint Programming (CCP) is a declarative model for concurrency where agents interact by telling and asking constraints (pieces of information) in a shared store. Some previous works have developed (approximated) declarative debuggers for CCP languages. However, the task of debugging concurrent programs remains difficult. In this paper we define a dynamic slicer for CCP (and other language variants) and we show it to be a useful companion tool for the existing debugging techniques. We start with a partial computation (a trace) that shows the presence of bugs. Often, the quantity of information in such a trace is overwhelming, and the user gets easily lost, since she cannot focus on the sources of the bugs. Our slicer allows for marking part of the state of the computation and assists the user to eliminate most of the redundant information in order to highlight the errors. We show that this technique can be tailored to several variants of CCP, such as the timed language ntcc, linear CCP (an extension of CCPbased on linear logic where constraints can be consumed) and some extensions of CCP dealing with epistemic and spatial information. We also develop a prototypical implementation freely available for making experiments.

How to Implement Lightweight Threads

Using continuations in high order languages such as Common Lisp is notvery efficient because they do not work close to the compiler . Other optionssuch as making an scheduler in C can be efficient when the sources of theinterpreter are available and they can be modified, otherwise, making aninterface with C using FFI causes an overhead, making it impossible toachive “lighweight”.To make an efficient implementation of lighweight threads in CommonLisp it is required to analyze the type of applications which will use thethreads. For example, for a Concurrent Constraint Programming (CCP)interpreter using Gecode, event driven programming seams very natural,but for the Omax system, it is not be appropriate.

ntccMC: A bounded-time model checker for ntcc

A disadvantage of concurrent constraint programming (ccp) calculi isthat it is difficult to exploit its declarative point of view because of the lackof automated verification tools available. This limits the applicability of theverification techniques to small problems. As an example, a model checkerfor a non-deterministic timed concurrent constaint (ntcc) will be useful notonly for music systems, but for many other fields on which ccp has beenproven successful (e.g., system biology and security systems). We claimfor the urgent need of a model checker for ntcc. First, because ntcc hasbeen widely used to model reactive system and verify properties about them,but the verification had to be done by hand. Second, because there are notmany frameworks to formally model and verify music interaction systemsand ntcc has been proved to be successful in that field. In this paper wepropose a model checker for ntcc.

Perspectives on Constraints, Process Algebras, and Hybrid Systems

Building on a technique for associating Hybrid Systems (HS) to stochastic programs written in a stochastic extension of Concurrent Constraint Programming (sCCP), we will discuss several aspects of performing such association. In particular, as we proved an sCCP program can be mapped in a HS varying in a lattice at a level depending on the amount of actions to be simulated continuously, we will discuss what are the problems involved in a semi-automatic choice of such level. Decidability, semantic, and efficiency issues will be taken into account, with special emphasis on their links with biological applications. We will also discuss about the role of constraints and of the constraint store is this construction.