摘要: De nos jours, l’informatique des programmes séquentiels laisse de plus en plus sa place au parallèlisme, qu’il s’ agisse d’un simple téléphone (les smartphones modernes ont bien souvent quatre coeurs), d’un ordinateur de bureau ou d’un super-calculateur.Cependant, si la programmation séquentielle a évolué pour donner lieux à des méthodes de programmation robustes et de haut niveau, ce n’est pas encore le cas pour la programmation parallèle, qui utilise bien souvent des langages de bas niveau, avec des coûts de débogage importants. De plus, un échecs lors d’un calcul parallèle a généralement un impact plus important que pour un programme séquentiel, par exemple s’ il faut ré-exécuter un calcul sur un super-calculateur. Pour ces raisons, il semble essentiel de pouvoir vérifier formellement les programmes parallèles. Pour les programmes séquentiels, les méthodes existent et sont bien rodées, mais plusieurs difficultés compliquent la tache dans le cas du parallèlisme. Les programmes ont une complexité accrue. Comme le code s’ exécute simultanément sur plusieurs processeurs, il y a un entrelacement des instructions, et plusieurs scénarios d’exécution sont possibles, d’où un non-déterminisme du résultat. Il est plus facile pour le programmeur de faire des erreurs lors de la conception du programme, et il est également plus difficile de tester le programme fini dans tous les cas possibles.
参考文章(0)