Changeset 3138


Ignore:
Timestamp:
Apr 12, 2013, 7:03:35 PM (4 years ago)
Author:
campbell
Message:

Sketch up-to-labelling bit.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.4/Report/report.tex

    r3131 r3138  
    417417\section{Input code to cost labelled program}
    418418
     419The simple form of labelling used in the formalised compiler is not
     420quite capable of capturing costs arising from complex C
     421\lstinline[language=C]'switch' statements, largely due to the
     422fall-through behaviour.  Our first pass replaces these statements with
     423simpler C code, allowing our second pass to perform the cost
     424labelling.  We show that the behaviour of programs is unchanged by
     425these passes.
     426
     427TODO: both give one-step-sim-by-many forward sim results; switch
     428removal tricky, uses aux var to keep result of expr, not central to
     429intensional correctness so curtailed proof effort once reasonable
     430level of confidence in code gained; labelling much simpler; don't care
     431what the labels are at this stage, just need to know when to go
     432through extra steps.  Rolled up into a single result with a cofixpoint
     433to obtain coinductive statement of equivalence (show).
     434
    419435\section{Finding corresponding measurable subtraces}
    420436
Note: See TracChangeset for help on using the changeset viewer.