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

rebuttal with MS response

parent bb8739f8
We thank the reviewers for their constructive comments.
We answer below to their main questions.
=== Generality of the result
Although we illustrate the usage of SLAH on the simple example
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
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
predicate does not capture the change of size of the new chunk.
In this case, the decision procedure is able to show that
the change of size in the first collapsed chunk implies
that a new chunk is defined, i.e.:
x2-x1=sz1 >= 2 /\ x3-x2=sz2 >= 2 :
x1->sz1+sz2 * blk(x1+1,x2) * x2->sz2 * blk(x2+1,x3)
|= x3-x1=sz1+sz2 >=4 : hls(x1,x3)
Reviewer 3 pointed out that our logic is limited to
"linear pointer arithmetic", which is true. However,
our approach can be extended to decidable extensions of
Presburger arithmetics, although we don't found any
application for that. Notice that Presburger arithmetics
may deal with modulo constraints, which may cover interesting
examples of non-linear pointer arithmetics.
=== Availability of the benchmark
Our benchmark is available in the directory samples/cade28 of
[1] https://github.com/gaochong1111/compspen
We are sorry not mentioning this explicitly in Section 6.
The reviewers may visit this site and notice that the status
of the benchmark is not changed from the submission deadline.
=== Complexity evaluation
Reviewer 1 highlighted a point concerning the complexity class of
entailment problem given the experimental results which are suggesting
co-nondeterministic complexity class. We notice that this behaviour
has been observed experimentally for our benchmark. Our heuristics
to quickly found an counter-example exploit the syntax of formulas.
However, the full fragment has an EXPTIME complexity.
Dear Mihaela,
Thank you for your submission to CADE-28. The rebuttal period starts now, and ends 6pm AOE March 31st 2021. During this time, you will have access to the current state of your reviews, and have the opportunity to submit a concise rebuttal. Please keep in mind the following during this process:
* The rebuttal must focus on any factual errors in the reviews and any questions posed by the reviewers. It may not provide new research results or reformulate the presentation. Try to be as concise and to the point as possible.
* The rebuttal period is an opportunity to react to the reviews, but not a requirement to do so. Thus, if you feel the reviews are accurate and the reviewers have not asked any questions, then you do not have to respond.
* The reviews are as submitted by the PC members, without any coordination between them. Thus, there may be inconsistencies. Furthermore, these are not the final versions of the reviews. The reviews can later be updated, and it may be necessary to solicit other outside reviews after the rebuttal period.
* The program committee will read your rebuttal carefully, and take it into account during the discussions. On the other hand, the program committee is nor required to respond to your rebuttal.
* Your response will be seen by all PC members who have access to the discussion of your paper, so please try to be polite and constructive.
The reviews on your paper are attached to this letter. To submit your rebuttal you should login to EasyChair for CADE-28 and select your submission on the menu.
Best wishes,
Geoff & Andre
----------------------- 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.
----------- Specific questions for rebuttal -----------
How can your results be reproduced?
Do your benchmarks reflect 'real' problems. How will your decision procedures scale to 'real' problems?
----------------------- 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