Sheep in wolf's Clothing: Implementation Models for Dataflow Multi-Threaded Software

International audienceConcurrent programming is notoriously difficult, especially in constrained embeddedcontexts. Threads, in particular, are wildly nondeterministic as a model of computation, anddifficult to analyze in the general case. Fortunately, it is often the case that multi-threaded,semaphore-synchronized embedded software implements high-level functional specifications writtenin a deterministic data-flow language such as Scade or (safe subsets of) Simulink. We claim thatin this case the implementation process should build not just the multi-threaded C code, but (firstand foremost) a richer model exposing the dataflow organization of the computations performed bythe implementation. From this model, the C code is extracted through selective pretty-printing,while knowledge of the data-flow organization facilitates analysis. We propose a language fordescribing such implementation models that expose the data-flow behavior (the sheep) hidingunder the form of a multi-threaded program (the wolf). The language allows the representationof efficient implementations featuring pipelined scheduling and optimized memory allocation andsynchronization. We show applicability on a large-scale industrial avionics case study and on acommercial many-core.La programmation concurrente est une discipline difficile, particulièrement dansun contexte de systèmes embarqués. Les threads, en particulier, sont un modèle de calcul non-déterministe et difficile à analyser dans le cas général. Heureusement, les logiciels embarquésmulti-threadés synchronisés par sémaphores sont souvent des implémentations de spécificationsfonctionnelles de haut niveau écrites dans un langage flot-de-données déterministe comme Scadeou (un sous-ensemble sûr de) Simulink. Dans ce cas, le processus d’implémentation devrait, nonseulement construire le code C multi-threadé de l’implémentation, mais avant tout un modèleplus riche exposant l’organisation du flot-de-données des calculs effectués par le code. De cemodèle, le code C peut être extrait par du simplepretty printing. En même temps, la structureflot-de-donnée facilite l’analyse. Nous proposons un langage pour la description de tels mod-èles d’implémentations qui exposent le comportement flot-de-donnée (la brebis) déguisé en unprogramme multi-threadé (le loup). Ce langage permet une représentation d’implémentations ef-ficaces avec ordonnancement pipeliné et allocation mémoire et synchronisations optimisées. Nousmontrons son application sur un cas d’étude de l’industrie aéronautique et sur une plateformemany-coeurs commercial