Partial-order methods accelerate the verification of concurrent programs. These methods are based on a concept of independence of actions, which induces an equivalence between different program runs. The equivalence allows for the construction of a reduced transition system that represents all runs up to this equivalence. Such a system can be orders of magnitude smaller than the full transition system representing all possible runs, while still containing all relevant information. We propose a new partial-order reduction method for concurrent acyclic programs that use variables and locks. Our algorithm is derived from first principles, suggesting it can be readily adapted to other settings. As our evaluation demonstrates, the algorithm offers substantial gains over existing partial-order methods.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Revisiting Stateful Partial-Order Reduction

  • Frédéric Herbreteau,
  • Gérald Point,
  • Gautham Viswanathan,
  • Igor Walukiewicz

摘要

Partial-order methods accelerate the verification of concurrent programs. These methods are based on a concept of independence of actions, which induces an equivalence between different program runs. The equivalence allows for the construction of a reduced transition system that represents all runs up to this equivalence. Such a system can be orders of magnitude smaller than the full transition system representing all possible runs, while still containing all relevant information. We propose a new partial-order reduction method for concurrent acyclic programs that use variables and locks. Our algorithm is derived from first principles, suggesting it can be readily adapted to other settings. As our evaluation demonstrates, the algorithm offers substantial gains over existing partial-order methods.