We use cookies to improve your experience with our site.
Zhao-Hui Li, Xin-Yu Feng. Verifying Contextual Refinement with Ownership Transfer[J]. Journal of Computer Science and Technology, 2021, 36(6): 1342-1366. DOI: 10.1007/s11390-021-1671-7
Citation: Zhao-Hui Li, Xin-Yu Feng. Verifying Contextual Refinement with Ownership Transfer[J]. Journal of Computer Science and Technology, 2021, 36(6): 1342-1366. DOI: 10.1007/s11390-021-1671-7

Verifying Contextual Refinement with Ownership Transfer

  • 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.
  • loading

Catalog

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return