- Timestamp:
- Mar 14, 2017, 5:42:26 PM (2 years ago)
- Location:
- Papers/jar-cerco-2017
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/jar-cerco-2017/cerco.bib
r3652 r3653 463 463 } 464 464 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 465 473 @inproceedings{DBLP:conf/sefm/BarthePS05, 466 474 author = {Gilles Barthe and … … 472 480 pages = {86--95}, 473 481 year = {2005}, 474 crossref = {DBLP:conf/sefm/2005},475 482 url = {http://dx.doi.org/10.1109/SEFM.2005.34}, 476 483 doi = {10.1109/SEFM.2005.34}, -
Papers/jar-cerco-2017/conclusions.tex
r3652 r3653 159 159 \label{subsect.further.work} 160 160 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. 161 Important future work is retargetting the CerCo verified C compiler to target hardware architectures characterised by history-dependent stateful components, like caches and pipelines. 162 Most moden microprocessors, including all commodity microprocessors that ship with desktop computers and servers, fall into this class. 163 A 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. 164 Further, once this cost model is lifted, it must be represented in a meaningful and easy-to-understand way to the user. 165 The dependent labelling approach that we have studied seems a promising tool to achieve this goal. 166 However, more work is required to provide good source level approximations of the relevant processor state. 172 167 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. 168 Another 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. 169 Whilst 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}. 170 In particular, DWARF contains various tables, and other debugging data, on how a compiler translated code. 171 This 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 173 Whether this debugging information can be harnessed to lift cost models back through the compilation chain is an open question. 174 Several problems immediately stand out. 175 First, advanced compilers often produce buggy DWARF, due to the challenge of precisely tracking how expressions are translated through aggressive control flow-altering optimisations. 176 Indeed, the difficulty of enacting this tracking reliably is a major reason why we verified the approach presented in this work. 177 Second, 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. 178 In 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 180 Other 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.