source: Papers/cpp-asm-2012/reviews.txt @ 2334

Last change on this file since 2334 was 2334, checked in by sacerdot, 7 years ago

Only relevant pieces of reviews left in place.

File size: 14.7 KB
1----------------------- REVIEW 1 ---------------------
21) The main weakness of the paper is the detailed presentation of lemma statements.  I believe it would be better to focus on the high-level insights, from which competent readers could then reconstruct the lemma statements and proofs.  Following this advice would open up substantial space, which I believe could profitably be used to combine this paper with the simultaneous CPP submission by the same group.  It would be nice to have a single conference-length paper that explains all the key insights.
42) One contribution of this paper is the novel way of reasoning about assembly programs that may do address arithmetic.  From the abstract, it is not clear that the current development supports no such safe arithmetic, but rather the approach is conjectured to support easy extension for that kind of code.  I think this is a reasonable position, but the speculative nature of the motivation ought to be made clearer earlier.
6Page 3, "We only remark", perhaps add "that" after?  (and there is a double "of of" shortly after)
8Page 4, "preinstruction" definition: why does "ADD" get two arguments, instead of merging the two "fixed-length vectors"?  Or perhaps I misunderstand what this last term means.
10Page 6, "problems consists", both shouldn't end in "s"
12Page 8, "In plain words, the type of assembly": last word should probably be in code font
14Page 10, "lemmas appears", both shouldn't end in "s"
16Page 12, extraneous comma, "corresponding, source"
18Page 14, "to constraint" should be "to constrain"
19Page 14, "modes than the" should be "modes that the"
22----------------------- REVIEW 2 ---------------------
231) The program committee noted that the research described here was split between two papers, "On the correctness of an optimising assembler for the MCS-51 microcontroller" and "On the correctness of a branch displacement algorithm".  After some discussion, we decided to accept only one of these two papers.  To strengthen the one accepted paper, we recommend (but do not require) that the key results from both submissions be presented in the one accepted paper.  This would, as the other reviews point out, lead to "a higher concentration of interesting results" with more "focus on the high-level insights".
252) The current implementation appears to be pretty restrictive in what operations are allowed on symbols.  As far as I could see, you can push and pop them from the stack (particularly in call/return instructions), but that's about it.  It appears that you can't compare symbols for equality (e.g. to test two function pointers for equality in C), for example.  In fact, I'm not sure you can even move function pointers around between variables (at least, I couldn't find the place that would update the map during moves).  Do you allow jump tables of code addresses to implement C switch statements?  These would be good examples to motivate the definitions in section 3.5, which is currently pretty hard to understand.  (If you want a more challenging example, you might consider garbage collection tables that map code addresses to GC data; some collectors do binary search on code addresses to find entries in the tables.)
273) The definition of assembly-level state (with symbolic addresses or a map that locates the symbolic addresses) and machine-level state (bytes, with no symbols) should be central to the paper.  Unfortunately, these concepts are buried in section 3.5's explanations of internal_pseudo_address_map, low_internal_ram_of_pseudo_low_internal_ram, status_of_pseudo_status, etc., which are too dense, appear too late in the paper, and rely on knowledge of the MCS-51 that the paper only hints at (e.g. low and high internal memory).  Furthermore, the definitions of Status and PseudoStatus never appear at all.  I'd suggest starting with the definitions of registers, memory, internal_pseudo_address_map, and Status/PseudoStatus, and then working through the details of the assembler later in the paper.  This would ensure that the main theorem is understandable.  Compared to the main theorem, the other lemmas are less critical to the paper.  Section 3.4, in particular, could be greatly shortened
28; much of it is devoted to showing how machine instructions and bytes are concatenated together, which I found less interesting and more tedious than the paper's other sections.
304) How do you model I/O operations?
315) How do you plan to run the assembler?  Can you extract an executable assembler from the Matita implementation?
326) Right now, the proofs and specifications are mixed together in the Matita files.  Is there a way to isolate and quantify the definitions that you trust for correctness (the "trusted computing base")?
347) "We first attempted to synthesise[sic] a solution bottom up...."  This paragraph is vague.  Either omit the paragraph, or be more specific about the "solutions" under consideration.
368) Section 3.1, definition of execute_1: say what "cm" stands for.  (In fact, throughout the paper, try to say what the variables are as they are introduced.)
389) Section 3.4: "is obtained by composition of expand_pseudo_instruction and assembly_1_pseudoinstruction":  "composition" usually means the output of one function is the input to the other function.
4010) Section 3.4, lemma fetch_assembly_pseudo: the variable "instructions" is not in scope (did you mean "instrs"?).
4211) Section 3.4: "Here, l is the number of machine code instructions".  "pc_plus_len" is computed by adding pc to l, so wouldn't "number of bytes" make more sense?
44----------------------- REVIEW 3 ---------------------
45page 2, line 4: giveth --> given, taketh --> taken ?
46page 9, Huth et al [15] --> Tuch et al [15] ?
48The term "total correctness" used in Sec. 3.4 and 3.5 is confusing,
49since it has already been used in Hoare logic with standard meaning.
52----------------------- REVIEW 4 ---------------------
53  (i)   The presentation is needlessly complicated and difficult to
54        understand; while individual sentences are well-written, they
55        sometimes lack precision,
57  (ii)  The most delicate and interesting part of the problem seems to be
58        the translation of jump offsets, but the algorithm for this has been
59        submitted as a companion paper; it may have been better to submit a
60        single, self-contained paper with a higher concentration of
61        interesting results.
63  (iii) The notion of `well behaved' assembly programs is either not
64        described clearly enough, or not adequately developed. It seems to
65        relie on `run-time' checks for correct address manipulation. In
66        fact, these checks seem to be made at `emulation-time' (since the
67        generated code is not changed to implement the checks), and it is
68        not clear whether (or how) this covers all possible program
69        behaviours.
711. The title talks about an _optimising_ assembler, but the only
72   optimisation seems to be in calculating branch displacements and this
73   question is only partially resolved in the paper. Can assemblers be
74   expected to perform any other optimisations?
762. The abstract talks about "the efficient expansion of
77   psuedoinstructions---particularly jumps---is complex", but given that
78   this is the sole optimisation, it would seem more accurate to say
79   "...---namely jumps". Furthermore, the word "complex" is perhaps
80   overreaching.
823. Some parts of the text lack precision. Namely:
84   a. p.2: "what one hand giveth, the other taketh away"---it seems rather
85      to be a question of a straight-out engineering tradeoff in processor
86      choice. Furthermore, the MCS51 is memory constrained by the fact that
87      it is an 8-bit microcontroller; but there would seem to be sufficient
88      memory for the tasks it is expected to perform. This does not mean
89      that the calculation of jumping instructions is not a worthy problem,
90      but I question whether it is as critical as stated.
92   b. p.2: The last paragraph states that the proof is effected in "a
93      rather profound way", and that the proof of correctness may descend
94      into a "diabolical quagmire". In my opinion, these literary
95      flourishes waste space that could instead be used for more accurate
96      descriptions.
98   c. p.3: "heavily exploit", why not just "exploit"?
100   d. p.4: suggest replacing "and so on" with a more accurate description.
102   e. p.6: "The function assembly_1_psuedo_instruction ... is essentially
103      the composition of the two passes": is it or isn't it?
105   f. p.6: "... markedly different ways": well, all of the instructions jump
106      to one place or another, so they're not that different!
108   g. p.6: "MCS-51's limited code memory"; why not state the limits?
110   h. p.14: "this policy is the only possible policy _in theory_ that can
111      preseve the semantics..."; what does this mean exactly? It would seem
112      that the approach being presented is a counterexample to this
113      statement.
1154. The question of the MCS51's precise and predictable timing model is quite
116   interesting, but not discussed thoroughly in the paper. The second page
117   talks about "timing characteristics" and I/O but it is not completely
118   clear what is meant. Choosing one branching strategy over another will
119   obviously change the cycle-level timing of a program. The paper does not
120   discuss this in detail, nor whether it is important or not. Apart from
121   that, how else could the timing be changed by choices in the assembler?
123   The paper talks about "costing" in the encompassing CerCo project, but
124   few precise details are given. In particular, whenever "cost" is used in
125   the paper, does it just refer to the number of cycles required to execute
126   a sequence of instructions? If so, why use the more abstract term?
1285. The paper does not mention the issue of placing assembler subroutines in
129   memory? Is this not an issue? Could placement choices affect code size
130   (from jump instructions) significantly?
1326. p.4: It seems to me that the paper would have been much easier to
133   understand had it included more "sign posting". For instance, the start of
134   section 3 might state that there will be two models: one where jump
135   destinations are specified using relative offsets, and another where they
136   are given as labels. And, in fact, that the whole point is to translate
137   accurately from one to the other. The paper might then summarise
138   reference [4], which is very nicely written, to motivate the issue of
139   calculating branch displacements.
141   It might also state the two other issues are the correctness of assembly
142   encoding/fetching, and a notion of "well behaved" programs that modify
143   addresses in "reasonable" ways.
1457. p.5: It would be nice to see the type of the "preamble"; is it just a
146   DATA section?
1488. The paper does not discuss the complete tool chain. Does the verified
149   development parse MCS51 assembler and spit out a binary image?
1519. p.5: Why is "Word" and not "Identifier" or "nat" used to index psuedo
152   instructions? Or maybe even a type synonym so there is no risk of
153   confusion with the type used to index instructions.
155   For instance, it would be nice if the statement "The function sigma maps
156   pseudo program counters to program counters" were better reflected in the
157   type of sigma.
15910. p.6: I did not really understand what the paragraph "In contrast to other
160    approaches, we do not perform any kind of symbolic execution..." was
161    trying to say.
16311. pp.7--9: this text talks about "program counters", when I think it
164    means "addresses" (i.e., values that the program counter may take).
16612. It is confusing that the variable called "policy" is only one part of
167    the concept "policy".
16913. p.8: I didn't understand why it is sometimes necessary to force the
170    expansion of jumps to the largest size possible.
17214. p.11: states that "we must detect (at run time) programs that manipulate
173    addresses in well behaved ways". But what does this mean exactly? Given
174    that the output program is not augmented with checks, it seems that the
175    authors mean "at emulation time". But how can this be exhaustive (for
176    all input values and for non-terminating executions)? Are there some
177    kind of necessary conditions for having a well-behaved program? Must
178    users provide a proof of well-behavedness for each program before they
179    can be sure that its assembly is correct? Isn't this rather a typing
180    issue? Is there any relation with the work of Greg Morriset et al on
181    Typed Assembly Language?
18315. The paper states that the work may be usable in the context of verified
184    operating systems kernels. This is a point worth discussing, but the
185    text could be more precise. The seL4 kernel requires memory protection
186    but the MCS51 has no MMU. Furthermore, the verification was specific to
187    the arm assembly language, where it would seem that the issue of branch
188    displacement is less significant.
190    Similarly, the paper discusses compilers like CompCert and the issue of
191    well-formedness. Again, this is a worthy point, but the discussion seems
192    to neglect the possibility that well formedness may be guaranteed by the
193    conversion from the high-level language, i.e. that all C programs may
194    compile into "well behaved" assembly programs. Is this true?
19616. The related work section touches on "timing properties of an assembly
197    program", but this issue is not treated in depth by the paper, and, in
198    fact, these sentences seem out of place.
20017. It is not clear why both references [5] and [6] are needed. Nor why both
201    references [7] and [8] are needed.
20318. Research Questions
205   a. Did you consider "running" your model in parallel with a real or
206      emulated MCS-51 to validate its correctness?
207      (as in the work of Peter Sewell et al's work on TCP/IP and memory
208       weak models; where they compare their models against real
209       implementations.)
211   b. Rather than verifying a branch displacement algorithm, did you
212      consider showing refinement between the input (assembler with labels) and
213      the output (modified assembler with offsets)? That way, the algorithm
214      could use whatever strategy it liked and the results would still be
215      verified. From my understanding, this is one of the approaches taken
216      in Xavier Leroy et al's CompCert project.
218x. Minor typos / issues
220   a. p.3: "we proved the implementation of the assembler": inconsistency of
221      verb tense.
223   b. p.3: The subsection heading "Overview of the paper." is unnecessary.
225   c. p.4: It would be helpful if the abbreviated definitions of
226       preinstruction, instruction, and pseudoinstruction included more
227       elements in common with themselves and with the other examples
228       (notably DEC).
230   d. p.10: "eject out" -> "project"
232   e. p.10: "lemmas appears" -> "lemmas appear"
234   f. p.11: "Huch" -> "Tuch"
236   g. p.14: "constraint" -> "constrain"
Note: See TracBrowser for help on using the repository browser.