Verified sequential Malloc/Free

Andrew W. Appel, David A. Naumann

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We verify the functional correctness of an array-of-bins (segregated free-lists) single-thread malloc/free system with respect to a correctness specification written in separation logic. The memory allocator is written in standard C code compatible with the standard API; the specification is in the Verifiable C program logic, and the proof is done in the Verified Software Toolchain within the Coq proof assistant. Our "resource-aware" specification can guarantee when malloc will successfully return a block, unlike the standard Posix specification that allows malloc to return NULL whenever it wants to. We also prove subsumption (refinement): the resource-aware specification implies a resource-oblivious spec.

Original languageEnglish (US)
Title of host publicationISMM 2020 - Proceedings of the 2020 ACM SIGPLAN International Symposium on Memory Management, co-located with PLDI 2020
EditorsChen Ding, Martin Maas
PublisherAssociation for Computing Machinery
Pages48-59
Number of pages12
ISBN (Electronic)9781450375665
DOIs
StatePublished - Jun 16 2020
Event19th ACM SIGPLAN International Symposium on Memory Management, ISMM 2020, in conjunction with PLDI 2020 - London, United Kingdom
Duration: Jun 16 2020 → …

Publication series

NameInternational Symposium on Memory Management, ISMM

Conference

Conference19th ACM SIGPLAN International Symposium on Memory Management, ISMM 2020, in conjunction with PLDI 2020
CountryUnited Kingdom
CityLondon
Period6/16/20 → …

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Software

Keywords

  • formal verification
  • memory management
  • separation logic

Fingerprint Dive into the research topics of 'Verified sequential Malloc/Free'. Together they form a unique fingerprint.

  • Cite this

    Appel, A. W., & Naumann, D. A. (2020). Verified sequential Malloc/Free. In C. Ding, & M. Maas (Eds.), ISMM 2020 - Proceedings of the 2020 ACM SIGPLAN International Symposium on Memory Management, co-located with PLDI 2020 (pp. 48-59). (International Symposium on Memory Management, ISMM). Association for Computing Machinery. https://doi.org/10.1145/3381898.3397211