Verifying Contextual Refinement with Ownership Transfer  

作　　者：Zhao-Hui Li Xin-Yu Feng 

机构地区：[1]School of Computer Science and Technology,University of Science and Technology of China,Hefei 230026,China [2]Department of Computer Science and Technology,Nanjing University,Nanjing 210023,China [3]State Key Laboratory for Novel Software Technology,Nanjing University,Nanjing 210023,China

出　　处：《Journal of Computer Science & Technology》2021年第6期1342-1366,共25页计算机科学技术学报（英文版）

基　　金：supported by the National Natural Science Foundation of China under Grant No.61632005。

摘　　要：Contextual refinement is a compositional approach to compositional verification of concurrent objects.There has been much work designing program logics to prove the contextual refinement between the object implementation and its abstract specification.However,these program logics for contextual refinement verification cannot support objects with resource ownership transfer,which is a common pattern in many concurrent objects,such as the memory management module in OS kernels,which transfers the allocated memory block between the object and clients.In this paper,we propose a new approach to give abstract and implementation independent specifications to concurrent objects with ownership transfer.We also design a program logic to verify contextual refinement of concurrent objects w.r.t.their abstract specifications.We have successfully applied our logic to verifying an implementation of the memory management module,where the implementation is an appropriately simplified version of the original version from a real-world preemptive OS kernel.

关 键 词：contextual refinement program logic concurrent object ownership transfer VERIFICATION 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]