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

计算机科学 ›› 2013, Vol. 40 ›› Issue (10): 148-154.

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

万良,石文昌,冯慧

中国人民大学信息学院北京100872;中国人民大学信息学院北京100872;中国人民大学信息学院北京100872

出版日期:2018-11-16 发布日期:2018-11-16
基金资助:
本文受国家自然科学基金项目(61070192,8,61170240),北京自然科学基金(4122041),国家高技术研究发展计划(2007AA01Z414),中国人民大学科学研究基金(中央高校基本科研业务费专项资金)项目成果(+12XNLF06),贵州自然科学基金项目(J[2011]2328)资助

Verification Method for Concurrent Programs Properties Based on Separation Logic

WAN Liang,SHI Wen-chang and FENG Hui

Online:2018-11-16 Published:2018-11-16

摘要/Abstract

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

关键词: 霍尔逻辑,分离逻辑,并行程序,逻辑组合式,性质验证

Abstract: With the popularity of multi-core,multi-thread and parallel execution,there is an increasing demand for formal verification of parallel programs．The uncertainty of execution flows in parallel program verification makes it difficult 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 simplifies them．Then separation logic’s axiom system is used to verify the expression and calculate the value of property formulae with verified assertions．Case studies further illustrate that the proposed method is effective and can reduce verification scales.

Key words: Hoare logic,Separation logic,Concurrent program,Combination expression,Property checking

万良,石文昌,冯慧. 基于分离逻辑的并行程序性质验证方法[J]. 计算机科学, 2013, 40(10): 148-154. https://doi.org/

WAN Liang,SHI Wen-chang and FENG Hui. Verification Method for Concurrent Programs Properties Based on Separation Logic[J]. Computer Science, 2013, 40(10): 148-154. https://doi.org/

参考文献

[1] Hoare C A R．An Axiomatic Basis for Computer Programming[J]．Communications of the ACM,1969,12(10):576-580
[2] O’Hearn P,Reynolds J,Yang H．Local Reasoning about Programs that Alter Data Structures[C]∥Proceedings of 15th Annual Conference of the European Association for Computer Science Logic．LNCS,Springer-Verlag,2001:1-19
[3] Reynolds J C．Separation logic:A logic for shared mutable data structures.In LICS[C]∥IEEE Computer Society．2002:55-74
[4] Reynolds J C．An overview of separation logic[C]∥ Meyer B,Woodcock J,eds．VSTTE,Lecture Notes in Computer Science．Springer,2005,4171:460-469
[5] O’Hearn P W．Tutorial on separation logic [C]∥ Gupta A,Malik S,eds．CAV．Springer,2008,5123:19-21
[6] Ding L,Dong L D,Piao Y．Deadlock prevention policy of concurrent programming base on Petri net[J]．Journal of Zhejiang University:Science Edition,2012,39(1)
[7] Owicki S,Lamport L．Proving liveness properties of concurrent programs[J]．ACM Transactions on Programming Languages and Systems(TOPLAS),1982,4(3):455-495
[8] Kleine M,Bartels B,Gthel T,et al．LLVM2CSP:extracting csp models from concurrent programs[M]．NASA Formal Methods,Springer Berlin Heidelberg,2011:500-505
[9] 肖美华,薛锦云．基于SPIN/Promela 的并发系统验证 [J]．计算机科学,2004,31(8):201-203
[10] Witkowski T,Blanc N,Kroening D,et al．Model checking concurrent linux device drivers[C]∥Proceedings of the Twenty-second IEEE/ACM International Conference on Automated Software Engineering．ACM,2007:501-504
[11] Grov G,Michaelson G,Ireland A．Formal verification of concurrent scheduling strategies using TLA[C]∥Parallel and Distri-buted Systems,2007International Conference on．IEEE,2007,2:1-6
[12] Apt K R,De Boer F S,Olderog E R．Verification of sequential and concurrent programs[M]．Springer,2010
[13] Feng X,Shao Z,Dong Y,et al．Certifying low-level programs with hardware interrupts and preemptive threads[C]∥PLDI’08:Conference on Programming Language Design and Implementation．ACM,2008:170-182
[14] Feng X,Shao Z,Vaynberg A,et al.Modular verification of assembly code with stack-based control abstractions[C]∥PLDI’06:Conference on Programming Language Design and Implementation．ACM,2006:401-414
[15] Stephan V S,Cristiano C,Bertrand M．Verifying Executable Object-Oriented Specifications with Separation Logic[C]∥24th European Conference．Maribor,Slovenia,June 2010:21-25
[16] Aquinas H,Andrew W A,Francesco Z N．Oracle Semantics for Concurrent Separation Logic[C]∥ESOP．April 2008
[17] Alexey G,Honseok Y．Modular verification of Preemptive OSKernels[C]∥ICEP’11．2011
[18] O’Hearn P W．Resources,concurrency and local reasoning[C]∥Gardner P,Yoshida N,eds．CONCUR,volume 3170of Lecture Notes in Computer Science．Springer,2004:49-67
[19] Yu S W．Formal verification of concurrent programs[D]．Durham University,1999
[20] Brookes S.A semantics for concurrent separation logic[J]．Theor．Computer Science,2007,375:227-270
[21] Hayman J,Winskel G.Independence and concurrent separation logic[C]∥LICS 2006．2006:147-156

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed