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. 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. 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. 2012, 77: 1006-1036 CrossRef Google Scholar

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

  • Figure 1

    (Color Online) A heap list of five chunks.

  •   
    1 void init();
    2 void* alloc(size_t sz);
    3 void* realloc(void* $p$, size_t sz);
    4 bool free(void* $p$);
  •   
  •   
  • Heap list Free list Fit Model in
    Case study Linked Split Defragment Array Shape Sorted policy Figure 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 early acyclic, $\leftrightarrow$ No Best MUAD
  •   
  •   
  •   
  •   
  •   
  •   
  •   
  •   
  •   
  •   
  •   
  • Copyright 2019 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有

    京ICP备18024590号-1