Lost in abstraction: Monotonicity in multi-threaded programs

详细信息    查看全文

• 作者：Alexander Kaiser^a ; Daniel Kroening^a ; Thomas Wahl^b ;
• 关键词：Multi-threaded software ; Parameterized verification ; Monotonicity ; Predicate abstraction
• 刊名：Information and Computation
• 出版年：2017
• 出版时间：February 2017
• 年：2017
• 卷：252
• 期：Complete
• 页码：30-47
• 全文大小：672 K
• 卷排序：252

文摘

Monotonicity in concurrent systems stipulates that, in any global state, system actions remain executable when new processes are added to the state. This concept is both natural and useful: if every thread's memory is finite, monotonicity often guarantees the decidability of safety properties even when the number of running threads is unknown. In this paper, we show that finite-data thread abstractions for model checking can be at odds with monotonicity: predicate-abstracting monotone software can result in non-monotone Boolean programs — the monotonicity is lost in the abstraction  . As a result, pertinent well-established safety checking algorithms for infinite-state systems become inapplicable. We demonstrate how monotonicity in the abstraction can be restored, without affecting safety properties. This improves earlier approaches of enforcing monotonicity via overapproximations. We implemented our solution in the unbounded-thread model checker monabsmonabs and applied it to numerous concurrent programs and algorithms, whose predicate abstractions are often fundamentally beyond existing tools.