Symbolic Executions of Symmetrical Parallel Programs

I. Vernier

Masi-IBP 1996/15: Rapport de Recherche Masi / Masi research reports
8 pages - Mai/May 1996 - Document en anglais.

PostScript : 38 Ko /Kb

Titre français : Exécutions Symboliques de Programmes Parallèles Symétriques
Titre anglais : Symbolic Executions of Symmetrical Parallel Programs

Résumé : Nous proposons un algorithme pour exécuter symboliquement des programmes parallèles définis pour un nombre fini mais non déterminé de processus. Habituellement, on instancie les programmes avant de les exécuter; le nombre de processus est fixé. Nous exploitons le comportement symétrique des processus pour exécuter simultanément tous les programmes instanciés. Nous définissons des états symboliques qui représentent des ensembles d'états d'un nombre infini de programmes instanciés. Nous calculons simultanément tous les successeurs des états représentés pas un état symbolique. Après une exécution exhaustive, nous construisons un graphe qui représente tous les états accessibles et exécutions possibles des programmes instanciés. Nous pouvons explorer ce graphe symbolique pour vérifier des propriétés exprimées par des formules de logique temporelle.

Abstract : We propose an algorithm to execute symbolically parallel programs with an unknown number of processes. Usually one instantiates the programs before their execution, i.e., one fixes the number of processes. We exploit the symmetrical behaviors of the processes to execute simultaneously all the instantiated programs. We define symbolic states that represent sets of states of an infinite number of instantiated programs. We compute simultaneously all the successors of states represented by a symbolic one. After an exhaustive execution, we build a graph that represents all the reachable states and possible executions of the instantiated programs. We can explore this symbolic graph to verify properties expressed with temporal logic formulas.

Mots-clés : Reseaux de Petri, execution symbolique, symétries, programmes paramétrés

Key-words : Petri nets, symbolic execution, symmetries, parameterized programs

Publications internes Masi 1996 / Masi research reports 1996