Commit fa95ba29 authored by ehilin02's avatar ehilin02
Browse files

section 4 and 5

parent 68d3878d
......@@ -4,7 +4,6 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\hide{
\subsection{{\EPbA} summary of $\hls{}$ atoms}
\label{ssec:sat-hls-abs}
......@@ -95,7 +94,6 @@ which can be further simplified into
%This constraint is unsatisfiable if $c > d_0$.
\qed
\end{proof}
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......
......@@ -79,7 +79,7 @@ Zhilin Wu\inst{2}\orcidID{0000-0003-0899-628X}
%\vspace{-2mm}
\input{conclusion.tex}
\newpage
%\newpage
%------------------------------------------------------------------------------
\bibliographystyle{splncs04}
\bibliography{../bibs/biblio}
......
......@@ -89,7 +89,7 @@ with respect to stacks %\mihaela{r3: not clear}
can be captured by an {\EPbA} formula.
\begin{lemma}\label{lem-eub}
For an {\slah} formula $\varphi \equiv \Pi: \hls{}(t'_1, t'_2; t'_3)$, an {\EPbA} formula $\xi_{eub,\varphi}(z)$ can be constructed in linear time such that for every store $s$ satisfying $s \models \abs(\varphi)$, we have $s[z \gets \eub_\varphi(s)] \models \xi_{eub,\varphi}(z)$.
For an {\slah} formula $\varphi \equiv \Pi: \hls{}(t'_1, t'_2; t'_3)$, a formula $\xi_{eub,\varphi}(z)$ can be constructed in linear time such that for every store $s$ satisfying $s \models \abs(\varphi)$, we have $s[z \gets \eub_\varphi(s)] \models \xi_{eub,\varphi}(z)$.
\end{lemma}
The following lemma (proof in the appendix) provides the correct test used
......@@ -97,9 +97,11 @@ The following lemma (proof in the appendix) provides the correct test used
%for deciding the ordered entailment $\Pi: \hls{}(t'_1, t'_2; t'_3) \models_\preceq \hls{}(t_1, t_2; t_3)$ .
\begin{lemma}\label{lem-hls-hls}
Let $\varphi \equiv \Pi: \hls{}(t'_1, t'_2; t'_3)$, $\psi \equiv \hls{}(t_1, t_2; t_3)$, and $\preceq$ be a total preorder over $\addr(\varphi) \cup \addr(\psi)$ such that $C_\preceq \models t'_1 < t'_2 \wedge t'_1 = t_1 \wedge t'_2 = t_2$.
Then $\varphi \models_\preceq \psi$ iff $C_\preceq \wedge \abs(\varphi) \models \exists z.\ \xi_{eub, \varphi}(z) \wedge z \le t_3$.
Then $\varphi \models_\preceq \psi$ iff
%$C_\preceq \wedge \abs(\varphi) \models \exists z.\ \xi_{eub, \varphi}(z) \wedge z \le t_3$.
$C_\preceq \wedge \abs(\varphi) \models \forall z.\ \xi_{eub, \varphi}(z) \rightarrow z \le t_3$.
\end{lemma}
From Lemma~\ref{lem-hls-hls}, it follows that the entailment of
%\vspace{-4mm}
\subsubsection{At least two atoms in the antecedent:} Recall that
......
......@@ -24,17 +24,17 @@ Given the symbolic heaps $\varphi$ and $\psi$ in \slah\ such that
Our goal in this section is to show that the entailment problem is decidable, as stated in the following theorem.
\begin{theorem}\label{thm-entail}
The entailment problem of {\slah} is in EXPTIME.\mihaela{state upperbound}
The entailment problem of {\slah} is coNP-complete.\mihaela{state upperbound}
\end{theorem}
For comparison, the entailment problem of quantifier-free ASL formulas is in coNP~\cite{BrotherstonGK17}.
The remainder of this section is devoted to the proof of Theorem~\ref{thm-entail}.
The coNP lower bound follows from the fact that the entailment problem of quantifier-free ASL formulas is also coNP-complete~\cite{BrotherstonGK17}.
The remainder of this section is devoted to the proof of the coNP upper bound.
%where we propose the decision procedure for the entailment problem
%Let
%$\varphi \models \psi$ where
%In the rest of this section, let us assume that
%$\varphi = \Pi: \Sigma$ and $\psi = \Pi': \Sigma'$.
%
In a nutshell, we show in Section~\ref{ssec:order}
that the entailment problem $\varphi \models \psi$
can be decomposed into a finite number of ordered entailment problems
......@@ -49,7 +49,7 @@ In Section~\ref{ssec:ent-1}, we consider the special case
The general case is dealt with in Section~\ref{ssec:ent-all};
the procedure calls the special case for the first atom of the consequent with
all the compatible prefixes of the antecedent, and
it does a recursive call for the remainders of the consequent and the antecedent. Note that to find all the compatible prefixes of the antecedent, some spatial atoms in the antecedent might be split into several ones. The EXPTIME complexity is explained in the sequel: 1) the number of total preorders as well as different splittings of the spatial atoms in the antecedent is at most exponential, 2) the entailment of {\EPbA} formulas (with modulo constraints) can be solved in exponential time.
it does a recursive call for the remainders of the consequent and the antecedent. Note that to find all the compatible prefixes of the antecedent, some spatial atoms in the antecedent might be split into several ones. The coNP upper bound is explained in the sequel: 1) the original entailment problem is reduced to at most exponentially many ordered entailment problems since there are exponentially total preorders, 2) each ordered entailment problem can be reduced further to exponentially many special ordered entailment problems where there is one spatial atom in the consequent, 3) the original entailment problem is invalid iff there is an invalid special ordered entailment problem instance, 4) the special ordered entailment problem is in coNP.
%At first, it is easy to observe that if $\abs(\varphi)$ is unsatisfiable,
%then the entailment holds. Moreover, if $\abs(\varphi) \not\models \abs(\psi)$,
......
......@@ -14,9 +14,9 @@ The satisfiability problem of {\slah} is NP-complete.
The NP lower bound follows from that of ASL in \cite{BrotherstonGK17}. The NP upper bound is achieved by encoding the satisfiability problem of {\slah} as that of an existentially quantified Presburger arithmetic formula. The rest of this section is devoted to the proof of the NP upper bound.
Presburger arithmetic (\PbA) is the first-order theory with equality
of the signature $\langle 0,1,+, <\rangle$ interpreted over the
domain of naturals $\NN$ with `$+$' interpreted as the addition and
`$<$' interpreted as the order relation.\footnote{%
of the signature $\langle 0,1,+, <, (\bmod\ n)_{n \in \NN \setminus \{0\}}\rangle$ interpreted over the
domain of naturals $\NN$ with `$+$' interpreted as the addition,
`$<$' interpreted as the order relation, and $\bmod\ n$ interpreted as the modulo function.\footnote{%
Although `$<$' may be encoded using existential quantification in \PbA\ over naturals,
we prefer to keep it in the signature of \PbA\ to obtain quantifier free formulas.%
}
......@@ -27,8 +27,8 @@ we prefer to keep it in the signature of \PbA\ to obtain quantifier free formula
\PbA\ is a useful tool for showing complexity classes because its
satisfiability problem belongs to various complexity classes depending
on the number of quantifier alternations~\cite{Haase2018ASG}.
Here, we employ the $\mathsf{\Sigma}_1$-fragment of \PbA, which
contains existentially quantified Presburger arithmetic formulas (abbreviated as \EPbA). The satisfiability problem of {\EPbA} is NP-complete.
In this paper, we consider quantifier-free \PbA\ formulas (abbreviated as \qfpa) and the $\mathsf{\Sigma}_1$-fragment of \PbA (abbreviated as \EPbA), which
contains existentially quantified Presburger arithmetic formulas. The satisfiability problem of {\qfpa} and {\EPbA} is NP-complete.
%When the number of existentially quantified variables is fixed,
%the problem is P-complete.
%Moreover, the existential fragment of \PbA\
......@@ -90,23 +90,26 @@ Intuitively, the abstraction of the predicate atoms $\hls{}(t_1, t_2; t_3)$
for all $k \ge 1$ unfoldings of the predicate atom.
From the fact that the pure constraint in the inductive rule of $\hls{}$ is $2 \le x' - x \le v$, it is easy to observe that
for each $k \ge 1$, $\hls{k}(t_1, t_2; t_3)$ can be encoded by $2 k \le t_2-t_1 \le k t_3$. It follows that $\hls{}(t_1, t_2; t_3)$ can be encoded by $\exists k.\ k \ge 1 \wedge 2k \le t_2 - t_1 \le k t_3$.
If $t_3 \equiv\infty$, then $\exists k.\ k \ge 1 \wedge 2 k \le t_2-t_1 \le k t_3$ is equivalent to $\exists k.\ k \ge 1 \wedge 2k \le t_2 - t_1$, thus an {\EPbA} formula.
If $t_3 \equiv\infty$, then $\exists k.\ k \ge 1 \wedge 2 k \le t_2-t_1 \le k t_3$ is equivalent to $\exists k.\ k \ge 1 \wedge 2k \le t_2 - t_1 \equiv 2 \le t_2 - t_1$, thus a {\qfpa} formula.
Otherwise, $2 k \le t_2-t_1 \le k t_3$ is a non-linear formula since $k t_3$ is a non-linear term if $t_3$ contains variables.
The following lemma states that
%In the sequel, we are going to show that
$\exists k.\ k \ge 1 \wedge 2 k \le t_2 - t_1 \le k t_3$ can actually be turned into an equivalent {\EPbA} formula.
$\exists k.\ k \ge 1 \wedge 2 k \le t_2 - t_1 \le k t_3$ can actually be turned into an equivalent {\qfpa} formula.
\begin{lemma}[Summary of $\hls{}$ atoms]
Let $ \hls{}(x, y; z)$ be an atom in \slah\
representing a non-empty heap, where $x, y, z$ are three distinct variables in $\cV$.
%Then there is an {\EPbA} formula, denoted by $\abs^+(\hls{}(x,y; z))$,
We can construct in polynomial time an {\EPbA} formula $\abs^+(\hls{}(x,y; z))$
We can construct in polynomial time an {\qfpa} formula $\abs^+(\hls{}(x,y; z))$
which summarizes $\hls{}(x, y; z)$, namely we have
for every stack $s$, $s \models \abs^+(\hls{}(x,y; z))$ iff
there exists a heap $h$ such that $s, h \models \hls{}(x, y, z)$.
%Similarly for $ \hls{}(x, y; \infty)$ and $ \hls{}(x, y; d)$ with $d \in \NN$.
\end{lemma}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\hide{
\begin{proof}
The constraint that the atom represents a non-empty heap means that
the inductive rule defining $\hls{}$ in Equation~(\ref{eq:hlsv-rec})
......@@ -155,11 +158,14 @@ To sum up, we obtain
\end{align*}
\vspace{-2eX}\qed
\end{proof}
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
The formula $\abs(\varphi)$ is essentially a quantifier-free \PbA\ formula containing modulo constraints $t_1 \equiv r \bmod n$; the satisfiability of such formulas is still NP-complete.
Since the satisfiability problem of {\qfpa} is NP-complete,
%We are using $\abs^+(\hls{}(x, y; z))$ defined above
%to obtain in polynomial time an equi-satisfiable \EPbA\ abstraction for a symbolic heap $\varphi$, denoted by $\abs(\varphi)$.
Therefore, the satisfiability problem of \slah\ is in NP.
the satisfiability problem of \slah\ is in NP.
%
% ESOP'21, Reviewer 3: At the end of page 10, when discussing the abstraction idea, I wondered to what extent this is related to the decision procedures for ASL itself; is the overall approach new, or is it a similar approach with suitable extensions?
%For this reason, we leave
......@@ -176,6 +182,6 @@ A \slah\ formula $\varphi$ is satisfiable iff $\abs(\varphi)$ is satisfiable.
%\vspace{-2mm}
%Notice that $\abs(\varphi)$ is essentially a quantifier-free \PbA\ formula containing modulo constraints $t_1 \equiv r \bmod n$. The satisfiability of such formulas is still NP-complete.
From now on, we shall assume that {\bf $\abs(\varphi)$ is a quantifier-free \PbA\ formula containing modulo constraints}. This enables using the off-the-shelf SMT solvers, e.g. Z3, to solve the satisfiability problem of \slah\ formulas.
From now on, we shall assume that {\bf $\abs(\varphi)$ is a \qfpa\ formula}. This enables using the off-the-shelf SMT solvers, e.g. Z3, to solve the satisfiability problem of \slah\ formulas.
......@@ -9,7 +9,7 @@ given in the overview, this logic may capture invariant properties
for more complex examples, like the ones described in Section 6:
splitting a chunk or joining two contiguous chunks.
The first reviewer has right when he claims that the properties
The first reviewer is right when he claims that the properties
of the data block are not summarised by the inductive definition
of hls (heap-list). However, we don't agree with the fact that
the generalisation of two collapsed chunks into a heap-list
......
......@@ -34,6 +34,7 @@
\newcommand{\slah}{\textsf{SLAH}}
\newcommand{\PbA}{\textsf{PA}}
\newcommand{\EPbA}{\textsf{EPA}}
\newcommand{\qfpa}{\textsf{QFPA}}
\newcommand{\sphead}{\texttt{head}}
......
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