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

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

Reviews committed.

File size: 22.5 KB
1Dear Claudio,
3Attached please find reviewer comments regarding your CPP submission,
4   On the correctness of an optimising assembler for the MCS-51 microcontroller.
6We trust that you will find these comments useful and constructive.
7Thank you for submitting to CPP.  We will send more information about
8submitting your final draft paper (in LNCS format) for the conference
9proceedings via EasyChair.
11We look forward to seeing you at the meeting in Kyoto. Note that APLAS
122012 is also collocated with CPP 2012.
14Sincerely, Chris Hawblitzel and Dale Miller, CPP 2012 PC Chairs
16Some useful links:
20----------------------- REVIEW 1 ---------------------
21PAPER: 16
22TITLE: On the correctness of an optimising assembler for the MCS-51 microcontroller
23AUTHORS: Dominic Mulligan and Claudio Sacerdoti Coen
27A partial Matita verification of the correctness of an optimizing assembler targeting a resource-constrained embedded processor.  The key challenge is compiling each jump to one of a variety of differently sized machine code instructions (or possibly a sequence of several) with different addressing modes.  Many of the proof obligations are discharged in the Russell style, using dependent sigma types in the original definitions of functions.  The assembler is parametrized over a "policy" explaining how each jump should be compiled, plus a proof that the policy is sound.  The final theorem establishes correct assembly for any sound policy, given that the input program satisfies a behavioral policy that rules out address arithmetic that would break key invariants.  The set-up also gives guarantees about worst-case execution time of programs.
29I think this is a useful piece of work that is just what we ought to be looking for in CPP.  Though the authors probably wouldn't think of it this way, this work is a good case study demonstrating that the relatively young proof assistant Matita has moved beyond "toy" status, and the paper is interesting in that respect, independently of the details of what has been verified.  Thus, I recommend acceptance.
31The 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.
33One 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.
35It is disappointing that the proofs still depend on some asserted axioms.  From the standpoint of evaluating Matita's maturity, one might wonder whether it will be at all practical to finish the proofs and remove all dependence on axioms.  The best way to address these objections is to finish the proofs and report on the results!  (This point is what holds me back from choosing "strong accept" as my rating.)
37Page 3, "We only remark", perhaps add "that" after?  (and there is a double "of of" shortly after)
39Page 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.
41Page 6, "problems consists", both shouldn't end in "s"
43Page 8, "In plain words, the type of assembly": last word should probably be in code font
45Page 10, "lemmas appears", both shouldn't end in "s"
47Page 12, extraneous comma, "corresponding, source"
49Page 14, "to constraint" should be "to constrain"
50Page 14, "modes than the" should be "modes that the"
53----------------------- REVIEW 2 ---------------------
54PAPER: 16
55TITLE: On the correctness of an optimising assembler for the MCS-51 microcontroller
56AUTHORS: Dominic Mulligan and Claudio Sacerdoti Coen
60Summary of program committee discussion:
62The 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".
65My review:
67This paper describes the formalization and verification of an optimizing assembler for MCS-51 assembly language code.  Such verification is nontrivial because the program and the assembler both want to control memory:  an assembly language program may need to observe and modify memory at a low level, while an optimizing assembler makes decisions that affect memory layout.  Thus, it's important to define semantics for assembly language that are more abstract or more constrained than the semantics for machine language, so that the assembler can influence memory layout while still preserving the assembly language program's semantics during the translation to machine language.
69As an example, suppose the assembly language program executes a call instruction, which pushes a code address on the stack.  The exact code address pushed on the stack depends on how the assembler lays out instructions in memory; this layout may depend on instruction encoding, padding, etc.  One possible approach is to allow assembly language registers and assembly language memory to hold symbolic addresses as well as concrete bytes.  For example, an assembly language call instruction could push a symbolic address onto the stack rather than pushing concrete bytes.  This approach makes it straightforward to define which operations are allowed (comparing two symbols for equality may be ok, but comparing a symbol with a concrete constant is probably illegal).  However, this mixture of symbolic addresses and concrete bytes complicates the assembly language semantics when compared to the machine language semantics.  Therefore, the paper rejects this approach in favor of what appea
70rs to be a variant of this approach.  Rather than putting symbolic addresses directly into registers and memory, the paper's approach defines a map that keeps track of which registers and memory locations hold symbols.  When looking up a value in a register or memory location, the map dictates whether to interpret the register/memory contents as a symbol or a concrete value.
72The 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.)
74The 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
75; 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.
77Other questions:
78- How do you model I/O operations?
79- How do you plan to run the assembler?  Can you extract an executable assembler from the Matita implementation?
80- 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")?
82I'm a little bothered that the proof still has unfinished pieces, although most of the important pieces appear finished.
85Minor comments:
87"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.
89Section 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.)
91Section 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.
93Section 3.4, lemma fetch_assembly_pseudo: the variable "instructions" is not in scope (did you mean "instrs"?).
95Section 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?
98----------------------- REVIEW 3 ---------------------
99PAPER: 16
100TITLE: On the correctness of an optimising assembler for the MCS-51 microcontroller
101AUTHORS: Dominic Mulligan and Claudio Sacerdoti Coen
105This paper certifies an assembler for Intel MCS-51 microprocessor.
106According to the authors, there are two major contributions: first
107the work abstract away details of the branch displacement algorithm
108when proving the correctness; second establish the correctness of
109the assembler only for input assembly programs that use addresses
110in safe ways. Their approach to check safety is more flexible than
111previous approaches that treat addresses as opaque values.
113The project looks interesting, but the presentation is not very
114readable. The major problem is that all the formal details are given
115in the form of Matita code. Comparing to the mathematical notations,
116the code in the boxes looks very verbose and is difficult to read.
117I know the work has been mechanized in Matita, but this doesn't mean
118the presentation has to show the code. The authors should use normal
119mathematical notations instead.
121For the second contribution (for checking safety of address usage),
122what is the problem here? Why addresses have to be treated as
123opaque values before? Here by addresses do you mean code labels
124only or both code labels and memory pointers for data? The new
125approach is said to be more flexible to support "benign" manipulations
126of addresses. Do you have examples to demonstrate this flexibility
127and show why it is a big deal?
129The title is about correctness of an optimizing assembler. However,
130the verification process shown in this paper abstracts away the branch
131displacement algorithm, the only optimization in the assembler. So it
132seems the optimization part is irrelevant.
134In the Intro the authors seem to also claim that the assembler is
135cost-preserving. Where is this issue discussed in the paper?
137page 2, line 4: giveth --> given, taketh --> taken ?
138page 9, Huth et al [15] --> Tuch et al [15] ?
140The term "total correctness" used in Sec. 3.4 and 3.5 is confusing,
141since it has already been used in Hoare logic with standard meaning.
144----------------------- REVIEW 4 ---------------------
145PAPER: 16
146TITLE: On the correctness of an optimising assembler for the MCS-51 microcontroller
147AUTHORS: Dominic Mulligan and Claudio Sacerdoti Coen
151This paper describes the modelling and verification of an assembler, a
152program for turning sequences of mnemonic assembly instructions into
153sequences of bytes, i.e., machine code. The program is modelled in the
154mechanical proof assistant Matita, and addresses MCS51 microcontrollers.
156The two main problems seem to be:
157 (i)  translating address labels into jump offets, and,
158 (ii) ensuring that programs manipulate addresses `correctly'.
160The approach is serious and treats an established and industrially
161significant hardware platform. But the paper suffers from three main
164  (i)   The presentation is needlessly complicated and difficult to
165        understand; while individual sentences are well-written, they
166        sometimes lack precision,
168  (ii)  The most delicate and interesting part of the problem seems to be
169        the translation of jump offsets, but the algorithm for this has been
170        submitted as a companion paper; it may have been better to submit a
171        single, self-contained paper with a higher concentration of
172        interesting results.
174  (iii) The notion of `well behaved' assembly programs is either not
175        described clearly enough, or not adequately developed. It seems to
176        relie on `run-time' checks for correct address manipulation. In
177        fact, these checks seem to be made at `emulation-time' (since the
178        generated code is not changed to implement the checks), and it is
179        not clear whether (or how) this covers all possible program
180        behaviours.
182The authors not that their proof is not yet finished, but it does seem that
183they have resolved all of the technical obstacles.
185The work is quite interesting and practically-oriented, and I would
186encourage the authors to revise their draft to make it more precise,
187self-contained, and all encompassing (perhaps as per my detailed comments
190* Detailed comments
1921. The title talks about an _optimising_ assembler, but the only
193   optimisation seems to be in calculating branch displacements and this
194   question is only partially resolved in the paper. Can assemblers be
195   expected to perform any other optimisations?
1972. The abstract talks about "the efficient expansion of
198   psuedoinstructions---particularly jumps---is complex", but given that
199   this is the sole optimisation, it would seem more accurate to say
200   "...---namely jumps". Furthermore, the word "complex" is perhaps
201   overreaching.
2033. Some parts of the text lack precision. Namely:
205   a. p.2: "what one hand giveth, the other taketh away"---it seems rather
206      to be a question of a straight-out engineering tradeoff in processor
207      choice. Furthermore, the MCS51 is memory constrained by the fact that
208      it is an 8-bit microcontroller; but there would seem to be sufficient
209      memory for the tasks it is expected to perform. This does not mean
210      that the calculation of jumping instructions is not a worthy problem,
211      but I question whether it is as critical as stated.
213   b. p.2: The last paragraph states that the proof is effected in "a
214      rather profound way", and that the proof of correctness may descend
215      into a "diabolical quagmire". In my opinion, these literary
216      flourishes waste space that could instead be used for more accurate
217      descriptions.
219   c. p.3: "heavily exploit", why not just "exploit"?
221   d. p.4: suggest replacing "and so on" with a more accurate description.
223   e. p.6: "The function assembly_1_psuedo_instruction ... is essentially
224      the composition of the two passes": is it or isn't it?
226   f. p.6: "... markedly different ways": well, all of the instructions jump
227      to one place or another, so they're not that different!
229   g. p.6: "MCS-51's limited code memory"; why not state the limits?
231   h. p.14: "this policy is the only possible policy _in theory_ that can
232      preseve the semantics..."; what does this mean exactly? It would seem
233      that the approach being presented is a counterexample to this
234      statement.
2364. The question of the MCS51's precise and predictable timing model is quite
237   interesting, but not discussed thoroughly in the paper. The second page
238   talks about "timing characteristics" and I/O but it is not completely
239   clear what is meant. Choosing one branching strategy over another will
240   obviously change the cycle-level timing of a program. The paper does not
241   discuss this in detail, nor whether it is important or not. Apart from
242   that, how else could the timing be changed by choices in the assembler?
244   The paper talks about "costing" in the encompassing CerCo project, but
245   few precise details are given. In particular, whenever "cost" is used in
246   the paper, does it just refer to the number of cycles required to execute
247   a sequence of instructions? If so, why use the more abstract term?
2495. The paper does not mention the issue of placing assembler subroutines in
250   memory? Is this not an issue? Could placement choices affect code size
251   (from jump instructions) significantly?
2536. p.4: It seems to me that the paper would have been much easier to
254   understand had it included more "sign posting". For instance, the start of
255   section 3 might state that there will be two models: one where jump
256   destinations are specified using relative offsets, and another where they
257   are given as labels. And, in fact, that the whole point is to translate
258   accurately from one to the other. The paper might then summarise
259   reference [4], which is very nicely written, to motivate the issue of
260   calculating branch displacements.
262   It might also state the two other issues are the correctness of assembly
263   encoding/fetching, and a notion of "well behaved" programs that modify
264   addresses in "reasonable" ways.
2667. p.5: It would be nice to see the type of the "preamble"; is it just a
267   DATA section?
2698. The paper does not discuss the complete tool chain. Does the verified
270   development parse MCS51 assembler and spit out a binary image?
2729. p.5: Why is "Word" and not "Identifier" or "nat" used to index psuedo
273   instructions? Or maybe even a type synonym so there is no risk of
274   confusion with the type used to index instructions.
276   For instance, it would be nice if the statement "The function sigma maps
277   pseudo program counters to program counters" were better reflected in the
278   type of sigma.
28010. p.6: I did not really understand what the paragraph "In contrast to other
281    approaches, we do not perform any kind of symbolic execution..." was
282    trying to say.
28411. pp.7--9: this text talks about "program counters", when I think it
285    means "addresses" (i.e., values that the program counter may take).
28712. It is confusing that the variable called "policy" is only one part of
288    the concept "policy".
29013. p.8: I didn't understand why it is sometimes necessary to force the
291    expansion of jumps to the largest size possible.
29314. p.11: states that "we must detect (at run time) programs that manipulate
294    addresses in well behaved ways". But what does this mean exactly? Given
295    that the output program is not augmented with checks, it seems that the
296    authors mean "at emulation time". But how can this be exhaustive (for
297    all input values and for non-terminating executions)? Are there some
298    kind of necessary conditions for having a well-behaved program? Must
299    users provide a proof of well-behavedness for each program before they
300    can be sure that its assembly is correct? Isn't this rather a typing
301    issue? Is there any relation with the work of Greg Morriset et al on
302    Typed Assembly Language?
30415. The paper states that the work may be usable in the context of verified
305    operating systems kernels. This is a point worth discussing, but the
306    text could be more precise. The seL4 kernel requires memory protection
307    but the MCS51 has no MMU. Furthermore, the verification was specific to
308    the arm assembly language, where it would seem that the issue of branch
309    displacement is less significant.
311    Similarly, the paper discusses compilers like CompCert and the issue of
312    well-formedness. Again, this is a worthy point, but the discussion seems
313    to neglect the possibility that well formedness may be guaranteed by the
314    conversion from the high-level language, i.e. that all C programs may
315    compile into "well behaved" assembly programs. Is this true?
31716. The related work section touches on "timing properties of an assembly
318    program", but this issue is not treated in depth by the paper, and, in
319    fact, these sentences seem out of place.
32117. It is not clear why both references [5] and [6] are needed. Nor why both
322    references [7] and [8] are needed.
32418. Research Questions
326   a. Did you consider "running" your model in parallel with a real or
327      emulated MCS-51 to validate its correctness?
328      (as in the work of Peter Sewell et al's work on TCP/IP and memory
329       weak models; where they compare their models against real
330       implementations.)
332   b. Rather than verifying a branch displacement algorithm, did you
333      consider showing refinement between the input (assembler with labels) and
334      the output (modified assembler with offsets)? That way, the algorithm
335      could use whatever strategy it liked and the results would still be
336      verified. From my understanding, this is one of the approaches taken
337      in Xavier Leroy et al's CompCert project.
339x. Minor typos / issues
341   a. p.3: "we proved the implementation of the assembler": inconsistency of
342      verb tense.
344   b. p.3: The subsection heading "Overview of the paper." is unnecessary.
346   c. p.4: It would be helpful if the abbreviated definitions of
347       preinstruction, instruction, and pseudoinstruction included more
348       elements in common with themselves and with the other examples
349       (notably DEC).
351   d. p.10: "eject out" -> "project"
353   e. p.10: "lemmas appears" -> "lemmas appear"
355   f. p.11: "Huch" -> "Tuch"
357   g. p.14: "constraint" -> "constrain"
Note: See TracBrowser for help on using the repository browser.