Verifying Contextual Refinement with Ownership Transfer |
| |
| Authors: | Zhao-Hui Li Xin-Yu Feng |
| |
| Affiliation: | 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 |
| |
| Abstract: | 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. |
| |
| Keywords: | contextual refinement program logic concurrent object ownership transfer verification |
| 本文献已被 万方数据 等数据库收录！ |
| 点击此处可从《计算机科学技术学报》浏览原始摘要信息 |
|
点击此处可从《计算机科学技术学报》下载全文 |
|
