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

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


File size: 4.6 KB
14) How do you model I/O operations?
25) How do you plan to run the assembler?  Can you extract an executable assembler from the Matita implementation?
36) 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")?
5----------------------- REVIEW 4 ---------------------
61. The title talks about an _optimising_ assembler, but the only
7   optimisation seems to be in calculating branch displacements and this
8   question is only partially resolved in the paper. Can assemblers be
9   expected to perform any other optimisations?
112. The abstract talks about "the efficient expansion of
12   psuedoinstructions---particularly jumps---is complex", but given that
13   this is the sole optimisation, it would seem more accurate to say
14   "...---namely jumps". Furthermore, the word "complex" is perhaps
15   overreaching.
173. Some parts of the text lack precision. Namely:
19   a. p.2: The MCS51 is memory constrained by the fact that
20      it is an 8-bit microcontroller; but there would seem to be sufficient
21      memory for the tasks it is expected to perform. This does not mean
22      that the calculation of jumping instructions is not a worthy problem,
23      but I question whether it is as critical as stated.
25   f. p.6: "... markedly different ways": well, all of the instructions jump
26      to one place or another, so they're not that different!
284. The paper talks about "costing" in the encompassing CerCo project, but
29   few precise details are given. In particular, whenever "cost" is used in
30   the paper, does it just refer to the number of cycles required to execute
31   a sequence of instructions? If so, why use the more abstract term?
335. The paper does not mention the issue of placing assembler subroutines in
34   memory? Is this not an issue? Could placement choices affect code size
35   (from jump instructions) significantly?
377. p.5: It would be nice to see the type of the "preamble"; is it just a
38   DATA section?
408. The paper does not discuss the complete tool chain. Does the verified
41   development parse MCS51 assembler and spit out a binary image?
439. p.5: Why is "Word" and not "Identifier" or "nat" used to index psuedo
44   instructions? Or maybe even a type synonym so there is no risk of
45   confusion with the type used to index instructions.
47   For instance, it would be nice if the statement "The function sigma maps
48   pseudo program counters to program counters" were better reflected in the
49   type of sigma.
51   CSC: because the semantics is shared!
5311. pp.7--9: this text talks about "program counters", when I think it
54    means "addresses" (i.e., values that the program counter may take).
5613. p.8: I didn't understand why it is sometimes necessary to force the
57    expansion of jumps to the largest size possible.
5915. The paper states that the work may be usable in the context of verified
60    operating systems kernels. This is a point worth discussing, but the
61    text could be more precise. The seL4 kernel requires memory protection
62    but the MCS51 has no MMU. Furthermore, the verification was specific to
63    the arm assembly language, where it would seem that the issue of branch
64    displacement is less significant.
66    Similarly, the paper discusses compilers like CompCert and the issue of
67    well-formedness. Again, this is a worthy point, but the discussion seems
68    to neglect the possibility that well formedness may be guaranteed by the
69    conversion from the high-level language, i.e. that all C programs may
70    compile into "well behaved" assembly programs. Is this true?
7218. Research Questions
74   a. Did you consider "running" your model in parallel with a real or
75      emulated MCS-51 to validate its correctness?
76      (as in the work of Peter Sewell et al's work on TCP/IP and memory
77       weak models; where they compare their models against real
78       implementations.)
80   b. Rather than verifying a branch displacement algorithm, did you
81      consider showing refinement between the input (assembler with labels) and
82      the output (modified assembler with offsets)? That way, the algorithm
83      could use whatever strategy it liked and the results would still be
84      verified. From my understanding, this is one of the approaches taken
85      in Xavier Leroy et al's CompCert project.
87x. Minor typos / issues
89   c. p.4: It would be helpful if the abbreviated definitions of
90       preinstruction, instruction, and pseudoinstruction included more
91       elements in common with themselves and with the other examples
92       (notably DEC).
94      CSC: there is nothing in common; we could put MUL/DEC
Note: See TracBrowser for help on using the repository browser.