基于模型检测的并发程序分析综述

摘要

程序分析可以被看作抽象解释的模型检测，这使得程序分析的系统化方法成为可能。并发程序日益重要，在多核平台和分布式系统有着广泛的应用。而并发程序分析仍然有巨大的困难，实践上的复杂性和理论上的不可判定性都使得程序分析难以简单进行。文献[19]指出即使只有两个递归线程的交互，断言检测也是不可判定的。为了克服这类障碍，一些并发程序的静态分析方法被提了出来。对基于模型检测的并发程序分析给出一个详尽的综述，包括使用的数学模型、已有工具、可判定以及不可判定结果。%Program analysis can be regarded as the model checking of abstract interpretation, this view makes the systematic way of programanalysis possible.Concurrent programming is becoming increasingly important with the trends that to be widely used in multi-core platforms and distributed systems.However, concurrent programming analysis raises huge difficulties, since the practical complexities and theoretical undecidability.Literature [ 19 ] gives a negative result that, even when the case is as simple as two interacted threads with recursionallowed, the checking assertions are still undecidable.To bypass this undecidable barrier, different techniques of static analysis of concurrent programs are proposed.We give a detailed survey on model checking-based concurrent programming analyses, including mathematicalmodels under use, existing tools, decidable and undecidable results.