Verified Sequential Malloc/Free

被引：10

作者：

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 [J].

Aspinall, D ;

Compagnoni, A .

JOURNAL OF AUTOMATED REASONING, 2003, 31 (3-4) :261-302

[2] Precise analysis of memory consumption using program logics [J].

Barthe, G ;

Pavlova, M ;

Schneider, G .

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 L, 2019, LECT NOTES COMPUT SC, V11800, 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 [J].

Birkedal, L ;

Torp-Smith, N ;

Reynolds, JC .

ACM SIGPLAN NOTICES, 2004, 39 (01) :220-231

[7] VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs [J].

Cao, Qinxiang ;

Beringer, Lennart ;

Gruetter, Samuel ;

Dodds, Josiah ;

Appel, Andrew W. .

JOURNAL OF AUTOMATED REASONING, 2018, 61 (1-4) :367-422

[8]

Cuellar Santiago, 2020, Technical Report TR- 014-19

[9] RustBelt Meets Relaxed Memory [J].

Dang, Hoang-Hai ;

Jourdan, Jacques-Henri ;

Kaiser, Jan-Oliver ;

Dreyer, Derek .

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2020, 4 (POPL)

[10]

Feng Yi., 2005, MEMORY SYSTEM PERFOR, P68

← 1 2 3 4 →