A Geometric View of Partial Order Reduction

Eric Goubault, Tobias Heindel, Samuel Mimram

Research output: Contribution to journalArticlepeer-review

Abstract

Verifying that a concurrent program satisfies a given property, such as deadlock-freeness, is computationally difficult. Naive exploration techniques are facing the state space explosion problem: they consider an exponential number of interleavings of parallel threads (relative to the program size). Partial order reduction is a standard method to address this difficulty. It is based on the observation that certain sets of instructions, called persistent sets, are not affected by other concurrent instructions and can thus always be explored first when searching for deadlocks. More recent models of concurrent processes use directed topological spaces: states are points, computations are paths, and equivalent interleavings are homotopic. This geometric approach applies theoretical results of algebraic topology to improve verification. Despite the very different origin of the approaches, the paper compares partial-order reduction with a construction of the geometric approach, the category of future components. The main result, which shows that the two techniques make essentially the same use of persistent transitions, is of foundational interest and aims for cross-fertilization of the two approaches to improve verification methods for concurrent programs.
Original languageEnglish
Pages (from-to)179-195
Number of pages17
JournalElectronic Notes in Theoretical Computer Science
Volume298
DOIs
Publication statusPublished - 4 Nov 2013

Fingerprint

Dive into the research topics of 'A Geometric View of Partial Order Reduction'. Together they form a unique fingerprint.

Cite this