Changeset 2377 for Papers

Sep 28, 2012, 6:18:25 PM (9 years ago)

typo fixed

2 edited


  • Papers/cpp-asm-2012/cpp-2012-asm.tex

    r2376 r2377  
    480480 let pi := $\pi_1$ (fetch_pseudo_instruction instr_list ppc) in
    481481 let pc := policy ppc in
    482  let instrs := expand_pseudo_instruction policy ppc pi in
     482 let instructions := expand_pseudo_instruction policy ppc pi in
    483483 let $\langle$l, a$\rangle$ := assembly_1_pseudoinstruction policy ppc pi in
    484484 let pc_plus_len := pc + l in
  • Papers/cpp-asm-2012/reviews.txt

    r2337 r2377  
    1 ----------------------- REVIEW 1 ---------------------
    2 1) The main weakness of the paper is the detailed presentation of lemma statements.
    3 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.
    4 It would be nice to have a single conference-length paper that explains all the key insights.
    6 2) One contribution of this paper is the novel way of reasoning about assembly programs that may do address arithmetic.
    7 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.
    8 I think this is a reasonable position, but the speculative nature of the motivation ought to be made clearer earlier.
    10 Page 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.
    12 ----------------------- REVIEW 2 ---------------------
    13 1) 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".
    15 2) 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.)
    17 3) 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
    18 ; 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.
    2014) How do you model I/O operations?
    2125) How do you plan to run the assembler?  Can you extract an executable assembler from the Matita implementation?
    2236) 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")?
    24 7) "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.
    26 8) 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.)
    28 9) 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.
    30510) Section 3.4, lemma fetch_assembly_pseudo: the variable "instructions" is not in scope (did you mean "instrs"?).
Note: See TracChangeset for help on using the changeset viewer.