Exposé Jade Algave (INRIA Rocquencourt)

Fences in Weak Memory Models

We present an axiomatic framework, implemented in Coq, to define weak memory models w.r.t. several parameters: local reorderings of reads and writes, and visibility of inter and intra processor communications through memory, including full store atomicity relaxation. Thereby, we give a formal hierarchy of weak memory models, in which we provide a formal study of what should be the action and placement of fences to restore a given model such as Sequential Consistency from a weaker one. Finally, we provide a tool, diy, that tests a given machine to determine the architecture it exhibits. We detail the results of our experiments on Power and the model we extract from it. This identified an implementation error in Power 5 memory barriers (for which IBM is providing a software workaround); our results also suggest that Power 6 does not suffer from this problem.

Exposé Loïc Hélouët

Discovering Covert channels with Information Theory

Dans cet exposé, nous montrerons comment la présence de canaux cachés dans un système peut être caractérisée à l'aide de la théorie de l'information. Dans un premier temps, nous montrons que les notions habituelles de non-interférence ne permettent pas de capturer la notion de flot d'information inhérente aux canaux cachés. Nous montrons ensuite qu'une extension pour obtenir une notion d'interférence itérée ne permet pas de capturer les cas où moins d'un bit d'information est transmis à chaque utilisation du canal caché. Enfin, nous montrons que dans certains cas particuliers, il est possible d'utiliser la théorie de l'information pour ramener la caractérisation d'un canal caché à un calcul de capacité d'un canal à état.

Exposé Elie Najm (ENST)

Exposé Nils Gesbert (Univ. Glasgow)

Modular session types for distributed object-oriented programming

Session types allow communication protocols to be specified type-theoretically so that protocol implementations can be verified by static type-checking. We extend previous work on session types for distributed object-oriented languages in three ways. (1) We attach a session type to a class definition, to specify the possible sequences of method calls. (2) We allow a session type (protocol) implementation to be modularized, i.e. partitioned into separately-callable methods. (3) We treat session-typed communication channels as objects, integrating their session types with the session types of classes. The result is an elegant unification of communication channels and their session types, distributed object-oriented programming, and a form of typestates supporting non-uniform objects, i.e. objects that dynamically change the set of available methods. We define syntax, operational semantics, a sound type system, and a correct and complete type checking algorithm for a small distributed class-based object-oriented language. Static typing guarantees that both sequences of messages on channels, and sequences of method calls on objects, conform to type-theoretic specifications, thus ensuring type-safety. The language includes expected features of session types, such as delegation, and expected features of object-oriented programming, such as encapsulation of local state.

Exposé T. Chatain (LSV)

Concurrent semantics of real-time distributed systems

Techniques that aim at improving reliability and safety of automated systems have dramatically improved during the last twenty years (synthesis, model-checking, test...) Studying a complex system generally requires the use of multiple techniques and tools. Consequently the system must be modeled in different formalisms. The difficulty is to convince one that that the multiple representations are equivalent. For instance, considering two popular formalisms for real-time distributed systems, we would like to be able to transform a time Petri net into a network of timed automata. But we require that this transformation preserves concurrency. Yet the first works about formal comparisons of the expressivity of these models do not consider preservation of concurrency. Here we formalize model transformations that preserve not only the timed sequential behavior, but also concurrency. The notion of preservation of concurrency will be formalized using a concurrent semantics based on partial orders.

Exposé Tayssir Touili (LIAFA)

Reachability Analysis of Networks of Communicating Pushdown Systems

We address the verification problem of networks of communicating pushdown systems modeling communicating parallel programs with procedure calls. Processes in such networks can read the control state of the other processes according to a given communication structure (specifying the observability rights between processes). The reachability problem of such models is undecidable in general. First, we prove that it becomes decidable for networks with acyclic communication structure. Then, we define a class of networks that effectively preserves recognizability (hence, its reachability problem is decidable). Next, we consider networks where the communication structure can change dynamically during the execution according to a phase graph. The reachability problem for these dynamic networks being undecidable in general, we consider reachability when the switches in the communication structures are bounded. We show that this problem is undecidable even for one switch. Then, we define a natural class of models for which this problem is decidable. This class can be used in the definition of an efficient semi-decision procedure for the analysis of the general model of dynamic networks. Our techniques allowed to find bugs in two versions of a Windows NT Bluetooth driver. This is joint work with Faouzi Atig and Ahmed Bouajjani.