Changeset 2343


Ignore:
Timestamp:
Sep 26, 2012, 2:46:57 PM (7 years ago)
Author:
mulligan
Message:

Fixed Claudio's horrifying use of American spellings (optimizing, etc.)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/cpp-asm-2012/cpp-2012-asm.tex

    r2342 r2343  
    8787too far away, larger and slower long jumps must be used. The use of a long jump may
    8888augment the distance between another pseudojump and its target, forcing
    89 another long jump use, in a cascading effect. The job of the optimizing
     89another long jump use, in a cascading effect. The job of the optimising
    9090compiler (assembler) is to individually expand every pseudo-instruction in such a way
    9191that all global constraints are satisfied and that the compiled program size
     
    104104model on the assembly code as a function of the assembly program and the
    105105strategy used to solve the branch displacement problem. In particular, the
    106 optimizing compiler should also return a map that assigns a cost (in clock
     106optimising compiler should also return a map that assigns a cost (in clock
    107107cycles) to every instruction in the source program. We expect the induced cost
    108108to be preserved by the compiler: we will prove that the compiled code
     
    129129The assembler fails to assemble an assembly program if and only if a correct policy does not exist. This is stated in an elegant way in the dependent type of the assembler: the assembly function is total over a program, a policy and the proof that the policy is correct for that program.
    130130
    131 The final complication in the proof of correctness of our optimizing assembler
     131The final complication in the proof of correctness of our optimising assembler
    132132is due to the kind of semantics associated to pseudo assembly programs.
    133133Should assembly programs be allowed to freely manipulate addresses? The
Note: See TracChangeset for help on using the changeset viewer.