Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions
Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions
复制标题
使用关系干扰抽象对并发程序进行精确的线程模块化抽象解释
DOI：
10.1007/978-3-319-52234-0_21
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
A. Miné
中科院分区：
文献类型：
--
作者：
Raphaël Monat;A. Miné
我们通过对多线程程序中的数字属性进行抽象解释来进行静态分析。该分析是合理的（假设内存顺序一致），通过选择抽象域进行参数化，并且为了扩展，它是模块化的，因为它单独迭代每个线程（可能多次）而不是迭代它们的乘积。我们以之前的工作为基础，将依赖保证验证方法形式化为具体的、基于固定点的语义，然后应用经典的数字抽象来独立地抽象线程状态和线程干扰。这产生了一种灵活的算法，允许大范围的精度与成本权衡，并且甚至能够推断流敏感和关系线程干扰。我们在简单语言的分析器原型中实现了我们的方法，并在两个或多个线程的几种经典互斥算法上进行了实验。我们的原型是用多面体域实例化的，并采用简单的控制分区来区分关键部分和周围的代码。它使用多面体关联所有线程的变量，这限制了其变量数量的可扩展性。尽管如此，初步实验以及与 ConcurInterproc 的比较表明，只要变量总数保持较小，模块化就可以扩展到大量线程实例。
We present a static analysis by abstract interpretation of numeric properties in multi-threaded programs. The analysis is sound (assuming a sequentially consistent memory), parameterized by a choice of abstract domains and, in order to scale up, it is modular, in that it iterates over each thread individually (possibly several times) instead of iterating over their product. We build on previous work that formalized rely-guarantee verification methods as a concrete, fixpoint-based semantics, and then apply classic numeric abstractions to abstract independently thread states and thread interference. This results in a flexible algorithm allowing a wide range of precision versus cost trade-offs, and able to infer even flow-sensitive and relational thread interference. We implemented our method in an analyzer prototype for a simple language and experimented it on several classic mutual exclusion algorithms for two or more threads. Our prototype is instantiated with the polyhedra domain and employs simple control partitioning to distinguish critical sections from surrounding code. It relates the variables of all threads using polyhedra, which limits its scalability in the number of variables. Nevertheless, preliminary experiments and comparison with ConcurInterproc show that modularity enables scaling to a large number of thread instances, provided that the total number of variables stays small.
影响因子：
0.8
作者：
Alastair F. Donaldson;A. Kaiser;D. Kroening;Michael Tautschnig;T. Wahl
通讯作者：
Alastair F. Donaldson;A. Kaiser;D. Kroening;Michael Tautschnig;T. Wahl