Verifying Contextual Refinement with Ownership Transfer

• 作者: Zhao-Hui Li Xin-Yu Feng
• 来源期刊: 计算机科学技术学报（英文版）
• 年，卷（期）: 2021,（6）
• 所属期刊栏目: Special Section on Software Systems 2021-Theme: Dependable Software Engineering
• 页码范围: 1342-1366
• 页数: 25页
• 语种: 英文
• DOI: 10.1007/s11390-021-1671-7

摘要

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.