A geometric view of partial order reduction

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.
Document type :
Journal articles
Complete list of metadatas

https://hal-cea.archives-ouvertes.fr/cea-01836517
Contributor : Léna Le Roy <>
Submitted on : Thursday, July 12, 2018 - 1:24:43 PM
Last modification on : Friday, April 12, 2019 - 10:20:14 AM

Links full text

Identifiers

Collections

CEA | DRT | LIST

Citation

E. Goubault, T. Heindel, S. Mimram. A geometric view of partial order reduction. Electronic Notes in Theoretical Computer Science, Elsevier, 2013, 298, pp.179-195. ⟨10.1016/j.entcs.2013.09.013⟩. ⟨cea-01836517⟩

Share

Metrics

Record views

44