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

remove DOI from bst to have 1 page citations; remove comments; fix notation...

remove DOI from bst to have 1 page citations; remove comments; fix notation for stack update to gets
parent 77e2ef70
......@@ -20,13 +20,13 @@ We show that the satisfiability problem of {\slah} is NP-complete and
We implemented the decision procedures in a solver, \cspenp, and use it
to efficiently solve more than hundred problems issued from program verification
or randomly generated. There are several directions for the future work.
At first, it is interesting to see whether the decision procedures for heap lists in this work can be extended to tackle free lists, another common data structure in memory allocators \cite{conf/lopstr/FangS16}. Moreover, since bit operations are also widely used in memory allocators, it would also be interesting to automate the reasoning about bit operations inside inductive definitions.
At first, it is interesting to see whether the decision procedures for heap lists in this work can be extended to tackle free lists, another common data structure in memory allocators \cite{Knuth97}. Moreover, since bit operations are also widely used in memory allocators, it would also be interesting to automate the reasoning about bit operations inside inductive definitions.
%%MS: moved into introduction
%\smallskip
%This study is original to our knowledge, although the separation logic
% with heap-list has been used in
% static analysis~\cite{CalcagnoDOHY06,conf/lopstr/FangS16}
% static analysis~\cite{CalcagnoDOHY06}
% and deductive verification~\cite{Chlipala11,MartiAY06}
% of memory allocators. Indeed, such work uses sound procedures
% or interactive theorem provers and does not consider the decision problem.
......
%!TEX root = tab2021.tex
%!TEX root = atva2021.tex
\subsection{Consequent with one spatial atom}
......@@ -9,7 +9,7 @@ $\varphi \models_\preceq \psi$, where
$\varphi \equiv \Pi: a_1 \sepc \cdots \sepc a_m$,
$\psi \equiv \Pi': b_1$
and the constraints (\ref{eq:order})--(\ref{eq:order-conseq}) are satisfied.
From~(\ref{eq:order}) and the definition of $\abs$, we have that\mihaela{r3}
From~(\ref{eq:order}) and the definition of $\abs$, we have that
$C_\preceq \land \abs(\varphi)$ implies $\Pi'$,
so we simplify this entailment to deciding:
\begin{align*}
......@@ -85,7 +85,7 @@ Let $\varphi \equiv x < y: \hls{}(x, y; 3)$ and $s$ be a store such that $s(x)=
The following lemma (proved in the appendix) states that
the effective upper bounds of chunks in heap lists atoms of $\varphi$
with respect to stacks\mihaela{r3: not clear}
with respect to stacks %\mihaela{r3: not clear}
can be captured by an {\EPbA} formula.
\begin{lemma}\label{lem-eub}
......
%!TEX root = tab2021.tex
%!TEX root = atva2021.tex
%\section{Decision procedure for $\sla(\blk,\hls{},\pto)$}
......@@ -75,8 +75,8 @@ Recall that a \emph{preorder} $\preceq$ over a set $A$
%\vspace{-2mm}
\begin{definition}[Total preorder compatible with $\abs(\varphi)$]
Let $\preceq$ be a total preorder over $\addr(\varphi) \cup \addr(\psi)$. Then $\preceq$ is said to be \emph{compatible with} $\varphi$ if\mihaela{r2: symmetry?}
$\abs(\varphi) \wedge C_\preceq$ is satisfiable, where
Let $\preceq$ be a total preorder over $\addr(\varphi) \cup \addr(\psi)$. Then $\preceq$ is said to be \emph{compatible with} $\varphi$ if
$C_\preceq \wedge \abs(\varphi)$ is satisfiable, where
\begin{align}\label{eq:start-end}
C_\preceq & \triangleq &
\bigwedge_{t_1, t_2 \in \addr(\varphi) \cup \addr(\psi), t_1 \simeq t_2} t_1 = t_2 \wedge \bigwedge_{t_1, t_2 \in \addr(\varphi) \cup \addr(\psi), t_1 \prec t_2} t_1 < t_2.
......
%!TEX root = tab2021.tex
%!TEX root = atva2021.tex
%\newpage
......@@ -25,7 +25,7 @@ supports the new theory \slah.
Internally, \cspenp\ parses the input file
which shall include the definition of $\hls{}$
%ESOP 21 Reviewer 3: so this isn't built in specially? Or is it just that the tool expects the definition to be there because of the format? Does the definition have to be in syntactically exactly the form expected?
and the satisfiability or entailment queries in the SL-COMP format~\cite{DBLP:conf/tacas/SighireanuPRGIR19}.
and the satisfiability or entailment queries in the SL-COMP format~\cite{SLCOMPsite}.
%
\begin{compactitem}
\item For satisfiability queries,
......
%!TEX root = tab2021.tex
%!TEX root = atva2021.tex
\section{Introduction}
......@@ -18,7 +18,7 @@ and predicate atoms $P(\vec{x})$ defining unbounded memory regions of a particul
are composed using the separating conjunction to specify the disjointness of memory blocks they specify.
Let us briefly summarize the results on the SH fragments in the sequel.
For the SH fragment with the list-segment predicate, arguably the simplest SH fragment, its satisfiability and entailment problems have been shown to be in PTIME~\cite{CookHOPW11} and efficient solvers have been developed for it~\cite{PerezR13,DBLP:conf/tacas/SighireanuPRGIR19}.
For the SH fragment with the list-segment predicate, arguably the simplest SH fragment, its satisfiability and entailment problems have been shown to be in PTIME~\cite{CookHOPW11} and efficient solvers have been developed for it~\cite{SLCOMPsite}.
%
The situation changes for more complex inductive predicates:
The satisfiability problem for the SH fragment with a class of general inductive predicates was shown to be EXPTIME-complete~\cite{DBLP:conf/csl/BrotherstonFPG14}. On the other hand, the entailment problem for the SH fragment with slightly less general inductive predicates was shown to be 2-EXPTIME-complete~\cite{KatelaanMZ19,DBLP:conf/lpar/EchenimIP20}.
......@@ -37,7 +37,7 @@ used to jump from a memory chunk to the next one \cite{Knuth97,WJ+95}.
%
%One of the fundamental data structures used in these programs are heap lists
%
There have been some work to use separation logic for the static analysis and deductive verification of these low-level programs~\cite{CalcagnoDOHY06,conf/lopstr/FangS16,Chlipala11,MartiAY06}.
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.
Furthermore, the decidability can be preserved even if ASL is extended with the list-segment predicate~\cite{DBLP:journals/corr/abs-1802-05935}.
......@@ -45,7 +45,9 @@ Very recently, Le identified in~\cite{DBLP:conf/vmcai/Le21} two fragments
of ASL extended with a class of general inductive predicates for which
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,conf/lopstr/FangS16,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}.}.
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 pointer arithmetic inside inductive definitions}?
......@@ -81,7 +83,7 @@ The first category includes the predicate specifying acyclic singly linked list
\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{PerezR13,DBLP:conf/tacas/SighireanuPRGIR19}.
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}
......@@ -120,7 +122,7 @@ From this definition, a heap list between addresses $x$ and $y$ is
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,conf/lopstr/FangS16} as well as deductive verification~\cite{Chlipala11,MartiAY06}, its decidability
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
......@@ -169,7 +171,7 @@ We also push the solver in the corner cases of our decision procedures
by providing randomly generated problems for each case.
This study is original to our knowledge, although the separation logic
with heap-list has been used in
static analysis~\cite{CalcagnoDOHY06,conf/lopstr/FangS16}
static analysis~\cite{CalcagnoDOHY06}
and deductive verification~\cite{Chlipala11,MartiAY06}
of memory allocators. Indeed, such work uses sound procedures
or interactive theorem provers and does not consider the decision problem.
......
%!TEX root = tab2021.tex
%!TEX root = atva2021.tex
\section{\slah, a separation logic fragment for heap-list}
\label{sec:logic-hls}
......@@ -72,7 +72,7 @@ the interpretation of terms in the given stack;
$s(t)$ is defined by structural induction on terms:
$s(n) = n$, and
$s(t + t') = s(t) + s(t')$.
We denote $s[x\mapsto n]$ for a stack defined as $s$ except for the
We denote $s[x\gets n]$ for a stack defined as $s$ except for the
interpretation of $x$ which is $n$.
Notice that $\infty$ is used only to give up the upper bound
on the value of the chunk size in the definition of $\hls{}$
......@@ -114,11 +114,11 @@ $s,h \models t_1 \pto t_2$ iff $\exists n\in\NN$ s.t.
\item $s,h \models \hls{}(t_1, t_2;t_3)$ iff
$\exists k \in\NN$ s.t. $s,h \models \hls{k}(t_1, t_2;t_3)$,
\item $s,h \models \hls{0}(t_1, t_2;t^\infty)$ iff
\item $s,h \models \hls{0}(t_1, t_2;t^\infty)$ iff
$s,h \models t_1 = t_2 : \emp$,
\item
$s,h \models \hls{\ell+1}(t_1, t_2;t^\infty)$ iff
$s,h \models \hls{\ell+1}(t_1, t_2;t^\infty)$ iff
$s,h \models
\exists z\cdot 2 \le z-t_1 \land \Pi' : t_1\pto z-t_1\ \sepc
\blk(t_1+1,z) \sepc \hls{\ell}(z,t_2;t^\infty),
......@@ -133,7 +133,7 @@ $s,h \models \Sigma_1 \sepc \Sigma_2 \mbox{ iff }
\item
$s,h \models \exists\vec{z}\cdot\Pi:\Sigma$ iff $\exists \vec{n}\in\NN^{|\vec{z}|}$ s.t.
$s[\vec{z}\mapsto\vec{n}],h\models\Pi$ and $s[\vec{z}\mapsto\vec{n}],h\models\Sigma$.
$s[\vec{z}\gets\vec{n}],h\models\Pi$ and $s[\vec{z}\gets\vec{n}],h\models\Sigma$.
\end{itemize}
\end{definition}
%\vspace{-2mm}
......@@ -149,14 +149,17 @@ because we consider that the location $y$ is the first after the last location i
%
Intuitively, an atom $\hls{}(x,y;v)$ with $v$ a variable
defines a heap lists where all chunks have sizes between $2$ and the value of $v$.
Notice that if $v < 2$ then the atom $\hls{}(x,y;v)$ has a model iff $x=y$.\mihaela{r2 CADE}
Notice that if $v < 2$ then the atom $\hls{}(x,y;v)$ has a model iff $x=y$.
%
With this semantics, the $\blk$ and $\hls{}$ predicates are compositional predicates~\cite{EneaSW15} and therefore they satisfy the following composition lemmas:\mihaela{r2 CADE}
With this semantics, the $\blk$ and $\hls{}$ predicates are compositional predicates~\cite{EneaSW15} and therefore they satisfy the following composition lemmas:
% \mihaela{r2 CADE}
%it is easy to show the following lemmas:
\begin{align}
\blk(x,y)\sepc\blk(y,z) \models & ~\blk(x,z) \label{lemma:blk}
\\
\hls{}(x,y;v_1)\sepc\hls{}(y,z;v_2) \models & ~\hls{}(x,z;\max(v_1,v_2)) \label{lemma:hls}
\hls{}(x,y;v)\sepc\hls{}(y,z;v) \models & ~\hls{}(x,z;v)
%\hls{}(x,y;v_1)\sepc\hls{}(y,z;v_2) \models & ~\hls{}(x,z;\max(v_1,v_2))
\label{lemma:hls}
\end{align}
%%i.e., such block definition is compositional.
%Similarly to \cite{BrotherstonGK17}, the block predicate may be employed
......
......@@ -1180,7 +1180,7 @@ FUNCTION {inproceedings}
}
if$
% new.block
format.doi output
% format.doi output
format.url output
% new.block
format.note output
......
......@@ -24,7 +24,7 @@
title = {Entailment Checking in Separation Logic with Inductive Definitions
is 2-EXPTIME hard},
booktitle = {{LPAR}},
series = {EPiC Series in Computing},
series = {EPiCSC},
volume = {73},
OPTpages = {191--211},
publisher = {EasyChair},
......@@ -299,8 +299,8 @@ series = {ISMM 2020}
number = {2},
OPTissn = {0001-0782},
doi = {10.1145/3211968},
journal = {Commun. ACM},
month = jan,
journal = {CACM},
OPTmonth = jan,
OPTpages = {86-95},
OPTnumpages = {10}
}
......
......@@ -2,7 +2,6 @@
\usepackage{amsmath,amssymb, latexsym, amsfonts}
\usepackage{mathtools}
\usepackage{stmaryrd}
\usepackage{cite}
%\usepackage{times}
%\usepackage{fancyhdr}
\usepackage{longtable}
......@@ -11,7 +10,7 @@
%\usepackage{hhline}
%\usepackage{url}
\usepackage{hyperref}
\usepackage{cite}
%\usepackage{cite}
\usepackage{graphicx}
\usepackage{wrapfig}
\usepackage{float}
......
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