Changeset 3653


Ignore:
Timestamp:
Mar 14, 2017, 5:42:26 PM (7 months ago)
Author:
mulligan
Message:

Added more ideas to future work, including use of DWARF for lifting cost models...

Location:
Papers/jar-cerco-2017
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Papers/jar-cerco-2017/cerco.bib

    r3652 r3653  
    463463}
    464464
     465@misc { dwarf,
     466  title = {The {DWARF} debugging format standard},
     467  url = {http://www.dwarfstd.org/},
     468  note = {Accessed March 2017},
     469  year = {2017},
     470  key = {dwarf}
     471}
     472
    465473@inproceedings{DBLP:conf/sefm/BarthePS05,
    466474  author    = {Gilles Barthe and
     
    472480  pages     = {86--95},
    473481  year      = {2005},
    474   crossref  = {DBLP:conf/sefm/2005},
    475482  url       = {http://dx.doi.org/10.1109/SEFM.2005.34},
    476483  doi       = {10.1109/SEFM.2005.34},
  • Papers/jar-cerco-2017/conclusions.tex

    r3652 r3653  
    159159\label{subsect.further.work}
    160160
    161 To prove that compilers can keep track of optimisations
    162 and induce a precise cost model on the source code, we targeted a simple
    163 architecture that admits a cost model that is execution history independent.
    164 The most important future work is dealing with hardware architectures
    165 characterised by history-dependent stateful components, like caches and
    166 pipelines. The main issue is to assign a parametric, dependent cost
    167 to basic blocks that can be later transferred by the labelling approach to
    168 the source code and represented in a meaningful way to the user. The dependent
    169 labelling approach that we have studied seems a promising tool to achieve
    170 this goal, but more work is required to provide good source level
    171 approximations of the relevant processor state.
     161Important future work is retargetting the CerCo verified C compiler to target hardware architectures characterised by history-dependent stateful components, like caches and pipelines.
     162Most moden microprocessors, including all commodity microprocessors that ship with desktop computers and servers, fall into this class.
     163A key issue here is the assignment of a parametric, dependent cost to basic blocks that can be later lifted to the source-code level by our labelling approach.
     164Further, once this cost model is lifted, it must be represented in a meaningful and easy-to-understand way to the user.
     165The dependent labelling approach that we have studied seems a promising tool to achieve this goal.
     166However, more work is required to provide good source level approximations of the relevant processor state.
    172167
    173 Other examples of future work are to improve the cost invariant
    174 generator algorithms and the coverage of compiler optimisations, to combining
    175 the labelling approach with the type and effect discipline of~\cite{typeffects}
    176 to handle languages with implicit memory management, and to experiment with
    177 our tools in the early phases of development. Larger case studies are also necessary
    178 to evaluate the CerCo's prototype on realistic, industrial-scale programs.
     168Another key question that we wish to address is how one could retrofit an existing compiler with facilities for lifting cost models, as presented in this paper.
     169Whilst we engineered the CerCo verified C compiler to track how each expression and statement of source-level code is translated, to a certain extent a more general tracking mechanism is already present in many commercial compilers which produce DWARF debug information~\cite{dwarf}.
     170In particular, DWARF contains various tables, and other debugging data, on how a compiler translated code.
     171This data includes a line number table, stored in the \texttt{.debug\_line} section, that contains the instructions of a simple state machine that may be executed to map code memory addresses back to file names and line numbers (and column numbers, for compilers that generate this data) at the source level.\footnote{Indeed, running \texttt{objdump -S} on an executable binary containing embedded DWARF debug information will display an interleaving of high-level source code and machine code, using this information.}
     172
     173Whether this debugging information can be harnessed to lift cost models back through the compilation chain is an open question.
     174Several problems immediately stand out.
     175First, advanced compilers often produce buggy DWARF, due to the challenge of precisely tracking how expressions are translated through aggressive control flow-altering optimisations.
     176Indeed, the difficulty of enacting this tracking reliably is a major reason why we verified the approach presented in this work.
     177Second, some of the information needed to effect the lifting of the cost model is not generated as a matter-of-course by mainstream compilers, despite being supported by the DWARF standard.
     178In particular, many compilers do not produce column information, needed to uniquely identify the subexpression or statement from which machine code originated, preferring only to generate line numbers.
     179
     180Other examples of future work are to improve the cost invariant generator algorithms and the coverage of compiler optimisations, to combining the labelling approach with the type and effect discipline of~\cite{typeffects} to handle languages with implicit memory management, and to experiment with our tools in the early phases of development.
Note: See TracChangeset for help on using the changeset viewer.