Commit 8a381810 authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

response CADE-28

parent a7ad9ed5
We thank the reviewers for their constructive comments. All the minor issues will be dealt with in the next version of this paper and the major concerns are addressed below.
---------- Review 1 ----------
Q: What worries me a little bit, is the possibility that the extension of SLA with hls is trivial, because heap chunks in hls do not talk about the contents of the data (memory block). So one could collapse the data field in heap chunks into a single object, and pretend that the size of each chunk is always 2, or perhaps extend SL with a sizeof operator.
A: It is right that the hls predicate does not talk about the contents of the chunk's data. Nevertheless, this does not mean that the size of each chunk can be assumed to be 2 since pointer arithmetics are used here and the differences between the begin and end addresses of the chunk does matter. The extension of array separation logic (ASL) with hls is far from trivial, as explained below. The atom hls(x, y; v) differs from blk(x, y) in the sense that hls(x, y; v) requires that the heap is of a specific structure (the heap consists of a collection of memory chunks, where each chunk starts with a points-to atom x |-> sz followed by a block from x+1 to x + sz = y, and 2<= y - x <= v), while blk(x, y) does not enforce any structure on the memory block. This difference makes the satisfiability and entailment problems for SLAH considerably more challenging than ASL. For instance, even the entailment between two *single* hls atoms is nontrivial to solve, evidenced by the validity of the entailment y-x = 4 /\ hls(x, y; 3) |= hls(x, y; 2) (Example 2 in section 5.2).
Q: 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?
A: Thank the reviewer for asking this question. Theorem 2 only states the EXPTIME upper bound for the entailment problem of SLAH, but not the EXPTIME lower bound. Moreover, we know that the entailment of SLAH is coNP-hard, since it extends ASL, whose entailment is coNP-hard. It is possible that the entailment of SLAH can be shown in co-nondeterministic polynomial time by a clever refinement of the current decision procedure, which nonetheless seems nontrivial to achieve.
---------- Review 2 and 3 ----------
Q: The tool and the benchmarks are not available. Do your benchmarks reflect 'real' problems. How will your decision procedures scale to 'real' problems?
A: The tool is available at https://github.com/gaochong1111/compspen (the first reference) and the benchmarks are available in the directory samples/cade28 therein. We are sorry that this fact was not stated clearly in Section 6. The reviewers may visit the github website and notice that the status of the benchmarks is not changed from the submission deadline.
We did apply our decision procedures to ‘real’ problems, namely, the MEM-SAT and MEM-ENT benchmark suites (occupying more than half of our benchmarks), which are generated from the path constraints and verification conditions of the building blocks of well-known open-source memory allocators.
Q: How can your results be reproduced?
A: Our tool and benchmarks are publicly available at github. The reviewers and interested readers can download the source code, compile and run it on the benchmarks to reproduce the results.
Q: First, the syntax and translation into Presburger arithmetic implies that only linear pointer arithmetic is supported which reduces the number of verifiable programs.
A: Indeed, our logic supports only linear pointer arithmetic. However, it already covers many pointer operations in low-level programs. For instance, normal field access can be expressed by pointer offsets, and bit operations used to align pointers can be expressed by modulo constraints. Our results show that even only linear pointer arithmetic inside inductive definitions already makes the automated reasoning nontrivial. We agree that separation logic with non-linear pointer arithmetic is still an interesting question to be explored for automated reasoning.
Q: 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.
A: This work focuses on heap lists. Our results show that even heap lists are already nontrivial to deal with, which lays down a solid foundation for dealing with more general inductive definitions containing pointer arithmetic in the future.
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