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

aplas: experiments size of problems

parent 5749735d
......@@ -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