Generating Representative Executions [Extended Abstract]

Hendrik Maarand
Tarmo Uustalu

Analyzing the behaviour of a concurrent program is made difficult by the number of possible executions. This problem can be alleviated by applying the theory of Mazurkiewicz traces to focus only on the canonical representatives of the equivalence classes of the possible executions of the program. This paper presents a generic framework that allows to specify the possible behaviours of the execution environment, and generate all Foata-normal executions of a program, for that environment, by discarding abnormal executions during the generation phase. The key ingredient of Mazurkiewicz trace theory, the dependency relation, is used in the framework in two roles: first, as part of the specification of which executions are allowed at all, and then as part of the normality checking algorithm, which is used to discard the abnormal executions. The framework is instantiated to the relaxed memory models of the SPARC hierarchy.

In Vasco T. Vasconcelos and Philipp Haller: Proceedings Tenth Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES 2017), Uppsala, Sweden, 29th April 2017, Electronic Proceedings in Theoretical Computer Science 246, pp. 39–48.
Published: 8th April 2017.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: