Verified Sequential Malloc/Free

被引：8
作者：
Appel, Andrew W. [1 ]
Naumann, David A. [2 ]
机构：
[1] Princeton Univ, Princeton, NJ 08544 USA
[2] Stevens Inst Technol, Hoboken, NJ 07030 USA
来源：
PROCEEDINGS OF THE 2020 ACM SIGPLAN INTERNATIONAL SYMPOSIUM ON MEMORY MANAGEMENT, ISMM 2020 | 2020年
基金：
美国国家科学基金会;
关键词：
memory management; separation logic; formal verification; FORMAL VERIFICATION;
D O I：
10.1145/3381898.3397211
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
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.
引用
收藏
页码：48 / 59
页数：12
相关论文
共 39 条
  • [1] Heap-bounded assembly language
    Aspinall, D
    Compagnoni, A
    [J]. JOURNAL OF AUTOMATED REASONING, 2003, 31 (3-4) : 261 - 302
  • [2] Precise analysis of memory consumption using program logics
    Barthe, G
    Pavlova, M
    Schneider, G
    [J]. SEFM 2005: THIRD IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2005, : 86 - 95
  • [3] Beringer L, 2005, LECT NOTES COMPUT SC, V3452, P347
  • [4] Beringer Lennart, 2019, Formal Methods - The Next 30 Years. Third World Congress, FM 2019. Proceedings. Lecture Notes in Computer Science (LNCS 11800), P573, DOI 10.1007/978-3-030-30942-8_34
  • [5] Beringer L, 2015, PROCEEDINGS OF THE 24TH USENIX SECURITY SYMPOSIUM, P207
  • [6] Local reasoning about a copying garbage collector
    Birkedal, L
    Torp-Smith, N
    Reynolds, JC
    [J]. ACM SIGPLAN NOTICES, 2004, 39 (01) : 220 - 231
  • [7] VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs
    Cao, Qinxiang
    Beringer, Lennart
    Gruetter, Samuel
    Dodds, Josiah
    Appel, Andrew W.
    [J]. JOURNAL OF AUTOMATED REASONING, 2018, 61 (1-4) : 367 - 422
  • [8] Cuellar Santiago, 2020, Technical Report TR- 014-19
  • [9] RustBelt Meets Relaxed Memory
    Dang, Hoang-Hai
    Jourdan, Jacques-Henri
    Kaiser, Jan-Oliver
    Dreyer, Derek
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2020, 4 (POPL):
  • [10] Feng Y., 2005, MEMORY SYSTEM PERFOR, P68, DOI DOI 10.1145/1111583.1111594
1234