Analysis of synchronisation patterns in active object based on behavioural types
Analyse de synchronisation dans les objets actifs basée sur les types comportementaux
Résumé
The active object concept is a powerful computational model for defining distributed and concurrent systems.
This model has recently gained prominence, largely thanks to its simplicity and its abstraction level.
Thanks to this characteristics, the Active object model help the programmer to implement large scale systems, with an higher degree of parallelism and better performance.
The literature presents many models based on active objects and each one is characterised by a different level of transparency for the programmer.
In this work we study an Active object model with no explicit future type and with wait-by-necessity synchronisations, a lightweight technique that synchronises invocations when the corresponding values are strictly needed.
Implicit future type and wait-by-necessity synchronisations entails the highest level of transparency that an Active object model can provide.
Although high concurrency combined with a high level of transparency leads to good performances, they also make the system more prone to problems such as deadlocks.This is the reason that led us to study deadlock analysis in this active objects model.
The development of our deadlock analysis is divided in two main works, which are presented in an incremental order of complexity. Each of these works faces a different difficulty of the proposed active object language.
In the first work we focus on the implicit synchronisation on the availability of some value (where the producer of the value might be decided at runtime), whereas previous work allowed only explicit synchronisation on the termination of a well-identified request.
This way we are able to analyse the data-flow synchronisation inherent to languages that feature wait-by-necessity.
In the second work we present a static analysis technique based on effects and behavioural types for deriving synchronisation patterns of stateful active objects and verifying the absence of deadlocks in this context.
This is challenging because active objects use futures to refer to results of pending asynchronous invocations and because these futures can be stored in object fields, passed as method parameters, or returned by invocations.
Our effect system traces the access to object fields, thus allowing us to compute behavioural types that express synchronisation patterns in a precise way.
For both analysis we provide a type-system and a solver inferring the type of a program so that deadlocks can be identified statically.
As a consequence we can automatically verify the absence of deadlocks in active object based programs with wait-by-necessity synchronisations and stateful active objects.
Le concept d'objet actif est un modèle de calcul puissant utilisé pour définir des systèmes distribués et concurrents.
Ce modèle a récemment gagné en importance, en grande partie grâce à sa simplicité et à son niveau d'abstraction.
Grâce à ces caractéristiques, le modèle d'objet actif aide le programmeur à implémenter des grands systèmes, avec un haut degré de parallélisme et de meilleures performances.
La littérature présente de nombreux modèles basés sur des objets actifs et chacun est caractérisé par un différent niveau de transparence pour le programmeur.
Dans ce travail, nous étudions un modèle d'objet actif sans type futur explicite et avec 'attente par nécessité', une technique qui déclenche uns synchronisation sur la valeur retournée par une invocation lorsque celle ci est strictement nécessaires. Les futurs implicites et l'attente par nécessité impliquent le plus haut niveau de transparence qu'un modèle d'objet actif peut fournir.
Bien que la concurrence élevée combinée à un haut niveau de transparence conduise à de bonnes performances, elles rendent le système plus propice à des problèmes comme les deadlocks.
C'est la raison qui nous a conduit à étudier l'analyse de deadlocks dans ce modèle d'objets actifs.
Le développement de notre analyse de les deadloks est divisé en deux travaux principaux, qui sont présentés dans un ordre de complexité croissant.
Chacun de ces travaux est confronté à une difficulté différente de la langue d'objet active proposée.
Dans le premier travail, nous nous concentrons sur la synchronisation implicite sur la disponibilité d'une certaine valeur (où le producteur de la valeur pourrait être décidé au moment de l'exécution), alors que les travaux précédents n'autorisaient que la synchronisation explicite lors de la fin d'une requête bien identifiée. De cette façon, nous pouvons analyser la synchronisation des flux de données inhérente aux langues qui permettent une attente par nécessité.
Dans le deuxième travail, nous présentons une technique d'analyse statique basée sur des effets et des types comportementaux pour dériver des modèles de synchronisation d'objets actifs et confirmant l'absence de deadlock dans ce contexte.
Cela est difficile parce que les objets actifs utilisent des futurs pour référencer les résultats d'invocations asynchrones en attente et que ces futurs peuvent être stockés dans des champs d'objet, passées comme paramètre de méthode ou retournés par des méthodes.
Notre système d'effets trace l'accès aux champs d'objet, ce qui nous permet de calculer des types comportementaux qui expriment des modèles de synchronisation de manière précise.
Pour les deux analyses, nous fournissons un système de type et un solveur dont ils déduisent le type du programme afin que les deadlocks puissent être identifiés de manière statique. En conséquence, nous pouvons vérifier automatiquement l'absence de blocages dans des programmes basés sur des objets actifs avec des synchronisations d'attente par nécessité et des objets actifs dotés d’un état interne.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...