Search

Establishing equivalences between programs is crucial both for verifying correctness of programs and for justifying optimisations and program transformations. There exist several equivalence relations for programs, and bisimulations are among the most versatile of these equivalences. Among bisimulations one distinguishes strong bisimulation that requires that each action of a program is simulated by a single action of the equivalent program, and weak bisimulation that allows some of the actions to be invisible, and thus not simulated.

Composite distributed services involve local and remote services that get orchestrated according to specific business logic. This logic can be programmed by applying a traditional general-purpose programming language, but is generally described using a workflow language that coordinates a set of given services. The services involved in the composition, or the composition may need to evolve both at the business logic level (workflow level) and the global architecture level. This paper presents a solution to ease such evolution for compound distributed services and the authors’ proposal enables the evolution of both the business logic and the underlying architecture. This paper suggests relying on a distributed software component model to represent and easily manage the set of local or remote software entities (services) involved in the composition. Composite services are represented in a model that combines the use of a distributed and hierarchical software component model and new timed-automata based workflow language. This combination makes explicit the separation between functional and non-functional concerns, and as a consequence this approach helps in defining the required and various evolution procedures in context to compound services.

On a system that exposes disjoint memory spaces to the software, a program has to address memory consistency issues and perform data transfers so that it always accesses valid data. Several approaches exist to ensure the consistency of the memory accessed. Here we are interested in the verification of a declarative approach where each component of a computation is annotated with an access mode declaring which part of the memory is read or written by the component. The programming framework uses the component annotations to guarantee the validity of the memory accesses. This is the mechanism used in VectorPU, a C++ library for programming CPU-GPU heterogeneous systems. This article proves the correctness of the software cache-coherence mechanism used in VectorPU. Beyond the scope of VectorPU, this article provides a simple and effective formalization of memory consistency mechanisms based on the explicit declaration of the effect of each component on each memory space. The formalism we propose also takes into account arrays for which a single validity status is stored for the whole array; additional mechanisms for dealing with overlapping arrays are also studied.

We present the content of the special issue consisting of selected articles from the 10th Interaction and Concurrency Experience workshop (ICE 2017). The theoretical results contributed by the ICE workshops and by these articles in particular aim at being applicable to real concurrent and distributed systems.