Changeset 3653 for Papers

Timestamp:

Mar 14, 2017, 5:42:26 PM (2 years ago)

Author:

mulligan

Message:

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

Location:

Papers/jar-cerco-2017

Files:

• cerco.bib (modified) (2 diffs)
• conclusions.tex (modified) (1 diff)

Papers/jar-cerco-2017/cerco.bib

@@ -463 +463 @@
 }
 
+@misc { dwarf,
+  title = {The {DWARF} debugging format standard},
+  url = {http://www.dwarfstd.org/},
+  note = {Accessed March 2017},
+  year = {2017},
+  key = {dwarf}
+}
+
 @inproceedings{DBLP:conf/sefm/BarthePS05,
   author    = {Gilles Barthe and
@@ -472 +480 @@
   pages     = {86--95},
   year      = {2005},
-  crossref  = {DBLP:conf/sefm/2005},
   url       = {http://dx.doi.org/10.1109/SEFM.2005.34},
   doi       = {10.1109/SEFM.2005.34},

Papers/jar-cerco-2017/conclusions.tex

@@ -159 +159 @@
 \label{subsect.further.work}
 
-To prove that compilers can keep track of optimisations
-and induce a precise cost model on the source code, we targeted a simple
-architecture that admits a cost model that is execution history independent.
-The most important future work is dealing with hardware architectures
-characterised by history-dependent stateful components, like caches and
-pipelines. The main issue is to assign a parametric, dependent cost
-to basic blocks that can be later transferred by the labelling approach to
-the source code and represented in a meaningful way to the user. The dependent
-labelling approach that we have studied seems a promising tool to achieve
-this goal, but more work is required to provide good source level
-approximations of the relevant processor state.
+Important future work is retargetting the CerCo verified C compiler to target hardware architectures characterised by history-dependent stateful components, like caches and pipelines.
+Most moden microprocessors, including all commodity microprocessors that ship with desktop computers and servers, fall into this class.
+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.
+Further, once this cost model is lifted, it must be represented in a meaningful and easy-to-understand way to the user.
+The dependent labelling approach that we have studied seems a promising tool to achieve this goal.
+However, more work is required to provide good source level approximations of the relevant processor state.
 
-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. Larger case studies are also necessary
-to evaluate the CerCo's prototype on realistic, industrial-scale programs.
+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.
+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}.
+In particular, DWARF contains various tables, and other debugging data, on how a compiler translated code.
+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.}
+
+Whether this debugging information can be harnessed to lift cost models back through the compilation chain is an open question.
+Several problems immediately stand out.
+First, advanced compilers often produce buggy DWARF, due to the challenge of precisely tracking how expressions are translated through aggressive control flow-altering optimisations.
+Indeed, the difficulty of enacting this tracking reliably is a major reason why we verified the approach presented in this work.
+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.
+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.
+
+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.