Counting dynamically synchronizing processes

详细信息    查看全文

• 作者：Zeinab Ganjei ; Ahmed Rezine ; Petru Eles…
• 关键词：Parameterized verification ; Counting predicate ; Barrier synchronization ; Deadlock freedom ; Multithreaded programs ; Counter abstraction ; Predicate abstraction ; Constrained monotonic abstraction
• 刊名：International Journal on Software Tools for Technology Transfer (STTT)
• 出版年：2016
• 出版时间：October 2016
• 年：2016
• 卷：18
• 期：5
• 页码：517-534
• 全文大小：1,821 KB
• 刊物类别：Computer Science
• 刊物主题：Software Engineering
  Software Engineering, Programming and Operating Systems
  Theory of Computation
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1433-2787
• 卷排序：18

文摘

We address the problem of automatically establishing correctness for programs generating an arbitrary number of concurrent processes and manipulating variables ranging over an infinite domain. The programs we consider can make use of the shared variables to count and synchronize the spawned processes. This allows them to implement intricate synchronization mechanisms, such as barriers. Automatically verifying correctness, and deadlock freedom, of such programs is beyond the capabilities of current techniques. For this purpose, we make use of counting predicates that mix counters referring to the number of processes satisfying certain properties and variables directly manipulated by the concurrent processes. We then combine existing works on counter, predicate, and constrained monotonic abstraction and build a nested counter example based refinement scheme for establishing correctness (expressed as non-reachability of configurations satisfying counting predicates formulas). We have implemented a tool (Pacman, for predicated constrained monotonic abstraction) and used it to perform parameterized verification on several programs whose correctness crucially depends on precisely capturing the number of processes synchronizing using shared variables.