AI Chat Paper
Note: Please note that the following content is generated by AMiner AI. SciOpen does not take any responsibility related to this content.
{{lang === 'zh_CN' ? '文章概述' : 'Summary'}}
{{lang === 'en_US' ? '中' : 'Eng'}}
Chat more with AI
Powered by AMiner. Clicking this button will take you away from SciOpen.
Home Journal of Computer Science and Technology Article
Article Link
Cite
EndNote(RIS) BibTeX
Collect
Submit Manuscript
Show Outline
Outline
Show full outline
Hide outline
Outline
Show full outline
Hide outline
Regular Paper

Verifying Contextual Refinement with Ownership Transfer

School of Computer Science and Technology, University of Science and Technology of China, Hefei, 230026, China
Department of Computer Science and Technology, Nanjing University, Nanjing, 210023, China
State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, 210023, China
Show Author Information

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 refinementprogram logicconcurrent objectownership transferverification

Electronic Supplementary Material

Download File(s)
jcst-36-6-1342-Highlights.pdf (94.3 KB)

References

[1]
Filipović I, O’Hearn P, Rinetzky N, Yang H. Abstraction for concurrent objects. In Proc. the 18th European Symposium on Programming, March 2009, pp.252-266. DOI: 10.1007/978-3-642-00590-9_19.
Crossref
[2]

Herlihy M P, Wing J M. Linearizability: A correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems, 1990, 12(3): 463-492. DOI: 10.1145/78969.78972.
Crossref Google Scholar
[3]
Gu R, Shao Z, Kim J, Wu X, Koenig J, Sjöberg V, Chen H, Costanzo D, Ramananandro T. Certified concurrent abstraction layers. In Proc. the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2018, pp.646-661. DOI: 10.1145/3192366.3192381.
Crossref
[4]
Liang H, Feng X. Modular verification of linearizability with non-fixed linearization points. In Proc. the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2013, pp.459-470. DOI: 10.1145/2491956.2462189.
Crossref
[5]
Liang H, Feng X. A program logic for concurrent objects under fair scheduling. In Proc. the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2016, pp.385-399. DOI: 10.1145/2837614.2837635.
Crossref
[6]

Liang H, Feng X. Progress of concurrent objects with partial methods. Proceedings of the ACM on Programming Languages, 2017, 2(POPL): Article No. 20. DOI: 10.1145/3158108.
Crossref Google Scholar
[7]
Xu F, Fu M, Feng X, Zhang X, Zhang H, Li Z. A practical verification framework for preemptive OS kernels. In Proc. the 28th International Conference on Computer Aided Verification, July 2016, pp.59-79. DOI: 10.1007/978-3-319-41540-6_4.
Crossref
[8]
Li Z, Feng X. Verifying contextual refinement with ownership transfer. Technical Report School of Computer Science and Technology, University of Science and Technology of China. https://www.researchgate.net/publication/353660416_Verifying_Contextual_Refinement_with_Ownership_TransferExtended_Version, Sept. 2021.
Crossref
[9]
Reynolds J C. Separation logic: A logic for shared mutable data structures. In Proc. the 17th Annual IEEE Symposium on Logic in Computer Science, July 2002, pp.55-74. DOI: 10.1109/LICS.2002.1029817.
Crossref
[10]
Liang H, Feng X, Fu M. A rely-guarantee-based simulation for verifying concurrent program transformations. In Proc. the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2012, pp.455-468. DOI: 10.1145/2103656.2103711.
Crossref
[11]
Dinsdale-Young T, Dodds M, Gardner P, Parkinson M J, Vafeiadis V. Concurrent abstract predicates. In Proc. the 24th European Conference on Object-Oriented Programming, June 2010, pp.504-528. DOI: 10.1007/978-3-642-14107-2_24.
Crossref
[12]
Boyland J. Checking interference with fractional permissions. In Proc. the 10th International Static Analysis Symposium, June 2003, pp.55-72. DOI: 10.1007/3-540-44898-5_4.
Crossref
[13]
Feng X. Local rely-guarantee reasoning. In Proc. the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2009, pp.315-327. DOI: 10.1145/1480881.1480922.
Crossref
[14]
Masmano M, Ripoll I, Crespo A, Real J. TLSF: A new dynamic memory allocator for real-time systems. In Proc. the 16th Euromicro Conference on Real-Time Systems, June 30-July 2, 2004, pp.79-86. DOI: 10.1109/EMRTS.2004.1311009.
Crossref
[15]
Gu R, Shao Z, Chen H, Wu X N, Kim J, Sjöberg V, Costanzo D. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Proc. the 12th USENIX Symposium on Operating Systems Design and Implementation, November 2016, pp.653-669.
[16]
Turon A, Dreyer D, Birkedal L. Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In Proc. the 18th ACM SIGPLAN International Conference on Functional programming, September 2013, pp.377-390. DOI: 10.1145/2500365.2500600.
Crossref
[17]
Tassarotti J, Jung R, Harper R. A higher-order logic for concurrent termination-preserving refinement. In Proc. the 26th European Symposium on Programming, April 2017, pp.909-936. DOI: 10.1007/978-3-662-54434-1_34.
Crossref
[18]
Svendsen K, Birkedal L. Impredicative concurrent abstract predicates. In Proc. the 23rd European Symposium on Programming, April 2014, pp.149-168. DOI: 10.1007/978-3-642-54833-89.
Crossref
[19]
Da Rocha P P, Dinsdale-Young T, Gardner P. TaDa: A logic for time and data abstraction. In Proc. the 28th European Conference on Object-Oriented Programming, July 28-August 1, 2014, pp.207-231. DOI: 10.1007/978-3-662-44202-9_9.
Crossref
[20]
Jung R, Swasey D, Sieczkowski F, Svendsen K, Turon A, Birkedal L, Dreyer D. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In Proc. the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2015, pp.637-650. DOI: 10.1145/2676726.2676980.
Crossref
[21]

Jung R, Krebbers R, Jourdan J H, Bizjak A, Birkedal L, Dreyer D. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program, 2018, 28: Article No. e20. DOI: 10.1017/S0956796818000151.
Crossref Google Scholar
[22]

Dinsdale-Young T, Da Rocha P P, Gardner P. A perspective on specifying and verifying concurrent modules. Journal of Logical and Algebraic Methods in Programming, 2018, 98: 1-25. DOI: 10.1016/j.jlamp.2018.03.003
Crossref Google Scholar
Journal of Computer Science and Technology
Volume 36 Issue 6,
November 2021
Pages 1342-1366
DOI: 10.1007/s11390-021-1671-7
Cite this article:
Li Z-H, Feng X-Y. Verifying Contextual Refinement with Ownership Transfer. Journal of Computer Science and Technology, 2021, 36(6): 1342-1366. https://doi.org/10.1007/s11390-021-1671-7

346

Views

2

Crossref

2

Web of Science

1

Scopus

0

CSCD

Altmetrics
Received: 01 July 2021
Accepted: 07 November 2021
Published: 30 November 2021
© Institute of Computing Technology, Chinese Academy of Sciences 2021
Return