Abstract
Synchronous coordination systems allow the exchange of data by logically indivisible actions involving all coordinated entities. This paper introduces behavioural automata, a logically synchronous coordination model based on the Reo coordination language, which focuses on relevant aspects for the concurrent evolution of these systems. We show how our automata model encodes the Reo and Linda coordination models and how it introduces an explicit predicate that captures the concurrent evolution, distinguishing local from global actions, and lifting the need of most synchronous models to involve all entities at each coordination step, paving the way to more scalable implementations. © J. Proença, D. Clarke, E. de Vink & F. Arbab.

Abstract
Coordination in Reo emerges from the composition of the behavioural constraints of primitives, such as channels, in a component connector. Understanding and implementing Reo, however, has been challenging due to the interaction of the channel metaphor, which is an inherently local notion, and the non-local nature of the constraints imposed by composition. In this paper, the channel metaphor takes a back seat. We focus on the behavioural constraints imposed by the composition of primitives and phrase the semantics of Reo as a constraint satisfaction problem. Not only does this provide a clear description of the behaviour of Reo connectors in terms of synchronisation and data flow constraints, it also paves the way for new implementation techniques based on constraint satisfaction. We also demonstrate that this approach is more efficient than the existing techniques based on connector colouring.

Abstract
The HATS project aims at developing a model-centric methodology for the design, implementation and verification of highly configurable systems, such as software product lines, centred around the Abstract Behavioural Specification (ABS) modelling Language. This article describes the variability modelling features of the ABS Modelling framework. It consists of four languages, namely, µTVL for describing feature models at a high level of abstraction, the Delta Modelling Language DML for describing variability of the 'code' base in terms of delta modules, the Product Line Configuration Language CL for linking feature models and delta modules together and the Product Selection Language PSL for describing a specific product to extract from a product line. Both formal semantics and examples of each language are presented. © 2011 Springer-Verlag Berlin Heidelberg.

Abstract
Formal modelling and verification are critical for managing the inherent complexity of systems with a high degree of variability, such as those designed following the software product line (SPL) paradigm. SPL models tend to be large-the number of products in an SPL can be exponential in the number of features. Modelling these systems poses two main challenges. Firstly, a modular modelling formalism that scales well is required. Secondly, the ability to analyse and verify complex models efficiently is key in order to ensure that all products behave correctly. The choice of a system modelling formalism that is both expressive and well-established is therefore crucial. In this paper we show how SPLs can be modelled in an incremental, modular fashion using a formal method based on Petri nets. We continue our work on Feature Petri Nets, a lightweight extension to Petri nets, by presenting a framework for modularly constructing Feature Petri Nets to model SPLs. © 2011 Springer-Verlag.

Abstract
Parallelizing rendering algorithms to exploit multiprocessor and multicore machines isn't straightforward. Certain methods require frequent synchronization among threads to obtain benefits similar to the sequential algorithm. One such algorithm is the irradiance cache (IC), an acceleration data structure that caches indirect diffuse irradiance values. In multicore systems, the threads must share the IC to achieve high efficiency. A proposed wait-free mechanism for accessing the shared IC doesn't use the common blocking or busy-waiting methods, thus avoiding most serialization and reducing contention. A comparison with two classic approachesa lock-based mechanism and a local-write techniqueon two systems with up to 24 cores shows that the wait-free approach significantly reduces synchronization overhead, thus improving performance. The Web extra PDF augments the article. The Web extra video is an animation that demonstrates the wait-free IC system running at close to interactive rates on an 8-core machine. © 2006 IEEE.

Abstract