Abstract
The classical problem of deadlock detection for concurrent programs has traditionally been accomplished by symbolic methods or by search of a state transition system. This work examines an approach that uses geometric semantics involving the topological notion of dihomotopy to partition the state space into components, followed by search of a reduced state space. Prior work partitioned the state-space inductively. in this work, a decomposition technique motivated by recursion coupled with a search guided by the decomposition is shown to effectively reduce the size of state transition systems. the reduced state space yields asymptotic improvement in overall runtime for verification. a prototype implementation of this method is introduced here, including a description of its theoretical foundation and its performance benchmarked against the SPIN model checker. © 2010 IEEE.
Recommended Citation
D. A. Cape et al., "Dihomotopic Deadlock Detection Via Progress Shell Decomposition," Proceedings - 2nd International Conference on Advances in System Testing and Validation Lifecycle, VALID 2010, pp. 20 - 25, article no. 5617168, Institute of Electrical and Electronics Engineers, Dec 2010.
The definitive version is available at https://doi.org/10.1109/VALID.2010.17
Department(s)
Computer Science
Keywords and Phrases
Deadlock; Dihomotopy; Verification
International Standard Book Number (ISBN)
978-076954146-4
Document Type
Article - Conference proceedings
Document Version
Citation
File Type
text
Language(s)
English
Rights
© 2024 Institute of Electrical and Electronics Engineers, All rights reserved.
Publication Date
13 Dec 2010
