Search

Concurrent programs often make use of futures, handles to the results of asynchronous operations. Futures provide means to communicate not yet computed results, and simplify the implementation of operations that synchronise on the result of such asynchronous operations. Futures can be characterised as implicit or explicit, depending on the typing discipline used to type them. Current future implementations suffer from "future proliferation", either at the type-level or at run-time. The former adds future type wrappers, which hinders subtype polymorphism and exposes the client to the internal asynchronous communication architecture. The latter increases latency, by traversing nested future structures at run-time. Many languages suffer both kinds. Previous work offer partial solutions to the future proliferation problems; in this paper we show how these solutions can be integrated in an elegant and coherent way, which is more expressive than either system in isolation. We describe our proposal formally, and state and prove its key properties, in two related calculi, based on the two possible families of future constructs (data-flow futures and control-flow futures). The former relies on static type information to avoid unwanted future creation, and the latter uses an algebraic data type with dynamic checks. We also discuss how to implement our new system efficiently.

Software components are a valuable programming abstraction that enables a compositional design of complex applications. In distributed systems, components can also be used to provide an abstraction of locations: each component is a unit of deployment that can be placed on a di fferent machine. In this article, we consider this kind of distributed components that are additionally loosely coupled and communicate by asynchronous invocations. Components also provide a convenient abstraction for verifying the correct behaviour of systems: they provide structuring entities easing the correctness veri fication. This article aims at providing a formal background for the generation of behavioural semantics for asynchronous components. We use the pNet intermediate language to express the semantics of hierarchical distributed components communicating asynchronously by a request-reply mechanism. We also formalise two crucial aspects of distributed components: recon figuration and one-to-many communications. This article both demonstrates the expressiveness of the pNet model and formally speci fies the complete process of the generation of a behavioural model for a distributed component system. The behavioural models we build are precise enough to allow veri fication by finite instantiation and model-checking, but also to use veri fication techniques for infi nite systems.; Les composants logiciels fournissent une abstraction de programmation intéressante pour la conception modulaire d'applications complexes. Dans les systèmes répartis, les composants peuvent également être utilisés pour fournir une abstraction de la localisation des processus: chaque composant est une unité de déploiement qui peut être placée sur une machine différente. Dans cet article, nous considérons ce type de composants distribuées, faiblement couplés et communiquant par des appels asynchrones. Les composants fournissent également une abstraction commode pour vérifier le bon comportement des systèmes: ils fournissent un concept structurant qui facilite la vérification de ses propriétés. Cet article vise à fournir un support formel pour la génération de la sémantique comportementale des composants asynchrones. Nous utilisons le formalisme intermédiaire pNet pour exprimer la sémantique des composants hiérarchiques distribués communiquant de manière asynchrone par un mécanisme de requêtes. Nous formalisons également deux aspects fondamentaux des composants distribués: la reconfiguration et les communications de groupe. Cet article d'une part démontre l'expressivité du modèle pNet et d'autre part spécifie formellement le processus complet de la génération du modèle comportemental d'un système de composants distribués. Les modèles de comportement que nous construisons sont suffisamment précis pour permettre la vérification par instanciation finie et model-checking, mais aussi pour utiliser des techniques de vérification de systèmes infinis.

My research focuses on distributed programming models, more precisely using ob jects and components. In this area, I provided tools easing the programming of large-scale distributed applications and verifying their correct behaviour. To facilitate the programming of distributed applications, I contributed to the design and the development of languages with a high level of abstraction: active ob jects, algorithmic skeletons, components. To verify correction of the behaviour of an application, I have contributed to the creation of tools for specifying and verifying behavioural distributed applications. My work aims to provide a strong model of programming languages, libraries, and runtime environments provided to the developer, and to guarantee the safe behaviour of distributed applications. During my thesis, I developed the ASP calculus for modelling the behaviour of active ob jects and futures. Since, we created a functional version of this calculus and formalised it in Isabelle/HOL. I also strongly contributed to the definition of a distributed component model - the GCM (Grid Component Model) -, to its formalisation, and to its use for programming adaptive or autonomous components. Finally, I contributed to the specification and behavioural verification of programs based on active ob jects and components, in order to ensure their safe execution. Currently we are working both on a multi-threaded extension of the active ob ject model, better suited for multi-core machine, and on the use of formal methods to design and prove the correction of an algorithm for broadcast on CAN-like peer-to-peer networks (Content Addressable Network). This manuscript provides an overview of all these works.; Mes travaux de recherche portent sur les modèles de programmation distribuée, principalement par objets et composants. Dans ce domaine, j'ai travaillé à fournir des outils facilitant la programmation d'applications distribuées à large échelle et vérifiant la correction de leur comportement. Pour faciliter la programmation d'applications distribuées je me suis intéressé à la mise au point de langages avec un fort niveau d'abstraction: objets actifs, squelettes algorithmiques, composants. Afin de vérifier la correction du comportement d'une application j'ai collaboré à la mise au point d'outils de spécification et de vérification comportementales d'applications distribuées. Mes travaux ont pour but de fournir un modèle formel des langages de programmations, des bibliothèques, et des environnements d'exécution fournies au programmeur afin de garantir un comportement sûr des applications distribuées. Ma thèse m'a permis de mettre au point le calcul ASP modélisant lecomportement des objets actifs et des futurs. Depuis, nous avons créé une version fonctionnelle de ce calcul que nous avons modélisé en Isabelle/HOL. Aussi j'ai fortement contribué à la définition d'un modèle à composants distribués -- le GCM (Grid Component model)--, à sa formalisation et à son utilisation pour programmer des composants adaptables ou autonomes. Enfin, j'ai contribué à la spécification et la vérification comportementale des programmes utilisant des objets actifs et des composants afin de garantir la sûreté de leur exécution. Actuellement, nous travaillons à la fois à une extension multi-threadée du modèle à objets actifs mieux adaptée aux machines multi-coeurs, et à l'utilisation de méthodes formelles pour mettre au point et prouver la correction d'un algorithme de diffusion pour réseau pair-à-pair de type CAN (Content Adressable Network). Ce manuscrit fournit une vue d'ensemble de tous ces travaux.

My research focuses on distributed programming models, more precisely using ob jects and components. In this area, I provided tools easing the programming of large-scale distributed applications and verifying their correct behaviour. To facilitate the programming of distributed applications, I contributed to the design and the development of languages with a high level of abstraction: active ob jects, algorithmic skeletons, components. To verify correction of the behaviour of an application, I have contributed to the creation of tools for specifying and verifying behavioural distributed applications. My work aims to provide a strong model of programming languages, libraries, and runtime environments provided to the developer, and to guarantee the safe behaviour of distributed applications. During my thesis, I developed the ASP calculus for modelling the behaviour of active ob jects and futures. Since, we created a functional version of this calculus and formalised it in Isabelle/HOL. I also strongly contributed to the definition of a distributed component model - the GCM (Grid Component Model) -, to its formalisation, and to its use for programming adaptive or autonomous components. Finally, I contributed to the specification and behavioural verification of programs based on active ob jects and components, in order to ensure their safe execution. Currently we are working both on a multi-threaded extension of the active ob ject model, better suited for multi-core machine, and on the use of formal methods to design and prove the correction of an algorithm for broadcast on CAN-like peer-to-peer networks (Content Addressable Network). This manuscript provides an overview of all these works.; Mes travaux de recherche portent sur les modèles de programmation distribuée, principalement par objets et composants. Dans ce domaine, j'ai travaillé à fournir des outils facilitant la programmation d'applications distribuées à large échelle et vérifiant la correction de leur comportement. Pour faciliter la programmation d'applications distribuées je me suis intéressé à la mise au point de langages avec un fort niveau d'abstraction: objets actifs, squelettes algorithmiques, composants. Afin de vérifier la correction du comportement d'une application j'ai collaboré à la mise au point d'outils de spécification et de vérification comportementales d'applications distribuées. Mes travaux ont pour but de fournir un modèle formel des langages de programmations, des bibliothèques, et des environnements d'exécution fournies au programmeur afin de garantir un comportement sûr des applications distribuées. Ma thèse m'a permis de mettre au point le calcul ASP modélisant lecomportement des objets actifs et des futurs. Depuis, nous avons créé une version fonctionnelle de ce calcul que nous avons modélisé en Isabelle/HOL. Aussi j'ai fortement contribué à la définition d'un modèle à composants distribués -- le GCM (Grid Component model)--, à sa formalisation et à son utilisation pour programmer des composants adaptables ou autonomes. Enfin, j'ai contribué à la spécification et la vérification comportementale des programmes utilisant des objets actifs et des composants afin de garantir la sûreté de leur exécution. Actuellement, nous travaillons à la fois à une extension multi-threadée du modèle à objets actifs mieux adaptée aux machines multi-coeurs, et à l'utilisation de méthodes formelles pour mettre au point et prouver la correction d'un algorithme de diffusion pour réseau pair-à-pair de type CAN (Content Adressable Network). Ce manuscrit fournit une vue d'ensemble de tous ces travaux.

International audience; A natural way to benefit from distribution is via asynchronous invocations to methods or services. Upon invocation, a request is enqueued at the destination side and the caller can continue its execution. But a question remains: “what if one wants to manipulate the result of an asynchronous invocation?” First-class futures provide a transparent and easy-to-program answer: a future acts as the placeholder for the result of an asynchronous invocation and can be safely transmitted between processes while its result is not needed. Synchronization occurs automatically upon an access to the result. As references to futures disseminate, a strategy is necessary to propagate the result of each request to the processes that need it. This paper studies the efficient transmission of results: it presents three strategies in a semi-formal manner, providing experimental results highlighting their benefits and drawbacks.

Several paradigms exist for distributed computing, this paper tries to provide a sound foundation for autonomous objects communicating in a very structured way. We define ASPfun, a calculus of functional objects, behaving autonomously, and communicating by a request-reply mechanism: requests are method calls handled asynchronously, futures represent awaited results for requests, and replies return the result of a request to an object that holds the corresponding future. This report first presents the ASPfun calculus and its semantics. Secondly we provide a type system for ASPfun, which ensure the ``progress'' property: while there is a request that is not reduced to a value, the computation can continue. ASPfun and its properties have been formalized and proved using the Isabelle theorem prover.

The objective of this thesis is to design an object calculus that allows one to write parallel and distributed applications, particularly on wide range networks, while ensuring good properties. This calculus is named ASP : Asynchronous Sequential Processes. The main characteristics of ASP are: asynchronous communications, futures, and a sequential execution within each process. ASP presents strong confluence and determinism properties, proved in a context as general as possible within this thesis. A first design decision is the absence of sharing : objects live in disjoint activities. An activity is a set of objects managed by a unique process and a unique active object. Active objects are accessible through global/distant references. They communicate through asynchronous method calls with futures. A future is a global reference representing a result not yet computed. This thesis models those aspects, their main properties, and the consequences of these mechanisms on the deterministic behavior of programs. The main result consists in a confluence property and its application to the identification of a set of programs behaving deterministically. From a practical point of view, ASP can also be considered as a model of the ProActive library. This library provides tools for developing parallel and distributed applications in Java.; L'objectif de cette thèse est de concevoir un calcul d'objets permettant d'écrire des applications parallèles et distribuées, en particulier dans un cadre à grande échelle, tout en assurant de bonnes propriétés. Le calcul proposé s'intitule ASP : Asynchronous Sequential Processes. Les principales caractéristiques de ce calcul sont : des communications asynchrones, la présence de futurs et une exécution séquentielle dans chacun des processus. Ce calcul exhibe de fortes propriétés de confluence et de déterminisme. Cette thèse a donc aussi pour objectif de prouver de telles propriétés dans un cadre aussi général que possible. ASP est basé sur une répartition des objets en différentes activités disjointes. Une activité est un ensemble d'objets gérés par un unique processus. Les objets actifs sont des objets accessibles par des références globales/distantes. Ils communiquent à travers des appels de méthodes asynchrones avec un mécanisme de futurs. Un futur est une référence globale désignant un résultat qui n'est pas encore calculé. Cette thèse modélise ces différents aspects, leurs principales propriétés et les conséquences de ces mécanismes sur la notion de comportement déterministe des programmes. Le résultat principal consiste en une propriété de confluence et son application à l'identification d'un ensemble de programmes se comportant de façon déterministe. Du point de vue pratique, ASP peut aussi être considéré comme une modélisation de la librairie ProActive. Cette librairie fournit des outils pour développer des applications parallèles et distribuées en Java.