Quasi-optimal partial order reduction
Formal Methods in System Design(2020)
摘要
dynamic partial order reduction (DPOR) algorithm is optimal when it always explores at most one representative per Mazurkiewicz trace. Existing literature suggests that the reduction obtained by the non-optimal, state-of-the-art Source-DPOR (SDPOR) algorithm is comparable to optimal DPOR. We show the first program with 𝒪(n) Mazurkiewicz traces where SDPOR explores 𝒪(2^n) redundant schedules. We furthermore identify the cause of this blow-up as an NP-hard problem. Our main contribution is a new approach, called Quasi-Optimal POR, that can arbitrarily approximate an optimal exploration using a provided constant k . We present an implementation of our method in a new tool called Dpu using specialised data structures. Experiments with Dpu , including Debian packages, show that optimality is achieved with low values of k , outperforming state-of-the-art tools.
更多查看译文
关键词
Program analysis,Dynamic analysis,Partial-order reduction,Non-interleaving semantics
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要