Abstract
Formal verification of real-time services is important because they are usually associated with safety-critical systems. In this paper, we present a verified Two-Level Segregated Fit (TLSF) memory management model. TLSF is a dynamic memory allocator and is designed for real-time operating systems. We formalize the specification of TLSF algorithm based on the client requirements. The specification contains both functional correctness of allocation and free services and invariants and constraints of the global memory state. Then we implement an abstract TLSF memory allocator using state monads in Isabelle/HOL. The allocator model is built from a high-level view and the details of data structures are simplified but it covers all the behavioral principles and procedures of a concrete TLSF implementation. Finally, we verify that our TLSF model is correct w.r.t. the specification using a verification condition generator (VCG) and verification tools in Isabelle/HOL.
This work has been supported in part by the National Natural Science Foundation of China (NSFC) under the Grant No. 61872016.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
TLSF: Memory allocator real time embedded systems. http://www.gii.upv.es/tlsf/
Masmano, M., Ripoll, I., Crespo, A., Real, J.: TLSF: a new dynamic memory allocator for real-time systems. In: Proceedings of the 16th Euromicro Conference on Real-Time Systems, ECRTS 2004, Catania, Italy, 2004, pp. 79–88.https://doi.org/10.1109/EMRTS.2004.1311009
Masmano, M., Ripoll, I., Real, J., Crespo, A., Wellings, A.J.: Implementation of a constant time dynamic storage allocator. Softw. Pract. Exp. 38, 995–1026 (2008). https://doi.org/10.1002/spe.858
Cock, D., Klein, G., Sewell, T.: Secure microkernels, state monads and scalable refinement. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 167–182. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71067-7_16
Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9
Saraswat, V.A., Jagadeesan, R., Michael, M., von Praun, C.: A theory of memory models. In: Proceedings of the 12th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP), pp. 161–172. ACM (2007)
Yu, D., Hamid, N.A., Shao, Z.: Building Certified libraries for PCC: dynamic storage allocation. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 363–379. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36575-3_25
Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformations. J. Autom. Reason. 41(1), 1–31 (2008)
Tews, H., Völp, M., Weber, T.: Formal memory models for the verification of low-level operating-system code. J. Autom. Reason. 42(2), 189–227 (2009)
Gallardo, M.d.M., Merino, P., Sanán, D.: Model checking dynamic memory allocation in operating systems. J. Autom. Reason. 42(2), 229–264 (2009)
Ševčík, J., Vafeiadis, V., Zappa Nardelli, F., Jagannathan, S., Sewell, P.: CompCertTSO: a verified compiler for relaxed-memory concurrency. J. ACM (JACM) 60(3), 22:1–22:50 (2013)
Mansky, W., Garbuzov, D., Zdancewic, S.: An axiomatic specification for sequential memory models. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 413–428. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21668-3_24
Vaynberg, A., Shao, Z.: Compositional verification of a baby virtual memory manager. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 143–159. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35308-6_13
Gu, R., et al.: CertiKOS: an extensible architecture for building certified concurrent OS kernels. In: 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Savannah, GA, pp. 653–669. USENIX Association (2016)
Klein, G., et al.: seL4: formal verification of an OS kernel. In: 22nd ACM SIGOPS Symposium on Operating Systems Principles (SOSP), pp. 207–220. ACM Press (2009)
Klein, G., Tuch, H.: Towards verified virtual memory in L4. In: TPHOLs Emerging Trends, Park City, Utah, USA, 16 pages, September 2004
Alkassar, E., Schirmer, N., Starostin, A.: Formal pervasive verification of a paging mechanism. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 109–123. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_9
Blanchard, A., Kosmatov, N., Lemerre, M., Loulergue, F.: A case study on formal verification of the anaxagoros hypervisor paging system with frama-C. In: Núñez, M., Güdemann, M. (eds.) FMICS 2015. LNCS, vol. 9128, pp. 15–30. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19458-5_2
Bolignano, P., Jensen, T., Siles, V.: Modeling and abstraction of memory management in a hypervisor. In: Stevens, P., Wąsowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 214–230. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49665-7_13
Su, W., Abrial, J., Pu, G., Fang, B.: Formal development of a real-time operating system memory manager. In: 2015 20th International Conference on Engineering of Complex Computer Systems (ICECCS), Gold Coast, QLD, pp. 130–139 (2015). https://doi.org/10.1109/ICECCS.2015.24
Fang, B., Sighireanu, M.: Hierarchical shape abstraction for analysis of free list memory allocators. In: Hermenegildo, M.V., Lopez-Garcia, P. (eds.) LOPSTR 2016. LNCS, vol. 10184, pp. 151–167. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63139-4_9
Fang, B., Sighireanu, M.: A refinement hierarchy for free list memory allocators. In: Proceedings of the 2017 ACM SIGPLAN International Symposium on Memory Management, pp. 104–114. ACM (2017)
Fang, B., Sighireanu, M., Pu, G., Su, W., Abrial, J.R., Yang, M., Qiao, L.: Formal modelling of list based dynamic memory allocators. Sci. China Inf. Sci. 61(12), 103–122 (2018)
Marti, N., Affeldt, R., Yonezawa, A.: Formal verification of the heap manager of an operating system using separation logic. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 400–419. Springer, Heidelberg (2006). https://doi.org/10.1007/11901433_22
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Zhang, Y., Zhao, Y., Sanan, D., Qiao, L., Zhang, J. (2019). A Verified Specification of TLSF Memory Management Allocator Using State Monads. In: Guan, N., Katoen, JP., Sun, J. (eds) Dependable Software Engineering. Theories, Tools, and Applications. SETTA 2019. Lecture Notes in Computer Science(), vol 11951. Springer, Cham. https://doi.org/10.1007/978-3-030-35540-1_8
Download citation
DOI: https://doi.org/10.1007/978-3-030-35540-1_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-35539-5
Online ISBN: 978-3-030-35540-1
eBook Packages: Computer ScienceComputer Science (R0)