Commit af7290ec authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

aplas: related work

parent 62e8dadb
......@@ -3,6 +3,9 @@
\section{Conclusion}
\label{sec:conc-hls}
\input{related.tex}
\paragraph{Conclusion.}
In this work, we investigated \slah, a separation logic fragment that allows pointer arithmetic inside inductive definitions so that the commonly used data structures e.g. heap lists can be defined.
We show that the satisfiability problem of {\slah} is NP-complete and
the entailment problem is coNP-complete.
......
......@@ -26,20 +26,17 @@ The satisfiability problem for the SH fragment with a class of general inductive
\mypar{Motivation.}
Vast majority of the work on the verification of heap manipulating programs based on SL assumes that the addresses are \emph{nominal}, that is, they can be compared with only equality or disequality, but not ordered or obtained by arithmetic operations.
However, pointer arithmetic is widely used in low-level programs % , e.g. memory allocators.
However, pointer arithmetic is widely used in low-level programs
to access data inside memory blocks. Memory allocators are such low-level programs.
%Such programs usually use pointer variables to refer to the start addresses of memory regions and use arithmetic expressions on these variables to visit the memory cells inside these regions.
They assume that the memory is organized into a linked list of memory chunks,
called heap lists in this paper; pointer arithmetic is
%where arithmetic expressions are
used to jump from a memory chunk to the next one \cite{Knuth97,WJ+95}.
%We call this data structure as heap lists in the sequel.
%
%One of the fundamental data structures used in these programs are heap lists
Classic implementations of memory allocators~\cite{Knuth97,WJ+95}
organize the heap into a linked list of memory chunks,
called heap lists in this paper; pointer arithmetic is
used to jump from a memory chunk to the next one.
%
There have been some work to use separation logic for the static analysis and deductive verification of these low-level programs~\cite{CalcagnoDOHY06,MartiAY06,Chlipala11}.
Moreover, researchers have also started to investigate the decision procedures for separation logic fragments containing pointer arithmetic.
For instance, \emph{Array separation logic} (ASL) was proposed in~\cite{BrotherstonGK17}, which includes pointer arithmetic, the constraints $\blk(x,y)$ denoting a block of memory units from the address $x$ to $y$, as well as the points-to constraints $x\pto v$. It was shown in~\cite{BrotherstonGK17} that for ASL, the satisfiability is NP-complete and the entailment is in coNEXP resp. coNP for quantified resp. quantifier-free formulas.
For instance, \emph{Array separation logic} (ASL) was proposed in~\cite{BrotherstonGK17}, which includes pointer arithmetic, the constraints $\blk(x,y)$ denoting a block of memory units from the address $x$ to $y$, as well as the points-to constraints $x\pto v$. It was shown in~\cite{BrotherstonGK17} that for ASL, the satisfiability is NP-complete and the entailment is in coNEXP (resp. coNP) for quantified (resp. quantifier-free) formulas.
Furthermore, the decidability can be preserved even if ASL is extended with the list-segment predicate~\cite{DBLP:journals/corr/abs-1802-05935}.
Very recently, Le identified in~\cite{DBLP:conf/vmcai/Le21} two fragments
of ASL extended with a class of general inductive predicates for which
......@@ -47,89 +44,9 @@ the satisfiability (but not entailment) problem is decidable.
Nevertheless, none of the aforementioned work is capable of reasoning about heap lists, or generally speaking, pointer arithmetic inside inductive definitions, in a \emph{sound and complete} way. The state-of-the-art static analysis and verification tools, e.g. \cite{CalcagnoDOHY06,Chlipala11,MartiAY06}, resort to sound (but incomplete) heuristics or interactive theorem provers, for reasoning about heap lists.
On the other hand, the decision procedures for ASL or its extensions, e.g. \cite{BrotherstonGK17,DBLP:journals/corr/abs-1802-05935,DBLP:conf/vmcai/Le21}, are unable to tackle heap lists.
%\footnote{The fact that heap lists are beyond the two decidable fragments in~\cite{DBLP:conf/vmcai/Le21} was confirmed by a personal communication with the author of \cite{DBLP:conf/vmcai/Le21}.}.
This motivates us to raise the following research question: \emph{Can decision procedures be achieved for separation logic fragments allowing heap lists}?
%Separation logic~\cite{Reynolds:2002,OHearn19}
%has a big impact on the verification or static analysis of programs
%manipulating the dynamic memory. Performant tools have been developed
%based on this formalism, among which we cite
%\textsc{Infer}~\cite{DBLP:journals/cacm/DistefanoFLO19} for static analysis
%and \textsc{VeriFast}~\cite{verifast} for deductive verification.\todo{MS: change tool}
%These tools employ the
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\hide{
The \emph{symbolic heap} (SH) fragment \todo{MS: change motivation}
of separation logic has been introduced in~\cite{BerdineCO04}
because it provides a good compromise between expressivity
and tractability. This fragment includes existentially quantified formulas
which are conjunctions of
aliasing constraints $x = y$ and $x \neq y$ between pointers $x$ and $y$,
and heap constraints $x\pto v$ expressing that at the address $x$ is allocated
a memory zone containing the value $v$.
The separating conjunction composes the heap constraints by ensuring
that the allocated memory blocks are disjoint.
To capture properties of heaps with unbounded data structures, the SH fragment is
extended with predicates that may be inductively defined using SH formulas or
defined by the semantics, i.e., built-in.
The first category includes the predicate specifying acyclic singly linked list segments defined by the following two rules:
\begin{eqnarray}
\ls{}(x,y) & \Leftarrow & x = y : \emp \label{eq:ls-0} \\
\ls{}(x,y) & \Leftarrow & \exists x'\cdot x \neq y : x \pto x' \sepc \ls{}(x',y) \label{eq:ls-rec}
\end{eqnarray}
The satisfiability problem for the SH fragment with the $\ls{}$ predicate is in PTIME~\cite{CookHOPW11} and efficient solvers have been implemented for it~\cite{SLCOMPsite}.
This situation changes for more complex definitions of predicates,
but still there are decidable fragments for which the satisfiability problem
is EXPTIME~\cite{DBLP:conf/lpar/EchenimIP20,DBLP:conf/lpar/KatelaanZ20}
% PSPACE~\cite{IosifRS13}.
in general and NP-complete if the arity of the predicate
is bound by a known constant~\cite{DBLP:conf/csl/BrotherstonFPG14}.
%
In the second category of predicates, one which is of interest for this paper
is the memory block predicate $\blk(x,y)$ introduced in \cite{CalcagnoDOHY06}
to capture properties of memory allocators. This predicate has been formalized
as part of the \emph{array separation logic} (ASL)
introduced in~\cite{BrotherstonGK17}.
The predicate denotes a block of memory units (bytes or integers)
between addresses $x$ and $y$. It is usually combined with
pointer arithmetics allowing to compute addresses in the memory blocks.
This combination is enough to increase the complexity class of the
decision problems in ASL: the satisfiability is NP-complete,
the bi-abduction is NP-hard and
the entailment is EXPTIME resp. coNP-complete for quantified resp. quantifier-free formulas~\cite{BrotherstonGK17}.
The ASL fragment extended with the $\ls{}$ predicate has been studied
in~\cite{DBLP:journals/corr/abs-1802-05935}, and it is decidable for
satisfiability and entailment.
This motivates us to raise the following research question: \emph{Can decision procedures be achieved for separation logic fragments allowing heap lists}?
Still, the ASL fragment or its extension with $\ls{}$ are not expressive enough
to specify the heap list data structure that is defined by the following rules:
\begin{eqnarray}
\hls{}(x,y) & \Leftarrow & x = y : \emp \label{eq:hls-0} \\
\hls{}(x,y) & \Leftarrow & \exists x'\cdot x'-x \ge 2 : x \pto x'-x \sepc \blk(x+1,x') \sepc \hls{}(x',y) \label{eq:hls-rec}
\end{eqnarray}
From this definition, a heap list between addresses $x$ and $y$ is
either an empty block if $x$ and $y$ are aliased,
or a list cell, called \emph{chunk}, starting at address $x$ and ending at
address $x'$ followed by a heap-list from $x'$ to $y$.
The chunk stores its size $x'-x$ at its start
(atom $x\pto x'-x$), that we also call \emph{chunk's header}.
The \emph{chunk's body} is a memory block (atom $\blk(x+1,x')$) starting
after the header and ending before the next heap-list's chunk.
Although this fragment has been used in the static analysis of memory
allocators~\cite{CalcagnoDOHY06} as well as deductive verification~\cite{Chlipala11,MartiAY06}, its decidability
has not been studied because these tools either employed sound heuristics or interactive theorem provers, but not decision procedures.
A special instance where all chunks have 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.
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -150,9 +67,6 @@ We also randomly generate some formulas, in order to test the scalability of {\c
The experimental results show that {\cspenp} is able to solve the satisfiability and entailment problems for {\slah} efficiently (in average, less than 1 second for satisfiability and less than 15 seconds for entailment).\zhilin{The anonymization is properly done.}
To the best of our knowledge, this work presents the first decision procedure and automated solver for decision problems in a separation logic fragment allowing both pointer arithmetic and memory blocks inside inductive definitions.
%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{}$.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -197,17 +111,13 @@ Our class of heap-list predicates is a strict sub-class of inductive definitions
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mypar{Organization.}
%The remainder of this paper is structured as follows.
A motivating example and an overview of the decision procedures are provided in Section~\ref{sec:over-hls}.
The logic {\slah} is defined in Section~\ref{sec:logic-hls}.
%
Then the decision procedures for the satisfiability and entailment problems are presented in Sections~\ref{sec:sat-hls} \resp~\ref{sec:ent}.
%
%Section~\ref{sec:sat-wfid} extends the satisfiability results to \slah\ with
% well-formed inductive definitions of heap-lists.
%
The implementation details and the experimental evaluation
are reported in Section~\ref{sec:exp-hls}.
%Finally, the conclusion is given in Section~\ref{sec:conc-hls}.
Section~\ref{sec:conc-hls} provides a summary of related works and concludes.
%by a comparison of our work with existing fragments and its impact on verification of memory allocators.
......@@ -91,16 +91,16 @@ where
{\small
\begin{eqnarray}
\phi_1 & \triangleq & \bigwedge\limits_{a_i,a_j \in \patoms(\varphi), i<j}
\begin{array}[t]{l}
\left(\begin{array}{l}
(\isnonemp_{a_i} \land \isnonemp_{a_j}) \limp \\
\quad (\atomtail(a_j) \le \atomhead(a_i)\lor \atomtail(a_i) \le \atomhead(a_j))
\end{array}
\end{array}\right)
\\
\phi_2 & \triangleq & \bigwedge\limits_{a_i \in \patoms(\varphi), a_j \in \overline{\patoms}(\varphi)}
\begin{array}[t]{l}
(\isnonemp_{a_i}) \limp \\
\phi_2 & \triangleq & \bigwedge\limits_{\tiny\begin{array}{l}a_i \in \patoms(\varphi), \\[1mm] a_j \in \overline{\patoms}(\varphi)\end{array}}
\left(\begin{array}{l}
\isnonemp_{a_i} \limp \\
\quad (\atomtail(a_j) \le \atomhead(a_i) \lor \atomtail(a_i) \le \atomhead(a_j))
\end{array}
\end{array}\right)
\\
\phi_3 & \triangleq & \bigwedge\limits_{a_i, a_j \in \overline{\patoms}(\varphi), i < j}
\atomtail(a_j) \le \atomhead(a_i) \lor \atomtail(a_i) \le \atomhead(a_j)
......
......@@ -513,8 +513,8 @@ series = {ISMM 2020}
OPTtitle = {The {CompSpen} Solver},
OPTyear = {2019},
OPTnote = {\url{https://github.com/suwy123/compspen2}},
title = {The XXX Solver},
note = {The GitHub address has been sent to chairs}
title = {The {XYZ} Solver},
note = {The GitHub address has been sent to chairs.}
}
@misc{benchmark,
......@@ -522,8 +522,8 @@ series = {ISMM 2020}
OPTtitle = {{CompSpen+} benchmarks},
OPTyear = {2021},
OPTnote = {\url{https://github.com/suwy123/compspen2/tree/master/samples/PAsamples}},
title = {{XXX+} benchmarks},
note = {The GitHub address has been sent to chairs}
title = {{XYZ+} benchmarks},
note = {The GitHub address has been sent to chairs.}
}
@inproceedings{EneaSW15,
......
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