Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development of substantial verified systems. Nevertheless, existing refinement techniques have limitations that impede their practical usefulness. Some techniques generate executable code automatically, which generally leads to implementations with sub-optimal performance. Others employ bottom-up program verification to reason about efficient implementations, but impose strict requirements on the structure of the code, the structure of the refinement proofs, as well as the employed verification logic and tools. In this paper, we present a novel refinement technique that removes these limitations. Our technique uses separation logic to reason about efficient concurrent implementations. It prescribes only a loose coupling between an abstract model and the concrete implementation. It thereby supports a wide range of program structures, data representations, and proof structures. We make only minimal assumptions about the underlying program logic, which allows our technique to be used in combination with a wide range of logics and to be automated using off-the-shelf separation logic verifiers. We formalize the technique, prove the central trace inclusion property, and demonstrate its usefulness on several case studies.
翻译:精炼将抽象的系统模型转换成一个具体、可执行的程序,使为抽象的模型所建立的属性能够传递到具体实施。精炼已经成功地用于开发大量经核实的系统。尽管如此,现有的精炼技术有其实际效用的局限性。有些技术自动产生可执行的代码,这通常导致以亚优性性性能执行。另一些技术则采用自下而上的程序核查,以说明高效率的实施,但对代码的结构、精炼证据的结构以及所使用的核查逻辑和工具提出严格要求。我们在本文件中介绍了一种消除这些限制的新改进技术。我们的技术使用分离逻辑来解释同时有效实施这些限制。它只规定了抽象模型和具体实施之间的松散的组合。它因此支持了广泛的程序结构、数据表达和证据结构。我们只对基本程序逻辑作出最起码的假设,使我们的技术能够与广泛的逻辑结合使用,并且使用离子分离逻辑校准器实现自动化。我们把技术正规化,证明核心跟踪属性,并演示其实用性。