Résumé de rapport du LIF

Téléchargement / Download : pdf 272k , ps.gz 244k , bibtex

Abstract

We develop new methods to statically bound the resources needed for the execution of systems of concurrent, interactive threads.

Our study is concerned with a synchronous model of interaction based on cooperative threads whose execution proceeds in synchronous rounds called instants. Our contribution is a system of compositional static analyses to guarantee that each instant terminates and to bound the size of the values computed by the system as a function of the size of its parameters at the beginning of the instant.

Our method generalises an approach designed for first-order functional languages that relies on a combination of standard termination techniques for term rewriting systems and an analysis of the size of the computed values based on the notion of quasi-interpretation.

We show that these two methods can be combined to obtain an explicit polynomial bound on the space needed for the execution of the system during an instant. We also provide evidence for the expressivity of our synchronous programming model and describe a bytecode for a related virtual machine.

Keywords

Resource control, synchronous programming, quasi-interpretation, termination, term rewriting systems.

Résumé

Nous présentons une nouvelle approche permettant de borner statiquement les ressources nécessaires à l'exécution de systèmes de threads interactifs et concurrents.

Notre étude porte sur un modèle d'interaction synchrone basé sur des threads coopératifs dont l'exécution procède par "segments synchrones" successifs appelés instants. Notre contribution est un système d'analyses statiques (toutes compositionnelles) qui garantissent que chaque instant se termine et qui permettent de borner la taille des valeurs calculées par le système en fonction de la taille de ses paramètres au début de l'instant.

Notre méthode généralise une approche conçue pour des langages de programmation fonctionnels de premier ordre qui se fonde sur la combinaison de techniques standards pour la preuve de terminaison de systèmes de réécriture et d'une analyse de la taille des valeurs calculées basée sur la notion de quasi-interprétation.

Nous prouvons que ces méthodes peuvent être combinées pour extraire de chaque programme un polynôme qui borne l'espace requis pour l'exécution du système pendant un instant. Nous montrons également, à l'aide d'exemples, l'expressivité de notre modèle de programmation synchrone et nous décrivons un possible langage de bytecode pour une machine virtuelle associée.

Mots clés

Contrôle de ressources, programmation synchrone, quasi-interprétations, terminaison, systèmes de réécriture.

Bibtex

@TECHREPORT{22-2004,
    AUTHOR	= {Roberto M. Amadio and Silvano Dal Zilio},
    TITLE	= {{Resource Control for Synchronous Cooperative Threads}},
    INSTITUTION	= {{LIF}},
    ADDRESS	= {Marseille, France},
    TYPE	= {Research report},
    NUMBER	= {22-2004},
    MONTH	= {May},
    YEAR	= {2004},
    NOTE	= {http://pageperso.lif.univ-mrs.fr/~edouard.thiel/RESP/Rapports/22-2004.html},
}