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

aplas: related work

parent 46ae939e
%!TEX root = aplas2021.tex
\mypar{Related work.}
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.
The \emph{symbolic heap} (SH) fragment
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 $\ls{}(x,y)$
specifying acyclic singly linked list segments between address $x$ and $y$.
%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 predicate's arity
is bound by a known constant~\cite{DBLP:conf/csl/BrotherstonFPG14}.
In the category of built-in predicate,
the memory block predicate $\blk(x,y)$ used in this paper
has been introduced in \cite{CalcagnoDOHY06}
to capture properties of memory allocators. This predicate has been formalized
as part of the Array Separation Logic (ASL)~\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 shown to be decidable for
satisfiability and entailment.
The decisions procedures proposed have been implemented in the solver SLar~\cite{KimuraT17}, which is not publicly available.
%
Le~\cite{DBLP:conf/vmcai/Le21} identified two fragments of ASL allowing
inductive definitions for which the satisfiability (but not entailment) problem
is decidable.
However, the ASL fragment or its above extensions are not expressive enough
to specify the heap list data structure.
Although other fragments of separation logic has been used
in the static analysis of memory allocators~\cite{CalcagnoDOHY06}
or in their deductive verification~\cite{Chlipala11,MartiAY06},
the decidability of verification problem has not been studied
because these tools either employed sound heuristics or
interactive theorem provers.
%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.
%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{}$.
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