Commit a7c7440b authored by ehilin02's avatar ehilin02
Browse files
parents 1a5a10f0 f4652813
......@@ -64,22 +64,30 @@ or \textsc{Hip}~\cite{DBLP:conf/atva/HeQLC09} for deductive verification.
The static analysis of memory allocators using separation logic was the focus of
several works starting with the pioneering work of~\cite{CalcagnoDOHY06}.
For example, \cite{LiuR15} defined an abstract domain for the analysis of array properties and applies it to the Minix 1.1 memory allocator, which uses chunks of fixed size. Also, \cite{BinS16} employed an extension of SL with data words and overlapping separating conjunction to analyze free list memory allocators.
For example, \cite{LiuR15} defined an abstract domain for the analysis of array properties and applies it to the Minix 1.1 memory allocator, which uses chunks of fixed size. Also, \cite{FangS16} employed an extension of SL with data words and overlapping separating conjunction to analyze free list memory allocators.
In these analyzers, the decidability of verification problem has not been studied
because these tools employ sound heuristics to decide satisfiability or entailment problems.
Deductive verification of memory allocators has been considered in
several works~\cite{Chlipala11,MartiAY06,AppelN20} based on ad-hoc solvers
or interactive theorem provers. In \cite{Chlipala11}, a Coq library based on separation logic is presented and used to verify an implementation of malloc.
several works~\cite{Chlipala11,MartiAY06,AppelN20}.
For example, \cite{Chlipala11} presents a Coq library based on SL that
allows to abstract the low level details of the memory organization
in order to obtain an almost-automatic verification
of an malloc implementation using heap and free lists. However, the
abstraction proposed can not deal with the coalescing of chunks in the heap lists.
Our logic fragment \slah{} is less general, but allows to reason about the coalescing operation.
Separation logic is also used in~\cite{AppelN20} to verify the functional correctness
of an malloc implementation Verified Software Toolchain within the Coq proof assistant.
%A special instance where all chunks have the same size
%A special instance of a memory allocator using chunks of the same size
%has been used in the deductive verification of
% an implementation of the array list collection~\cite{CauderlierS18},
%but required an interactive prover \textsc{VeriFast} and user-provided
%lemma.
Our work provides insights on strategies for automatizing these deductive verification based work.
%
%As mentioned before, the logic ASL was introduced in~\cite{BrotherstonGK17}, but it contains no inductive predicates.
%As mentioned before, an extension of ASL with the classic singly linked list $\ls{}$ was considered in~\cite{DBLP:journals/corr/abs-1802-05935}
% where the only inductive predicate is the classic singly linked list $\ls{}$.
......
......@@ -194,17 +194,17 @@ author = {Appel, Andrew W. and Naumann, David A.},
title = {Verified Sequential Malloc/Free},
year = {2020},
isbn = {9781450375665},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
publisher = {ACM},
OPTaddress = {New York, NY, USA},
OPTurl = {https://doi.org/10.1145/3381898.3397211},
doi = {10.1145/3381898.3397211},
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.},
booktitle = {Proceedings of the 2020 ACM SIGPLAN International Symposium on Memory Management},
booktitle = {{ISMM}},
OPTpages = {48–59},
numpages = {12},
keywords = {formal verification, separation logic, memory management},
location = {London, UK},
series = {ISMM 2020}
OPTseries = {ISMM 2020}
}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment