Modular Analysis of Suspension Free cc Programs^{∗}

Enea Zaffanella Dipartimento di Informatica Università di Pisa Corso Italia 40, 56125 Pisa

                  zaffanel@di.unipi.it

Abstract

Compositional semantics allow to reason about programs in an incremental way, thus providing the formal base for the development of modular data-flow analyses. The major drawback of these semantics is their complexity, which increases as the interactions between different program modules become more sophisticated. As a consequence, the benefits of a compositional approach can be easily overcome by the incurred computational overhead. This observation applies in particular to concurrent constraint (cc) program modules, which can interact in very complicated ways by means of their synchronization primitive (the ask guard). In this work we provide a modular abstract interpretation framework for cc programs that partially solves this problem. By assuming the whole program suspension free, we show that it is possible to compositionally compute an approximation of its run-time behavior while keeping complexity under control. To this end we translate the cc program into a clp program and analyze the latter. Correctness results are easily stated in an implicative form. The approach is truly incremental and it does not depend on the chosen program decomposition; in particular no hypotheses are needed on the suspension freeness of each single module.

1 Introduction

Modular development is essential for the successful construction of large programs. Modularity imposes several requirements on the tools and techniques used for program development. In particular, it requires tools which behaves nicely with respect to the (explicit or implicit) program composition operators of the language. The notion of compositional semantics emerges from the need of providing a semantic support to modularity, since these semantics allow to express the meaning of a program in terms of the meaning of its constituent parts. In this paper we consider the problem of providing a compositional abstract interpretation framework for the analysis of concurrent constraint (cc) programs, the concurrent extension of constraint logic programs (clp) defined by Saraswat et al. [15, 14]. In particular, here we are interested in the compositionality with respect to the union of cc programs. Consider a cc program P which is split into modules M_{1}, …, M_{n}, each module M_{i} having being analyzed separately so to obtain the information S_{i} on its run-time behavior. In a truly compositional analysis framework, the information on the run-time behavior of the program P can be obtained by suitably composing S_{1}, …, S_{n}. This has the big advantage that, should M_{k} be changed into M′_{k} for some reason, the information on the new overall program P′ can be obtained by (1) analyzing only the changed module M′_{k} obtaining S′_{k}, and (2) combining S′_{k} with the old S_{1}, … S_{k−1}, S_{k+1}, … S_{n}, thus avoiding to re-analyze the unchanged modules. This is possible, of course, only if our analyzer is based on a compositional abstract interpretation, i.e. both the concrete and the abstract semantics are compositional. However, we have no a priori guarantee on the effectiveness of the approach. It might well be the case that our potential advantages (e.g., savings on the analysis time) are destroyed by the overhead imposed by the need of a compositional semantics. In our opinion, indeed, such an approach is very likely to be uneffective in the cc case, as a compositional semantics for these languages seems to be too complex for a practical use. This is because cc agents can interact in a subtle and complicated way by means of their synchronization mechanism and therefore easily introduce very strong dependencies between different modules.

∗This work has been supported by the “PARFORCE” (Parallel Formal Computing Environment) BRA-Esprit II Project n. 6707.

Things are much better if we restrict ourselves to cc programs which are suspension free, meaning that their terminating computations do not contain suspended processes. This reactive property of cc programs is important for several reasons. First of all suspended computations usually correspond to undesired behaviors of the program; their presence is very likely to denote a programming error and, indeed, a lot of research work has been directed to the development of tools for proving a program suspension free [3, 4, 7]. Moreover, suspension freeness does not behave well with respect to compositionality, as it can be shown that by combining suspension free program modules we can produce suspended computations. These considerations suggest a two steps approach to the abstract interpretation of cc programs. In the first step the program is proved suspension free. The second step assumes suspension freeness and uses this information to perform the static analysis in a more efficient and precise way. In this paper we show how to perform the second step of the outlined approach in a modular and effective way, i.e. avoiding the complexity problems stated before. For the purposes of program analysis, as shown in [17], a suspension free cc program P can be safely translated into a clp program P′ by removing all synchronizations (i.e. ask guards). The abstract interpretation of P′, computed within any framework for clp, yields a correct approximation of the semantics of the original program P. Following [9], we will introduce a semantics for the translated programs which is compositional wrt the union of programs. This semantics is then approximated by applying the theory of abstract interpretation. The correctness result do not depend on the program decomposition we have chosen; in particular, it holds even if all the modules are not suspension free. Another important point to stress is that the two steps do not need to be chronologically ordered; the compositional abstract interpretation can be performed even before proving suspension freeness, thus allowing a truly incremental approach to analysis.

2 Constraint Systems and cc Languages

Constraint systems are semantic domains formalizing the gathering and the management of partial information.

Definition 2.1 (partial information system) [16] A partial information system is a quadruple ⟨ D, Δ, Con, ⊢ ⟩ where D is a denumerable set of elementary assertions (tokens), Δ ∈ D is a distinguished assertion (the least informative token), Con is a family of finite subsets of D (the consistent subsets of tokens) and ⊢⊆ Con × Con is the entailment relation satisfying (for u, v, w ∈ Con) ∅ ⊢ {Δ}, u ⊢ v if v ⊆ u and u ⊢ w if (u ⊢ v ∧ v ⊢ w).

Entailment closed sets of tokens are called constraints and provide representatives for the equivalence classes induced by the entailment relation; in particular, true denotes the set of all the trivial tokens. Note that, in a partial information system, all constraints are consistent. In order to model inconsistent information, we add a special token ∇ to D and say that, for all P ∈ D, the entailment {∇} ⊢ {P } holds; we also take Con = {u ⊆ D | card(u) < ω }. Therefore, the entailment closure of {∇} is the whole set D, which is denoted false. The simple constraint system generated by a partial information system is the complete lattice ⟨ C, ⊣, true, false, ⊔, ⊓ ⟩ of all the constraints together with the partial order induced by the reverse of the entailment relation (which we will denote ⊣). We write ⊔ to denote the constraint composition operator (the lub of the constraint system). Cylindric constraint systems [14] (constraint systems for short) are simple constraint systems in which the notion of variable is explicitly taken into account. The constraint algebra is enriched by diagonal elements d_{xy} and cylindric operators ∃_{x} [13].

Definition 2.2 (constraint system) A (cylindric) constraint system C = ⟨ C, ⊣, true, false, ⊔, ⊓, ∃_{x}, d_{xy} ⟩_{x,y∈V} is an algebraic structure where ⟨ C, ⊣, true, false, ⊔, ⊓ ⟩ is a simple constraint system; V is a denumerable set of variables; ∀x, y ∈ V, ∀c, c′ ∈ C we have ∃_{x} false = false, ∃_{x}c ⊣ c, c ⊣ c′ implies ∃_{x}c ⊣ ∃_{x}c′, ∃_{x}(c ⊔ ∃_{x}c′) = ∃_{x}c ⊔ ∃_{x}c′, ∃_{x}(∃_{y}c) = ∃_{y}(∃_{x}c); ∀x, y, z ∈ V, ∀c ∈ C we have d_{xx} = true, z ≢ x, y implies d_{xy} = ∃_{z}(d_{xz} ⊔ d_{zy}), x ≢ y implies c ⊣ d_{xy} ⊔ ∃_{x}(c ⊔ d_{xy}).

We refer to [16] and [14] for a more detailed presentation. In the following, we write x̂ to denote a sequence of distinct variables; we often write x̂ to denote the set of variables occurring in the sequence x̂. Given x̂ = (x_{1}, …, x_{n}) we write ∃x̂c to denote the constraint ∃_{x_{1}}(… ∃_{x_{n}}(c)); given ŷ = (y_{1}, …, y_{n}), we write d_{x̂ŷ} to denote the constraint d_{x_{1}y_{1}} ⊔ … ⊔ d_{x_{n}y_{n}}. When it is not specified in the context, we always assume that the arities of such tuples are matching. The projection operator \overline{∃}x̂ is defined as \overline{∃}x̂c = ∃_{V \x̂} c, i.e. it hides the information of all the variables but x̂. The set of variables that occurs free in a constraint c is vars(c) = {x ∈ V | ∃_{x}c ≠ c}.

As an example, let us formalize the constraint system of dependency relations, which can be used to propagate interesting properties of program variables (e.g. definiteness).

Example 2.1 [Dependency relations][3] Let V be a finite set of variables and π be a property. The set of tokens is defined as D = (℘(V) × ℘(V)) ∪ {∇}; the interpretation of a token (X, Y) ∈ D is that if all the variables in Y satisfy property π, then all the variables in X satisfy the property too. The entailment ⊧ is defined (accordingly to the intuitive meaning of a set of tokens) as the minimal entailment relation on D such that, for all R ⊆ D and X, Y, W, Z ⊆ V, if X ⊆ Y then ∅ ⊧ {(X, Y)}, if (R ⊧ {(X, Y)} ∧ R ⊧ {(Y, Z)}) then R ⊧ {(X, Z)}, if (R ⊧ {(X, Y)}∧R ⊧ {(W, Z)}) then R ⊧ {(X ∪W, Y ∪Z)}. Given a set of tokens R ⊆ D, let ϱ(R) denote its entailment closure. Moreover we can define ∃_{x}R = ϱ (ϱ(R)\{(X, Y) | x ∈ X ∪ Y }) and d_{xy} = ϱ ({({x}, {y}), ({y}, {x})}). □

In the following we systematically confuse a set of tokens and the constraint generated by this set, that is its entailment closure.

2.1 Modeling nondeterminism

Each element in the domains of [14] models the result of a single computation (using the terminology of [11], each element of such domains is a simple constraint). In order to characterize the nondeterministic choice of (concurrent) constraint languages, sets of computations are considered in all the semantic definitions given in the literature.

In this paper, following [11], we adopt a more general solution by considering an algebraic “solution merging” operator ⊕. Let ρ : ℘(C) → ℘(C) be an upper closure operator on ℘(C); define P_{ρ}(C) = {ρ(S) | S ∈ ℘(C)}.

Definition 2.3 (disjunctive lifting) The disjunctive lifting of the constraint system C = ⟨ C, ⊣, true, false, ⊔, ⊓, ∃_{x}, d_{xy} ⟩_{x,y∈V} wrt ρ is defined as P_{ρ}(C) = ⟨ P_{ρ}(C)), ⊆, 0, 1, ⊕, ∩, ⊗, ∃∃_{x}, δ_{xy} ⟩_{x,y∈V}, where ⟨ P_{ρ}(C), ⊆, 0, 1, ⊕, ∩ ⟩ is a complete lattice; 0 = ρ(∅), 1 = ρ(C) = C and δ_{xy} = ρ( {d_{xy}}); for all S, S′ ∈ P_{ρ}(C) we have S ⊗S′ = ρ( {c ⊔ c′ | c ∈ S, c′ ∈ S′ }), S ⊕S′ = ρ(S ∪S′) and ∃∃_{x}(S) = ρ( {∃_{x}c | c ∈ S }). The lifting function {| · |} : C → P_{ρ}(C) is defined as {|c|} = ρ( {c}).

Note that the (lifted) composition operator ⊗ is associative and commutative, but in general it is not idempotent. By taking ρ = id, we obtain the powerset of the constraint system C, where ⊕ = ∪, and the other operators on P_{id}(C) (namely ⊗, ∃∃_{x} and δ_{xy}) are simply the linear extensions of the corresponding operators on C. This domain can be used to model computed answer constraints and indeed it is at the base of the extension to the clp case of the s-semantics construction defined in [8] for pure logic programs. It is worth to stress that, in the general case, the disjunctive lifting of a constraint system is not itself a constraint system, as the lifted operators do not necessarily satisfy the axioms of Definition 2.2. In the following, when no confusion can arise, we freely omit the subscript ρ; moreover, depending on the context, the symbol c will be used to denote an element ranging both on the set of constraints C and on the set of disjunctive elements P(C).

2.2 The Language

In order to simplify the program translation defined in subsection 3.1, we introduce concurrent constraint languages [15, 14] by giving a syntax based on clauses; each concurrent process is thus defined by a set of clauses. Each clause consists of three parts: a head, a (ask and tell) pair of constraints and a body part, which is a sequence of process calls representing their parallel composition (see Table 1). Given a body B = p_{1}(x̂_{1}), …, p_{n}(x̂_{n}) we define the variables tuple of B as vt(B) = x̂_{1} · . . . · x̂_{n}; then, given a clause cl ≡ p_{0}(x̂_{0}) :– a : c □ B, we define vt(cl) = x̂_{0} · vt(B). We consider only clauses in normal form.

Definition 2.4 (normal form) A cc clause cl ≡ h:– a : c □ B is in normal form iff the variables in vt(cl) are all distinct, vars(a) ⊆ vt(cl) and vars(c) ⊆ vt(cl).

All the variables that do not occur in the head (namely, all the variables in the body B) are considered local variables (this is needed in order to preserve the referential transparency property). Note that we are not restricting the expressive power of the language as any cc clause can be easily mapped to an equivalent clause in normal form.

Program ::= ϵ | Clause Program
Clause  ::= Head :– Ask : Tell □ Body.
Body  ::= ϵ | Call Body
Head, Call ::= p(x̂)
Ask, Tell ::= c

Table 1: The syntax

The operational model is described by a transition system T = (Conf , ⟶^{W}_{P}), where Conf = {⟨ c □ B ⟩ | c ∈ C, B ∈ Body} and the transition relation ⟶^{W}_{P} is defined by the following transition rule:

\frac{cl ≪_{X} P a ⊣ (d_{x̂ŷ} ⊔ σ)}{⟨ σ □ B_{1}, p(x̂), B_{2} ⟩ ⟶^{W}_{P} ⟨ c ⊔ d_{x̂ŷ} ⊔ σ □ B_{1} · B′ · B_{2} ⟩}

where cl ≡ p(ŷ) :– a : c □ B′ and X = W ∪ vars(σ) ∪ vt(B_{1}, p(x̂), B_{2}).

Note that ⟶^{W}_{P} is indexed on the program P and on the set of variables of interest W ⊆ V, which are the variables occurring in the initial configuration. When no confusion can arise we simply write ⟶^{W}, thus omitting the program index P. In a configuration ⟨ σ □ B ⟩ ∈ Conf, the (finite) constraint σ ∈ C is the global store while the body B represents the residual computation. The reduction of a process call p(x̂) implements nondeterministic choice, parameter passing, synchronization and constraint publication all at once. We nondeterministically select a program clause cl ≡ p(ŷ) :– a : c □ B′ which is renamed apart wrt both the current configuration and the set of variables of interest W (notation obj ≪_{X} S means that the object obj is obtained by choosing an element of S and renaming it so that it contains none of the variables in X). Then we check whether the ask constraint a is entailed by the current store σ augmented with the parameter passing constraint d_{x̂ŷ}. If this is the case then the computation commits, i.e. the call p(x̂) is replaced by the clause body B′ and the global store is augmented by the parameter passing information and the tell constraint c. Note that we do not perform any consistency check on the tell constraint. Otherwise, if no such clause exists, the process call cannot be reduced and we say that p(x̂) is stuck in the current configuration. A computation s for a program P and an initial configuration ⟨ σ □ B ⟩ is a possibly infinite sequence of configurations { ⟨ c_{i} □ B_{i} ⟩ }_{i} such that B_{0} = B and c_{0} = σ and for all i < |s|, ⟨ c_{i} □ B_{i} ⟩ ⟶^{W} ⟨ c_{i+1} □ B_{i+1} ⟩. Let / ⟶ denote the absence of admissible transitions. Sequences reaching configurations ⟨ c_{n} □ B_{n} ⟩ such that ⟨ c_{n} □ B_{n} ⟩ / ⟶ are called terminating computations and c_{n} ∈ C is the (finite) computed answer constraint. A terminating computation such that B_{n} = ϵ is a successful computation, otherwise (B_{n} ≠ ϵ) it is a suspended computation.

Definition 2.5 (finite semantics) Let G = ⟨ σ □ B ⟩ and let W = vars(σ) ∪ vt(B). The finite semantics for program P and configuration G is

O[[ P ]](G) = ⨁ \{\{| \overline{∃}_{W} c |\} | G (⟶^{W}_{P})^{∗} ⟨ c □ B′ ⟩ / ⟶_{P} \}

Note that the computed answer constraints are projected onto the set of variables of interest, namely the variables occurring in the initial configuration G. Moreover, the finite semantics considers the results of all the terminating computations, regardless of whether they are successful or suspended. We say that program P and configuration G are suspension free if there is no suspended computation for P starting from G.

3 Compositional Analysis: a Compromise

In many contexts, e.g. for the designing and analysis of complex concurrent programs, adopting a compositional approach is a must. Unfortunately, it is known that the suspension freeness of a program is not compositional, namely we can obtain suspended computations by combining suspension free program chunks.

Example 3.1 Consider the following programs.

P 1 : \{ \begin{matrix}p(x) :– true : x = a □ . \\ r(x) :– true : x = y □ q_{1}(y, z). \\ q_{1}(y, z) :– y = a : true □ . \\ q_{1}(y, z) :– z = a : true □ . \end{matrix}  P 2 : \{ \begin{matrix}p(x) :– true : x = b □ . \\ r(x) :– true : x = y □ q_{2}(y, z). \\ q_{2}(y, z) :– y = b : true □ . \\ q_{2}(y, z) :– z = b : true □ . \end{matrix}

Given the initial configuration G = ⟨ x = y □ p(x), r(y) ⟩, it can be easily observed that P 1 (resp. P 2) and G are suspension free, while for P = P 1 ∪ P 2 and G we have the following suspended computation (where we have renamed variables and projected the store for readability):

\begin{aligned}⟨ x_{1} = x_{2} □ p(x_{1}), r(x_{2}) ⟩ & ⟶^{W}_{P} & ⟨ x_{1} = x_{2} = a □ r(x_{2}) ⟩ \\ & ⟶^{W}_{P} & ⟨ x_{1} = x_{2} = a □ q_{2}(x_{2}, z) ⟩ / ⟶_{P} \end{aligned}

□

The viceversa also holds, i.e. it is possible to obtain a suspension free program by combining two or more program chunks which are not suspension free.

Example 3.2 Consider the following programs.

P 1 : \{ \begin{matrix}p(x, y) :– true : x = a □ . \\ q(x, y) :– y = b : true □ . \end{matrix}  P 2 : \{ \begin{matrix}p(x, y) :– true : y = b □ . \\ q(x, y) :– x = a : true □ . \end{matrix}

Given the initial configuration G = ⟨ x_{1} = x_{2}, y_{1} = y_{2} □ p(x_{1}, y_{1}), q(x_{2}, y_{2}) ⟩, it can be easily observed that both P 1 and P 2 with configuration G are not suspension free (they have no successful computation at all), while for P = P 1 ∪ P 2 and G we can easily prove suspension freeness. □

Hence, even if we are able to prove the suspension freeness of all the program modules, the whole program is not proved to be suspension free. Obviously, a semantics which is compositional wrt the union of cc programs can be defined, but it is very likely that, in order to be correct, this semantics would have to encode the whole computation structure.

NoSynch[ ϵ] = ϵ

NoSynch[ cl progr ] = NoSynch[ cl ] NoSynch[ progr ] NoSynch[ p(x̂) :– a : c □ G.] = p(x̂) :– (a ⊔ c) □ G.

Table 2: The transformation NoSynch

3.1 The two-steps approach

These considerations suggest a two step approach to the modular abstract interpretation of cc programs. In the first step we prove that the complete program is suspension free. The second step assumes the suspension freeness and uses this information to perform the static analysis in a more efficient way. Following [17], we now define a semantics for cc programs that observes successful computations only.

Definition 3.1 (success semantics) Let G = ⟨ σ □ B ⟩ and let W = vars(σ)∪vt(B). The success semantics for program P and configuration G is

SS[[ P ]](G) = ⨁ \{\{| \overline{∃}_{W} c |\} | G (⟶^{W}_{P})^{∗} ⟨ c □ . ⟩\}

Remark 3.1 If P and G are suspension free then O[[ P ]](G) = SS[[ P ]](G).

Hence, if our program is suspension free, we can use the success semantics for the correctness proofs of our abstract interpretation framework. The success semantics for cc programs can be easily approximated by defining a syntactic transformation called NoSynch [17], mapping all the ask constraints of the program into equivalent tell constraints, i.e. removing all the synchronization tests. As pointed out in [17], the transformed program is a sequential constraint logic program (plus syntactic sugar), thus allowing the application of the generalized approach as developed in [11]. To make this observation more evident, in this work we redefine NoSynch as a translation, directly mapping cc programs into clp programs (see Table 2); note that, while translating the clauses, we also map each constraint a ⊔ c ∈ C to its disjunctive lifting {|a ⊔ c|} ∈ P(C). By lifting the function vars on P(C) (i.e. by defining vars(c) = {x ∈ V | ∃∃_{x}c ≠ c}), it can be easily proved that NoSynch preserves the normal form of clauses.

3.2 The semantics of Ω-programs

Definition 3.2 (Ω-program) [1, 9] An Ω-program is a (concurrent) constraint logic program P together with a set Ω of predicate symbols.

Let pred(P) denote the set of predicates that are defined in P (this set can be a proper subset of the predicates occurring in P). A predicate symbol occurring in Ω is considered to be only partially defined in P, i.e. it is open in P. On the other hand, predicate symbols occurring in P but not in Ω have to be considered closed, i.e. fully specified^{1}. This means that an Ω-program P can be composed with other programs provided that these ones do not further specify the predicates which are closed in P.

1In order to avoid technical problems when defining the compositional semantics, we assume that all the closed predicates are defined in P; namely, if p ∈ Π \ Ω occurs in P then p ∈ pred(P). This condition can always be met by eventually adding a dummy definition p(x̂) :– 0 □ .

Definition 3.3 (Ω-union) [1, 9] Let P_{1} be an Ω_{1}-program and P_{2} be an Ω_{2}-program. If Ω ⊆ Ω_{1} ∩ Ω_{2} and (pred(P_{1}) ∩ pred(P_{2})) ⊆ (Ω_{1} ∩ Ω_{2}) then P_{1} ∪_{Ω} P_{2} is the Ω-program P_{1} ∪ P_{2}. Otherwise P_{1} ∪_{Ω} P_{2} is not defined.

From now on, we consider a clp program P obtained by applying the translation NoSynch. The key observation of [1] is that compositionality wrt program union can be achieved by considering interpretations based on (possibly non-unit) clauses. Hence, the compositional fixpoint semantics F_{Ω}(P) is obtained by extending the semantic construction of the previous section.

Definition 3.4 (clause skeleton) Let cl : p_{0}(x̂_{0}) :– c □ p_{1}(x̂_{1}), …, p_{n}(x̂_{n}) be a clp clause in normal form. The skeleton of cl is defined as skel(cl) = ⟨ p_{0}, p_{1}, …, p_{n} ⟩ ∈ Π^{+}. Given a set Ω ⊆ Π of predicate symbols, the set of Ω-skeletons is defined as ΠΩ^{∗} = {⟨ p_{0}, …, p_{n} ⟩ | p_{0} ∈ Π, ⟨ p_{1}, …, p_{n} ⟩ ∈ Ω^{∗} }.

Definition 3.5 (Ω-interpretation) Let cl ≡ p_{0}(x̂_{0}) :– c □ B and cl′ ≡ p′_{0}(ŷ_{0}) :– c′ □ B′ be two clauses in normal form. We write cl ⪯ cl′ iff skel(cl) = skel(cl′) and ∃∃x̂(δ_{x̂ẑ} ⊗ c) ⊆ ∃∃ŷ(δ_{ŷẑ} ⊗ c′), where x̂ = vt(cl), ŷ = vt(cl′) and ẑ is a tuple of distinct variables such that x̂ ∩ ẑ = ŷ ∩ ẑ = ∅. Then cl ∼ cl′ iff both cl ⪯ cl′ and cl′ ⪯ cl hold. The interpretation base is B_{Ω}^{Π} = { [cl]_{∼} | skel(cl) ∈ ΠΩ^{∗} }. An Ω-interpretation I ∈ ℑ_{Ω}^{Π} is any subset of B_{Ω}^{Π} such that for each sk ∈ ΠΩ^{∗} there exists one and only one clause cl ∈ I such that skel(cl) = sk.

As in the previous section, we omit the superscript Π when no confusion can arise and we order Ω-interpretations by extending the partial order ⪯ defined on clauses. The domain ⟨ ℑ_{Ω}, ⪯ ⟩ is again a complete lattice.

Let us introduce the merge operator (·)^{♭} : ℘(B_{Ω}) → ℑ_{Ω}.

(S)^{♭} = \{ [cl]_{∼} | \begin{matrix}∃ sk ∈ ΠΩ^{∗} such that \\ cl ≡ h:– c □ B, skel(cl) = sk, x̂ = vt(cl) \\ c = ⨁ \{ ∃∃ŷ(δ_{ŷx̂} ⊗ c′) | \begin{matrix}cl′ ≡ h′:– c′ □ B′ ≪x̂ S \\ skel(cl′) = sk, ŷ = vt(cl′) \end{matrix} \} \end{matrix} \}

The lub ⊎ on ℑ_{Ω} is defined as before: ⨄_{i∈J} I_{i} = ( ⋃_{i∈J} I_{i} )^{♭}.

Given the set of predicates Ω, let Id_{Ω} = { [p(x̂) :– δ_{ŷx̂} □ p(ŷ).]_{∼} | p ∈ Ω}. The T_{P}^{Ω} operator is obtained by unfolding the program P wrt the Ω-interpretation I augmented with Id_{Ω}. A careful use of clauses renaming and cylindric operators allows to preserve normal forms.

Definition 3.6 (T_{P}^{Ω}) [9] Let cl_{0} ≡ p_{0}(x̂_{0}) :– c_{0} □ B be a clp clause, where B = p_{1}(x̂_{1}), …, p_{n}(x̂_{n}); let I be an Ωinterpretation and X_{0} = ∅. We define the operator T_{cl_{0}}^{Ω} : ℑ_{Ω} → ℘(B_{Ω}) as follows:

T_{cl_{0}}^{Ω}(I) = \{ [p_{0}(x̂_{0}) :– c □ B_{1}, …, B_{n}]_{∼} | \begin{matrix}∀ i ∈ \{1, …, n\} . X_{i} = X_{i−1} ∪ vt(cl_{i−1}) \\ ∃ cl_{i} ≡ p_{i}(ŷ_{i}) :– c_{i} □ B_{i} ≪_{X_{i}} (I ∪ Id_{Ω}) \\ c = ∃∃_{vt(B)} ( c_{0} ⊗ ( ⨂_{i=1}^{n} ∃∃ŷ_{i}(δ_{ŷ_{i}x̂_{i}} ⊗ c_{i}))) \end{matrix} \}

Thus T_{P}^{Ω} : ℑ_{Ω} → ℑ_{Ω} is defined as T_{P}^{Ω}(I) = ( ⋃ { T_{cl}^{Ω}(I) | cl ∈ P })^{♭} and F_{Ω}(P) = T_{P}^{Ω} ↑ ω.

If Ω ≠ ∅ then any Ω-interpretation is an infinite set, as the set of Ω-skeletons ΠΩ^{∗} is infinite. For simplicity, when denoting an Ω-interpretation we usually drop all the clauses h:– c □ B such that c = 0. Even by adopting this representation convention, in general Ω-interpretations are infinite sets (we will discuss this point later in subsection 4.1). As a special case, by taking Ω = ∅, we obtain the set of ∅-interpretations ℑ_{∅} = ℑ which is exactly the set of interpretations defined in the previous section; moreover, T_{P}^{∅} = T_{P} and F_{∅} = F.

Theorem 3.1 (compositionality) [9] Let P_{1} be an Ω_{1}-program, P_{2} be an Ω_{2}-program and let P_{1} ∪_{Ω} P_{2} be defined. Then F_{Ω}(F_{Ω_{1}}(P_{1}) ∪_{Ω} F_{Ω_{2}}(P_{2})) = F_{Ω}(P_{1} ∪_{Ω} P_{2}).

We have seen that the compositional semantics of an Ω-program P encodes the dependences of P from the open predicates Ω. By giving the semantics of the predicates in Ω we fully specify the semantics of P; for this reason we call Ω-closure any interpretation I ∈ ℑ_{∅}^{Ω}. Given the Ω-programs P_{1} and P_{2}, we define the equivalence relation ≈_{Ω} that holds whenever P_{1} and P_{2} are equivalent under all the possible Ω-closures (here we regard an Ω-closure as an Ω-program).

Definition 3.7 P_{1} ≈_{Ω} P_{2} iff for all Ω-closures I we have F(P_{1} ∪_{∅} I) = F(P_{2} ∪_{∅} I).

Proposition 3.2 [1] P_{1} ≈_{Ω} F_{Ω}(P_{1}) and (F_{Ω}(P_{1}) = F_{Ω}(P_{2}) ⇒ P_{1} ≈_{Ω} P_{2}).

4 Correctness Results

In this section we formalize the notion of correctness of an abstract domain wrt (the disjunctive lifting of) a constraint system. This condition implies the correctness of the (compositional) abstract semantic construction, which is obtained my mimicking the concrete one on the abstract domain. The definitions are inspired by [11, 12], which in turn are based on the classical works on abstract interpretation theory [5, 6].

Definition 4.1 An abstract domain A = ⟨ L, ⊑^{♯}, 0^{♯}, 1^{♯}, ⊕^{♯}, ⊓^{♯}, ⊗^{♯}, ∃∃_{x}^{♯}, δ_{xy}^{♯} ⟩_{x,y∈V} is a complete lattice ⟨ L, ⊑^{♯}, 0^{♯}, 1^{♯}, ⊕^{♯}, ⊓^{♯} ⟩ together with a binary operator ⊗^{♯}, a family of unary operators ∃∃_{x}^{♯} for x ∈ V and a family of distinguished elements δ_{xy}^{♯} ∈ L for x, y ∈ V.

The safeness of the overall construction can be achieved by suitably relating the concrete and abstract elements and by imposing correctness conditions regarding the domain’s operators.

Definition 4.2 An abstract domain A = ⟨ L, ⊑^{♯}, 0^{♯}, 1^{♯}, ⊕^{♯}, ⊓^{♯}, ⊗^{♯}, ∃∃_{x}^{♯}, δ_{xy}^{♯} ⟩_{x,y∈V} is correct wrt the concrete domain P(C) = ⟨ P(C), ⊆, 0, 1, ⊕, ∩, , ⊗, ∃∃_{x}, δ_{xy} ⟩_{x,y∈V} using α iff there exists an upper Galois insertion (α, γ) relating P(C) and L and ∀c, c′ ∈ P(C), ∀x, y ∈ V α(c ⊗ c′)⊑^{♯}α(c) ⊗^{♯} α(c′), α(∃∃_{x}c)⊑^{♯}∃∃_{x}^{♯}α(c) and α(δ_{xy})⊑^{♯}δ_{xy}^{♯}.

Example 4.1 [groundness][11] Consider the Herbrand constraint system (together with the disjunctive lifting induced by ρ = id) and consider the abstract domain induced by the constraint system of dependency relations defined in Example 2.1. It is known that the latter is equivalent to the domain Def of definite and positive boolean functions defined on variables V, together with the element False. We now relate the two domains by exploiting the groundness dependency information. Let c ≡ ∃_{Y} {x_{i} = t_{i} | i = 1, …, n} ∈ H be a Herbrand constraint in solved form^{2} and, for all i ∈ {1, …, n}, let W_{i} = vars(t_{i}). Define the function α_{H} : H → Def such that α(c) = ∃_{Y} ( ∧_{i=1}^{n}(x_{i} ↔ ∧W_{i}) ) and let α_{H}(false) = False. The abstraction function α : ℘(H) → Def is defined as the additive extension of α_{H}, i.e. α(S) = ⊕^{♯} {α_{H}(c) | c ∈ S }. Then the constraint system Def is correct wrt P(H) using α [11]. □

By substituting each occurrence of elements and operators of the concrete domain by the corresponding elements and operators of the abstract domain, we systematically derive the notions of abstract program, goal and clauses; abstract clauses are ordered by ⪯^{♯} and we easily define the set ℑ_{Ω}^{♯} of abstract Ω-interpretations, which is ordered, as before, by extending the relation ⪯^{♯}; then we define the abstract immediate consequences operator and the abstract bottom-up semantic function F_{Ω}^{♯}.

Theorem 4.1 (correctness) (α ∘ F_{Ω})(P) ⪯^{♯} (F_{Ω}^{♯} ∘ α)(P)

We are now ready to formalize the relation between the semantics of a cc program and the semantics of its NoSynch translation, the latter semantics being computed compositionally.

Let P_{1} and P_{2} be two cc programs; let Ω_{1} (resp. Ω_{2}) be the set of predicates that are open in P_{1} (resp. P_{2}), such that P = P_{1} ∪_{∅} P_{2} is defined. Given the cc configuration G, let G^{♯} be its corresponding abstract clp goal and define P_{i}^{♯} = α(NoSynch(P_{i})), where i = 1, 2.

Corollary 4.2 α( SS[[ P ]](G) ) ⊑^{♯} F_{∅}^{♯}( F_{Ω_{1}}^{♯}(P_{1}^{♯}) ∪_{∅} F_{Ω_{2}}^{♯}(P_{2}^{♯}) )(G^{♯})

Corollary 4.3 If program P = P_{1} ∪_{∅} P_{2} and configuration G are suspension free then

α( O[[ P ]](G) ) ⊑^{♯} F_{∅}^{♯}( F_{Ω_{1}}^{♯}(P_{1}^{♯}) ∪_{∅} F_{Ω_{2}}^{♯}(P_{2}^{♯}) )(G^{♯})

Obviously, these results can be generalized to the case of n > 2 program modules. Also note that they do not depend on the program decomposition we have chosen.

4.1 Termination

Up to now, we have described an abstract interpretation framework. To turn the abstract interpretation into a static analysis, we have to be sure that the approximation of the semantics is finitely computable. Note that, as the set ΠΩ^{∗} is infinite (unless Ω = ∅), we can obtain a diverging computation even if our abstract domain is finite. A general way to overcome the problem is the definition of a widening operator on the lattice of abstract Ω-interpretations. Some proposals are in the literature; e.g., in [3] sequences of process calls in a cc configuration are handled by applying another approximation layer, called ∗- abstraction; the same technique has been applied in [2] for the compositional analysis of pure logic programs; this solution enforces termination but must pay in terms of accuracy. An interesting result has been achieved in [10] for the case of finite abstract domains. In this case a finite characterization of the compositional semantics of a (constraint) logic program can be obtained (without any loss of precision) as the result of a finite number of iterations of the immediate consequences operator T_{P}^{Ω}. In practice, instead of checking if we have reached the fixpoint of T_{P}^{Ω}, we check for the T -stability of the n-th iterate.

Theorem 4.4 [10] Let P be an Ω-program computing on a finite constraint system. There exists an n < ω such that for all m ≥ n we have (T_{P}^{Ω} ↑ n) ≈_{Ω} (T_{P}^{Ω} ↑ m).

2Namely, i ≠ j entails x_{i} ≢ x_{j}, Y = ⋃_{i=1}^{n} vars(t_{i}) and x_{i} ∉ Y for all i ∈ {1, …, n}.

Note that having assumed the finiteness of the domain, we obtain the finiteness of the T - stability check also, as we have a finite number of possible Ω-closures each one being a finite object.

5 Example

To clarify the picture, we now show a compositional analysis computing the groundness dependencies between the variables of a cc program defined on the Herbrand constraint system. In the program chunk P, process q is left unspecified (as usual, we denote anonymous Herbrand variables by underscores).

P : \{ \begin{matrix}g(x, y) :– true : x = x_{1} = z, y = y_{1} □ p(x_{1}, y_{1}), q(z). \\ p(x, y) :– x = [a| ] : x = [a|x_{1}], y = [b|y_{1}] □ p(x_{1}, y_{1}). \\ p(x, y) :– x = [] : y = [] □ . \end{matrix}

The corresponding abstract program is P^{♯} = (α ∘ NoSynch)(P), where we use the α defined in Example 4.1:

P^{♯} : \{ \begin{matrix}g(x, y) :– (x ↔ x_{1} ↔ z) ∧ (y ↔ y_{1}) □ p(x_{1}, y_{1}), q(z). \\ p(x, y) :– (x ↔ x_{1}) ∧ (y ↔ y_{1}) □ p(x_{1}, y_{1}). \\ p(x, y) :– x ∧ y □ . \end{matrix}

Let Ω_{1} = {q}; then F_{Ω_{1}}^{♯}(P^{♯}) = { p(x, y) :– x ∧ y □ . , g(x, y) :– x ∧ y ∧ z □ q(z). }. Let us consider the initial configuration G = ⟨ true □ g(x, y) ⟩ and let Q be any Ω_{2}-program such that P ∪_{∅} Q is defined. The informal reading of the previous abstract denotation is that all the successful computations of P ∪_{∅} Q starting from G bind both variables to ground terms. Indeed, let Ω_{2} = ∅ and consider the following two alternative Ω_{2}-programs defining the process q.

Q_{1} : \{ \begin{matrix}q(x) :– true : x = [a|x_{1}] □ q(x_{1}). \\ q(x) :– true : x = [] □ . \end{matrix} Q_{2} : \{ \begin{matrix}q(x) :– true : x = [ |x_{1}] □ q(x_{1}). \\ q(x) :– true : x = [] □ . \end{matrix}

Program P_{1} = P ∪ Q_{1} and goal G are suspension free and it can be easily observed that in all the answers of the finite semantics O[[ P_{1} ]](G) the variables x and y are ground, thus showing the correctness of the analysis. Things are different when considering program P_{2} = P ∪ Q_{2}, which is not suspension free; in this case the finite semantics contains terminating computations reaching final stores in which both x and y are not ground. Nonetheless, for all the successful computations, correctness still holds (there is only one successful computation for P_{2} and G, yielding the store (x = [], y = [])).

6 Conclusions

Due to the sophisticated synchronization mechanism provided by ask guards, the complexity overhead of a compositional semantics for concurrent constraint programs can easily overcome the benefits of a modular approach to the static analysis of these languages. In this work we have provided a modular abstract interpretation framework that partially solves this problem by assuming that the complete cc program is suspension free. For the purposes of program analysis, a suspension free cc program can be safely translated into a clp program by removing all its ask guards. The abstract interpretation of the new program, computed within any framework for clp, yields a correct approximation of the semantics of the original program. The complexity of this construction is limited, as the translation greatly simplifies the interactions between the program modules. This methodology provides results in implicative form: all the computations of the complete program that do not suspend are correctly described by the compositionally computed approximation. The approach is truly incremental and it does not depend on the chosen program decomposition: no hypotheses are made on the suspension freeness of each program module.

References

[1] A. Bossi, M. Gabbrielli, G. Levi, and M. C. Meo. A Compositional Semantics for Logic Programs. TCS, 122(1-2):3–47, 1994.

[2] M. Codish, S. K. Debray, and R. Giacobazzi. Compositional Analysis of Modular Logic Programs. In Proc. POPL’93, pages 451–464. ACM Press, 1993.

[3] M. Codish, M. Falaschi, and K. Marriott. Suspension Analysis for Concurrent Logic Programs. In Proc. ICLP’91, pages 331– 345. The MIT Press, 1991.

[4] M. Codish, M. Falaschi, K. Marriott, and W. Winsborough. Efficient Analysis of Concurrent Constraint Logic Programs. In Proc. ICALP’93, LNCS, pages 633–644, 1993.

[5] P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. POPL’77, pages 238– 252, 1977.

[6] P. Cousot and R. Cousot. Systematic Design of Program Analysis Frameworks. In Proc. POPL’79, pages 269–282, 1979.

[7] M. Falaschi, M. Gabbrielli, K. Marriott, and C. Palamidessi. Confluence and Concurrent Constraint Programming. In Proc. AMAST’95, 1995.

[8] M. Falaschi, G. Levi, M. Martelli, and C. Palamidessi. A new Declarative Semantics for Logic Languages. In Proc. ICLP’88, pages 993–1005. The MIT Press, 1988.

[9] M. Gabbrielli, M.G. Dore, and G. Levi. Observable semantics for Constraint Logic Programs. JLC, 5(2):133–171, 1995.

[10] M. Gabbrielli, R. Giacobazzi, and D. Montesi. Modular logic programs over finite domains. In Proc. GULP’93, pages 663–678, 1993.

[11] R. Giacobazzi, S. K. Debray, and G. Levi. A Generalized Semantics for Constraint Logic Programs. In Proc. FGCS’92, pages 581–591, 1992.

[12] R. Giacobazzi, S.K. Debray, and G. Levi. Generalized Semantics and Abstract Interpretation for Constraint Logic Programs. JLP, 1995.

[13] L. Henkin, J.D. Monk, and A. Tarski. Cylindric Algebras. Part I and II. North-Holland, Amsterdam, 1971.

[14] V. A. Saraswat, M. Rinard, and P. Panangaden. Semantic Foundation of Concurrent Constraint Programming. In Proc. POPL’91, pages 333–353. ACM, 1991.

[15] V.A. Saraswat and M. Rinard. Concurrent constraint programming. In Proc. POPL’90, pages 232–245. ACM, 1990.

[16] D. Scott. Domains for Denotational Semantics. In Proc. ICALP’82, LNCS, pages 577–613. Springer-Verlag, 1982.

[17] E. Zaffanella, G. Levi, and R. Giacobazzi. Abstracting Synchronization in Concurrent Constraint Programming. In Proc. PLILP’94, LNCS, pages 57–72. Springer-Verlag, 1994.