Efficient state-space exploration for asynchronous distributed programs ˸ Adapting unfolding-based dynamic partial order reduction to MPI programs
Exploration efficace de l'espace d'états adaptée aux programmes distribués asynchrone ˸ adaptation de la réduction d'ordre partiel basée sur les dépliages pour les programmes MPI
Résumé
Distributed message passing applications are in the mainstream of information technology since they exploit the power of parallel computer systems to produce higher performance. Designing distributed programs remains challenging because developers have to reason about concurrency, non-determinism, data distribution… that are main characteristics of distributed programs. Besides, it is virtually impossible to ensure the correctness of such programs via classical testing approaches since one may never successfully reach the execution that leads to unwanted behaviors in the programs. There is thus a need for more powerful verification techniques. Model-checking is one of the formal methods that allows to verify automatically and effectively some properties on models of computer systems by exploring all possible behaviors (states and transitions) of the system model. However, state spaces increase exponentially with the number of concurrent processes, leading to “state space explosion”.Unfolding-based Dynamic Partial Order Reduction (UDPOR) is a recent technique mixing Dynamic Partial Order Reduction (DPOR) with concepts of concurrency theory such as unfoldings to efficiently mitigate state space explosion in model-checking of concurrent programs. It is optimal in the sense that each Mazurkiewicz trace, i.e. a class of interleavings equivalent by commuting adjacent independent actions, is explored exactly once. And it is applicable to running programs, not only models of programs.The thesis aims at adapting UDPOR to verify asynchronous distributed programs (e.g. MPI programs) in the setting of the SIMGRID simulator of distributed applications. To do so, an abstract programming model of asynchronous distributed programs is defined and formalized in the TLA+ language, allowing to precisely define an independence relation, a main ingredient of the concurrency semantics. Then, the adaptation of UDPOR, involving the construction of an unfolding, is made efficient by a precise analysis of dependencies in the programming model, allowing efficient computations of usually costly operation. A prototype implementation of UDPOR adapted to distributed asynchronous programs has been developed, giving promising experimental results on a significant set of benchmarks.
Les applications de transmission de messages distribués font partie du courant dominant des technologies de l'information car elles exploitent la puissance des systèmes informatiques parallèles pour produire des performances plus élevées. La conception de programmes distribués reste difficile car les développeurs doivent raisonner sur la concurrence, le non-déterminisme, la distribution de données… qui sont les principales caractéristiques des programmes distribués. En outre, il est pratiquement impossible de garantir l'exactitude de tels programmes via des approches de test classiques, car il est possible que l'on n'atteigne jamais avec succès l'exécution qui conduit à des comportements indésirables dans les programmes. Il existe donc un besoin de techniques de vérification plus puissantes. La vérification des modèles est l'une des méthodes formelles qui permet de vérifier automatiquement et efficacement certaines propriétés des modèles de systèmes informatiques en explorant tous les comportements possibles (états et transitions) du modèle de système. Cependant, les espaces d'état augmentent de façon exponentielle avec le nombre de processus simultanés, conduisant à une «explosion de l'espace d'état» .La réduction dynamique de l'ordre partiel basée sur le dépliage (UDPOR) est une technique récente mélangeant la réduction dynamique de l'ordre partiel (DPOR) avec des concepts de théorie de la concurrence tels que dépliages pour atténuer efficacement l'explosion de l'espace d'états lors de la vérification des modèles de programmes simultanés. Il est optimal dans le sens où chaque trace de Mazurkiewicz, c'est-à-dire une classe d'entrelacements équivalents en commutant des actions indépendantes adjacentes, est explorée exactement une fois. Et elle s'applique aux programmes en cours d'exécution, pas seulement aux modèles de programmes.La thèse vise à adapter UDPOR pour vérifier les programmes distribués asynchrones (par exemple les programmes MPI) dans le cadre du simulateur SIMGRID d'applications distribuées. Pour ce faire, un modèle de programmation abstrait de programmes distribués asynchrones est défini et formalisé en langage TLA +, permettant de définir avec précision une relation d'indépendance, ingrédient principal de la sémantique concurrentielle. Ensuite, l'adaptation de l'UDPOR, impliquant la construction d'un dépliage, est rendue efficace par une analyse précise des dépendances dans le modèle de programmation, permettant des calculs efficaces d'opérations habituellement coûteuses. Un prototype d'implémentation d'UDPOR adapté aux programmes asynchrones distribués a été développé, donnant des résultats expérimentaux prometteurs sur un ensemble significatif de références.
Origine : Version validée par le jury (STAR)
Loading...