基于分离逻辑的并行程序性质验证方法

Verification Method for Concurrent Programs Properties Based on Separation Logic

随着多核多线程并行执行方式的普及,并行程序形式化验证的需求日显突出。并行程序验证中执行流程的不确定性使验证的内容与目标的关系难以确定,且从并行程序直接进行性质验证会导致验证规模大。为此,提出一种基于分离逻辑的新的验证方法。该方法根据分离逻辑的程序语义描述兼有解释语义和公理语义的特点,从验证的性质出发,把要验证的性质式转换成并行语句序列的逻辑组合式,并进行整理和化简;然后,利用分离逻辑公理系统对语句序列进行验证,用验证了的断言集来求出性质的真值。实例进一步说明,此方法更有效,同时也简化了验证的规模。

With the popularity of multi-core, multi-thread and parallel execution, there is an increasing demand for for-real verification of parallel programs. The uncertainty of execution flows in parallel program verification makes it diffi-cult to determine the relation between verification contents and targets. Verifying directly from the parallel programs will lead to large-scale verification. To this end, we proposed a new verification method based on separation logic. On the basis of the feature that the semantics of separation logic＇ s programming language are both interpretive and axiomatic, our method transforms the property formulae to be verified into logical composition expression, and reforms and simpli- fies them. Then separation logic＇s axiom system is used to verify the expression and calculate the value of property for-mulae with verified assertions. Case studies further illustrate that the proposed method is effective and can reduce verifi-cation scales.