Commit 64946efe authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

review CADE-28

parent 8a381810
----------------------- REVIEW 1 ---------------------
SUBMISSION: 92
TITLE: Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions
AUTHORS: Mihaela Sighireanu, Wanyun Su and Zhilin Wu
----------- Overall evaluation -----------
The paper introduces a fragment of separation logic that the authors
call SLAH. (Separation Logic with Arrays + Hls predicate,
not sure what Hls means, maybe 'header list'?)
I find the paper nice and well-writen. The paper has a good
theoretical result, which has been implemented and seems to
be performing well.
What worries me a little bit, is the possibility that the extension
of SLA with hls is trivial, because chunks have form
struct chunk
{
unsigned int size; // total size of this chunk.
char[ ] data; // size >= 1.
}
and the algorithm of the running example is:
for( int* t = hbeg; t != hend; t += t -> size )
if( rsz == infty || rsz <= t -> size ) return t;
return nullptr
This algorithm
returns a pointer to the first chunk which has
sizeof( data ) >= rsz - 1 in a range of consecutive chunks.
This algorithm never does anything with the
data. So one could collapse the data field
into a single object, and pretend that the size of chunck
is always 2, or perhaps extend SL with a sizeof operator.
The resulting structure is only slightly richer than natural numbers.
I am not sufficiently familiar with the state of literature in SL
to judge this,
I find the paper well-written, technically transparant, and
I believe correct.
There are very few typos or possible improvements of presentation.
So, I put a good score combined with a low confidence, because
that is the place where this doubt belongs.
Page 6, Definition 1. Just add the truth constants \top and \bot to
the pure formulas, so that you don't have to write
(x=x) on page 7 line 6, which I find ugly.
Page 8, line 'constraint the address' -> 'constraint on the address'.
I think that the names head and tail are not well-chosen.
They somewhat fit to blk(t1,t2) if one remembers that blocks are part
of a kind of list, but not to the other cases.
Maybe begin( blk( t1,t2)) and end( blk( t1, t2 ))
(being consistent with C++ terminology) ?
Page 8, Lemma 1, 3d line, 'then there is an EPA formula' ->
'we can construct in polynomial time an EPA formula' (You write
it on top of page 9, but it must be part of the lemma,
which is a definition at the same time. If space permits
it would be better to put Abs^{+} in a separate definition.
4th line of Lemma 1, 'namely or every stack s, s \models Abs^{+} ...'
In such case, you must always put a filler, for example 'we have'.
Page 15, 3d last line before the conclusion. 'We noticed that when
the entailment problem is invalid, the heuristics implemented are able to
quickly find some total preorder'. This suggests a co-nondeterministic
complexity class, but you proved EXPTIME completeness in Theorem 2.
Do you believe that the problems that you are using
are in a lower class?
----------------------- REVIEW 2 ---------------------
SUBMISSION: 92
TITLE: Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions
AUTHORS: Mihaela Sighireanu, Wanyun Su and Zhilin Wu
----------- Overall evaluation -----------
This paper investigates a separation logic SLAH, an extension of Array Separation Logic (ASL) with a predicate for heap lists. The paper contributes decision procedures for the satisfiability and entailment problems leading to NP-complete and EXPTIME results respectively.
The NP-complete result for satisfiability is by reduction from EPA satisfiability (from the stronger equi-satisfiability result). The EXPTIME result for entailment is via a decision procedure that explores the (exponential) space of possible orderings of endpoints of spatial atoms.
The problem is reasonably well-motivated, although the example and evaluation problems are relatively small. As highlighted in the paper, pointer arithmetic is mostly confined to low-level programs. Although it is notoriously difficult to reason with.
The writing is relatively dense and makes slightly more assumptions about the reader's awareness of separation logic terminology than I would expect at CADE. The motivating example in Section 2 is a good idea but I felt a bit lost until I returned to it after going through Section 3. There appear to be some assumptions made in a few places that could be explained.
The encoding in EPA is nice but the encoding of blocks and heap lists seemed straightforward (perhaps one of those 'easy when you see it' things) whilst the more involved issue of encoding separation is left for the Appendix. The decision procedure for entailment could have been summarised more clearly at the start as the overall idea is simple (with the details clearly requiring some effort).
I didn't find any problems in the proofs.
The evaluation section was nice, demonstrating effectiveness for some problems. Are your benchmarks available? One thing that is unclear is the scale of the benchmarks being addressed and the generality of this result. Are the numbers artificial due to the artificial nature of the benchmarks - will these methods be applicable in 'real' situations?
Overall, this paper seems to have a nicely sized contribution to an interesting (timely?) problem. The presentation doesn't appear to have major issues although could be improved. Therefore, I (weakly) recommend acceptance.
Small comments:
- I found things like '0 < b = t' as shorthand for 'e < b /\ b=t' a bit difficult to parse at points.
- p4, explain the two-arg hls predicate earlier - I wasted time trying to match the three-arg definition against the two-arg usage in Fig 1.:
- p4, you could include some intuition about the summaries: if v=2 then every chunk has size 2 and the overall heap list has even size.
- p5, near top. We don't know what 'a' is or what 'head(a)' and 'tail(a)' are here.
- p7,in the SLAH semantics in the rule for hls^{l+1} what is x? how does the recursion work as t1, t2, t2 do not change.
- It strikes me that equation 8 could be more general if v were replaced by v1 and v2 on the left and by max(v1,v2) on the right. I assume this doesn't really help.
----------------------- REVIEW 3 ---------------------
SUBMISSION: 92
TITLE: Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions
AUTHORS: Mihaela Sighireanu, Wanyun Su and Zhilin Wu
----------- Overall evaluation -----------
= Summary =
This article describes SLAH, a separation logic
for handling pointer arithmetic in heap lists.
The article defines the syntax and semantics,
satisfiability and entailment problem of SLAH formulas.
Decision procedures are provided to address
the satisfiability and entailment problem.
An implementation on top of the Compspen tool
is described and evaluated on a number of benchmarks.
= Review =
Being able to reason about an inductive definition with pointer
arithmetic is an important point in real-world software verification.
The solutions proposed in the paper for handling heap
lists are a valuable contribution.
The idea of rewriting the SLAH formulas in Presburg
arithmetic for the satisfiability problem, and using
this rewriting, in combination with an unfolding, splitting
and merging system, to solve the heaping problem is interesting.
This idea result in the implementation and evaluation of a automatic
solver for SLAH formulas.
However, the tool and benchmark are not available.
It would have been interesting to see the benchmark suite
to better judge the potential of the work.
I see two main limitations to this work.
First, the syntax and translation into
Presburg arithmetic implies that only
linear pointer arithmetic is supported
which reduces the number of verifiable programs.
Second, SLAH is limited to the heap list.
Thus, different inductive definitions are not supported.
This restricts the logic to the specific case where
we have a continuous memory region.
As proposed in the paper, memory allocators can
be an example of application, but it is not always true.
Future work seems to address this limitation.
Finally, the reading of the document is sometimes difficult in Section 5
due to the lack of explanation or internal reference to the appendixes.
A few comments/questions on parts of the paper follow.
== 1. Introduction ==
Page 2: subsection Motivation:
I think a work worth mentioning is
"Ghost for Lists: A Critical Module of Countiki Verified in Frama-C"
by Allan Blanchard et al.
The paper presents verification of a linked list library with
a tool based on array separation logic.
The proposed approach use lot of annotation but shows
that array separation logic can be applied to the verification
of inductive definition of lists in C.
== 2. Motivating example and overview ==
Page 4, 4th line before the end "the translation of \phi
into an equi-satisfiable Presburger arithmetic" :
what is \phi in this context (a formula of SLAH, but it is not said).
Page 5, 2th line : "For v = \infty, the summary is 2 < y-x."
Wouldn't it be rather the case "2 < v" (according to the Lemma 1) instead of "v = \infty"
== 3. SLAH, a separation logic fragment for heap-list ==
Page 6: "Notice that \infty is used only to give up the upper bound
on the value of the chunk size in the defintion of hle"
I don't understand the sentence in this context. Where is the expression \infty used?
Page 7, second item of the SLAH semantic:
shouldn't the third parameter of "hls" be "t^(\infty)" rather than "t_3"?
Page 7, fourth item of the SLAH semantic:
What does "x" represent here? Shouldn't it be "t_1". Shouldn't the recursive call to "hls" be made with "t_1'".
Page 7 "Notice that if v < 2 then the atom hls(x,y:v) has no model and is unsatifiable"
Isn't an empty heap and a stack s(v) = 0 (associating all address
variables to 0) a model of hls(x,y:v) when v < 2?
== 5. Entailment problem of SLAH ==
Page 10, line 2 of Defintion 3 "is said to be compatible with \phi if EXP" :
In the rest of the article, the symmetry of EXP is used.
Perhaps use the symmetry of EXP also here.
Page 10 subsection 5.2 Consequent with one spatial atom "Because EXP, we simplify this entailment to deciding":
It is not clear where the claim EXP comes from, unless you go to the appendix by yourself since
the complete definition of "Abs" is never given or described.
Page 12 Lemma 3:
It is not clear what the meaning of the variable z is,
unless you go to the appendix by yourself.
In general for this section high level explanations would be welcome
for compression reasons and avoid switching to the appendices.
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