source: src/ASM/TACAS2013-policy/REVIEWS @ 3415

----------------------- REVIEW 1 ---------------------
PAPER: 9
TITLE: On the correctness of a branch displacement algorithm
AUTHORS: Jaap Boender and Claudio Sacerdoti Coen

REVIEWER'S CONFIDENCE: 4 (expert)

Matita verification of an algorithm for branch displacement, which is
compilation of assembly language jump instructions into concrete machine
language jump instructions of various sizes and performance characteristics and
with varying addressing modes, aiming to optimize performance.  Execution is by
a fixed-point iteration, repeatedly promoting short-range jumps into
longer-range jumps as needed.

This seems to be the first treatment of an important part of a full verified
compiler pipeline, so I recommend acceptance.  The prose is good, but I found
the Matita code examples to be outright punitive for the reader (or at least
for this reader).  Anyone wanting that much detail will read your
implementation; you can use a conference paper more effectively by sticking to
the big picture, favoring diagrams and conventional mathematical notation.  I
expect most of the code details would really be close to obvious to a proof
assistant expert who had read a good informal description of your approach.

So, I would recommend removing almost all of that part of the paper, which
opens up space that could be used to merge with the concurrent CPP submission
on a different aspect of the same project.  The introduction and related work
sections of the two papers are already almost the same.

p4: "the distance between L0 and the branch to it are too large": "are" ought 
o be "is".
p9: "exeception" -> "exception"
p10: Problem with underscores being interpreted by LaTeX as subscripts in
"ppc_pc_map"

----------------------- REVIEW 2 ---------------------
PAPER: 9
TITLE: On the correctness of a branch displacement algorithm
AUTHORS: Jaap Boender and Claudio Sacerdoti Coen

REVIEWER'S CONFIDENCE: 3 (high)

This paper discusses the formal verification of an important assembler-level
code-size optimisation for a simple, resource constrained processor: deciding
which branch instruction to use for each conditional and unconditional jump (the
branch instructions vary in size).  The algorithm and the informal reasons why
it is correct are well explained.  However, the paper, as presented, is not
ready for publication; it sketches the proof, but does not draw out general
ideas that might be of use to the reader.  Because the algorithm verified is not
particularly complicated, this kind of contribution is essential if the paper to
stand on its own.

Here are two possibilities that would strengthen the paper and address the above
criticism:

- an analysis of the trade-offs made in the design of the algorithm in order to
 support verification.  Quantifying how much, in practice, the choices about
 always lengthening branches (which lead to an easy termination proof) increase
 the code size would give a good idea of whether its worth trying to invest the
 effort to verify a more complex version in the future.

- motivation for the main statement of correctness, by showing how it fits in to
 the overall verification of the assembler.  I can see how the main theorem on
 page 9 is a necessary condition for the algorithm to be correct, but it is not
 clear that it is sufficient, or how it would be used in the overall
 correctness statement of an assembler.  It constrains sigma (which is what the
 verified algorithm calculates), but the paper does not formalise the use of
 sigma to actually transform the code.  Thus, it is unclear that the
 correctness statement is really saying everything it needs to.  In particular,
 the semantics of the assembly language or machine code are not mentioned in
 it, even though the correctness of the assembler must be stated in term of
 them.

----------------------- REVIEW 3 ---------------------
PAPER: 9
TITLE: On the correctness of a branch displacement algorithm
AUTHORS: Jaap Boender and Claudio Sacerdoti Coen

REVIEWER'S CONFIDENCE: 3 (high)

This paper presents a new branch displacement algorithm, and certified
its correctness in the Matita proof assistant. 

I feel the technical contribution of the work is a bit too thin. 
For the algorithm design, if the authors view it as a contribution,
there should be more justification of it. The authors mention
the existence of sub-optimal algorithms in SDCC and gcc. Is the new
algorithm better than them? The authors mention that the new algorithm
is "at least as good as the ones from SDCC and gcc, and potentially
better. Its complexity remains the same ..." Can the authors provide
data to justify the claim? Also such a claim does not sound impressive
at all.

For the verification, it is unclear to me why it is challenging. 
It seems the correctness is defined based on syntactic comparison
between the assembly code and the target machine code only, which
should be straightforward. It does not involve semantics preservation 
and simulation proof. 

Also, instead of verifying the algorithm directly, would it be simpler
to implement a validator to check the consistency between the input
and the output of the algorithm, and then verify the correctness of the 
validator?

----------------------- REVIEW 4 ---------------------
PAPER: 9
TITLE: On the correctness of a branch displacement algorithm
AUTHORS: Jaap Boender and Claudio Sacerdoti Coen

REVIEWER'S CONFIDENCE: 4 (expert)

This paper verifies an algorithm for choosing branch instructions in an
assembler.  The algorithm requires multiple iterations, since a choice for one
branch instruction can affect the available choices for other branch
instructions.

I found it hard to consider this paper separately from the CPP submission
number 16 ("On the correctness of an optimising assembler for the MCS-51
microcontroller").  The "main correctness statement", for example, isn't so
interesting in isolation; what's more interesting is that the correctness of
the branch displacement algorithm is a building block for the correctness of
the entire assembler.  Both papers contain text introducing the same issues
regarding branch displacement, although this paper is the only one that
presents the actual algorithm for solving the branch displacement problem.
The algorithm itself is short enough to fit in either paper; it's the
exhaustive list of detailed invariants that require a second paper.  However,
these invariants aren't particularly easy or interesting to read.

One problem with the invariants' readability is the disconnection between the
algorithm's notation (in Figure 5) and the invariants' notation.  The variable
names are often different, and types are sometimes different ("acc" is a triple
in Figure 5, but is described as a pair in section 4.1).  To improve the
readability, I'd suggest annotating Figure 5 with Floyd-Hoare style invariants
(e.g. putting something like "invariant sigma_compact_unsafe(..., sigma)"
directly in the code).  To reduce the bulkiness of the invariants, you might
also consider using mathematical notation rather than Matita text, and only
showing a few small examples of Matita text to give the reader a sense of what
they look like.

Two cited papers (Robertson[8] and Szymanski[11]) show the NP-completeness of
problems closely related to the MCS-51 branch displacement problem.  However,
it's not obvious that the results imply the NP-completeness for MCS-51.  Each
cited paper shows a polynomial-time solution on a simple problem followed by an
NP-completeness proof for an extended problem.  For Robertson[8], the extension
has to do with storage allocation, which seems different from the MCS-51
problem.  For Szymanski[11], the extension has to do with complex assembly-level
expressions based on adding and subtracting label addresses.  The MCS-51
assembler doesn't seem to have this feature, so it's not clear that the
NP-completeness result can be taken directly from Szymanski[11], even if both
settings deal with similar "pathological" jumps.  If you want to rigorously
claim NP-completeness for your particular problem, you probably have to do your
own reduction.  Alternately, you can just say that similar problems are known
to be NP-complete, without claiming NP-completeness for the MCS-51 problem.

minor comments:

Figure 1 lists sizes of x86-64 instructions.  The last two entries appear to be
64-bit direct jumps, which surely would require more than 8 bytes to encode. 
Perhaps these are indirect jumps?

Figure 5 doesn't initialize the variable "new_sigma".

Section 4.1: "ppc_pc_map" is misformatted in the third paragraph.