Jonathan Passerat-Palmbach

Romain Reuillon

Claude Mazel

David R C Hill

Prototyping Parallel Simulations on Manycore Architectures Using Scala: A Case Study

Keywords: Parallelization of Simulation, Threads, OpenCL, Scala, Automatic Parallelization, GPU, Manycore

At the manycore era, every simulation practitioner can take advantage of the computing horsepower delivered by the available high performance computing devices. From multicore CPUs (Central Processing Unit) to thousand-thread GPUs (Graphics Processing Unit), several architectures are now able to offer great speed-ups to simulations. However, it is often tricky to harness them properly, and even more complicated to implement a few declinations of the same model to compare the parallelizations. Thus, simulation practitioners would mostly benefit of a simple way to evaluate the potential benefits of choosing one platform or another to parallelize their simulations. In this work, we study the ability of the Scala programming language to fulfill this need. We compare the features of two frameworks in this study: Scala Parallel Collections and ScalaCL. Both of them provide facilities to set up a data-parallelism approach on Scala collections. The capabilities of the two frameworks are benchmarked with three simulation models as well as a large set of parallel architectures. According to our results, these two Scala frameworks should be considered by the simulation community to quickly prototype parallel simulations, and choose the target platform on which investing in an optimized development will be rewarding.

Introduction

Simulations tend to become more and more accurate, but also more and more complex. In the same time, manycore architectures and hardware accelerators are now widespread and allow great speedups to applications that can be parallelized in a way to take advantage of their overwhelming power. Anyway, several problems arise when one is trying to parallelize a simulation. First, you need to decide which hardware accelerator will best fit your application, second, you must master its architecture's characteristics, and last but not least, you need to choose the programming language and Application Programming Interface (API) that will best suit this particular hardware.

Depending on their underlying models and algorithms, simulations will display greater speedups when parallelized on some architectures than others. For example, model relying on cellular automata algorithms are likely to scale smoothly on GPU devices or any other vector architecture [START_REF] Caux | Accelerating 3d cellular automata computation with gp-gpu in the context of integrative biology[END_REF]; [START_REF] Topa | Gpgpu implementation of cellular automata model of water flow[END_REF].

The problem is sometimes, scientists champion a given architecture without trying to evaluate the potential benefits their applications could gain from other architectures. This can result in disappointing performances from the new parallel application and a speed-up far from the original expectations. Such hasty decisions can also lead to wrong conclusions where an underexploited architecture would display worse performance than the chosen one [START_REF] Lee | Debunking the 100x gpu vs. cpu myth: an evaluation of throughput computing on cpu and gpu[END_REF]. One of the main examples of this circle of influence are GPUs, which have been at the heart of many publications for the last 5 years. Parallel applications using this kind of platform are often proved relevant by comparing them to their sequential counterparts. Now, the question is: is it fair to compare the performances of an optimized GPU application to those of a single CPU core? Wouldn't we obtain far better performances trying to make the most of all the cores of a modern CPU?

On the other hand, many platforms are available today, and in view of the time and workload involved in the development of a parallel application for a given architecture, it is nearly impossible to invest much human resources in building several prototypes to determine which architecture will best support an application. As a matter of fact, parallel developers need programming facilities to help them build a reasonable set of parallel prototypes targeting a different parallel platform each.

This proposition implies that developers master many parallel programming technologies if they want to be able to develop a set of prototypes. Thus, programming facilities must also help them to factor their codes as much as possible. The ideal paradigm in this case is Write Once, Run Anywhere, that suggests different parallel platforms understand the same binaries. To do so, a standard called OpenCL (Open Computing Language) was proposed by the Khronos group Khronos OpenCL Working Group (2011). OpenCL aims at unifying developments on various kinds of architectures like CPUs, GPUs and even FPGAs. It provides programming constructs based upon C99 to express the actual parallel code (called the kernel). They are enhanced by APIs (Application Programming Interface) used to control the device and the execution. OpenCL programs execution relies on specific drivers issued by the manufacturer of the hardware they run on. The point is OpenCL kernels are not compiled with the rest of the application, but on the fly at runtime. This allows specific tuning of the binary for the current platform.

OpenCL solves the aforementioned obstacles: as a cross-platform standard, it allows developing simulations once and for all for any supported architecture. It is also a great abstraction layer that lets clients concentrate on the parallelization of their algorithm, and leave the device specific mechanics to the driver. Still, OpenCL is not a silver bullet; designing parallel applications might still appear complicated to scientists from many domains. Indeed, OpenCL development can be a real hindrance to parallelization. We need high-level programming APIs to hide this complexity to scientists, while being able to automatically generate OpenCL kernels and initializations.

Another widespread cross-platform tool is Java and especially its virtual machine execution platform. The latter makes of Java-enabled solutions a perfect match for our needs, since any Java-based development is Write Once, Run Anywhere. Although the Java Virtual Machine (JVM) tends to become more and more efficient, the Java language itself evolves slower and several new languages running on top of the JVM appeared during the last few years, including Clojure, Groovy and Scala. These languages reduce code bloating and offer solutions to better handle concurrency and parallelism. Among JVM based languages, we have chosen to focus on Scala in this study because of its hybrid aspect: mixing both functional and object oriented paradigms. By doing so, Scala allows object-oriented developers to gently migrate to powerful functional constructs. Meanwhile, functional programming copes very well with parallelism due to its immutability principles. Having immutable objects and collections highly simplifies parallel source code since no synchronization mechanism is required when accessing the original data. As many other functional languages such as Haskell, F# or Erlang, Scala has leveraged these aspects to provide transparent parallelization facilities. In the standard library, these parallelization facilities use system threads and are limited to CPU parallelism. In the same time, the ScalaCL library generates OpenCL code at compile-time and produces OpenCL-enabled binaries from pure Scala code. Consequently, it is easier to generate automatically parallelized functional programming constructs.

To sum up, OpenCL and Scala both appear like relevant tools to quickly build a various set of parallel prototypes for a given application. This study therefore benchmarks solutions where one or the two of the these technologies were used to build prototypes of parallel simulations on manycore CPU and GPU architectures. We concentrate on simulations that can benefit from data-parallelism in this study. As a matter of fact, the tools that we have chosen are designed to deal with this kind of parallelism, as opposed to task-parallelism. We intend to show that prototypes harnessing Scala's automatic parallelization frameworks display the same trend in terms of speed-up than handcrafted parallel implementations. To do so, we will:

• Introduce Scala frameworks providing automatic parallelization facilities;

• Present the models at the heart of the study and their properties;

• Discuss the results of our benchmark when faced with a representative selection of parallel platforms;

• Show the relevancy of using Scala to quickly build parallel prototypes prior to any technological choice.

Automatic Parallelization with Scala

2.1 Why is Scala a good candidate for parallelization of simulations?

Many attempts to generate parallel code from sequential constructs can be found in the literature.

For the sole case of GPU programming with CUDA (Compute Unified Device Architecture), a programming paradigm developed by NVIDIA that specifically runs on this manufacturer's hardware, we can cite great tools like HMPP Dolbeau et al. (2007), FCUDA Papakonstantinou et al. (2009) andPar4all Amini et al. (2011). Other studies [START_REF] Karimi | A performance comparison of cuda and opencl[END_REF], as well as our own experience, show that CUDA displays far better performance on NVIDIA boards than OpenCL, since it is precisely optimized by NVIDIA for their devices. However, automatically generated CUDA cannot benefit of the same tuning quality. That is why we rather consider OpenCL code generation instead of CUDA. The former having been designed as a cross-platform technology, it is consequently better suited for generic and automatic code production. First of all, let us make a brief recall on what is Scala. Scala is a programming language mixing two paradigms: object oriented and functional programming. Its main feature is that it runs on top of the Java Virtual Machine (JVM). In our case, it means that Scala developments can interoperate like clockwork with Java, thus allowing the wide range of simulations developed in Java to integrate Scala parts without being modified.

The second asset of Scala is its compiler. In fact, Scalac (for Scala Compiler) offers the possibility to enhance its behavior through plugins. ScalaCL, which we will study later in this section, uses a compiler plugin to transform Scala code to OpenCL at compile time. This mechanism offers great opportunities to generate code and the OpenCL proposal studied in this work is just a concrete example of what can be achieved when extending the Scala compiler.

Finally, Scala presents a collection framework that intrinsically facilitates parallelization. As a matter of fact, Scala default collections are immutable: every time a function is applied to an immutable collection, this one remains unchanged and the result is a modified copy returned by the function. On the other hand, mutable collections are also available when explicitly summoned, albeit the Scala specification does not ensure any thread-safe access on these collections. Such an approach appears to be very interesting and efficient, when trying to parallelize an application, since no lock mechanisms are involved anymore. Thus, concurrent accesses to the collection elements are not a problem anymore as long as they are read-only accesses that don't introduce any overhead. It is a classical functional programming pattern to issue a new collection as the result of applying a function to an initial immutable collection. Although this procedure might appear costly, works have been done to optimize the way it is handled, and efficient implementations do not copy the entire immutable collection Okasaki (1999).

Scala Parallel Collections

Scala 2.9 release introduced a new set of Parallel collections mirroring the classical ones. They have been described in [START_REF] Prokopec | A generic parallel collection framework[END_REF]. These parallel collections offer the same methods than their sequential equivalents, but the method execution will be automatically parallelized by a framework implementing a divide and conquer algorithm.

The point is they integrate seamlessly in already existing source codes because the parallel operations have the same names as their sequential variants. As the parallel operations are implemented in separate classes they can be invoked if their data are in a parallel collection class. This is made possible thanks to a par method that returns a parallel equivalent of the sequential implementation of the collection still pointing to the same data. Any subsequent operation invoked by an instance of the collection will benefit of a parallel execution without any other add from the client. Instead of applying the selected operation to each member of the collection sequentially, it is applied on each element in parallel. Such a function is referred to as closure in functional programming jargon. It commonly designates an anonymous function embedded in the body of another function. A closure can also access the variables from the calling host function.

Scala Parallel Collections rely on the Fork/Join framework proposed by Doug [START_REF] Lea | A java fork/join framework[END_REF]. This framework was released with the latest Java 7 SDK. It is based upon the divide and conquer paradigm. Fork/Join introduces the notion of tasks, which is basically a unit of work to be performed. Tasks are then assigned to worker threads waiting in a sleeping state in a Thread Pool. The pool of worker threads is created once and only once when the framework is initialized. Thus, creating a new task does not suffer of thread creation and initialization that could, depending on the task content, be slower than processing the task itself.

Fork/Join is implemented using work stealing. This adaptive scheduling technique offers efficient load balancing features to the Java framework, provided that work is split into tasks of a small enough granularity. Tasks are assigned to workers' queues, but when a worker is idle, it can steal tasks from another worker's queue, which helps achieve the whole computation faster. Scala Parallel Collections implement an exponential task splitting technique detailed in [START_REF] Cong | Solving large, irregular graph problems using adaptive work-stealing[END_REF] to determine the ideal task granularity.

ScalaCL

ScalaCL is a project, part of the free and open-source Nativelibs4java initiative, led by Olivier Chafik. The Nativelibs4java project is an ambitious bundle of libraries trying to allow users to take advantage of various native binaries in a Java environment.

From ScalaCL itself, two projects have recently emerged. The first one is named Scalaxy. It is a plugin for the Scala compiler that intends to optimize Scala code at compile time. Indeed, Scala functional constructs might run slower than their classical Java equivalents. Scalaxy deals with this problem by pre-processing Scala code to replace some constructs by more efficient ones. Basically, this plugin intends to transform Scala's loop-like calls such as map or foreach by their while loops equivalents. The main advantage of this tool is that it is applicable to any Scala code, without relying on any hardware.

The second element resulting of this fork is the ScalaCL collections. It consists in a set of collections that support a restricted amount of Scala functions. However, these functions can be mapped at compile time to their OpenCL equivalents. Up to version 0.2, a compiler plugin dedicated to OpenCL generation was called at compile time to normalize the code of the closure applied to the collection. Version 0.3, the current one, has led to a whole rewriting of the library. ScalaCL now leverages the Scala macros system, introduced in the 2.10 release of the Scala language. Thanks to macros, ScalaCL modifies the program's syntax tree during the compilation to provide transparent parallelization to manycore architectures from high level functional constructs. In both cases, the resulting source is then converted to an OpenCL kernel. At runtime, another part of ScalaCL comes into play, since the rest of the OpenCL code, like the initializations, are coupled to the previously generated kernel to form the whole parallel application. The body of the closure will be computed by an OpenCL Processing Element (PE), which can be a thread or a core depending on the host where the program is being run.

The two parallelization approaches introduced in this section are compared in Figure 1.

Case study: three different simulation models

In this section, we will show how parallel Scala implementations of three different simulation models are close to the sequential Scala implementation. We compare sequential Scala code with its parallel declinations using Scala, and put the light on the automatic aspect of the two studied approaches, which respective source codes remain very close to the genuine. Our benchmark consists in running several iterations of the automatically parallelized models, and to compare them with handcrafted parallel implementations.

The three models used in the benchmark were carefully chosen so that they remain simple to describe, while being representative of several main modeling methods. They are: the Ising Model [START_REF] Ising | Beitrag zur theorie des ferromagnetismus[END_REF], a forest Gap Model Passerat-Palmbach et al. ( 2012) and the Schelling's segregation model [START_REF] Schelling | Dynamic models of segregation[END_REF], and will be described more thoroughly in this section. Three categories are considered to classify the models: Table 1: Summary of the studied models' characteristics

• Is the model stepwise or agent-based?

• Does the model outputs depend on stochasticity?

• Is the model performing more computations or data accesses?

Let us sum the characteristics of our three models according to the three aforementioned categories in Table 1.

The case of Discrete Event Simulations (DES)

Discrete-event based models do not cope well with data-parallelism approaches. In fact, they are more likely to fit a task parallel framework. For instance, Odersky et al. introduce a discrete-event model of a circuit in [START_REF] Odersky | Programming in Scala[END_REF]. The purpose of this model is to design and implement a simulator for digital circuits. Such a model is the perfect example of the difficulty to take advantage of parallel collections implementations when the problem is not suited. Indeed, this parallel discrete-event model implies communications to broadcast the events. Furthermore, events lead the order in which task are executed, whereas data-parallel techniques rely on independent computations. Task parallelism approaches are not considered in this work, but Scala also provides ways to easily parallelize such problems through the Scala Actors framework [START_REF] Haller | Scala actors: Unifying thread-based and event-based programming[END_REF]. The interested reader can find further details on the task-parallel implementation of the previously mentioned digital circuit model using Actors in [START_REF] Odersky | Programming in Scala[END_REF].

Models description

Ising models

The Ising model is a mathematical model representing ferromagnetism in statistical physics [START_REF] Ising | Beitrag zur theorie des ferromagnetismus[END_REF]. Basically, Ising models deal with a lattice of points, each point holding a spin value, which is a quantum property of physical particles. At each step of the stochastic simulation process and for every spin of the lattice, the algorithms determines whether it has to be flipped or not.

The decision to flip or not the spin of a point in the lattice is taken in view of two criteria. The first is the value of the spins belonging to the Von Neumann neighborhood of the current point, and the second is a random process called the Metropolis criterion.

Ising models have been studied in many dimensions, but for the purpose of this study, we consider a 2D toric lattice, solved using the Metropolis algorithm [START_REF] Metropolis | Equation of state calculations by fast computing machines[END_REF].

Forest Gap Model

The second model on which we apply automatic parallelization techniques is a Forest Gap Model described in [START_REF] Passerat-Palmbach | Automatic parallelization of a gap model using java and opencl[END_REF]. It depicts the dynamics of trees spawning and falling in a French Guiana rainforest area. The purpose of this model is to serve as a basis for a future agent-based model rendering the settling of ant nests in the area, depending on the trees and gaps locations. At each simulation step, a random number of trees will fall, carrying a random numbers of their neighbors in their fall. In the same time, new trees are spawning in the gaps area to repopulate them.

Here, we focus on the bottleneck of the model: a method called several times at each simulation step that represents about 70% of the whole execution time. Although the whole model is stochastic, the part we consider in this work is purely computational. The idea is to figure out the boundaries of the gaps in the forest. The map is a matrix of boolean wherein cells carrying a true value represents parts of gaps, while any other cell carries a false value. According to the value of its neighbors, a cell can determine whether it is part of a gap boundary or not.

Schelling's Segregation Model

The dynamic models of segregation of Schelling [START_REF] Schelling | Dynamic models of segregation[END_REF] is a specialized individual based model that simulates the dynamic of two populations of distinct colors. Each individual wants to live in an area where at least a certain ratio of individuals of the same color as his own are living. Individuals that are unhappy with their neighborhood move at random to another part of the map. This model converges toward a space segregated by colors with huge clusters of individual of the same color.

At the heart of the segregation model is all the decisions taken by the individuals to move from their place to another. As long as this is the most computation intensive part of the segregation model, we will concentrate our parallelization efforts on this part of the algorithm. Furthermore, it presents a naturally parallel aspect since individuals decide whether they feel the need to move independently from each other.

Scala implementations

In this section we will focus on the implementation details of the Ising model. The other implementations would not bring more precisions concerning the use of the two Scala parallelization frameworks studied in this work.

Our Scala implementation of the Ising model represents the spin lattice by an IndexedSeq. IndexedSeq is a trait, i.e. an enhanced interface in the sense of Java that also allows methods definition; it abstracts all sorts of indexed sequences. Indexed sequences are collections that have a defined order of elements and provide efficient random access to the elements. It bears operations on this collection such as applying a given function to every element of the collection (map) or applying a binary operator on a collection, going through elements from left or right (foldLeft, foldRight). These operations are sufficient to express most of the algorithms. Moreover, they can be combined since they build and return a new collection containing the new values of the elements.

For instance, computing the magnetization of the whole lattice consists in applying a foldLeft on the IndexSeq to sum the values corresponding to the spin of the elements. Indeed, our lattice is a set of tuples contained in the IndexedSeq. Each tuple stores its coordinates in the 2D-lattice in order to easily build its Von Neumann neighborhood, and a boolean indicating the spin of the element (false is a negative spin, whereas true stands for a positive spin).

To harness parallel architectures, we need to slightly rewrite this algorithm. The initial version consists in trying to flip the spin of a single point of the lattice at each step. This action is considered as a transformation between two configurations of the lattice. However, each point can be treated in parallel, provided that its neighbors are not updated at the same time. Therefore, the points cannot be chosen at random anymore, this would necessarily lead to a biased configuration A way to avoid this problem is to separate the lattice in two halves that will be processed sequentially. This technique is commonly referred to as the "checkerboard algorithm" [START_REF] Preis | Gpu accelerated monte carlo simulation of the 2d and 3d ising model[END_REF]. In fact, the Von Neumann neighborhood of a point located on what will be considered a white square, will only be formed by points located on black squares, and vice versa. The whole lattice is then processed in two times to obtain a result equivalent to the sequential process. The process is summed up in Figure 2.

The implementation lies in applying an operation to update each spin through two successive map invocations on the two-halves of the lattice. Not only this approach is crystal clear for the reader, but also it is quite easy to parallelize. Indeed, map can directly interact with the two Scala automatic parallelization frameworks presented earlier: Scala Parallel Collections and ScalaCL. Let us describe how the parallelization APIs integrate smoothly in already written Scala code with a concrete example.

Listing 1 is a snippet of our Ising model implementation in charge of updating the whole lattice in a sequential fashion:

1 def processLattice(_lattice: Lattice)(implicit rng: Random) = 2 3 new Lattice { 4
val size = _lattice.size 5 val lattice = 6

IndexedSeq.concat ( 7 _lattice.filter{case((x, y), _) => isEven(x, y)}.map(spin => processSpin( _lattice, spin)), 8 _lattice.filter{case((x, y), _) => isOdd(x, y)}.map(spin => processSpin( _lattice, spin)) 9) Scala enables us to write both concise and expressive code, while keeping the most important parts of the algorithm exposed. Here, the two calls to map aiming at updating each half of the lattice can be noticed, they will process in turn all the elements within the subset they have received in input. This snippet suggests an obvious parallelization of this process thanks to the par method invocation. This call automatically provides the parallel equivalent of the collection, where all the elements will be treated in parallel by the mapped closure that processes the energy of the spins. The resulting code differs only by the extra call to the par method upstream of the map action, so as Listing 2 shows: An equivalent parallelization using ScalaCL is obtained just by replacing the par method by the cl one from the ScalaCL framework, thus enabling the code to run on GPUs.

1
As automatic parallelization applies on determined parts of the initial code, the percentage of the sequential execution time affected by the parallel declinations can be computed through a profiler. Thanks to this tool, we were able to determine the theoretical benefits of attempting to parallelize part of a given model. These figures are presented in Table 2, along with the intrinsic parameters at the heart of each model implementation. For more details about the purpose of these parameters, the interested reader can refer to the respective papers introducing each model thoroughly.

Results

In this section, we will study how the different models implementations behaved when run on a set of different architectures. All the platforms that were used in the benchmark are listed hereafter:

• 2-CPU 8-core Intel Xeon E5630 (Westmere architecture) running at 2.53GHz with ECCmemory enabled

• 8-CPU 8-core Intel Xeon E7-8837 running at 2.67GHz

• 4-core 2-thread Intel i7-2600K running at 3.40GHz

• NVIDIA GeForce GTX 580 (Fermi architecture)

• NVIDIA Tesla C2075 (Fermi architecture)

• NVIDIA Tesla K20 (Kepler architecture)

We compare a sequential Scala implementation executed on a single core of the Intel Xeon E5630 with its Scala Parallel Collections and ScalaCL declinations executed on all the platforms. Each model had to process the same input configurations for this benchmark. Measures resulting from these runs are displayed in Table 3. Unfortunately, at the time of writing ScalaCL is not able to translate an application as complex as Schelling's segregation model to OpenCL yet. In the meantime, while ScalaCL managed to produce OpenCL versions of the Gap Model and the Ising Model, these two declinations were killed by the system before being able to complete their execution.

Not only this last result show that the automatic prototypes approach gives significant results, when using Scala Parallel Collections, but this also validates the relevancy of the whole approach when considering the characteristics of the involved simulation model. In Table 1, the Forest Gap Model had been stated as a model performing more data accesses than computations. Thus, it is logical than a parallelization attempt on GPU suffers from the latency related to memory accesses on this kind of architecture. Indeed GPUs can only be fully exploited by applications with a high computational workload. Here, the OpenCL declination performs slightly faster than the sequential one (1.11X), but it is the perfect case of the unsuited architecture choice that leads to disappointing performance, as exposed in Introduction.

Automatically built parallel prototypes quickly put the light on this weakness, and avoid wasting time to develop a GPU implementation that would be less efficient than the parallel CPU version.

In the same way, we can see from Table 3 that the number of available cores is not the only thing to consider when selecting a target platform. Depending on the characteristics of the model, which are summed up in Table 1, parallel prototypes behave differently when faced to manycore architectures they cannot fully exploit due to frequent memory accesses. The perfect example of this trend is the results obtained when running the models on the Xeon E5630, ECCenabled host. As fast as it can be, this CPU-based host is significantly slowed down by its ECC memory. Indeed, ECC is known to impact execution times of about 20%.

Conclusion

In this work we have benchmarked two Scala proposals aiming at automatically parallelizing applications and their ability to help simulation practitioners to figure out the best target platform to parallelize their simulation on. The two frameworks have been detailed and compared: Scala parallel collections that automatically creates tasks, and execute them in parallel thanks to a pool of worker threads; ScalaCL, part of the nativelibs4java project, which intends to produce OpenCL code from Scala closures, and to run it on the most efficient device available, be it GPU or multicore CPU.

Our study has stated that ScalaCL is still in its infancy and can only translate a limited set of Scala constructs to OpenCL at the time of writing. Although it is not able to produce a parallel prototype for a simulation yet, it deserves to be regarded as a future great language extension if it manages to improve its reliability. For its part, Scala Parallel Collections is a really satisfying framework that mixes ease of use and efficiency.

Considering data-parallel simulations, this works shows how simulation practitioners can easily determine the best parallel platform on which to concentrate their development efforts. Especially, this study puts forward the inefficiency of some architectures, in our case GPUs, when faced with problems they were not designed to process initially. In the literature, some architectures have often been favored because of their cutting-edge characteristics. However, they might not be the best solution to retain and other solutions might be underrated [START_REF] Lee | Debunking the 100x gpu vs. cpu myth: an evaluation of throughput computing on cpu and gpu[END_REF]. Thus, being able to quickly benchmark several architectures without further code rewriting is a great decision support tool. Such an approach is very important when speed-up matters to make sure that the underlying architecture is the most suited to fasten the problem.

In the future, we plan to propose metrics to set out the benefits of automatically built prototypes using Scala compared to handcrafted ones when considering the human resources involved and the development time. In this way, we will evaluate the possibilities to take part to the development of ScalaCL, to shorten the gap between this tool and the Scala Parallel Collections.

Figure 1 :

 1 Figure 1: Schema showing the similarities between the two approaches: Scala Parallel Collections spreads the workload among CPU threads (T), while ScalaCL spreads it among OpenCL Processing Elements (PEs) Stepwise/Agent-based Stochastic Computational/Data Ising Stepwise Yes Computational Gap Model Stepwise No Data Schelling Agent-based Yes Data

Figure 2 :

 2 Figure 2: Lattice updated in two times following a checkerboard approach

Table 2 :

 2 Characteristics of the three studied models

	1 def processLattice(_lattice: Lattice)(implicit rng: Random) =
	2
	3 new Lattice {
	4	val size = _lattice.size
	5	val lattice =
	6	IndexedSeq.concat (
	7	_lattice.filter{case((x, y), _) => isEven(x, y)}.par.map(spin =>
		processSpin(_lattice, spin)),
	8	_lattice.filter{case((x, y), _) => isOdd(x, y)}.par.map(spin =>
		processSpin(_lattice, spin))
	9	)
	10 }
	Listing 2: Parallel version of method processLattice from class IsingModel, using Scala Parallel
	Collections

As a consequence, we are not able to provide any result about a ScalaCL implementation of these models. This leads to the first result of this work: at the time of writing, ScalaCL cannot be used to build parallel prototypes of simulations on GPU. It is just a proof of concept that Scala closures can be transformed to OpenCL code, but it is not reliable enough to achieve such transformations on real simulation codes yet.

On the other hand, the Scala Parallel Collection API succeeded to build a parallel declination of the three benchmarked models. These declinations have successfully run on the CPU architectures retained in the benchmark, and have shown a potential performance gain when parallelizing the 3 studied models.

Let us validate this trend by now comparing handcrafted implementations on CPU and GPU. For the sake of brevity, we will focus on the Forest Gap Model, which Scala Parallel Collections implementation runs twice as fast as the sequential implementation on the Intel i7, according to Table 3. The CPU declination uses a Java Thread Pool, whereas the GPU is leveraged using OpenCL. Figure 3 shows the speed-ups obtained with the different parallelizations of the Forest Gap Model. 3 show that an handcrafted parallelization on CPU follows the trend of the parallel prototype in terms of performance gain. In view of the lower speed-up obtained on GPU using an OpenCL implementation, it is likely that a automatically built GPU-enabled prototype would have displayed worse performance than its CPU counterpart.


Luis F Pino

Filippo Bonchi

Frank D Valencia

A Behavioral Congruence for Concurrent Constraint Programming with Nondeterministic Choice ⋆

Concurrent constraint programming (ccp) is a well-established model of concurrency for reasoning about systems of multiple agents that interact with each other by posting and querying partial information on a shared space. (Weak) bisimilarity is one of the most representative notions of behavioral equivalence for models of concurrency. A notion of weak bisimilarity, called weak saturated bisimilarity ( ≈sb ), was recently proposed for ccp. This equivalence improves on previous bisimilarity notions for ccp that were too discriminating and it is a congruence for the choice-free fragment of ccp. In this paper, however, we show that ≈sb is not a congruence for ccp with nondeterministic choice. We then introduce a new notion of bisimilarity, called weak full bisimilarity (≈ f ), and show that it is a congruence for the full language of ccp. We also show the adequacy of ≈ f by establishing that it coincides with the congruence induced by closing ≈sb under all contexts. The advantage of the new definition is that, unlike the congruence induced by ≈sb , it does not require quantifying over infinitely many contexts.

Introduction

The Context. Concurrency theory studies the description and the analysis of systems made of interacting processes. Processes are typically viewed as infinite objects, in the sense that they can produce arbitrary and possibly endless interactions with their environment. Process calculi treat these processes much like the λ-calculus treats computable functions. They provide a formal language in which processes are represented by terms, and a set of rewriting rules to represent process evolution (or transitions). For example, the term P Q represents the process that results from the parallel composition of the processes P and Q. A (labeled) transition P α -→ P ′ represents the evolution of P into P ′ given an interaction α with the environment.

Concurrent Constraint Programming (ccp) [START_REF] Saraswat | Concurrent constraint programming[END_REF][START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] is a well-established formalism that combines the traditional algebraic and operational view of process calculi with a declarative one based upon first-order logic. Ccp processes can then be seen as computing agents as well as first-order logic formulae. In ccp, processes interact asynchronously by posting (or telling) and querying (or asking) information, traditionally referred to as constraints, in a shared-medium referred to as the store. Furthermore, ccp is parametric in a constraint system indicating interdependencies (entailment) between constraints and providing for the specification of data types and other rich structures. The above features have recently attracted a renewed attention as witnessed by the works [START_REF] Palamidessi | On the expressiveness of linearity vs persistence in the asychronous pi-calculus[END_REF][START_REF] Buscemi | Open bisimulation for the concurrent constraint picalculus[END_REF][START_REF] Bengtson | Psi-calculi: Mobile processes, nominal data, and logic[END_REF][START_REF] Bartoletti | A calculus of contracting processes[END_REF] on calculi exhibiting data-types, logic assertions as well as tell and ask operations. More recently in [START_REF] Knight | Spatial and epistemic modalities in constraint-based process calculi[END_REF] the authors proposed the post and ask interaction model of ccp as an abstraction of social networks.

In any computational model of processes, a central notion is that of behavioral equivalences [START_REF] Nicola | Behavioral equivalences[END_REF]. These equivalences determine what processes are deemed indistinguishable and they are expected to be congruences. The congruence issue is of great importance for algebraic and compositional reasoning: If two processes are equivalent, one should be able to replace one with the other in any context and preserve the equivalence (see e.g, [START_REF] Fokkink | Is timed branching bisimilarity a congruence indeed?[END_REF]). For example, if ⊲⊳ is a behavioral congruence, then P ⊲⊳ Q should imply P R ⊲⊳ Q R.

Reasoning on processes and their equalities therefore means dealing with, and comparing, infinite structures. For this, a widely used mathematical tool is coinduction (see e.g. [START_REF] Arbab | A coinductive calculus of component connectors[END_REF]). Coinduction is the dual of induction; while induction is a pervasive tool to reason about finite and stratified structures, coinduction offers similar strengths on structures that are circular or infinite. The most widely applied coinductive concept is bisimulation: bisimilarity is used to study behavioral equivalences, and the bisimulation proof method is used to prove such equivalences. In fact, most process calculi are equipped with a notion of bisimilarity.

The Problem. There have been few attempts to define notions of bisimilarity equivalence for ccp processes. These equivalences are, however, not completely satisfactory: As shown in [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF], the one in [START_REF] Saraswat | Concurrent constraint programming[END_REF] is too fine grained; i.e. it may tell apart processes whose logic interpretation is identical. The one in [START_REF] Mendler | A logical view of concurrent constraint programming[END_REF] quantifies over all possible inputs from the environment, and hence it is not clear whether it can lead to a feasible proof technique. The notion introduced in [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF], called (weak) saturated barbed bisimilarity ( ≈sb ), solves the above-mentioned issues and it is a congruence for ccp without nondeterministic choice. Unfortunately, as we will show in this paper, it is not a congruence for the full language of ccp. In particular, in ccp with nondeterministic choice, P ≈sb Q does not imply P R ≈sb Q R.

The goal of this paper is therefore to provide ccp with an adequate behavioral congruence based on the bisimulation proof method.

Our Approach. We build on a result of [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF] showing that ≈sb can be characterized by a novel bisimulation game (called, for simplicity, weak bisimulation) which relies at the same time on both barbs and labeled transitions. Barbs are basically predicates on the states, processes or configuration stating the observation we can make of them. This is rather peculiar with respect to the existing notions of bisimulations introduced for other process calculi where one usually exploits labeled transitions to avoid thinking about barbs and contexts. Indeed, labeled transitions usually capture barbs, in the sense that a state exposes a certain barb if and only if it performs a transition with a certain label. This is not the case of ccp, where barbs are observations on the store, while labeled transitions are determined by the processes. A more abstract understanding of this peculiarity of ccp can be given within the framework of [START_REF] Bonchi | Towards a general theory of barbs, contexts and labels[END_REF] which is an extension of [START_REF] Leifer | Deriving bisimulation congruences for reactive systems[END_REF] featuring barbs and weak semantics.

As it is customary for weak barbed equivalences, in our weak bisimulation game whenever a player exposes a barb ↓ e , the opponent should expose the weak barb ⇓ e , i.e. it should be able to reach a state satisfying ↓ e , but then the game restarts from the original state ignoring the arriving state. One of our contributions is to show that for ccp the arriving state cannot be ignored.

Our Contributions. In this work, we prove that ≈sb is a congruence for ccp without nondeterministic choice but not for the full language of ccp. We then propose a new notion of bisimilarity, called (weak) full bisimilarity (≈ f ). We show that ≈ f is a congruence for the full language of ccp. We also show the adequacy of the new notion by establishing that it is the largest congruence included in ≈sb . In other words ≈ f coincides with the congruence induced by closing ≈sb under all contexts. Beyond being a congruence, the advantage of ≈ f is that it does not require quantifying over infinitely many contexts. This is also important as it may simplify decision procedures for the equivalence. To the best of our knowledge, this is the first behavioral equivalence, which does not appeal to quantification over arbitrary process contexts in its definition, that is a congruence for ccp with nondeterministic choice.

A technical report with detailed proofs of this paper can be found in [START_REF] Pino | A behavioral congruence for concurrent constraint programming with nondeterministic choice (extended version)[END_REF].

Structure of the paper. The paper is organized as follows: In Section 2 we recall the ccp formalism. In Section 3 we introduce the standard notion of observational equivalence (∼ o ) for ccp (from [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]), we then show its relation with the weak saturated barbed bisimilarity ( ≈sb ) (from [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF]) for ccp with nondeterministic choice. We also prove that ≈sb is not a congruence for the full ccp. In Section 4 we introduce our new notion ≈ f , and we prove that (i) ≈ f coincides with ≈sb in the choice-free fragment of ccp; (ii) ≈ f is a congruence for ccp with summation; and (iii) ≈ f coincides with the equivalence obtained after closing ≈sb under any context. In Section 5 we present our conclusions and future work.

Background

We begin this section by recalling the notion of constraint system. We then present the concurrent constraint programming (ccp) formalism.

Constraint Systems

The ccp model is parametric in a constraint system (cs) specifying the structure and interdependencies of the information that processes can ask or and add to a central shared store. This information is represented as assertions traditionally called constraints. Following [START_REF] De Boer | Nondeterminism and infinite computations in constraint programming[END_REF][START_REF] Mendler | A logical view of concurrent constraint programming[END_REF] we regard a cs as a complete algebraic lattice in which the ordering ⊑ is the reverse of an entailment relation: c ⊑ d means d entails c, i.e., d contains "more information" than c. The top element false represents inconsistency, the bottom element true is the empty constraint, and the least upper bound ⊔ is the join of information.

Definition 1 (Constraint Systems). A constraint system (cs) C is a complete algebraic lattice (Con, Con 0 , ⊑, ⊔, true, false) where Con, the set of constraints, is a partially ordered set w.r.t. ⊑, Con 0 is the subset of compact elements of Con, ⊔ is the lub operation defined on all subsets, and true, false are the least and greatest elements of Con, respectively.

Recall that C is a complete lattice if every subset of Con has a least upper bound in Con. An element c ∈ Con is compact if for any directed subset D of Con, c ⊑ D implies c ⊑ d for some d ∈ D. C is algebraic if each element c ∈ Con is the least upper bound of the compact elements below c.

In order to model hiding of local variables and parameter passing, in [START_REF] Saraswat | Concurrent constraint programming[END_REF][START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] the notion of constraint system is enriched with cylindrification operators and diagonal elements, concepts borrowed from the theory of cylindric algebras [START_REF] Monk | Cylindric Algebras (Part I)[END_REF].

Let us consider a (denumerable) set of variables Var with typical elements x, y, z, . . . and let us define ∃ Var as the family of operators ∃ Var = {∃ x | x ∈ Var } (cylindric operators) and D Var as the set D Var = {d xy | x, y ∈ Var } (diagonal elements).

A cylindric constraint system over a set of variables Var is a constraint system whose underlying support set Con ⊇ D Var is closed under the cylindric operators ∃ Var and quotiented by Axioms C1 -C4, and whose ordering ⊑ satisfies Axioms C5 -C7:

C1. ∃x∃yc = ∃y∃xc C2. dxx = true C3. if z = x, y then dxy = ∃z(dxz ⊔ dzy) C4. ∃x(c ⊔ ∃xd) = ∃xc ⊔ ∃xd C5. ∃xc ⊑ c C6. if c ⊑ d then ∃xc ⊑ ∃xd C7. if x = y then c ⊑ dxy ⊔ ∃x(c ⊔ dxy)
where c and d indicate compact constraints, and ∃ x c ⊔ d stands for (∃ x c) ⊔ d. For our purposes, it is enough to think the operator ∃ x as existential quantifier and the constraint d xy as the equality x = y.

Cylindrification and diagonal elements allow us to model the variable renaming of a formula φ; in fact, by the aforementioned axioms, we have that the formula ∃ x (d xy ⊔ φ) can be depicted as the formula φ[y/x], i.e., the formula obtained from φ by replacing all free occurrences of x by y.

We assume notions of free variable and of substitution that satisfy the following conditions, where c[y/x] is the constraint obtained by substituting x by y in c and fv (c) is the set of free variables of c:

(1) if y / ∈ fv (c) then (c[y/x])[x/y] = c; (2) (c ⊔ d)[y/x] = c[y/x] ⊔ d[y/x]; (3) x / ∈ fv (c[y/x]); (4) fv (c ⊔ d) = fv (c) ∪ fv (d).
We now illustrate a constraint system for linear-order arithmetic.

Example 1 (A Constraint System of Linear Order Arithmetic). Consider the following syntax:

φ, ψ . . .

:= t = t ′ | t > t ′ | φ ∨ ψ | ¬φ
where the terms t, t ′ can be elements of a set of variables Var , or constant symbols 0, 1, . . .. Assume an underlying first-order structure of linear-order arithmetic with the obvious interpretation in the natural numbers ω of =, > and the constant symbols.

A variable assignment is a function µ : Var -→ ω. We use A to denote the set of all assignments; P(X) to denote the powerset of a set X, ∅ the empty set and ∩ the intersection of sets. We use M(φ) to denote the set of all assignments that satisfy the formula φ, where the definition of satisfaction is as expected.

We can now introduce a constraint system as follows: the set of constraints is P(A), and define c ⊑ d iff c ⊇ d. The constraint false is ∅, while true is A. Given two constraints c and d, c ⊔ d is the intersection c ∩ d. By abusing the notation, we will often use a formula φ to denote the corresponding constraint, i.e., the set of all assignments satisfying φ. E.g. we use x > 1 ⊑ x > 5 to mean M(x > 1) ⊑ M(x > 5). For this constraint system one can show that e is a compact constraint (i.e., e is in Con 0 ) iff e is a co-finite set in A (i.e., iff the complement of e in A is a finite set). For example, x > 10 ∧ y > 42 is a compact constraint for Var = {x, y}.

From this structure, let us now define the cylindric constraint system S as follows. We say that an assignment µ ′ is an x-variant of µ if ∀y = x, µ(y) = µ ′ (y). Given x ∈ Var and c ∈ P(A), the constraint ∃ x c is the set of assignments µ such that exists

µ ′ ∈ c that is an x-variant of µ. The diagonal element d xy is x = y. ⊓ ⊔ Assumption 1
We shall assume that the constraint system is well-founded and, for practical reasons, that its ordering ⊑ is decidable. Well-foundedness is needed for technical reasons in the definition of the labeled transition semantics in Section 3.2.

Syntax of CCP

Let C = (Con, Con 0 , ⊑, ⊔, true, false) be a constraint system. The ccp processes are given by the following syntax:

P, Q, . . . ::= tell(c) | i∈I ask (c i ) → P i | P Q | ∃ x P | p(z)
where I is a finite set of indexes and c, c i ∈ Con 0 . We use Proc to denote the set of all processes.

Finite processes. Intuitively, the tell process tell(c) adds c to the global store. The addition is performed regardless the generation of inconsistent information. The process P Q stands for the parallel execution of P and Q.

The guarded-choice i∈I ask (c i ) → P i where I is a finite set of indexes, represents a process that can nondeterministically choose one of the P j (with j ∈ I) whose corresponding guard constraint c j is entailed by the store. The chosen alternative, if any, precludes the others. We shall often write ask (c i1

) → P i1 + . . . + ask (c in ) → P in if I = {i 1 , . . . , i n }.
If no ambiguity arises, we shall omit the " ask(c) → " when c = true. The blind-choice process i∈I ask (true) → P i , for example, can be written i∈I P i . We shall omit the " i∈I " when I is a singleton. We use stop as an abbreviation of the empty summation i∈∅ P i .

∃ x is a hiding operator, namely it indicates that in ∃ x P the variable x is local to P . The occurrences of x in ∃ x P are said to be bound. The bound variables of P , bv (P ), are those with a bound occurrence in P , and its free variables, fv (P ), are those with an unbound occurrence 3 .

Infinite processes. To specify infinite behavior, ccp provides parametric process definitions. A process p(z) is said to be a procedure call with identifier p and actual parameters z. We presuppose that for each procedure call p(z 1 . . . z m ) there exists a unique procedure definition possibly recursive, of the form p(x 1 . . . x m ) def = P where fv (P ) ⊆ {x 1 , . . . , x m }. Furthermore we require recursion to be guarded: I.e., each procedure call within P must occur within an ask process. The behavior of p(z 1 . . . z m ) is that of P [z 1 . . . z m /x 1 . . . x m ], i.e., P with each x i replaced with z i (applying αconversion to avoid clashes). We shall use D to denote the set of all process definitions.

Remark 1 (Choice-free fragment of ccp). Henceforth, we use ccp\+ to refer to the fragment of ccp without nondeterministic choice. More precisely ccp\+ processes are those in which every occurrence of i∈I ask (c i ) → P i has its index set I of cardinality 0 or 1.

Reduction Semantics

A configuration is a pair P, d representing a state of a system; d is a constraint representing the global store, and P is a process, i.e., a term of the syntax given above. We use Conf with typical elements γ, γ ′ , . . . to denote the set of all configurations. We will use Conf ccp\+ for the configurations whose processes are in the ccp\+ fragment.

The operational semantics of ccp is given by an unlabeled transition relation between configurations: a transition γ -→ γ ′ intuitively means that the configuration γ can reduce to γ ′ . We call these kind of unlabeled transitions reductions and we use -→ * to denote the reflexive and transitive closure of -→.

Formally, the reduction semantics of ccp is given by the relation -→ defined in Table 1. Rules R1 and R2 are easily seen to realize the intuitions described in Section 2.2. Rule R3 states that i∈I ask (c i ) → P i can evolve to P j whenever the global store d entails c j and j ∈ I.

Rule R4 is somewhat more involved, first we extend the syntax by introducing a process ∃ e

x P representing the evolution of a process of the form ∃ x P , where e is the local information (local store) produced during this evolution. The process ∃ x P can be seen as a particular case of ∃ e

x P : it represents the situation in which the local store is empty. Namely, ∃ x P = ∃ true x P . Intuitively, ∃ e

x P behaves like P , except that the variable x possibly present in P must be considered local, and that the information present in e has to be taken into account. It is convenient to distinguish between the external and the internal points of view. From the internal point of view, the variable x, possibly occurring in the global store d, is hidden. This corresponds to the usual scoping rules: the x in d is global, hence "covered" by the local x. Therefore, P has no access to the information on x in d, and this is achieved by filtering d with ∃ x . Furthermore, P can use the information (which may also concern the local x) that has been produced locally and accumulated in e. In conclusion, if the visible store at the external level is d, then the store that is visible internally by P is e ⊔ ∃ x d. Now, if P is able to make a step, thus reducing to P ′ and transforming the local store into e ′ , what we see from the external point of view is

R1 tell(c), d -→ stop, d ⊔ c R2 P, d -→ P ′ , d ′ P Q, d -→ P ′ Q, d ′ R3 j ∈ I and cj ⊑ d i∈I ask (ci) → Pi, d -→ Pj, d R4 P, e ⊔ ∃xd -→ P ′ , e ′ ⊔ ∃xd ∃ e x P, d -→ ∃ e ′ x P ′ , d ⊔ ∃xe ′ R5 P [z/x], d -→ γ ′ p(z), d -→ γ ′ where p(x) def = P is a process definition in D Table 1.
Reduction semantics for ccp (symmetric rule for R2 is omitted). D is the set of process definitions.

that the process is transformed into ∃ e ′ x P ′ , and that the information ∃ x e present in the global store is transformed into ∃ x e ′ . 4

Barbed Semantics

In [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF], the authors introduced a barbed semantics for ccp. Barbed equivalences have been introduced in [START_REF] Milner | Barbed bisimulation[END_REF] for CCS, and have become a classical way to define the semantics of formalisms equipped with unlabeled reduction semantics. Intuitively, barbs are basic observations (predicates) on the states of a system. In the case of ccp, barbs are taken from the underlying set Con 0 of the constraint system. ⊓ ⊔

In this context, the equivalence proposed is the saturated bisimilarity [START_REF] Bonchi | Saturated semantics for reactive systems[END_REF][START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF]. Intuitively, in order for two states to be saturated bisimilar, then (i) they should expose the same barbs, (ii) whenever one of them moves then the other should reply and arrive at an equivalent state (i.e. follow the bisimulation game), (iii) they should be equivalent under all the possible contexts of the language.

Using this idea, in [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF], the authors propose a saturated bisimilarity for ccp where condition (iii) requires the bisimulations to be upward closed instead of closing under any process context. A process context C is a term with a single hole • such that if we replace • with a process P , we obtain a process term C[P ]. For example, for the parallel context C = • R we obtain C[P ] = P R.

Definition 3 (Saturated Barbed Bisimilarity).

A saturated barbed bisimulation is a symmetric relation R on configurations s.t. whenever (γ 1 , γ 2 ) ∈ R with γ 1 = P, c and γ 2 = Q, d implies that:

(i) if γ 1 ↓ e then γ 2 ↓ e , (ii) if γ 1 -→ γ ′ 1 then there exists γ ′ 2 s.t. γ 2 -→ γ ′ 2 and (γ ′ 1 , γ ′ 2 ) ∈ R, (iii) for every a ∈ Con 0 , ( P, c ⊔ a , Q, d ⊔ a ) ∈ R.
We say that γ 1 and γ 2 are saturated barbed bisimilar (γ

1 ∼sb γ 2 ) if there is a saturated barbed bisimulation R s.t. (γ 1 , γ 2 ) ∈ R. We write P ∼sb Q iff P, true ∼sb Q, true .
We shall prove that the closure condition (iii) is enough to make ≈sb a congruence in ccp\+. This means that P ≈sb Q implies C[P ] ≈sb C[Q] for every process context. However, this is not the case for ccp with nondeterministic choice as we shall demonstrate later on.

Weak saturated bisimilarity ( ≈sb ) is obtained from Definition 3 by replacing the strong barbs in condition (i) for its weak version (⇓) and the transitions in condition (ii) for the reflexive and transitive closure of the transition relation (-→ * ).

Definition 4 (Weak Saturated Barbed Bisimilarity). A weak saturated barbed bisimulation is a symmetric relation R on configurations s.t. whenever (γ 1 , γ 2 ) ∈ R with γ 1 = P, c and γ 2 = Q, d implies that:

(i) if γ 1 ⇓ e then γ 2 ⇓ e , (ii) if γ 1 -→ * γ ′ 1 then there exists γ ′ 2 s.t. γ 2 -→ * γ ′ 2 and (γ ′ 1 , γ ′ 2 ) ∈ R, (iii) for every a ∈ Con 0 , ( P, c ⊔ a , Q, d ⊔ a ) ∈ R.
We say that γ 1 and γ 2 are weak saturated barbed bisimilar (γ 1 ≈sb γ 2 ) if there exists a weak saturated barbed bisimulation R s.t. (γ 1 , γ 2 ) ∈ R. We shall write P ≈sb Q iff P, true ≈sb Q, true .

We now illustrate ∼sb and ≈sb with the following two examples.

Example 3. Consider the constraint system from Example 1 and let Vars = {x}. Take P = ask (x > 5) → stop and Q = ask (x > 7) → stop. One can check that P ∼sb Q since P, x > 5 -→, while Q, x > 5 -→. Then consider P +Q, true and observe that P + Q, true ∼sb P, true . Indeed, for all constraints e, s.t. x > 5 ⊑ e, both the configurations evolve into stop, e , while for all e s.t. x > 5 ⊑ e, both configurations cannot proceed. Since x > 5 ⊑ x > 7, the behavior of Q is somehow absorbed by the behavior of P .

⊓ ⊔ Example 4. Take P and Q as in Example 3. One can check that P ≈sb Q. First notice that P, true -→ and also Q, true -→. Now note that for all e it is the case that both configurations evolve to a γ where γ ⇓ e . Intuitively, none of the configurations adds information to the store and, since ≈sb does not care about the silent transitions, then P and Q should be weakly bisimilar.

⊓ ⊔

Finally, notice that in ccp\+ configurations are confluent in the following sense.

Proposition 1 (Confluence [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]). Let γ ∈ Conf ccp\+ . If γ -→ * γ 1 and γ -→ * γ 2 then there exists γ ′ such that γ 1 -→ * γ ′ and γ 2 -→ * γ ′ .

The proposition above will be a cornerstone for the results we shall obtain in ccp\+.

Congruence issues

A typical question in the realm of process calculi, and concurrency in general, is whether a given process equivalence is a congruence. In other words, whether the fact that P and Q are equivalent implies that they are still equivalent in any context. More precisely, a given equivalence ⊲⊳ is said to be a congruence if

P ⊲⊳ Q implies C[P ] ⊲⊳ C[Q]
for every process context C5 . The congruence issue is fundamental for algebraic as well as practical reasons; one may not be content with having P ⊲⊳ Q equivalent but R P ⊲⊳ R Q. Nevertheless, some of the representative equivalences in concurrency are not congruences. For example, in CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF], trace equivalence and strong bisimilarity are congruences but weak bisimilarity is not because it is not preserved by summation contexts. So given a notion of equivalence one may wonder in what contexts the equivalence is preserved. For instance, the problem with weak bisimilarity can be avoided by using guarded-summation (see [START_REF] Milner | Communicating and mobile systems: the π-calculus[END_REF]). We shall see that ≈sb is a congruence for ccp\+. However, this is not the case in the presence of nondeterministic choice. Moreover, unlike CCS, the problem arises even in the presence of guarded summation/choice. In fact, our counterexample reveals that the problem is intrinsic to ccp.

Observational Equivalence

In this section we shall introduce the standard notion of observational equivalence (∼ o ) [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] for ccp as well as its relation with ≈sb .

The notion of fairness is central to the definition of observational equivalence for ccp. We introduce this notion following [START_REF] Falaschi | Confluence in concurrent constraint programming[END_REF]. Any derivation of a transition involves an application of R1 or R3. We say that P is active in a transition t = γ -→ γ ′ if there exists a derivation of t where rule R1 or R3 is used to produce a transition of the form P, d -→ γ ′′ . Moreover, we say that P is enabled in γ if there exists γ ′ such that P is active in γ -→ γ ′ . A computation γ 0 -→ γ 1 -→ γ 2 -→ . . . is said to be fair if for each process enabled in some γ i there exists j ≥ i such that the process is active in γ j -→ γ j+1 .

Note that a finite fair computation is guaranteed to be maximal, namely no outgoing transitions are possible from its last configuration.

The standard notion of observables for ccp are the results computed by a process for a given initial store. The result of a computation is defined as the least upper bound of all the stores occurring in the computation, which, due to the monotonic properties of ccp, form an increasing chain. More formally: Definition 5 (Result). Given a finite or infinite computation ξ of the form:

ξ = Q 0 , d 0 -→ Q 1 , d 1 -→ Q 2 , d 2 -→ . . .

The result of ξ, denoted by Result(ξ), is the constraint

i d i .
Note that for a finite computation the result coincides with the store of the last configuration. Now since ccp\+ is confluent (Proposition 1), the following theorem from [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] states that all the fair computations of a configuration have the same result.

Proposition 2 ([26]

). Let γ be ccp\+ configuration and let ξ 1 and ξ 2 be two computations of γ. If ξ 1 and ξ 2 are fair, then Result(ξ 1 ) = Result(ξ 2 ).

Before introducing the notion of observational equivalence we need some notation. Below we define the set of possible computations of a given configuration.

Definition 6 (Set of Computations). The set of computations starting from γ, denoted Comp(γ), is defined as:

Comp(γ) = {ξ | ξ = γ -→ γ ′ -→ γ ′′ -→ . . .}
Now we introduce the notion of observables. Intuitively, the set of observables of γ is the set of results of the fair computations starting from γ.

Definition 7 (Observables). Let O : Proc → Con 0 → 2 Con be given by:

O(P )(d) = {e | ξ ∈ Comp( P, d ), ξ is fair and Result(ξ) = e}.
Using these elements we define the notion of observational equivalence. Two configurations are deemed equivalent if they have the same set observables for any given store.

Definition 8 (Observational equivalence). We say that P and Q are observational equivalent, written

P ∼ o Q, iff O(P ) = O(Q).
Notice that in the case of ccp\+, as defined in [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF], the set of observables is a singleton because of Proposition 2. In [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF] it was shown that, in ccp\+, weak saturated barbed bisimilarity and observation equivalence coincide. Recall that P ≈sb Q means P, true ≈sb Q, true .

Proposition 3 ([2]

). Let P and Q be ccp\+ processes. Then P ∼ o Q iff P ≈sb Q.

Nevertheless, the above theorem does not hold for ccpwith nondeterministic choice. We can show this by using a counter-example reminiscent from the standard one for CCS. Let P = (ask (b) → tell(c)) + (ask (b) → tell(d)) and Q = ask (b) → ((ask (true) → tell(c)) + (ask (true) → tell(d))). One can verify that P ∼ o Q but P ≈sb Q. However, the (⇐) direction of the theorem does hold as we show next.

Theorem 1. If P ≈sb Q then P ∼ o Q. LR1 tell(c), d true -→ stop, d ⊔ c LR2 P, d α -→ P ′ , d ′ P Q, d α -→ P ′ Q, d ′ LR3 j ∈ I and α ∈ min{a ∈ Con0 | cj ⊑ d ⊔ a} i∈I ask (ci) → Pi, d α -→ Pj, d ⊔ α LR4 P [z/x], e[z/x] ⊔ d α -→ P ′ , e ′ ⊔ d ⊔ α ∃ e x P, d α -→ ∃ e ′ [x/z] x P ′ [x/z], ∃x(e ′ [x/z]) ⊔ d ⊔ α with x ∈ fv (e ′ ), z ∈ fv (P ) ∪ fv (e ⊔ d ⊔ α) LR5 P [z/x], d α -→ γ ′ p(z), d α -→ γ ′ where p(x) def = P is a process definition in D Table 2.
Labeled semantics for ccp (symmetric rule for LR2 is omitted).

Congruence

We begin this section by showing that weak bisimilarity is a congruence in a restricted sense: It is preserved by all the contexts from the choice-free fragment. For this purpose it is convenient to recall the labeled semantics of ccp as well as the (labeled) weak bisimilarity introduced in [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF].

Labeled Semantics In a labeled transition of the form

P, d α -→ P ′ , d ′
the label α ∈ Con 0 represents a minimal information (from the environment) that needs to be added to the store d to reduce from P, d to P ′ , d ′ , i.e., P, d ⊔ α -→ P ′ , d ′ . As a consequence, the transitions labeled with the constraint true are in one to one correspondence with the reductions defined in the previous section. For this reason, hereafter we will sometimes write -→ to mean true -→. The LTS (Conf , Con 0 , -→) is defined by the rules in Table 2. The rule LR3, for example, says that i∈I ask (c i ) → P i , d can evolve to P j , d ⊔ α if j ∈ I and the environment provides a minimal constraint α that added to the store d entails the guard c j , i.e., α ∈ min{a ∈ Con 0 | c j ⊑ d ⊔ a}. Notice that Assumption 1 guarantees the existence of α. The rule LR4 follows the same approach as R4, however it uses variable substitution instead of hiding with the existential operator. 6 The other rules are easily seen to realize the intuition given in Section 2.2.

We can now introduce the notion of weak bisimilarity ( ≈) from [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF]. In [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF] it is shown that ≈ coincides with ≈sb and, by exploiting the labeled semantics, avoids the upward closure from condition (iii) in ≈sb .

Definition 9 (Weak bisimilarity).

A weak bisimulation is a symmetric relation R on configurations such that whenever (γ 1 , γ 2 ) ∈ R with γ 1 = P, c and γ 2 = Q, d :

(i) if γ 1 ↓ e then γ 2 ⇓ e , (ii) if γ 1 α -→ γ ′ 1 then ∃γ ′ 2 s.t. Q, d ⊔ α -→ * γ ′ 2 and (γ ′ 1 , γ ′ 2 ) ∈ R.
We say that γ 1 and γ 2 are weakly bisimilar, written γ 1 ≈ γ 2 , if there exists a weak bisimulation R such that (γ 1 , γ 2 ) ∈ R. We write P ≈ Q iff P, true ≈ Q, true .

To illustrate this definition consider the following example. ⊓ ⊔

The following result from [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF] states that weak bisimilarity coincides with weak saturated barbed bisimilarity (Definition 4).

Proposition 4 ([2]). ≈sb = ≈.

We can now prove that ≈sb is a congruence in ccp\+.

Theorem 2. Let P and Q be ccp\+ processes and assume that P ≈sb Q. Then for every process context

C[•] in ccp\+ we have C[P ] ≈sb C[Q].
Notice that this result implies that observational equivalence (∼ o ) is a congruence. Unfortunately the theorem above does not hold for ccp with nondeterministic choice, as shown next. Theorem 3. There exists For (a) we can show that P ′ , true ≈sb P, e ≈sb Q, true . The first equation is trivial. For the second we define a relation on configurations R. The set of pairs in R are those linked in Figure 1. It can easily be verified that (the symmetric closure of) R is a weak bisimulation (see Definition 9). The point (a) then follows from Proposition 4.

P ′ , Q, R in ccp s.t. (a) P ′ ≈sb Q but (b) P ′ R ≈sb Q R.
For proving the part (b) of the above claim, we let R = (ask (e) → tell(α)) + (ask (e) → tell(β)). We shall prove that no weak bisimulation can contain the pair ( P R, e , Q R, true ). The results then follows from Proposition 4 and the fact that P ′ R, true ≈sb P R, e which can be easily verified.

Consequently, let us assume that P R, e -→ P tell(α), e by executing the left summand of R. By condition (ii) of weak bisimulation Q R, true must match the move. We have two cases: -Q R, true does not make a transition. And now let us suppose that Q R, true e -→ Q tell(β), true . This means that P tell(α), e now has to match this transition. However Q tell(β), true -→ Q, β ⇓ β while P tell(α), e ⇓ β . Thus we cannot satisfy condition (i) of weak bisimulation.

-Q R, true makes a transition. To match the move it should also execute the left summand of R. However, since e is not the store of Q R, true , Q must be executed first. and this means executing of one of summands in Q to be able to add e to the store. If the left summand of Q is executed, we get Q R, true -→ * tell(α), c ⊔ e . In this case we could then take the move P tell(α), e -→ tell(d) tell(α), e . But then tell(α), c ⊔ e ⇓ c and notice that tell(d) tell(α), e ⇓ c , thus we cannot satisfy condition (i) of weak bisimulation. The case where the right summand of Q is executed is symmetric.

Weak full bisimilarity

In the previous section we showed that ≈ (and ≈sb ) for the full ccp is not entirely satisfactory since it is not a congruence. By building on ≈, in this section we propose a new equivalence which we call (weak) full bisimilarity, written ≈ f . This new equivalence does not quantify over infinitely many process contexts in its definition yet we will show that is a congruence. Furthermore, we will also prove that adequacy of ≈ f by showing that it is the largest congruence included in ≈sb .

More than weak barbs

The key to figure out the element missing in the definition of ≈sb (Definition 4) lies in Figure 1. If we look at the configurations in the figure we can see that while P, e is able to produce a barb e without choosing between c and d, Q, true is not. The definition of ≈sb tries to capture this in the condition (i), namely by checking that P, e ⇓ e then requiring that Q, true ⇓ e . However, this condition does not capture the fact that in order to produce e, Q, true may have to evolve into a configuration which can no longer produce some of the weak barbs Q, true can produce. 7Using this insight, we shall define a new notion of weak bisimilarity that changes condition (i) in ≈ (Definition 9) in order to deal with the problem present in Figure 1. More concretely, condition (i) requires that whenever P, c ↓ α then Q, d ⇓ α , Q, d -→ * Q ′ , d ′ ↓ α without imposing any condition between P, c and Q ′ , d ′ . This makes it possible that P, c ↓ β and Q ′ , d ′ does not: indeed, it might be the case that that Q, d -→ * Q ′′ , d ′′ ↓ β for some other branch Q ′′ , d ′′ . Hence P, c and Q, d would pass condition (i) as in Figure 1.

Weak full bisimilarity deals with this problem by adding a condition between P, c and Q ′ , d ′ , namely Q, d ⇓ c has to hold by reaching a bisimilar configuration: P, c has to be weakly bisimilar Q ′ , d ′ .

Definition 10 (Weak Full Bisimilarity). A weak full bisimulation is a symmetric relation R on configurations s.t. whenever (γ 1 , γ 2 ) ∈ R with γ 1 = P, c and γ 2 = Q, d implies that:

(i) there is γ ′ 2 = Q ′ , d ′ such that Q, d -→ * γ ′ 2 where c ⊑ d ′ and (γ 1 , γ ′ 2 ) ∈ R, (ii) if γ 1 α -→ γ ′ 1 then there exists γ ′ 2 = Q ′ , d ′ s.t. Q, d ⊔ α -→ * γ ′ 2 where c ′ ⊑ d ′ and (γ ′ 1 , γ ′ 2 ) ∈ R.
We say that γ 1 and γ 2 are weak fully bisimilar (γ

1 ≈ f γ 2 ) if there exists a weak full bisimulation R s.t. (γ 1 , γ 2 ) ∈ R. We write P ≈ f Q iff P, true ≈ f Q, true .
In the definition above, the fist condition states that Q, d has to produce c by reaching a (weakly) bisimilar configuration. The second condition is the bisimulation game from ≈ (Definition 9) plus a condition requiring the store c ′ to be matched too.

To better explain this notion consider again the counterexample to ≈ from Figure 1.

Example 6. Let P, e , Q, true as in Figure 1. Let us build a relation R that is a weak full bisimulation where ( P, e , Q, true ) ∈ R. By condition (i) in Definition 10 we need a γ

′ 2 = Q ′ , d ′ s.t. Q, d -→ * γ ′
2 and e ⊑ d ′ and (γ 1 , γ ′ 2 ) ∈ R. We have two options Q ′ = stop and d ′ = c ⊔ e or d ′ = d ⊔ e. 8 However, if we take ( P, e , stop, c ⊔ e ) ∈ R we have that P, e ⇓ d while stop, c ⊔ e ⇓ d . A similar argument works for stop, d ⊔ e . Therefore, no weak full bisimulation may contain ( P, e , Q, true ). Hence P, e ≈ f Q, true . ⊓ ⊔

Congruence issues

We shall now prove that full bisimilarity is a congruence w.r.t all possible contexts in ccp. Namely, whenever γ and γ ′ are in ≈ f then they can be replaced for one another in any context.

Theorem 4. Let P and Q be ccp processes and assume that P ≈ f Q. Then for every process

context C[•] we have that C[P ] ≈ f C[Q].
Proof. Here we consider the parallel case; the other cases are trivial or easier to verify. We shall prove that R

= {( P R, c , Q R, d ) | P, c ≈ f Q, d } is a weak full bisimulation as in Definition 10. To prove (i), since P, c ≈ f Q, d we have that Q, d -→ * Q ′ , d ′ where c ⊑ d ′ and Q ′ , d ′ ≈ P, c (1)
, c ≈ f Q, d then Q, d ⊔ α -→ * Q ′ , d ′ where P ′ , c ′ ≈ f Q ′ , d ′ and c ′ ⊑ d ′ (3). By R2 we have Q R, d ⊔ α -→ * Q ′ R, d ′ and from (3) we can conclude that ( P ′ R, c , Q ′ R, d ′ ) ∈ R. Using LR2 (right), then P 1 = (P R ′ ) and c ′ = (c ⊔ α ⊔ e) with R, c α -→ R ′ , c ′ by a shorter inference. From (1) we know that Q, d -→ * Q ′ , d ′ where c ⊑ d ′ and Q ′ , d ′ ≈ P, c . Hence Q R, d ⊔ α -→ * Q ′ R, d ′ ⊔ α . Now since c ⊑ d ′ then by monotonicity R, d ′ ⊔ α -→ R, d ′′ where d ′′ = d ′ ⊔ α ⊔ e. Therefore by R2 we get Q R, d ⊔ α -→ * Q ′ R ′ , d ′′ and from (1) and monotonicity P, c ′ = P, c ⊔ α ⊔ e ≈ Q ′ , d ′ ⊔ α ⊔ e = Q ′ , d ′′ . Using this we can conclude that ( P R ′ , c ′ , Q ′ R ′ , d ′′ ) ∈ R.
Note that ≈ f is more distinguishing than ≈ and the result above shows that this level of granularity is needed to obtain a weak bisimilarity that is a congruence for ccp.

Relation with observational equivalence

In section 3.1 we described the relation between weak (saturated) bisimilarity ( ≈sb , Definition 4) and the standard observational equivalence (∼ o , Definition 8) for ccp. Concretely, we know that, in ccp\+, ≈sb coincides with ∼ o , while for the full ccp ≈sb implies ∼ o but the converse does not hold. In this section we shall see the relation between weak full bisimilarity (≈ f , Definition 10) and ∼ o . We shall prove that ≈ f coincides with ∼ o in ccp\+ by proving that ≈ f corresponds to ≈sb in the choice-free fragment of ccp. Furthermore, for the full language of ccp, we shall prove that ≈ f implies ∼ o again by showing that ≈ f implies ≈sb in ccp.

Let us start by showing that ≈ f and ≈ coincide in ccp\+. This theorem strongly relies on the confluent nature of ccp\+ (Proposition 1).

Theorem 5. Let γ, γ ′ ∈ Conf ccp\+ , γ ≈ f γ ′ iff γ ≈ γ ′ .
The corollary below follows from Proposition 3 and 4, and Theorem 5.

Corollary 1. Let P and Q be ccp\+ processes. Then P ≈ f Q iff P ∼ o Q.

We shall now prove that ≈ f implies ∼ o for the full ccp. In order to do this we first prove that ≈ f implies ≈sb .

Theorem 6. If γ ≈ f γ ′ then γ ≈ γ ′ .
The corollary below follows from Theorem 1 and 6, and Proposition 4.

Corollary 2. If P ≈ f Q then P ∼ o Q.
The above statement allows us to use the co-inductive techniques of full bisimulation to prove observational equivalence. We now state that ≈ f coincides with ∼ = for ccp with nondeterministic choice.

Language Relation among equivalences

Congruence w.r.t. C[•] C[•]\+ ccp\+ ∼ = = ≈ f = ≈ = ≈sb = ∼o N/A ∼ =, ≈ f , ≈, ≈sb , ∼o ccp ∼ = = ≈ f ⊆ ≈ = ≈sb ⊆ ∼o ∼ =, ≈ f ∼ =, ≈ f , ≈, ≈sb Table

Conclusions and Related Work

In this paper we showed that the weak saturated barbed bisimilarity ( ≈sb ) proposed in [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF] is not a congruence for ccp. Nevertheless, we also showed that the upward closure, i.e. condition (iii), is enough to make ≈sb a congruence in the choice-free fragment (ccp\+). We then proposed a new notion of bisimilarity, called weak full bisimilarity (≈ f ), and we proved that it is a congruence for the full ccp despite the fact that ≈ f does not require any quantification over a (potentially) infinite number of contexts in its definition. Furthermore, we showed that ≈ f implies the standard observational equivalence (∼ o ) for ccp from [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]. Finally we demonstrated that ≈ f is not too restrictive by showing that it is the largest congruence included in ≈sb . See Table 3 for a summary of the contributions of this paper. This is the first weak behavioral ccp congruence for ccp with nondeterministic choice that does not require implicit quantification over all contexts.

Most of the related work has already been discussed in the introduction (Section 1). There has been other attempts for finding a good notion of bisimilarity for ccp such as [START_REF] Saraswat | Concurrent constraint programming[END_REF] and [START_REF] Mendler | A logical view of concurrent constraint programming[END_REF]. In [START_REF] Saraswat | Concurrent constraint programming[END_REF] the authors propose a ccp bisimilarity that requires processes to match the exact label in the bisimulation game, a condition which is standard in process calculi realm, however this notion is known to be too distinguishing for ccp as shown in [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF]. As for [START_REF] Mendler | A logical view of concurrent constraint programming[END_REF], their notion of (strong) bisimilarity resembles to the saturated barbed bisimilarity from [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF] and, although they do not give a notion of weak bisimilarity, the results in this paper can be related directly.

We plan to adapt the algorithms from [START_REF] Aristizábal | Partition refinement for bisimilarity in CCP[END_REF][START_REF] Pino | Efficient computation of program equivalence for confluent concurrent constraint programming[END_REF] to verify ≈ f . We conjecture that the decision procedure for ≈sb can be exploited to check ≈ f by modifying the way the (weak) barbs are considered. Furthermore, in this paper we obtained a notion of weak bisimilarity that is a congruence even if we do not consider a label for observing the tell actions. Since ccp is an asynchronous language, not observing the tell follows the philosophy of considering as labels the minimal information needed to proceed, namely a tell process does not need a stimulus from the environment to post its information in the store. Following the same reasoning, we plan to investigate whether it is possible to define a labeled semantics for the asynchronous π-calculus (Aπ) [START_REF] Milner | Communicating and mobile systems: the π-calculus[END_REF][START_REF] Sangiorgi | The π-Calculus -a theory of mobile processes[END_REF] with a τ label for the output transitions, instead of a co-action, and we shall check if a notion of bisimilarity similar to ours would also be a congruence.

Definition 2 (

 2 Barbs). A configuration γ = P, d is said to satisfy the barb c, written γ ↓ c , iff c ∈ Con 0 and c ⊑ d. Similarly, γ satisfies a weak barb c, written γ ⇓ c , iff there exist γ ′ s.t. γ -→ * γ ′ ↓ c . Example 2. Consider the constraint system from Example 1 and let Vars = {x}. Let γ = ask (x > 10) → tell(x > 42), x > 10 . We have γ ↓ x>5 since (x > 5) ⊑ (x > 10) and γ ⇓ x>42 since γ -→ tell(x > 42), x > 10 -→ stop, (x > 42) ↓ x>42 .

Remark 2 .

 2 Let P, d ∈ Conf ccp\+ . Note that O : Proc → Con 0 → Con because of Proposition 2 and it is defined as O(P )(d) = Result(ξ) where ξ is any fair computation of P, d .

Example 5 .

 5 Let γ 1 = tell(true), true and γ 2 = ask (c) → tell(d), true . We can show that γ 1 ≈ γ 2 when d ⊑ c. Intuitively, this corresponds to the fact that the implication c ⇒ d is equivalent to true when c already entails d. The LTSs of γ 1 and γ 2 are the following: γ 1 -→ stop, true and γ 2 c -→ tell(d), c -→ stop, c . It is now easy to see that the symmetric closure of the relation R = {(γ 2 , γ 1 ), (γ 2 , stop, true ), ( tell(d), c , stop, c ), ( stop, c , stop, c )} is a weak bisimulation as in Definition 9.

  Proof. To prove this claim we let P = (ask (true) → tell(c)) + (ask (true) → tell(d)), P ′ = P tell(e) and Q = (ask (true) → tell(c ⊔ e)) + (ask (true) → tell(d ⊔ e)) with c ⊑ d, c ⊑ e, d ⊑ c, d ⊑ e, e ⊑ c, e ⊑ d.

Fig. 1 .

 1 Fig. 1. Let P = (ask (true) → tell(c))+(ask (true) → tell(d)) and Q = (ask (true) → tell(c ⊔ e)) + (ask (true) → tell(d ⊔ e)). The linked configurations are weakly bisimilar.

3 .

 3 Summary of the contributions. Recall that ≈sb stands for the weak saturated barbed bisimilarity (Definition 4), ∼o is the standard observational equivalence (Definition 8), ≈ represents weak bisimilarity (Definition 9), ≈ f is the notion of weak full bisimilarity proposed in this paper (Definition 10) and ∼ = stands for the behavioral congruence (Definition 11). C[•]\+ stands for the contexts where the summation operator does not occur, while C[•] represents any possible context, hence the summation operator may occur in C[•]. For this reason we put N/A (Not Applicable) in the row corresponding to ccp\+. Notice that the correspondence ≈ = ≈sb = ∼o comes from [2].

4. 4

 4 Behavioral congruenceFinally, we prove that ≈ f is the largest congruence included in ≈ by showing that it coincides with the congruence ∼ = defined next.Definition 11 (Behavioral Congruence). We say that P is behaviorally congruent toQ, denoted P ∼ =Q, ifffor every process context C[•] we have C[P ] ≈ C[Q]. We use P, e ∼ = Q, d to denote (P tell(e)) ∼ =(Q tell(d)).

Theorem 7 .

 7 P, e ≈ f Q, d iff P, e ∼ = Q, d .

  . Therefore by R2 we get Q R, d -→ * Q ′ R, d ′ and by[START_REF] Arbab | A coinductive calculus of component connectors[END_REF] we can conclude that ( Q ′ R, d

				′ , P
	R, c ) ∈ R. To prove (ii) let us assume that P	R, c	α -→ P 1 , c 1 . We proceed
	by induction (on the depth) of the inference of P	R, c	α -→ P 1 , c ′ . Using LR2
	(left), then P 1 = (P ′	R) with P, c

α

-→ P ′ , c ′ by a shorter inference. Since P

Notice that we also defined fv (.) on constraints in the previous section.

For more details about the operational semantics we refer the reader to[START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF].

Recall that the expression C[P ] denotes the process that results from replacing in C, the hole • with P . For example C = R • then C[P ] = R P .

See[START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF] for a detailed explanation of the rule LR4.

In the case of ccp\+ this is not a concern given that in this fragment weak barbs are always preserved during evolution.

The cases for Q ′ = tell(c ⊔ e) or Q ′ = tell(d ⊔ e) with d ′ = true are equivalent.

⋆ This work has been partially supported by the project ANR 12IS02001 PACE, ANR-09-BLAN-0169-01 PANDA, and by the French Defence procurement agency (DGA) with a PhD grant.