Modèle n-synchrone pour la programmation de réseaux de Kahn à mémoire bornée
Institution:
Paris 11Disciplines:
Directors:
Abstract EN:
In this thesis, we are interested in models and languages to program stream processing applications with real-time constraints, such as multimedia applications. They manipulate infinite data flows, on which they apply successive operations. These systems can be represented by Kahn Process Networks. In this model, computation nodes are executed concurrently and communicate through unbounded buffers. It has the advantage of being deterministic and yet allowing to express the intrinsic parallelism of applications. Nevertheless, it does not guarantee that the system is deadlock free and that it can be executed with bounded memory. Dataflow Synchronous Languages are a simple framework to program Kahn Process Networks without buffers. They offer strong guarantees on memory bounds and absence of deadlocks. The downside of these guarantees is a lack of flexibility in the composition of flows: communication must be done synchronously, that is without buffers. The n-synchronous model is an extension of the synchronous model that relaxes the synchronous constraint in a controlled way. It allows a more flexible composition while preserving static guarantees given by synchronous languages. We present a n-synchronous language and we focus on the analysis which statically checks that a program can be executed with bounded buffers and automatically computes those sizes.
Abstract FR:
Dans cette thèse, nous nous intéressons aux modèles et aux langages pour la programmation d'applications de traitement de flux ayant des contraintes de temps-réel, comme les applications multimédias. Elles manipulent des flots de données infinis, auxquels sont appliquées des opérations successives. Ces systèmes peuvent être représentés par des réseaux de Kahn. Dans ce modèle, des noeuds de calcul s'exécutent de manière concurrente et communiquent à travers des buffers infinis. Son intérêt est d'être déterministe tout en permettant d'exprimer le parallélisme intrinsèque aux applications. Néanmoins, il présente l'inconvénient de ne pas donner de garanties sur l'absence d'interblocage et sur le caractère borné des buffers. Les langages synchrones flot de données fournissent un cadre simple pour la programmation de réseaux de Kahn sans buffers. Ils offrent des garanties fortes comme l'absence de blocage et un besoin en mémoire bornée. La contrepartie de ces garanties est un manque de souplesse dans la composition des flots : celle-ci doit être réalisée sans buffers. Le modèle n-synchrone est une extension du modèle synchrone qui relâche cette contrainte de manière contrôlée. Il permet une composition plus souple, tout en conservant les garanties statiques offertes par les langages synchrones. Nous présentons un langage qui met en oeuvre le modèle n-synchrone. En particulier, nous détaillons les analyses permettant de vérifier statiquement qu'un programme est exécutable avec des buffers bornés et de calculer automatiquement leur taille.