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

Last change on this file since 3415 was 3304, checked in by boender, 8 years ago
  • added 2012 reviews
  • updated affiliation
File size: 8.4 KB
1----------------------- REVIEW 1 ---------------------
3TITLE: On the correctness of a branch displacement algorithm
4AUTHORS: Jaap Boender and Claudio Sacerdoti Coen
8Matita verification of an algorithm for branch displacement, which is
9compilation of assembly language jump instructions into concrete machine
10language jump instructions of various sizes and performance characteristics and
11with varying addressing modes, aiming to optimize performance.  Execution is by
12a fixed-point iteration, repeatedly promoting short-range jumps into
13longer-range jumps as needed.
15This seems to be the first treatment of an important part of a full verified
16compiler pipeline, so I recommend acceptance.  The prose is good, but I found
17the Matita code examples to be outright punitive for the reader (or at least
18for this reader).  Anyone wanting that much detail will read your
19implementation; you can use a conference paper more effectively by sticking to
20the big picture, favoring diagrams and conventional mathematical notation.  I
21expect most of the code details would really be close to obvious to a proof
22assistant expert who had read a good informal description of your approach.
24So, I would recommend removing almost all of that part of the paper, which
25opens up space that could be used to merge with the concurrent CPP submission
26on a different aspect of the same project.  The introduction and related work
27sections of the two papers are already almost the same.
29p4: "the distance between L0 and the branch to it are too large": "are" ought
30o be "is".
31p9: "exeception" -> "exception"
32p10: Problem with underscores being interpreted by LaTeX as subscripts in
35----------------------- REVIEW 2 ---------------------
36PAPER: 9
37TITLE: On the correctness of a branch displacement algorithm
38AUTHORS: Jaap Boender and Claudio Sacerdoti Coen
42This paper discusses the formal verification of an important assembler-level
43code-size optimisation for a simple, resource constrained processor: deciding
44which branch instruction to use for each conditional and unconditional jump (the
45branch instructions vary in size).  The algorithm and the informal reasons why
46it is correct are well explained.  However, the paper, as presented, is not
47ready for publication; it sketches the proof, but does not draw out general
48ideas that might be of use to the reader.  Because the algorithm verified is not
49particularly complicated, this kind of contribution is essential if the paper to
50stand on its own.
52Here are two possibilities that would strengthen the paper and address the above
55- an analysis of the trade-offs made in the design of the algorithm in order to
56 support verification.  Quantifying how much, in practice, the choices about
57 always lengthening branches (which lead to an easy termination proof) increase
58 the code size would give a good idea of whether its worth trying to invest the
59 effort to verify a more complex version in the future.
61- motivation for the main statement of correctness, by showing how it fits in to
62 the overall verification of the assembler.  I can see how the main theorem on
63 page 9 is a necessary condition for the algorithm to be correct, but it is not
64 clear that it is sufficient, or how it would be used in the overall
65 correctness statement of an assembler.  It constrains sigma (which is what the
66 verified algorithm calculates), but the paper does not formalise the use of
67 sigma to actually transform the code.  Thus, it is unclear that the
68 correctness statement is really saying everything it needs to.  In particular,
69 the semantics of the assembly language or machine code are not mentioned in
70 it, even though the correctness of the assembler must be stated in term of
71 them.
73----------------------- REVIEW 3 ---------------------
74PAPER: 9
75TITLE: On the correctness of a branch displacement algorithm
76AUTHORS: Jaap Boender and Claudio Sacerdoti Coen
80This paper presents a new branch displacement algorithm, and certified
81its correctness in the Matita proof assistant.
83I feel the technical contribution of the work is a bit too thin.
84For the algorithm design, if the authors view it as a contribution,
85there should be more justification of it. The authors mention
86the existence of sub-optimal algorithms in SDCC and gcc. Is the new
87algorithm better than them? The authors mention that the new algorithm
88is "at least as good as the ones from SDCC and gcc, and potentially
89better. Its complexity remains the same ..." Can the authors provide
90data to justify the claim? Also such a claim does not sound impressive
91at all.
93For the verification, it is unclear to me why it is challenging.
94It seems the correctness is defined based on syntactic comparison
95between the assembly code and the target machine code only, which
96should be straightforward. It does not involve semantics preservation
97and simulation proof.
99Also, instead of verifying the algorithm directly, would it be simpler
100to implement a validator to check the consistency between the input
101and the output of the algorithm, and then verify the correctness of the
104----------------------- REVIEW 4 ---------------------
105PAPER: 9
106TITLE: On the correctness of a branch displacement algorithm
107AUTHORS: Jaap Boender and Claudio Sacerdoti Coen
111This paper verifies an algorithm for choosing branch instructions in an
112assembler.  The algorithm requires multiple iterations, since a choice for one
113branch instruction can affect the available choices for other branch
116I found it hard to consider this paper separately from the CPP submission
117number 16 ("On the correctness of an optimising assembler for the MCS-51
118microcontroller").  The "main correctness statement", for example, isn't so
119interesting in isolation; what's more interesting is that the correctness of
120the branch displacement algorithm is a building block for the correctness of
121the entire assembler.  Both papers contain text introducing the same issues
122regarding branch displacement, although this paper is the only one that
123presents the actual algorithm for solving the branch displacement problem.
124The algorithm itself is short enough to fit in either paper; it's the
125exhaustive list of detailed invariants that require a second paper.  However,
126these invariants aren't particularly easy or interesting to read.
128One problem with the invariants' readability is the disconnection between the
129algorithm's notation (in Figure 5) and the invariants' notation.  The variable
130names are often different, and types are sometimes different ("acc" is a triple
131in Figure 5, but is described as a pair in section 4.1).  To improve the
132readability, I'd suggest annotating Figure 5 with Floyd-Hoare style invariants
133(e.g. putting something like "invariant sigma_compact_unsafe(..., sigma)"
134directly in the code).  To reduce the bulkiness of the invariants, you might
135also consider using mathematical notation rather than Matita text, and only
136showing a few small examples of Matita text to give the reader a sense of what
137they look like.
139Two cited papers (Robertson[8] and Szymanski[11]) show the NP-completeness of
140problems closely related to the MCS-51 branch displacement problem.  However,
141it's not obvious that the results imply the NP-completeness for MCS-51.  Each
142cited paper shows a polynomial-time solution on a simple problem followed by an
143NP-completeness proof for an extended problem.  For Robertson[8], the extension
144has to do with storage allocation, which seems different from the MCS-51
145problem.  For Szymanski[11], the extension has to do with complex assembly-level
146expressions based on adding and subtracting label addresses.  The MCS-51
147assembler doesn't seem to have this feature, so it's not clear that the
148NP-completeness result can be taken directly from Szymanski[11], even if both
149settings deal with similar "pathological" jumps.  If you want to rigorously
150claim NP-completeness for your particular problem, you probably have to do your
151own reduction.  Alternately, you can just say that similar problems are known
152to be NP-complete, without claiming NP-completeness for the MCS-51 problem.
154minor comments:
156Figure 1 lists sizes of x86-64 instructions.  The last two entries appear to be
15764-bit direct jumps, which surely would require more than 8 bytes to encode.
158Perhaps these are indirect jumps?
160Figure 5 doesn't initialize the variable "new_sigma".
162Section 4.1: "ppc_pc_map" is misformatted in the third paragraph.
Note: See TracBrowser for help on using the repository browser.