Dynamic Partial Order Reduction Based on Interference Solution

Research Square (Research Square)(2023)

引用 0|浏览0
暂无评分
摘要
Abstract In verifying the process of concurrent programs, dynamic partial order reduction (DPOR) exhaustively explores all the interactions of the equivalent execution traces in the concurrent system through dynamic judgment. Existing DPOR algorithms strive for optimal exploration (i.e., exploring only one interleaving per equivalence class), leading to exponential redundancy in the interleaving, state-space explosion, and memory overflow. In this study, the Interference Solution (IntSo) algorithm is proposed to achieve linear memory consumption by exploring only one interleaving per equivalence class through the exchange of causally-happened-before (CHB) conflicting relationships. In the sequential consistency memory model, the IntSo algorithm realizes parallelism while curtailing time and memory consumption in data-independent scenarios, as well as maximum path lengths. Empirical validation using GenMC demonstrates that the IntSo algorithm compares favorably with state-of-the-art techniques in terms of time and memory, fulfills linear time complexity, and reduces memory consumption by more than 30%.
更多
查看译文
关键词
dynamic partial order reduction,interference
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要