一句话：提出结合上下文敏感与观察者条件独立性的DPOR算法，显著提升无状态模型检验效率。
动态偏序归约（DPOR）用于无状态模型检验，通过步骤独立性避免等价执行序列。已有工作分别提出上下文敏感DPOR和带观察者的最优DPOR：前者根据 p·t 与 t·p 所得状态判断独立，后者仅在存在未来事件观察操作时才视其为依赖。本文提出 Optimal Context-Sensitive DPOR with Observers，将两类条件独立性结合并挖掘协同效应，从而更精确地判定可交换步骤并减少冗余探索。实验表明，该算法相对现有方法有显著性能提升，且收益随输入规模增大呈指数级增长。
Dynamic Partial Order Reduction (DPOR) algorithms are used in stateless model checking to avoid the exploration of equivalent execution sequences. DPOR relies on the notion of independence between execution steps to detect equivalence. Recent progress in the area has introduced more accurate ways to detect independence: Context-Sensitive DPOR considers two steps p and t independent in the current state if the states obtained by executing p · t and t · p are the same; Optimal DPOR with Observers makes their dependency conditional to the existence of future events that observe their operations. We introduce a new algorithm, Optimal Context-Sensitive DPOR with Observers, that combines these two notions of conditional independence, and goes beyond them by exploiting their synergies. Experimental evaluation shows that our gains increase exponentially with the size of the considered inputs.
DOI 原文 ·
@inproceedings{paperbot5368,
title = {Optimal context-sensitive dynamic partial order reduction with observers},
author = {Elvira Albert and Maria Garcia de la Banda and Miguel Gómez-Zamalloa and Miguel Isabel and Peter J. Stuckey},
booktitle = {ISSTA},
year = {2019},
doi = {10.1145/3293882.3330565}
}