Commit 38655c8d authored by ehilin02's avatar ehilin02
Browse files
parents 9646cea8 1f8a4ce9
%!TEX root = aplas2021.tex
\begin{abstract}
Pointer arithmetic is widely used in memory allocators. Moreover, heap list is a data structure used in many memory allocators, to describe the layout of the physical memory.
Heap list is a data structure used by many implementations of memory allocators
to organize the heap part of the program's memory.
%
%The verification of such programs usually requires simultaneous reasoning about pointer arithmetic and unbounded heap regions.
The specification of the programs in memory allocators usually requires using pointer arithmetic inside inductive definitions to define heap lists. % in memory allocators.
Operations on heap lists employ pointer arithmetics and therefore,
reasoning about the correctness of heap list implementations requires
to deal simultaneously with pointer arithmetic inside the inductive definition
specifying the heap list.
%
In this work, we investigate decision problems for SLAH, a separation logic fragment
that allows pointer arithmetic and an inductive definition for heap lists,
......
......@@ -72,7 +72,11 @@ and the satisfiability or entailment queries in the SL-COMP format~\cite{SLCOMPs
\smallskip
\mypar{Benchmarks.}
We generated 190 benchmarks,
ASL and \slah\ are not theories covered by the SL-COMP competition.
For ASL, the solver SLar~\cite{KimuraT17} provides some examples in an ad-hoc format
and not including inductive definitions with pointer arithmetics.
% Moreover, the examples used by SLar, available online, are in a format that seems nontrivial to translate into the SL-COMP format.
For these reasons, we had to generate a benchmark of 190 problems,
available at~\cite{benchmark},
%with 88 and 102 instances for the satisfiability and entailment problem respectively. These benchmarks are
classified into four suites, whose sizes are given in Table~\ref{tab-exp}, as follows:
......@@ -86,6 +90,7 @@ classified into four suites, whose sizes are given in Table~\ref{tab-exp}, as fo
join two memory chunks (equivalent to cell delete),
search a memory chunk of size bigger than a given parameter (our running example),
or search an address inside a heap-list.
The problems include formulas over 6 to 24 variables with 3 to 21 spatial atoms.
%
\item RANDOM-SAT and RANDOM-ENT are satisfiability resp. entailment problems
which are randomly or manually generated.
......@@ -96,6 +101,7 @@ classified into four suites, whose sizes are given in Table~\ref{tab-exp}, as fo
and end address terms are generated randomly.
In addition, we generate some benchmarks manually.
This suite is motivated by testing the scalability of \cspenp.
The problems include formulas over 4 to 48 variables with 4 to 16 spatial atoms.
%which usually contain more spatial atoms than those in MEM-SAT and MEM-ENT, motivated by testing the scalability of \cspenp.
\end{itemize}
%
......@@ -119,11 +125,13 @@ classified into four suites, whose sizes are given in Table~\ref{tab-exp}, as fo
\smallskip
\mypar{Experiments.}
We run \cspenp over the four benchmark suites, using a Ubuntu-16.04 64-bit lap-top with an Intel Core i5-8250U CPU and 2GB RAM.
We run \cspenp\ over the four benchmark suites, using a Ubuntu-16.04 64-bit lap-top with an Intel Core i5-8250U CPU and 2GB RAM.
The experimental results are summarized in Table~\ref{tab-exp}. We set the timeout to 60 seconds. The statistics of average time and maximum time do not include the time of timeout instances.
To the best of our knowledge, there have not been solvers that are capable of solving the \slah\ formulas that include, points-to, block, and $\hls{}$ atoms.
To the best of our knowledge, the existing solvers are not able to solve \slah\ formulas that include points-to, block and $\hls{}$ atoms.
The solver SLar~\cite{KimuraT17} was designed to solve entailment problems involving points-to, block, and $\ls{}$ atoms. Nevertheless, we are unable to find a way to access SLar, thus failing to compare with it on ASL formulas.
Moreover, the examples used by SLar, available online, are in a format that seems nontrivial to translate into the SL-COMP format.
% Moreover, the examples used by SLar, available online, are in a format that seems nontrivial to translate into the SL-COMP format.
%In satisfiability problems, sat means the formula is satisfiable;
%In entailment problems, unsat means the entailment is valid.
......@@ -169,13 +177,13 @@ namely MEM-SAT and MEM-ENT, with the average time in 0.05 and 3.05 seconds respe
Table~\ref{tab-exp} shows that some entailment instances
are challenging for \cspenp. %\todo{speed if size increase}
For instance, the maximum time in MEM-ENT suite is
9.98, and there are 2 timeout instances in RANDOM-ENT suite (more than 2 min).
9.98 seconds, and there are 2 timeout instances in RANDOM-ENT suite (solved in more than 2 minutes).
By inspecting these challenging instances, we found that
(i) they require splitting some spatial atoms ($\blk{}$ or $\hls{}$) in the antecedent,
which is potentially time-consuming, and
(i) they require splitting some spatial atoms ($\blk{}$ or $\hls{}$) in the antecedent,
which is potentially time consuming, and
(ii) they correspond to valid entailment problems
where \cspenp\ has to explore all the total preorders,
which is time-consuming.
which is time consuming.
We noticed that when the entailment problem is invalid,
the heuristics implemented are able to quickly
find some total preorder under which the entailment does not hold.
......
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