Ignore:
Timestamp:
Sep 26, 2012, 2:08:42 PM (7 years ago)
Author:
sacerdot
Message:

More introduction.

File:
1 edited

Legend:

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

    r2340 r2341  
    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 rest of this paper is a detailed description of our proof that is, in part, still a work in progress.
     131The final complication in the proof of correctness of our optimizing assembler
     132is due to the kind of semantics associated to pseudo assembly programs.
     133Should assembly programs be allowed to freely manipulate addresses? The
     134answer to the question deeply affects the proof of correctness.
     135The traditional answer is no: values stored in memory or registers are either
     136concrete data or symbolic addresses. The latters can be manipulated only
     137in very restrictive ways and many programs that do not do so, for malign or
     138benign reasons, are not assigned a semantics and cannot be reasoned about.
     139All programs that have a semantics have it preserved by the compiler.
     140Instead we took a different, novel approach: we allow programs to freely
     141manipulate
     142addresses non symbolically, but we only grant preservation of the semantics
     143for those programs that do behave in a correct, anticipated way. At least
     144in principle, this should allow some reasoning on the actual semantics of
     145malign programs. In practice, we note how the alternative approach allows
     146more code reusal between the semantics of assembly code and object code,
     147with benefits on the size of the formalization.
     148
     149The rest of this paper is a detailed description of our proof that is, in
     150minimal part, still a work in progress.
    132151
    133152We provide the reader with a brief `roadmap' for the rest of the paper.
Note: See TracChangeset for help on using the changeset viewer.