Reliable Concurrent Software Development Via Reliable Concurrency Controllers

该方案提出了一种基于接口的并发控制器规范和验证的可靠并发编程框架。提出的并发控制器规范和验证技术通过将行为和接口规范解耦而模块化。行为规范是由受保护的命令组成的一组操作(对应于方法或过程)。接口规范是一个有限状态机，其转换表示操作。Con-Currency控制器可以通过组合它们的接口来模块化设计。该方法将并发控制器的验证(行为验证)与使用并发控制器的线程的验证(接口验证)分开。对于行为验证，可以使用符号和无限状态验证技术，该技术允许使用参数常量、无界变量和任意数量的客户端线程来验证控制器。对于接口验证，可以使用显式状态程序验证技术，这使得可以不受任何限制地验证任意线程实现。利用并发控制器接口生成的存根验证用户线程的正确性，显著提高了线程验证的效率。可以从并发控制器规范合成高效的Java监视器，并且生成的实现保留了规范的经过验证的属性。提出的框架将作为一套并发控制器规范、验证和综合的工具来实现

This proposal presents a framework for reliable concurrent programming based on interface-based specification and verification of concurrency controllers. Proposed specification and verification techniques for concurrency controllers are modularized by decoupling behavior and interface specifications. The behavior specification is a set of actions (which correspond to methods or procedures) composed of guarded commands. The interface specification is a finite state machine whose transitions represent actions. Con-currency controllers can be designed modularly by composing their interfaces. The proposed approach separates the verification of the concurrency controllers (behavior verification) from the verification of the threads, which use them (interface verification). For behavior verification it is possible to use symbolic and infinite-state verification techniques, which enables verification of controllers with parameterized constants, unbounded variables and arbitrary number of client threads. For interface verification it is possible to use explicit state program verification techniques, which enables verification of arbitrary thread implementations without any restrictions. The correctness of the user threads can be verified using stubs generated from the concurrency controller interfaces, which improves the efficiency of the thread verification significantly. It is possible to synthesize efficient Java monitors from the concurrency controller specifications, and the generated implementations preserve the verified properties of the specifications. The proposed framework will be implemented as a set of tools for concurrency controller specification, verification and synthesis