Sep 28, 2012, 6:24:44 PM (8 years ago)


1 edited


  • Papers/cpp-asm-2012/reviews.txt

    r2377 r2378  
    336) 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 10) Section 3.4, lemma fetch_assembly_pseudo: the variable "instructions" is not in scope (did you mean "instrs"?).
    7 11) 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?
    9 ----------------------- REVIEW 3 ---------------------
    11 The term "total correctness" used in Sec. 3.4 and 3.5 is confusing,
    12 since it has already been used in Hoare logic with standard meaning.
    155----------------------- REVIEW 4 ---------------------
    16   (i)   The presentation is needlessly complicated and difficult to
    17         understand; while individual sentences are well-written, they
    18         sometimes lack precision,
    20   (ii)  The most delicate and interesting part of the problem seems to be
    21         the translation of jump offsets, but the algorithm for this has been
    22         submitted as a companion paper; it may have been better to submit a
    23         single, self-contained paper with a higher concentration of
    24         interesting results.
    26   (iii) The notion of `well behaved' assembly programs is either not
    27         described clearly enough, or not adequately developed. It seems to
    28         relie on `run-time' checks for correct address manipulation. In
    29         fact, these checks seem to be made at `emulation-time' (since the
    30         generated code is not changed to implement the checks), and it is
    31         not clear whether (or how) this covers all possible program
    32         behaviours.
    3461. The title talks about an _optimising_ assembler, but the only
    357   optimisation seems to be in calculating branch displacements and this
    45173. Some parts of the text lack precision. Namely:
    47    a. p.2: "what one hand giveth, the other taketh away"---it seems rather
    48       to be a question of a straight-out engineering tradeoff in processor
    49       choice. Furthermore, the MCS51 is memory constrained by the fact that
     19   a. p.2: The MCS51 is memory constrained by the fact that
    5020      it is an 8-bit microcontroller; but there would seem to be sufficient
    5121      memory for the tasks it is expected to perform. This does not mean
    5323      but I question whether it is as critical as stated.
    55    b. p.2: The last paragraph states that the proof is effected in "a
    56       rather profound way", and that the proof of correctness may descend
    57       into a "diabolical quagmire". In my opinion, these literary
    58       flourishes waste space that could instead be used for more accurate
    59       descriptions.
    61    e. p.6: "The function assembly_1_psuedo_instruction ... is essentially
    62       the composition of the two passes": is it or isn't it?
    6425   f. p.6: "... markedly different ways": well, all of the instructions jump
    6526      to one place or another, so they're not that different!
    67    h. p.14: "this policy is the only possible policy _in theory_ that can
    68       preseve the semantics..."; what does this mean exactly? It would seem
    69       that the approach being presented is a counterexample to this
    70       statement.
    72 4. The question of the MCS51's precise and predictable timing model is quite
    73    interesting, but not discussed thoroughly in the paper. The second page
    74    talks about "timing characteristics" and I/O but it is not completely
    75    clear what is meant. Choosing one branching strategy over another will
    76    obviously change the cycle-level timing of a program. The paper does not
    77    discuss this in detail, nor whether it is important or not. Apart from
    78    that, how else could the timing be changed by choices in the assembler?
    80    The paper talks about "costing" in the encompassing CerCo project, but
     284. The paper talks about "costing" in the encompassing CerCo project, but
    8129   few precise details are given. In particular, whenever "cost" is used in
    8230   the paper, does it just refer to the number of cycles required to execute
    8634   memory? Is this not an issue? Could placement choices affect code size
    8735   (from jump instructions) significantly?
    89 6. p.4: It seems to me that the paper would have been much easier to
    90    understand had it included more "sign posting". For instance, the start of
    91    section 3 might state that there will be two models: one where jump
    92    destinations are specified using relative offsets, and another where they
    93    are given as labels. And, in fact, that the whole point is to translate
    94    accurately from one to the other. The paper might then summarise
    95    reference [4], which is very nicely written, to motivate the issue of
    96    calculating branch displacements.
    98    It might also state the two other issues are the correctness of assembly
    99    encoding/fetching, and a notion of "well behaved" programs that modify
    100    addresses in "reasonable" ways.
    102377. p.5: It would be nice to see the type of the "preamble"; is it just a
    11449   type of sigma.
    116 10. p.6: I did not really understand what the paragraph "In contrast to other
    117     approaches, we do not perform any kind of symbolic execution..." was
    118     trying to say.
     51   CSC: because the semantics is shared!
    1205311. pp.7--9: this text talks about "program counters", when I think it
    12154    means "addresses" (i.e., values that the program counter may take).
    123 12. It is confusing that the variable called "policy" is only one part of
    124     the concept "policy".
    1265613. p.8: I didn't understand why it is sometimes necessary to force the
    12757    expansion of jumps to the largest size possible.
    129 14. p.11: states that "we must detect (at run time) programs that manipulate
    130     addresses in well behaved ways". But what does this mean exactly? Given
    131     that the output program is not augmented with checks, it seems that the
    132     authors mean "at emulation time". But how can this be exhaustive (for
    133     all input values and for non-terminating executions)? Are there some
    134     kind of necessary conditions for having a well-behaved program? Must
    135     users provide a proof of well-behavedness for each program before they
    136     can be sure that its assembly is correct? Isn't this rather a typing
    137     issue? Is there any relation with the work of Greg Morriset et al on
    138     Typed Assembly Language?
    1405915. The paper states that the work may be usable in the context of verified
    15069    conversion from the high-level language, i.e. that all C programs may
    15170    compile into "well behaved" assembly programs. Is this true?
    153 16. The related work section touches on "timing properties of an assembly
    154     program", but this issue is not treated in depth by the paper, and, in
    155     fact, these sentences seem out of place.
    1577218. Research Questions
    17691       elements in common with themselves and with the other examples
    17792       (notably DEC).
     94      CSC: there is nothing in common; we could put MUL/DEC
Note: See TracChangeset for help on using the changeset viewer.