Abstracting Synchronization in Concurrent Constraint Programming ^{⋆}

Enea Zaffanella^{1} Roberto Giacobazzi^{2} Giorgio Levi^{1}

1 Dipartimento di Informatica, Università di Pisa Corso Italia 40, 56125 Pisa (zaffanel,levi)@di.unipi.it

2 LIX, Laboratoire d’Informatique, École Polytechnique 91128 Palaiseau cedex giaco@lix.polytechnique.fr

Abstract. Because of synchronization based on blocking ask, some of the most important techniques for data flow analysis of (sequential) constraint logic programs (clp) are no longer applicable to cc languages. In particular, the generalized approach to the semantics, intended to factorize the (standard) semantics so as to make explicit the domain-dependent features (i.e. operators and semantic objects which may be influenced by abstraction) becomes useless for relevant applications. A possible solution to this problem is based on a more abstract (non-standard) semantics: the success semantics, which models non suspended computations only. With a program transformation (NoSynch) that simply ignores synchronization, we obtain a clp-like program which allows us to apply standard techniques for data flow analysis. For suspension-free programs the success semantics is equivalent to the standard semantics thus justifying the use of suspension analysis to generate sound approximations. A second transformation (Angel) is introduced, applying a different abstraction of synchronization in possibly suspending programs and resulting in a framework which is adequate to suspension analysis. Applicability and accuracy of these solutions are investigated.

1 Introduction

Abstract interpretation is intended to formalize the idea of approximating program properties by evaluating them on suitable non-standard domains. The standard domain of values is replaced by a domain of descriptions of values and the basic operators are provided with a corresponding non-standard interpretation.

⋆ The work of E. Zaffanella and G. Levi has been supported by the “PARFORCE” (Parallel Formal Computing Environment) BRA-Esprit II Project n. 6707. The work of R. Giacobazzi has been partly supported by the EEC Human Capital and Mobility individual grant: “Semantic Definitions, Abstract Interpretation and Constraint Reasoning”, N. ERB4001GT930817, and by the Project inter-PRC: “Langages Logiques Concurrents avec Contraintes”.

In the classical framework of abstract interpretation [5], the relation between abstract and concrete semantic objects is provided by a pair of adjoint functions referred to as abstraction α and concretization γ. The definition of an abstract interpreter for a language actually corresponds to a semantics abstraction. However, many aspects of the (concrete) semantic construction are not affected by the abstraction. The generalized approach to the semantics in [11] has been introduced to factorize the semantics with respect to its domain-dependent features (i.e. operators and semantic objects). This technique can be naturally applied to clp programs, where the notion of constraint system provides a uniform framework to deal with semantic objects (constraints) and operators at different levels of abstraction. In this case, abstract interpretation is obtained simply by evaluating the abstract program into an instance of clp, provided with a suitable abstract constraint system. The key issue here is that both concrete and abstract computations are instances, at the constraint system level, of the clp paradigm. In general, the abstraction is characterized by weakening constraints.

In this paper we extend the generalized semantics approach to the abstract interpretation of cc programs, and show that in general we cannot provide any correct approximation by evaluating an abstract version of the program. The ask-tell paradigm [16] is an extension of constraint logic programming: in addition to satisfiability (tell), entailment (ask) is introduced. This different view of constraint programming leads to a powerful paradigm for concurrent computations: concurrent constraint programming (cc) in a shared store [16]. A store is a constraint representing the global state of the computation. Synchronization is achieved through blocking ask. This mechanism introduces some problems when dealing with abstraction. Intuitively a correct approximation of the program meaning generates weaker answers for any possible program behaviour. Thus, in order to correctly characterize answers associated with suspended computations, we must guarantee that whenever a concrete computation suspends the corresponding abstract computation suspends too. This can only be obtained by replacing ask constraints with stronger constraints, which is usually not the case in abstract interpretation. To overcome this “negative” result we consider a more abstract semantics modeling non suspended computations only. A transformation which ignores synchronization can be applied to make applicable the generalized semantics approach to the static analysis of cc programs. For suspension-free programs the standard and the success semantics are equivalent, thus justifying the use of suspension analysis [2] to generate sound approximations.

A different schema can be obtained by introducing hybrid primitives to deal with ask constraints. As before, we use a program transformation (Angel) which essentially replaces don’t care nondeterminism with don’t know nondeterminism. Following the semantic characterization of angelic cc processes given in [14], we obtain the denotational counterpart of the transition system based suspension analysis in [2] (modulo the absence of the consistency check). Simple results relate the accuracy of these different solutions when the program is suspensionfree, showing that the first approach is always better than the second one.

2 Constraint Systems

The algebraic specification (for sequential constraint logic programs) given in [11] is of major interest for abstract interpretation as it defines the minimal properties such a structure has to satisfy in order to obtain a suitable base for the generalized semantic construction. The resulting domains are very weak, allowing non-commutative and non-idempotent constraint composition operators and a wide range of (possibly non-distributive) constraint disjunction operators, i.e. widenings. On the other hand, the denotational semantics construction in [16] for cc languages requires stronger domains (only commutative and idempotent constraint composition operators are allowed). In this case constraint systems are not required to have a disjunction operator. Disjunctions arise only when considering different execution paths and they are modeled at the program semantics level (i.e. outside the constraint system definition) using sets of possible behaviours or a (fixed) powerdomain construction. As a consequence, these structures can be seen as specific instances of the previous ones (with minor modifications). Because of its specificity to the cc case, in the following we consider the latter approach.

The construction in [16] is an extension of Scott’s partial information systems [17]. Informally, we have a denumerable set D of elementary assertions (containing distinct elements 1 and 0 representing the least informative assertion and the contradiction respectively) and a compact entailment relation ⊢⊆ P^{f}(D) × D. By taking the entailment closure^{3} δ(u) of a set of assertions u we obtain the equivalence relation ∼ (u ∼ v iff δ(u) = δ(v)). Hence, a simple constraint system is C = ⟨ P(D), ⊣ ⟩/_{∼}, which is a complete ω-algebraic lattice [17]. An arbitrary element of C is called a constraint. Compact elements are called finite constraints, since they are equivalent to a finite subset of D. Finite constraints form the base B_{C} of the constraint system. In order to treat the hiding operator, [16] introduces a family of unary operations called cylindrifications [13]. Intuitively, given a constraint c, the cylindrification operation ∃_{x}(c) yields the constraint obtained by “projecting out” information about the variable x from c. Diagonal elements [13] are considered as a way to provide parameter passing. Note that special variables (not accessible to the user) together with a suitable use of cylindrification and diagonal elements make variable renaming no longer needed.

Definition 1. A (cylindric) constraint system^{4} ⟨C, ⊢, false, true, ⊗, V, ∃_{x}, d_{xy}⟩ is an algebraic structure where: ⟨C, ⊣⟩ is a simple constraint system, true = [1]_{∼} and false = [0]_{∼}, ⊗ is the glb, V is a denumerable set of variables and ∀x, y ∈ V, ∀c, d ∈ C, the operator ∃_{x} : C → C satisfies

3 The entailment closed representation, when it is finite, is a domain independent strong normal form for constraints and it is very useful when there are not simpler ones (e.g. clp(FD)). However, many domains do have a simpler strong normal form (Herbrand, Prop, Sharing, etc.) which greatly simplifies their representation.

4 In order to have a standard approach when dealing with abstract interpretation, we order constraints in a dual fashion w.r.t. [17, 16], i.e. lower constraints are the strongest ones and the constraint composition ⊗ is the glb operator.

1. c ⊢ ∃_{x}c

2. if c ⊢ d then ∃_{x}c ⊢ ∃_{x}d

3. ∃_{x}(c ⊗ ∃_{x}d) ∼ ∃_{x}c ⊗ ∃_{x}d

4. ∃_{x}(∃_{y}c) ∼ ∃_{y}(∃_{x}c)

∀x, y, z ∈ V, ∀c ∈ C, the diagonal element d_{xy} satisfies

1. d_{xx} ∼ true

2. if z ≠ x, y then d_{xy} ∼ ∃_{z}(d_{xz} ⊗ d_{zy})

3. if x ≠ y then d_{xy} ⊗ ∃_{x}(c ⊗ d_{xy}) ⊢ c

In the following, we denote by x̂ both a tuple and a set of variables. For syntactic convenience, given x̂ = (x_{1}, …, x_{n}) and ŷ = (y_{1}, …, y_{n}), the notation ∃x̂c stands for ∃_{x_{1}}(… ∃_{x_{n}}(c) …), while d_{x̂ŷ} stands for d_{x_{1}y_{1}} ⊗ … ⊗ d_{x_{n}y_{n}}.

Example 1. Let Σ = {a/0, b/0, …, f/n, g/n, …} be a finite set of function symbols with arity, and V be a finite set of variables. Consider the first order language defined over the term system induced by Σ, by using syntactic equality as unique predicate symbol. The Herbrand constraint system C_{H} has atomic propositions as elementary assertions and an entailment relation satisfying Clark’s equality axioms. Cylindrification ∃ is the usual existential quantification, while diagonal elements are d_{xy} ∼ (x = y). Thus constraints are equivalent to quantified syntactic equation systems.

Example 2. Let V be a finite set of variables and ϕ be a property. The elementary assertions in the constraint system of variable dependencies DEP_{ϕ}(V) are pairs of variable’s subsets. Assertion (A, B) means that if all the variables in B satisfy property ϕ, then all the variables in A satisfy the property too. The entailment relation is defined as follows. If A ⊆ B then ∅ ⊢ (A, B); if R ⊢ (A, B) and R ⊢ (B, C) then R ⊢ (A, C); finally, if R ⊢ (A, C) and R ⊢ (B, D) then R ⊢ (A ∪ B, C ∪ D). ∃_{x}R ∼ δ(R) \ {(A, B) ∈ R | x ∈ A ∪ B } is the cylindrification operator, while diagonal elements are d_{xy} ∼ {({x}, {y}), ({y}, {x})}. The disjunctive completion of this constraint system is isomorphic to the constraint system Prop. We can easily associate with each dependency relation R = {(A_{i}, B_{i}) | 1 ≤ i ≤ n} the propositional formula ∧_{i=1}^{n} (∧A_{i} ← ∧B_{i}). In the following we will use the simpler Prop representation.

3 The Language

In this section we introduce concurrent constraint languages, as defined in [16]. The syntax and the semantics are parametric with respect to a given constraint system C. Elementary actions (ask and tell), hiding (∃), parallel composition (∥), guarded nondeterministic choice (∑) and recursion are the syntactic operators (see Table 1). For notational convenience, we write ⊕_{i=1}^{n} A_{i} to de-

note the pure nondeterministic choice operator (local choice), namely the agent

∑_{i=1}^{n} ask(true) → A_{i}.

Progr ::= Dec . Agent

Dec ::= ϵ
| p(x̂) :− Agent . Dec

Agent ::= tell(c)
| ∃x̂.Agent
| Agent ∥ Agent
| ∑_{i=1}^{n} (ask(c_{i}) → Agent_{i})
| p(ŷ)

Table 1: The syntax

3.1 Operational Semantics

The operational model is described by a transition system T = (Conf, ⟶). Elements of Conf (configurations) consist of an agent and a constraint, representing the residual computation and the global store respectively. ⟶ is the minimal relation satisfying axioms R1–R5 of Table 2.

R1 ⟨ tell(c) , σ ⟩⟶⟨ ϵ , σ ⊗ c ⟩
R2 \frac{σ ⊢ c_{i}}{⟨ ∑_{i=1}^{n} (ask(c_{i}) → A_{i}) , σ ⟩⟶⟨ A_{i} , σ ⟩}

R3 \begin{matrix}⟨ A , d ⊗ ∃x̂σ ⟩ & ⟶ & ⟨ B , e ⟩ \\ ⟨ ∃(x̂, d).A , σ ⟩ & ⟶ & ⟨ ∃(x̂, e).B , σ ⊗ ∃x̂e ⟩ \end{matrix}

\begin{matrix}R4 & \frac{⟨ A , σ ⟩⟶⟨ A′ , σ′ ⟩}{\begin{matrix}⟨ A∥B , σ ⟩ & ⟶ & ⟨ A′∥B , σ′ ⟩ \\ ⟨ B∥A , σ ⟩ & ⟶ & ⟨ B∥A′ , σ′ ⟩ \end{matrix}} \\ R5 & \frac{p(x̂) :− A ∈ P}{⟨ p(ŷ) , σ ⟩⟶⟨ Δŷ ; x̂.A , σ ⟩} \end{matrix}

Table 2: The transition system

The execution of an elementary action tell(c) simply adds the constraint c to the current store σ (no consistency check). A guard g_{i} = ask(c_{i}) in the nondeterministic choice operator is a global test. It is enabled if the current store σ is strong enough to entail the constraint c (i.e. when σ ⊢ c). The nondeterministic choice operator selects one enabled guard g_{i} and then behaves like the agent A_{i}. If no guards are enabled, then it suspends, waiting for other agents to add more information to the store. Axiom R3 describes the hiding operator. The syntax is extended to deal with a local store d holding information about the hidden variables x̂. Hence the information about x̂ produced by the external environment does not affect the process behaviour and conversely the external environment cannot access the local store. Initially the local store is empty, i.e. ∃x̂.A ≡ ∃(x̂, true).A. Parallelism is modeled as interleaving of basic actions. Processes A and B never communicate synchronously in A∥B. Finally, when executing a procedure call, Δŷ ; x̂A denotes the agent ∃ψ̂.(tell(d_{ŷψ̂})∥∃x̂.(tell(d_{ψ̂x̂})∥A)) and models parameter passing without variable renaming (variables in x̂ can occur in ŷ). Variables ψ̂ are special, meaning that they are not allowed to occur in user programs.

Let / ⟶ denote the absence of admissible transitions. Sequences of transitions reaching configurations ⟨ A_{n}, c_{n} ⟩ such that ⟨ A_{n}, c_{n} ⟩ / ⟶ are called terminating sequences and c_{n} ∈ B_{C} is the answer constraint. If A_{n} contains some guarded choice operators then the corresponding sequence is suspended, otherwise it is a successful sequence (in the latter case we denote A_{n} by ϵ).

Definition 2. The finite semantics for program P = D.A is

O_{D}[[ A]] = λσ. {c | ⟨ A , σ ⟩⟶^{∗}⟨ B , c ⟩ / ⟶}

Note that the finite semantics observes answer constraints associated with terminating configurations, regardless of whether the associated computations are successful or suspended.

3.2 Denotational Semantics

The standard denotational semantics for concurrent constraint languages models processes as sets of reactive sequences [6] or trace operators [16]. In this paragraph we consider the simpler denotational semantics modeling the angelic language [14], i.e. the language obtained by replacing the global choice operator by the local choice operator. This semantics is a suitable base for reasoning about synchronization approximation, since it separates the choice operator from the synchronization operator (while in the standard semantics their interaction gives the so-called demonic nondeterminism or indeterminism).

The angelic transition system T′, yelding the operational semantics O′, is obtained by imposing n = 1 in rule R2 of Table 2 and by adding rule R6:

⟨ ⊕_{i=1}^{n} A_{i} , σ ⟩ ⟶⟨ A_{i} , σ ⟩.

[16] defines the finite semantics of deterministic cc languages (without choice operator) as a lower closure operator^{5} (lco) on B_{C} (the set of finite elements of the constraint system C), mapping divergent computations to false. A lco on a complete lattice is characterized by its image (i.e. the set of fixpoints). Furthermore, lco’s form a complete lattice. By using the fixpoint representation, we have that the pointwise ordering is ⊆, the bottom element is {false} (i.e. λx.false), the top element is C (i.e. id) and the glb is given by set intersection.

Since the local choice operator introduces nondeterminism, we have to consider sets of constraints in order to model the computational behaviour, because in general the lub of two constraints is weaker than their disjunction. Intuitively, we want to record the minimal guarantee of a set of constraints, i.e. the pre-order: S_{1} ⊑ S_{2} iff ∀c ∈ S_{1}∃ d ∈ S_{2} . c ⊢ d.

Definition 3. Given a partial order ⟨C, ≤_{C}⟩, the downward closure of S ⊆ C is defined by down(S) = {d ∈ C | ∃c ∈ S.d ≤_{C} c}. A subset S is downward closed iff S = down(S). Given a function f : C → P(C′), the downward closure of f is the function g = Down(f) : C → P↓(C′) such that g(c) = down(f(c)).

5 Recall that we are ordering the constraint system in a dual fashion. Lower closure operators and downward-closed sets of constraints correspond to upper closure operators and upward-closed sets of constraints in [16] and [14].

By identifying sets of constraints that are equivalent with respect to ⊑, we obtain a domain isomorphic to the complete lattice P↓(C) of downward-closed subsets of C. The partial order is ≤≡⊆, the lub and the glb are given by set union and set intersection respectively. Furthermore the immersion function ↓: C → P↓(C) is given by ↓c = down({c}).

Since for cc programs disjunction arises only when considering alternative computations, the finite semantics of angelic processes is modeled as a linear lco (llco) on P ↓(C) [14], i.e. a lco f satisfying f(∪S_{i}) = ∪f(S_{i}). A llco f is fully characterized by the set SF (f) ⊆ C of its singleton fixpoints, i.e. constraints c such that f(↓c) = ↓c. By using this characterization we easily see that llco(P↓(C)) (the set of llco’s on P↓(C)) is a complete lattice with lub and glb given by set union and set intersection respectively.

Table 3 shows the angelic semantic functions E, D and N. Env is the set of environments, i.e. the set of functions from process names to their denotation in llco(P↓(C)). Note that the denotational semantics actually extends to the cc paradigm the C-semantics of pure logic programs [10].

Proposition 4. O_{D}[[ A]](c) ⊆ O′_{D}[[ A]](c) ⊆ Down(O′_{D}[[ A]])(c) = N [[ D.A]](↓c)

E : Agent × Env → llco(P↓(C))

E[[ tell(c) ]]e =↓c

E[[ ask(c) → A]]e = {d ∈ C | d ⊢ c ⇒ d ∈ E[[ A]]e }

E[[ ∃x̂.A]]e = {d ∈ C | there exists c ∈ E[[ A]]e s.t. ∃x̂c = ∃x̂d } E[[ A ∥ B]]e = E[[ A]]e ∩ E[[ B]]e

E[[ ⊕_{i=1}^{n} A_{i}]]e = ∪_{i=1}^{n} E[[ A_{i}]]e

E[[ p(ŷ) ]]e = {d ∈ C | d = ∃ψ̂(d_{ŷψ̂} ⊗ c), c ∈ (e p)}

D : Dec × Env → Env

D[[ ϵ]]e = e

D[[ p(x̂) :− A . D]]e = D[[ D]] (e [p ↦ E[[ ∃x̂.(tell(d_{ψ̂x̂}) ∥ A) ]]e])

N : Progr → llco(P↓(C)) N [[ D.A]] = E[[ A]](lfp D[[ D]])

Table 3: The finite angelic semantic operators

4 Program Properties and Approximations

The operational semantics of a cc program associates each initial store c to the set of all the answer constraints that we obtain by executing P = D.A at c. In a similar way we define a semantic property ϕ as a subset of the constraint system, namely the set of constraints that satisfy the property ϕ. Thus, a program satisfies a semantic property ϕ iff (for each initial store) the observables of the program are a subset of the property, i.e. for all c ∈ C . O_{D}[[ A]](c) ⊆ ϕ. Following this general view, also pursued in [7] in the context of partial correctness proofs for cc programs, we can formalize the static analysis as a finite construction of an approximation (a superset) of the program denotation. If the approximation satisfies the semantic property, then we can safely say that our program satisfies the property too.

Let us define a program property to be ordering closed iff it is downward closed or upward closed. Ordering closed properties are easier to verify, as shown by the following proposition.

Proposition 5. A program P = D.A satisfies a downward closed (upwardclosed) property ϕ ⊆ C iff the downward closure (upward closure) of O_{D}[[ A]] satisfies ϕ.

Simplification arises because we can base our abstract interpretation framework on a semantics that returns ordering closed observables. An example of downward closed property is definiteness. If a variable x is fully instantiated in a constraint c then it is fully instantiated in all the constraints d such that d ⊢ c.

The adjoint framework of [5] is a powerful tool for the analysis of ordering closed properties. The best approximations for both concrete objects and semantic functions always exist and we can compare accuracy of different abstract semantic functions. Consider downward closed properties.

Definition 6. Let ⟨M, ≤, ⊔, ⊓⟩ and ⟨M′, ≤′, ⊔′, ⊓′⟩ be complete lattices. An upper Galois connection between M and M′ is a pair of functions ⟨α, γ⟩ such that: ∀x ∈ M . ∀y ∈ M′ . α(x) ≤′ y ⇔ x ≤ γ(y). An upper Galois insertion between M and M′ (denoted by ⟨M, α, γ, M′⟩) is an upper Galois connection such that α is surjective (equivalently, γ is one-to-one).

Upper Galois insertions are commonly used in abstract interpretation of (constraint) logic languages. Here the approximation process returns weaker (w.r.t. ⊢) semantic objects (an example for the clp case is in [11]).

5 Generalized Abstract Interpretation

Generalized abstract interpretation is intended to perform static analysis using the same semantic construction for both the concrete and abstract computations. Given an abstract constraint system A that correctly approximates the concrete constraint system C, the program P computing on C is syntactically transformed into a program P′ computing on A. The static analysis of P is obtained by computing the semantics of P′.

Definition 7. A constraint system ⟨A, ⊢′, false′, true′, ⊗′, V, ∃′_{x}, d′_{xy}⟩ is upper correct with respect to the constraint system ⟨C, ⊢, false, true, ⊗, V, ∃_{x}, d_{xy}⟩, using a surjective and monotonic function α : C → A, iff (for each c ∈ C, x, y ∈ V) α(∃_{x}c) ⊢′ ∃′_{x}α(c) and α(d_{xy}) ⊢′ d′_{xy}.

Proposition 8. If A is upper correct w.r.t. constraint system C using α then there exists an upper Galois insertion relating P↓(C) and P↓(A).

Example 3. Let C_{H} be the Herbrand constraint system, let DEP_{g} be the dependency relation between variables induced by groundness and let the function sol map an equational constraint into its (equivalent) solved form. Define α_{g} : C_{H} → DEP_{g} as follows.

α_{g}(c) = \{ \begin{matrix}∃ŷ (∪ \{ \{(\{x_{i}\}, var(t_{i})), (var(t_{i}), \{x_{i}\}) \} | x_{i} = t_{i} ∈ E \}) & if sol(c) = ∃ŷE \\ F alse & if sol(c) = false \end{matrix}

Proposition 9. DEP_{g} is upper correct w.r.t. C_{H} using α_{g}.

As usual, termination is guaranteed by assuming finite constraint systems.

5.1 The Abstract Synchronization Problem

Consider the angelic cc language and let f be a llco on P ↓(C) (the concrete semantics of an agent). Let A be an abstract constraint system upper correct w.r.t. C using α and let (α̃, γ) be the induced upper Galois insertion relating the concrete domain P↓(C) and the abstract domain P↓(A). The best correct approximation for f on P↓(A) is f^{♯} = (α̃ ∘ f ∘ γ). Let f′ : P↓(A) → P↓(A) be an abstract semantic operator. f′ is a correct upper approximation of f on P↓(A) iff f^{♯} ⊢′ f′ [5].

Proposition 10. f^{♯} = (α̃ ∘ f ∘ γ) is a llco on P↓(A).

The abstract and the concrete semantics of angelic processes can be modeled in the same way and we can write f^{♯} ⊢′ f′ as f^{♯} ⊆ f′. However, the simple transformation considered in [11] is no longer admissible for cc programs because the abstract synchronization operator would not be correct. The following theorem justifies this observation.

Theorem 11.

[ \begin{matrix}∀ c ∈ C, ∀ f ∈ llco(P↓(C)), f′ ∈ llco(P↓(A)) \\ s.t. f^{♯} ⊆ f′ \\ [ask(c) → f]^{♯} ⊆ ask(α(c)) → f′ \end{matrix} ] ⇔ [ α is an isomorphism ]

A “solution” to the abstract synchronization problem can be found by considering a different (more abstract) concrete semantics which models only some aspects of the program behaviour.

Definition 12. The success semantics for program P = D.A is

SS_{D}[[ A]] = λ σ ∈ C . {c | ⟨ A , σ ⟩⟶^{∗}⟨ ϵ , c ⟩}

This semantics does not observe answer constraints associated to suspended computations. It observes successful computations only.

Proposition 13. If P = D.A is suspension-free then O_{D}[[ A]] = SS_{D}[[ A]].

Turning our attention to the success semantics, we easily see that correctness depends on the following condition:

“concrete computation proceeds ⇒ abstract computation proceeds”

Thus, whenever we cannot prove the contrary, we assume that the concrete computation proceeds. The simplest way to satisfy this correctness condition consists in removing all synchronizations from the program. Consider the transformation NoSynch : Progr → Progr, acting on nondeterministic choice operators only.

NoSynch[∑_{i=1}^{n} (ask(c_{i}) → A_{i})] = ⊕_{i=1}^{n} (tell(c_{i}) ∥ NoSynch[A_{i}])

In the following let P_{1} = D_{1}.A_{1} = NoSynch[P]. Since we have discarded every meaningful synchronization test, processes in P_{1} always proceed, providing a correct approximation of the success semantics of P.

Proposition 14. SS_{D}[[ A]](c) ⊆ SS_{D_{1}}[[ A_{1} ]](c)

Transformed programs are very similar to sequential constraint logic programs. As in [11], their semantics can easily be modeled by a single (disjunctive) constraint (see [12]). For space reasons, we omit the presentation of this simpler semantics and use Table 3 again, where the equation dealing with asks has become useless.

Corollary 15. Down(SS_{D_{1}}[[ A_{1} ]]) = N [[ D_{1}.A_{1} ]]

To obtain the abstract semantics of the transformed program P_{1} we now apply the generalized approach of [11]. This amounts to instantiate Table 3 over the abstract constraint system A and then to compute the semantics of the abstract program P′_{1} corresponding to P_{1}.

Definition 16. Given the program P on C, the corresponding abstract program P′ on A = α(C) is obtained by replacing each tell constraint c of P by α(c).

Note that this transformation does not affect ask constraints. Let P′_{1} be the abstract program corresponding to P_{1}.

Theorem 17. (α̃ ∘ N [[ P ]] ∘ γ) ⊆ N′[[ P′]]

Example 4. Consider the program P which appends two lists.

app(X,Y,Z) :- ask(X=[]) -> tell(Y=Z)
            + ask(∃H,X1 X=[H|X1]) ->

                 ∃ H,X1,Z1. tell(X=[H|X1],Z=[H|Z1]) || app(X1,Y,Z1).

P_{1} = NoSynch[P], after a straightforward simplification, is

app(X,Y,Z) :- tell(X=[],Y=Z)
            ⊕ ∃ H,X1,Z1. tell(X=[H|X1],Z=[H|Z1]) || app(X1,Y,Z1).

Let us consider the abstract constraint system A = Prop. The program P′_{1} on Prop corresponding to P_{1} is

app(X,Y,Z) :- tell(X∧Y↔Z)
            ⊕ ∃ H,X1,Z1. tell(X↔(H∧X1)∧Z ↔(H∧Z1)) || app(X1,Y,Z1).

We obtain N′[[ P′_{1}.app(x, y, z) ]](↓ a) =↓ a ∩ ↓ ((x ∧ y) ↔ z) specifying that in all the answer constraints associated to successful computations of the original program, the third argument of app is bound to a ground term iff both the first and the second argument are bound to ground terms.

6 An “Angelic” Solution

To approximate the standard semantics of a program without any suspension freeness information, e.g. if we are trying to prove suspension-freeness, the previous approach is no longer applicable. As an alternative, we can consider the best correct lower approximation of the synchronization operator, that is

[ask(c) → f]^{♯} = λS′ ∈ P↓(A).∪{if γ(↓a) ⊆ (↓c) then f^{♯}(↓a) else ↓a | a ∈ S′ }

Note however that in general we cannot statically compute the concrete object γ(a). In practice, we have to implement a “hybrid” synchronization test which verifies whether an abstract constraint definitely entails a concrete one,

test : (A × C) → Bool such that test(a, c) = true ⇒ γ(↓a) ⊆ (↓c).

Informally, this condition means “if the abstract computation proceeds then every concrete computation it approximates proceeds too”. Notice that this approach is not based on generalizing the semantics, as the abstract program does not perform all computations on the abstract constraint system. Moreover, this synchronization primitive strongly depends upon the specific analysis, i.e. upon the specific choice of the abstract domain.

Given a synchronization primitive, we have to choose a suitable approximation of the nondeterministic operator. In order to get an efficient abstract interpretation framework, we cannot directly abstract global choice, since the associated denotational models are too complex [2, 8]. Local choice (i.e. angelic languages) seems to be a good cost/precision tradeoff.

Consider the transformation Angel, mapping don’t care choice operators into don’t know choice operators with multiple synchronization.

Angel[∑_{i=1}^{n}(ask(c_{i}) → A_{i})] = ask(c_{1}; …; c_{n}) → ⊕_{i=1}^{n} (tell(c_{i}) ∥ Angel[A_{i}])

The meaning of a multiple synchronization test is to ask the disjunction of all

the guard constraints: ∀σ ∈ S . ∃j ∈ {1, …, n} . (↓σ) ⊆ (↓c_{j}) ⇔ S ⊆ ∪_{i=1}^{n} (↓c_{i}).

Remark. This is not true when we consider a widening as disjunction operator. As an example, consider a constraint system dealing with rational intervals with entailment given by inclusion. Process ask(x ∈ [0, 1]; x ∈ [1, 2]) → A and its widened version ask(x ∈ [0, 2]) → A are not equivalent. Given the initial store x ∈ [0, 2], the first computation (correctly) suspends, while the latter proceeds, possibly providing uncorrect results.

The denotational semantics of this kind of programs can be obtained by using Table 3 and by replacing the equation for the (simple) synchronization operator with the following equation.

E[[ ask(c_{1}; …; c_{n}) → A]]e = {d ∈ C | ∃ i ∈ {1, …, n}.d ⊢ c_{i} ⇒ d ∈ E[[ A]]e}

Therefore, given S′ ∈ P↓(A) and c_{1}, …, c_{n} ∈ C, the multiple abstract synchronization test has to satisfy

mtest(S′, c_{1}; …; c_{n}) = true ⇒ ∀σ ∈ γ(S′) . ∃i ∈ {1, …, n} . σ ⊢ c_{i}

The abstract semantics of a transformed program is computed by using Table 3 (instantiated over A) and by replacing the equation dealing with simple ask by the following

E′[[ ask(c_{1}; …; c_{n}) → A]]e = {a ∈ A | mtest(↓a, c_{1}; …; c_{n}) = true ⇒ a ∈ E′[[ A]]e}

Example 5. The producer pzaff sends messages to consumers cgiaco and clevi by using a single channel. For each input message, the distributor distr forwards the text to the appropriate output channel.

pzaff(X) :-
   ask(true) -> ∃ Y,M. tell(X=[msg(levi,M)|Y]) || write(M) || pzaff(Y)
      +
   ask(true) -> ∃ Y,M. tell(X=[msg(giaco,M)|Y]) || write(M) || pzaff(Y)
      +
   ask(true) -> tell(X=[]).
distr(X,L,G) :-
   ask(∃T,X1X=[msg(levi,T)|X1]) ->
      ∃ T,X1,L1. tell(X=[msg(levi,T)|X1],L=[T|L1]) || distr(X1,L1,G)
      +
   ask(∃T,X1X=[msg(giaco,T)|X1]) ->
      ∃ T,X1,G1. tell(X=[msg(giaco,T)|X1],G=[T|G1]) || distr(X1,L,G1)
      +
   ask(X=[]) -> tell(L=[],G=[]).
g(X,L,G) :- pzaff(X) || distr(X,L,G) || clevi(L) || cgiaco(G).

[figure: giaco; levi; OR; msg; Any; cons; nil; OR]

Fig. 1. The rigid typegraph for X

Assuming that write, clevi and cgiaco are suspension free, the suspension freeness of g(X,L,G) may only depend on pzaff and distr. By applying the Angel transformation, we note that the only process that can suspend is distr. Suspension freeness can be analyzed by evaluating the following multiple ask

   (∃T,X1X=[msg(levi,T)|X1]) ; ∃T,X1X=[msg(giaco,T)|X1]) ; X=[])

For this purpose, the rigid types abstraction [15] provides an adequate abstract domain. Intuitively, the process pzaff binds the variable X to any of the terms described by the rigid type graph in Figure 1. Therefore, we have to show that all such terms satisfy the synchronization test. In this case it is an easy task. However, in other cases it is necessary to extend the abstract domain of rigid types with some kind of variable dependency information (we are currently working on a formal solution for the general case).

Given P = D.A, let P′_{1}, P′_{2} be the abstract programs corresponding to P_{1} = NoSynch[P] and P_{2} = Angel[P] respectively. Next proposition states Angel correctness wrt the standard semantics, provided that we defined a correct multiple abstract synchronization test.

Proposition 18. N [[ P ]] ⊆ N [[ P_{2} ]] and (α̃ ∘ N [[ P ]] ∘ γ) ⊆ N′[[ P′_{2} ]].

If P is suspension-free, we can compare the accuracy of the two transformations, showing that NoSynch is always better than Angel.

Proposition 19. N [[ P_{1} ]] ⊆ N [[ P_{2} ]] and N′[[ P′_{1} ]] ⊆ N′[[ P′_{2} ]].

The two transformations have the same precision degree only when Angel can actually “prove” suspension-freeness.

7 Related Works

The initial approaches to the static analysis of concurrent logic languages are based on the operational semantics [4, 2]. In particular, in order to get independence from the scheduling policy, [2] analyze cc programs (with consistency check) by using a non-standard (operational) semantics that makes the computation confluent. Our program transformation Angel can be seen as the denotational translation of this approach (modulo the absence of the consistency check). To our knowledge, [8] defines the first abstract interpretation framework for cc programs based on a denotational (and compositional) semantics. Even in this case there is a two level approximation. The standard semantics is first abstracted by considering a semantics recording the input/output relation between concrete constraints, and then the constraint system is abstracted, by assuming the existence of a correct abstract synchronization test. Global choice operators are simply mapped into local choice operators. This is a heavy approximation, because one blocked guard causes the suspension of the process, even if there are other definitely enabled guards in the choice operator (e.g. in a deterministic choice we always suspend, because there can be only one enabled guard at a time).

[3] considers the problem of giving a generalized abstract interpretation framework for cc languages, where only local choice is allowed. In contrast with Theorem 11, they claim that it is correct to directly abstract the program and evaluating it on the abstract constraint system. However, simple counterexamples show that in general this approach returns uncorrect results because of the abstract synchronization problem.

A more recent paper [9] considers the analysis of compositionally confluent cc programs and defines an abstract interpretation framework which is very similar to that obtained by our transformation Angel. This approach, based on the denotational semantics of angelic cc, maps each (non-confluent) guarded choice operator into the agent ask( ∨_{i=1}^{n} c_{i}) → ⊕_{i=1}^{n} A_{i}, where ∨ denotes the disjunction

over P↓(C). The difference is that, once the synchronization test is passed, this transformation does not use the guard constraints to strength each branch of the computation. On the contrary, Angel tells each branch’s guard before proceeding in the abstract computation, obtaining better results.

8 Conclusions

We have shown that the ask operators cannot be safely upper approximated using the generalized semantics approach. The interest in a solution to this problem in the context of abstract interpretation is not only related to the analysis of cc programs. Indeed, the basic problem in the abstraction of synchronization for cc programs is shared by a number of different semantic constructions, not necessarily related with the ask-based synchronization of concurrent languages. As shown in [1], the semantics of (pure) Prolog programs (logic programs with depth-first search) can be specified in term of implicit ask mappings. A reduction with a clause can only be applied to a goal provided that there are no infinite branches on the left-hand side of the proof tree for that goal, by applying any of the previous clauses in the textual order. A similar behaviour is also shared by semantic models for builtins in Prolog. While the implicit ask mapping-based semantic definitions for Prolog’s search or builtins provide a more declarative model for control features in standard Prolog interpreters, their use as semantic bases for abstract interpretation may lead to some of the problems discussed in the previous sections. It is interesting to note that, in the case of Prolog depthfirst search, a NoSynch-like abstraction approximates the program meaning (the Prolog success set) by its interpretation as a pure logic program (i.e. without depth-first search). This, indeed, is a common practice in data-flow analysis of Prolog programs (a discussion on this topic is in [1]).

References

1. R. Barbuti, M. Codish, R. Giacobazzi, and G. Levi. Modelling Prolog Control. In Proc. Nineteenth Annual ACM Symp. on Principles of Programming Languages, pages 95–104. ACM Press, 1992.

2. M. Codish, M. Falaschi, K. Marriott, and W. Winsborough. Efficient Analysis of Concurrent Constraint Logic Programs. In A. Lingas, R. Karlsson, and S. Carlsson, editors, Proc. of the 20th International Colloquium on Automata, Languages, and Programming, volume 700 of Lecture Notes in Computer Science, pages 633–644, 1993.

3. C. Codognet and P. Codognet. A general semantics for Concurrent Constraint Languages and their Abstract Interpretation. In M. Meyer, editor, Workshop on Constraint Processing at the International Congress on Computer Systems and Applied Mathematics, CSAM’93, 1993.

4. C. Codognet, P. Codognet, and M. Corsini. Abstract Interpretation for Concurrent Logic Languages. In S. K. Debray and M. Hermenegildo, editors, Proc. North American Conf. on Logic Programming’90, pages 215–232. The MIT Press, Cambridge, Mass., 1990.

5. P. Cousot and R. Cousot. Systematic Design of Program Analysis Frameworks. In Proc. Sixth ACM Symp. Principles of Programming Languages, pages 269–282, 1979.

6. F. S. de Boer and C. Palamidessi. A Fully Abstract Model for Concurrent Constraint Programming. In S. Abramsky and T. Maibaum, editors, Proc. TAP-SOFT’91, volume 493 of Lecture Notes in Computer Science, pages 296–319. Springer-Verlag, Berlin, 1991.

7. F.S. de Boer, M. Gabbrielli, E. Marchiori, and C. Palamidessi. Proving Concurrent Constraint Programs Correct. In Proc. 21st Annual ACM Symp. on Principles of Programming Languages, pages 98–108. ACM Press, 1994.

8. M. Falaschi, M. Gabbrielli, K. Marriott, and C. Palamidessi. Compositional Analysis for Concurrent Constraint Programming. In Proceedings of the Eight Annual IEEE Symposium on Logic in Computer Science, pages 210–221. IEEE Computer Society Press, 1993.

9. M. Falaschi, M. Gabbrielli, K. Marriott, and C. Palamidessi. Confluence and Concurrent Constraint Programming. Technical report, Dipartimento di Elettronica e Informatica, University of Padova, 1993.

10. M. Falaschi, G. Levi, M. Martelli, and C. Palamidessi. Declarative Modeling of the Operational Behavior of Logic Languages. Theoretical Computer Science, 69(3):289–318, 1989.

11. R. Giacobazzi, S. K. Debray, and G. Levi. A Generalized Semantics for Constraint Logic Programs. In Proceedings of the International Conference on Fifth Generation Computer Systems 1992, pages 581–591, 1992.

12. R. Giacobazzi, G. Levi, and E. Zaffanella. Abstracting Synchronization in Concurrent Constraint Programming. Technical Report TR 25/93, Dip. di Informatica, Univ. di Pisa, 1993.

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

14. R. Jagadeesan, V. Shanbhogue, and V. Saraswat. Angelic non-determinism in concurrent constraint programming. Technical report, System Science Lab., Xerox PARC, 1991.

15. G. Janssens and M. Bruynooghe. Deriving descriptions of possible values of program variables by means of abstract interpretation. Journal of Logic Programming, 13(2 & 3):205–258, 1992.

16. V. A. Saraswat, M. Rinard, and P. Panangaden. Semantic Foundation of Concurrent Constraint Programming. In Proc. Eighteenth Annual ACM Symp. on Principles of Programming Languages, pages 333–353. ACM, 1991.

17. D. Scott. Domains for Denotational Semantics. In M. Nielsen and E. M. Schmidt, editors, Proc. ninth Int. Coll. on Automata, Languages and Programming, volume 140 of Lecture Notes in Computer Science, pages 577–613. Springer-Verlag, Berlin, 1982.

This article was processed using the LaTEX macro package with LLNCS style