Abstraction-guided synthesis of synchronization
Abstraction-guided synthesis of synchronization
复制标题
抽象引导的同步综合
DOI：
10.1007/s10009-012-0232-3
复制
发表时间：
2010
影响因子：
1.5
通讯作者：
G. Yorsh
中科院分区：
文献类型：
--
作者：
Martin T. Vechev;Eran Yahav;G. Yorsh
我们提出了一个新的框架，自动推理的高效同步并发程序，一个任务是困难和容易出错的手动完成时。我们的框架基于抽象解释，并且可以推断无限状态程序的同步。给定一个程序，一个规范，和一个抽象，我们推断同步，避免所有（抽象）交织，可能违反规范，但允许尽可能多的有效交织。结合抽象细化，我们的框架可以被看作是一种新的方法验证程序和抽象可以修改的飞行过程中的验证过程中。修改程序的能力，而不仅仅是抽象，允许我们删除程序交织，不仅当他们知道是无效的，而且当他们不能使用给定的抽象验证。我们实现了我们的方法使用数值抽象的原型，并应用它来验证几个例子程序。
We present a novel framework for automatic inference of efficient synchronization in concurrent programs, a task known to be difficult and error-prone when done manually. Our framework is based on abstract interpretation and can infer synchronization for infinite state programs. Given a program, a specification, and an abstraction, we infer synchronization that avoids all (abstract) interleavings that may violate the specification, but permits as many valid interleavings as possible. Combined with abstraction refinement, our framework can be viewed as a new approach for verification where both the program and the abstraction can be modified on-the-fly during the verification process. The ability to modify the program, and not only the abstraction, allows us to remove program interleavings not only when they are known to be invalid, but also when they cannot be verified using the given abstraction. We implemented a prototype of our approach using numerical abstractions and applied it to verify several example programs.