logo

SCIENCE CHINA Information Sciences, Volume 61, Issue 12: 122103(2018) https://doi.org/10.1007/s11432-017-9280-9

Formal modelling of list based dynamic memory allocators

More info
  • ReceivedJun 26, 2017
  • AcceptedNov 8, 2017
  • PublishedNov 13, 2018

Abstract

Existing implementations of dynamic memory allocators (DMA) employ a large spectrum of policies and techniques. The formal specifications of these techniques are quite complicated in isolation and very complex when combined. Therefore, the formal reasoning on a specific DMA implementation is difficult for automatic tools and mostly single-use.This paper proposes a solution to this problem by providing formal models for a full class of DMA, the class using various kinds of lists to manage the memory blocks controlled by the DMA.To obtain reusable formal models and tractable formal reasoning, we organise these models in a hierarchy ranked by refinement relations. We prove the soundness of models and the refinement relations using the modeling framework Event-B and the theorem prover Rodin.We demonstrate that our hierarchy is a basis for an algorithm theory for list based DMA:it abstracts various existing implementations of DMA and leads to new DMA implementations.The applications of this formalisation include model-based code generation, testing, and static analysis.


References

[1] Donald E K. The Art of Computer Programming, Volume I: Fundamental Algorithms. 3rd ed. Upper Saddle River: Addison-Wesley, 1973. Google Scholar

[2] Paul R W, Mark S J, Michael N, et al. Dynamic storage allocation: a survey and critical review. In: Proceedings of International Workshop on Memory Management, Kinross, 1995. 986: 1--116. Google Scholar

[3] Brian W K, Dennis R. The C Programming Language. 2nd ed. Upper Saddle River: Prentice-Hall, 1988. Google Scholar

[4] Doug L. dlmalloc. 2012. ftp://gee.cs.oswego.edu/pub/misc/malloc.c. Google Scholar

[5] Cristiano C, Dino D, Peter W O, et al. Beyond reachability: shape abstraction in the presence of pointer arithmetic. In: Proceedings of Static Analysis Symposium, Seoul, 2006. 4134: 282--203. Google Scholar

[6] Adam C. Mostly-automated verification of low-level programs in computational separation logic. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, San Jose, 2011. 234--245. Google Scholar

[7] Gerwin K, Kevin E, Gernot H, et al. seL4: formal verification of an OS kernel. In: Proceedings of ACM Symposium on Operating Systems Principles, Big Sky, 2009. 207--220. Google Scholar

[8] Nicolas M, Reynald A, Akinori Y. Formal verification of the heap manager of an operating system using separation logic. In: Proceedings of International Conference on Formal Engineering Methods, Macao, 2006. 4260: 400--419. Google Scholar

[9] Harvey T, Gerwin K, Michael N. Types, bytes, and separation logic. In: Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages, Nice, 2007. 97--108. Google Scholar

[10] Peter W O, John C R, Yang H. Local reasoning about programs that alter data structures. In: Proceedings of European Association for Computer Science Logic, Paris, 2001. 1--19. Google Scholar

[11] Smith D R, Lowry M R. Algorithm theories and design tactics. Sci Comput Programming, 1990, 14: 305-321 CrossRef Google Scholar

[12] Leslie A. Memory allocation in C. Embedded Systems Programming, 2008. 35--42. Google Scholar

[13] Jonathan B. Inside memory management. 2004. http://www.ibm.com/developerworks/library/l-memory/sidefile.html. Google Scholar

[14] Abrial J-R. Modeling in Event-B: System and Software Engineering. Cambridge: Cambridge University Press, 2010. Google Scholar

[15] Abrial J R, Butler M, Hallerstede S. Rodin: an open toolset for modelling and reasoning in Event-B. Int J Softw Tools Technol Transfer, 2010, 12: 447-466 CrossRef Google Scholar

[16] Fang B, Sighireanu M. A refinement hierarchy for free list memory allocators. In: Proceedings of ACM SIGPLAN International Symposium on Memory Management, Barcelona, 2017. 104--114. Google Scholar

[17] Fang B, Sighireanu M. A Refinement Hierarchy for Free List Memory Allocators. Research Report hal-01510166, IRIF. 2017. Google Scholar

[18] George F, Christian C, Eckart Z, et al. Topsy - A Teachable Operating System. Technical report, Version 1.1, 20000322. 2000. Google Scholar

[19] Miguel M, Ismael R, Alfons C, et al. TLSF: a new dynamic memory allocator for real-time systems. In: Proceedings of Euromicro Conference on Real-Time Systems, Catania, 2004. 79--86. Google Scholar

[20] Malik Q A, Lilius J, Laibinis L. Model-based testing using scenarios and Event-B refinements. In: Methods, Models and Tools for Fault Tolerance. Berlin: Springer, 2009. 177--195. Google Scholar

[21] Fang B, Sighireanu M. Hierarchical shape abstraction for analysis of free-list memory allocators. In: Proceedings of International Symposium on Logic-based Program Synthesis and Transformation, Edinburgh, 2016. 151--167. Google Scholar

[22] Liu J C, Xavier R. Abstraction of arrays based on non contiguous partitions. In: Proceedings of International Conference on Verification, Model Checking, and Abstract Interpretation, Paris, 2015. 8931: 282--299. Google Scholar

[23] Su W, Abrial J R, Pu G G, et al. Formal development of a real-time operating system memory manager. In: Proceedings of International Conference on Engineering of Complex Computer Systems, Gold Coast, 2015. 130--139. Google Scholar

[24] Chris H, Erez P. Automated verification of practical garbage collectors. In: Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages, Savannah, 2009. 441--453. Google Scholar

[25] Qin S C, Xu Z W, Ming Z. Survey of research on program verification via separation logic. J Softw, 2017, 28: 2010--2025. Google Scholar

[26] Chin W N, David C, Nguyen H H. Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci Comput Programming, 2012, 77: 1006-1036 CrossRef Google Scholar

[27] Qin S, He G, Luo C. Automatically refining partial specifications for heap-manipulating programs. Sci Comput Programming, 2014, 82: 56-76 CrossRef Google Scholar

  • Figure 1

    (Color Online) A heap list of five chunks.

  • Table 1   Interface of DMA
    1void init();
    2void* alloc(size_t sz);
    3void* realloc(void* $p$, size_t sz);
    4bool free(void* $p$);
  • Table 2   Most abstract specification $A$
  • Table 3   Design tactics employed in case studies
  • Heap listFree listFit Model in
    Case study Linked Split Defragment ArrayShape Sorted policyFigure 2
    IBM [12] addr, $\rightarrow$ First MH
    DL-small [4] size, $\rightarrow$ Yes First MH
    Topsy [18] size, $\rightarrow$ At end lazy First MHL
    Buddy [1] size, $\leftrightarrow$ At start partial First MHP
    L4 [7] addr, $\rightarrow$ lazy Yes acyclic, $\rightarrow$ Yes First MASAF
    DKff [1] size, $\rightarrow$ At start early acyclic, $\rightarrow$ Yes First MSAF
    DKbf [1] size, $\rightarrow$ At start early acyclic, $\rightarrow$ Yes Best MSAB
    LA [13] size, $\rightarrow$ At start early acyclic, $\rightarrow$ Yes First MSAF
    DKnf [1] size, $\rightarrow$ At start early acyclic, $\rightarrow$ Yes Next MSAN
    KR [3] size, $\rightarrow$ At start early cyclic, $\rightarrow$ Yes Next MSC
    DKbt [1] size, $\leftrightarrow$ At start early acyclic, $\leftrightarrow$ No Best MUAD
    DL-list [4] size, $\leftrightarrow$ At start early acyclic, $\leftrightarrow$ No Best MUAD
    TLSF [19] size, $\leftrightarrow$ At start earlyacyclic, $\leftrightarrow$ No Best MUAD
  • Table 4   Refinement of $A$ for heap list models
  • Table 5   Refinements of heap list operations for remove, insert, and search
  • Table 6   Refinements of heap list operation for chunk splitting
  • Table 7   Refinements of heap list operation for chunk merging
  • Table 8   Refinements of methods for heap list
  • Table 9   Overview of heap list models and statistics on proofs
  • Table 10   States and invariants used by free list refinements;$x~\in\{A,C\}$ denotes refinements for the shape of the free list
  • Table 11   Some refinements of basic operations on free list
  • Table 12   Refinement of methods for free list
  • Table 13   Overview of free list models and statistics on proofs
  • Table 14   Examples of refinement to code
  • Copyright 2020 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有

    京ICP备18024590号-1       京公网安备11010102003388号