[gforth] / res / PP-compiler.tex  

gforth: res/PP-compiler.tex

Diff for /res/PP-compiler.tex between version 1.2 and 1.16

version 1.2, Mon Jun 22 14:23:22 2009 UTC version 1.16, Mon Jun 29 18:13:13 2009 UTC
Line 3 
Line 3 
 \usepackage{url}  \usepackage{url}
 %\usepackage{times}  %\usepackage{times}
 \usepackage{comment}  \usepackage{comment}
   
 \pagestyle{plain}  \pagestyle{plain}
 \setlength{\textwidth}{16truecm}  \setlength{\textwidth}{16truecm}
 \setlength{\textheight}{24truecm}  \setlength{\textheight}{24truecm}
Line 19 
Line 18 
   
 \title{\bf PP \emph{Compilation Techniques for Robust Embedded Systems}}  \title{\bf PP \emph{Compilation Techniques for Robust Embedded Systems}}
   
 \author{{\sc Ulrich Schmid}\\  \author{{\sc Jens Knoop and Andreas Krall}\\
 s@ecs.tuwien.ac.at  \{knoop,andi\}@complang.tuwien.ac.at
 }  }
   
 \bibliographystyle{unsrt}  \bibliographystyle{unsrt}
Line 28 
Line 27 
 \begin{document}  \begin{document}
 \maketitle  \maketitle
   
 PP leader: \emph{Jens Knoop and Andreas Krall}  PP leader: \emph{Jens Knoop and Andreas Krall (beide E185.1)}
   
 Associated researchers: \emph{}  
   
   
   Associated researchers: \emph{Anton Ertl (E185.1), Bernhard Gramlich (E185.2),}\\
   \phantom{Associated researchers: } \ \ \ \ \emph{Franz Puntigam (E185.1)}
   
 \subsubsection*{Motivation:}  \subsubsection*{Motivation:}
 %\emph{Informal description of the purpose of the PP (3-5 lines)}  %\emph{Informal description of the purpose of the PP (3-5 lines)}
 Every embedded system consists of software which is written in a high  Every embedded system consists of software which is written in a high
 level language, compiled to machine language and executed on a  level language, compiled to machine language and executed on a
 processor. For robust embedded systems new verified compilation  processor. For robust embedded systems new verified analysis and
 techniques are necessary to optimize for performance, power, space,  compilation, simulation, and specification methods are necessary to
 concurrency and reliability.  support the programmer during application development and maintenance
   and to optimize for performance, power, space, concurrency and
   reliability during compilation.
   %for short, new programming and
   %compilation techniques for robust embedded systems development and
   %deployment.
   
 \subsubsection*{State of the art and related work:}  \subsubsection*{State of the art and related work:}
 %\emph{Briefly describe the scientific state of the art (20-30 lines)}  %\emph{Briefly describe the scientific state of the art (20-30 lines)}
   
 %Compilation Techniques for Reliability  %Compilation Techniques for Reliability
   
 Because of the exponential increase of the number of transistors and  Because of the exponential increase of the number of transistors and
 the continuing decrease of the feature sizes of current processors  the continuing decrease of the feature sizes of current processors
 soft errors mainly caused by energetic particles are becoming an  \emph{soft errors} mainly caused by energetic particles are becoming an
 important design issue for robust embedded systems. Blome et  important design issue for robust embedded systems. Blome et
 al.~\cite{Blome+06} observed that a majority of faults that affect the  al.~\cite{Blome+06} observed that a majority of faults that affect the
 architectural state of a processor come from the register file. Lee  architectural state of a processor come from the register file. Lee
 and Shrivastava and proposed different solutions to cope with this  and Shrivastava \cite{LeeShrivastava09a,LeeShrivastava09c} proposed
 problem. The first assigns variables depending on their lifetime to  different solutions to cope with this problem. The first assigns
 either the ECC protected or the unprotected part of a register file to  variables depending on their lifetime to either the ECC protected or
 balance energy consumption and reliability \cite{LeeShrivastava09a}.  the unprotected part of a register file to balance energy consumption
 The second spills registers to ECC protected memory if the register  and reliability \cite{LeeShrivastava09a}.  The second spills registers
 contents are not used for a long period \cite{LeeShrivastava09c}.  to ECC protected memory if the register contents are not used for a
   long period \cite{LeeShrivastava09c}.  There exist complete software
   solutions which use different forms of code duplications
   \cite{Oh+02a,Reis+05}, which do failure virtualization
   \cite{WapplerMueller08} or which use techniques like control flow
   checking \cite{Oh+02b}. A complete overview of processor description
   languages and generation of compilers and simulators from processor
   specifications gives the book of Mishra and Dutt \cite{MishraDutt08}.
   A good survey of current instruction set simulators gives our chapter
   in the \emph{Handbook of Signal Processing systems} \cite{BrHoKr09}. A
   famous instruction set simulator with modelling of energy consumption
   is \emph{Wattch} \cite{BrooksTiwariMartonosi00}.
   
   Methods for \emph{compiler verification} do exist
   \cite{Langmaack97a,Po-lncs124,MMO-lncs1283,Goos:99:verifix,Goos:00:ASM,1328444}.
   Most notably are the pioneering approaches of the
   \emph{ProCoS} \cite{Langmaack96a} and the \emph{Verifix}
   \cite{Goerigk-et-al:CC96,GlesnerGoosZimmeermann04,GoosZimmermann00} projects, and more recently of
   the \emph{CompCert} project \cite{CompCert,BDL-fm06,Le-popl06}. There
   is also a rich body of work on the related approaches of
   \emph{translation validation}
   \cite{Pnueli98a,Pnueli98b,Ne-pldi00,ZaksPnueli08},
   \emph{certifying compilation}
   \cite{NL-pldi98,Colby-etal-pldi00,BlechPoetzsch07}, and
   \emph{proof-carrying code} \cite{Ne-popl97,AF-popl00,FNSG-tlfi07}.
   However, an integratedly verified compiler, which is optimizing and
   ensures non-functional program properties such as on time and space
   resources required by the compiled program is still
   missing. Complementary to these approaches are approaches focusing on
   frameworks for verifying compiler optimizations
   \cite{781156,1040335,Kundu+09} or the verification of specific
   compiler optimizations, such as the \emph{Lazy Code Motion}
   \cite{TristanLeroy09} or instruction scheduling
   \cite{TristanLeroy08}. By far more ambitious and a grand challenge for
   computing research is Tony Hoare's vision of a \emph{verifying
   compiler} which proves properties of the translated program
   \cite{Hoare03}.
   
   \emph{Resource analysis}, especially worst-case execution time analysis $($WCET$)$ for real-time systems, which are often safety-critical, is a vibrant field of research in academia and industry and of fast growing economical relevance,
   especially in the avionics and automotive industry. A survey on
   state-of-the-art tools and methods for WCET analysis has recently been
   given by Wilhelm et al.~\cite{Wilhelm:TECS2008}. The outcomes of the
   WCET Tool Challenges \cite{Gus:ISoLA2006,Holsti:WCET2008}, however,
   demonstrate that all these tools have their own strengths and
   limitations. In particular, they all rely to some extent on
   user-assistance and thus a \emph{trusted information basis} guiding
   the WCET analysis \cite{Prantl:WCET2009}.
   
   
   %\paragraph{AK}
   %Three aspects of program and compiler correctness exist. The verifying
   %compiler proves properties of the translated program and is a grand challenge
   %for computing research \cite{Hoare03}. A certified compiler like Verifix is
   %proven once to do semantically equivalent optimizations and translations
   %\cite{GlesnerGoosZimmeermann04,GoosZimmermann00}. Translation validation proves
   %at every compiler run that the translation is correct and was introduced by
   %Pnueli et al.\ \cite{Pnueli98a,Pnueli98b} and Necula \cite{Necula00}. Until now
   %some optimizations have been verified, recently lazy code motion
   %\cite{TristanLeroy09}, instruction scheduling \cite{TristanLeroy08}, or the whole
   %code generation phase \cite{BlechPoetzsch07}. Another research direction is the
   %construction of general frameworks for validation \cite{ZaksPnueli08} or
   %generalizations like parameterized equivalence checking \cite{Kundu+09}.
   
 %ADL and Instruction Set Simulators \cite{MishraDutt08}  
   
 Compiler Verification \cite{Hoare,1328444,1314860}  
   
 WCET \cite{}  
   
 \subsubsection*{Previous achievements:}  \subsubsection*{Previous achievements:}
 %\emph{Brief description of your own contributions to the related  %\emph{Brief description of your own contributions to the related
 %scientific state-of-the art (5-10 lines)}  %scientific state-of-the art (5-10 lines)}
 Jens Knoop has a long history on work on program analysis with topics  Jens Knoop's research focuses on proven correct and optimal program
 like partial redundancy elimination or lazy code motion  analyses and optimizations \cite{Kn-lncs1428}. He is the co-inventor
 \cite{knoop:DSP:2008:1575,conf/cc/XueK06,scholz04}. Recently he  of the \emph{Lazy Code Motion}
 changed his research focus on worst case execution time analysis  \cite{KRS-pldi92,KRS-retrolcm04,XueK06}, and numerous other program
 \cite{SchrSchoKn09,Prantl:WLPE2008,prantl_et_al:DSP:2008:1661,  analyses and optimizations including
 kirner_et_al:DSP:2008:1657,kirner_et_al:DSP:2007:1197}. He is involved  \emph{partial dead-code elimination}  \cite{KRS-pldi94} and
 in the organization of many compiler conferences and since 2002 program  \emph{partially redundant assignment elimination} \cite{KRS-pldi94},
 cochair of the yearly workshop on compiler optimization meets verification.  which are now part of state-of-the-art compilers. Regarding the
   present PP, particularly important are the achievements on
   resource-aware program analyses and optimizations including the
   code-size sensitive \emph{Sparse Code Motion} \cite{RKS-popl00}, and its
   counterpart for \emph{Speculative Code Motion} \cite{scholz04}.
   Recent research in the frame of the FWF project CoSTA and the EU FP7
   project ALL-TIMES focuses on compiler support for
   \emph{worst-case execution time analysis} for safety-critical
   real-time embedded systems
   \cite{Prantl:WCET2009,SchrSchoKn09,Prantl:WLPE2008,prantl_et_al:DSP:2008:1661,kirner_et_al:DSP:2008:1657,kirner_et_al:DSP:2007:1197}.
   
   % He served on $50+$
   %programme committees of international conferences including PLDI, CC,
   %TACAS, Formal Methods, and Supercomputing. He was the General Chair of
   %PLDI'02 and ETAPS'06, and is Programme Committee Co-Chair of PACT'10. He is the
   %iniator and co-founder of the annual workshop series on
   %\emph{Compiler Optimization meets Compiler Verification} (since 2002),
   %co-organizer of 4 Dagstuhl seminars, most recently on \emph{Verifying
   %Optimizing Compilation}, and a member of the European Network of
   %Excellence HiPEAC.
   %, and the IFIP WG 2.4 \emph{Software Implementation Technology}.
   
 Andreas Krall does research in the area of architecture description  Andreas Krall does research in the area of architecture description
 languages and the automatic generation of highly optimizing compilers,  languages and the automatic generation of highly optimizing compilers,
Line 84 
Line 164 
 specification of a processor \cite{BrFeKrRi09,BrEbKr07,FaKrHo07,  specification of a processor \cite{BrFeKrRi09,BrEbKr07,FaKrHo07,
 FarKrStBrand06,Krall+04micro}. An important focus is on optimization  FarKrStBrand06,Krall+04micro}. An important focus is on optimization
 techniques for embedded processors  techniques for embedded processors
 \cite{EbBrSchKrWiKa08,MeKr07,PrKrHo06,HiKr03} as he lead the Christian  \cite{EbBrSchKrWiKa08,MeKr07,PrKrHo06,HiKr03} as he leads the Christian
 Doppler research laboratory {\em compilation techniques for embedded  Doppler research laboratory {\em compilation techniques for embedded
 processors} with partners from industry (Infineon, OnDemand  processors} with partners from industry (Infineon, OnDemand
 Microelectronics).  Microelectronics).
   
   The PP is designed to synergetically combine the complementary
   expertises of Jens Knoop on verified resource-aware program analyses
   and optimizations and of Andreas Krall on compilation techniques for
   embedded processors. Their complementary expertise is essential for
   the PP.
   
   
 \subsubsection*{Goals (first 4 years):}  \subsubsection*{Goals (first 4 years):}
 %\emph{Description of the research  %\emph{Description of the research
 %topics to be addressed during the first 4 years. Make sure to explicitly  %topics to be addressed during the first 4 years. Make sure to explicitly
 %stress what the significant additions to the scientific knowledge are,  %stress what the significant additions to the scientific knowledge are,
 %and why they are important. (30-40 lines)}  %and why they are important. (30-40 lines)}
   The goals of the first 4 years are as follows:
   
 New modeling and representation techniques of non-functional program and system properties on the programming and intermediate language levels  \begin{itemize}
 Definitions and measures of non-functional program and system properties (performance, time, space/memory, power, concurrency).  \item New modeling and representation techniques of non-functional
 Modeling and representation of these properties alongside with the programming languages semantics        program and system properties on the programming and
 Adapting and enhancing state-of-the-art compilation techniques towards non-functional property and platform awareness        intermediate language levels
 New functional and non-functional property and platform-aware compilation techniques  \item Definitions and measures of non-functional program and system
 Analyses for non-functional program and system properties        properties (performance, time, space/memory, power,
 Functional and non-functional property and platform-aware code generation techniques        concurrency).
 Enabling validation and verification throughout the compilation process  \item Modeling and representation of these properties alongside
 Techniques for reducing or eliminating trusted code, annotation, etc., bases        with the programming languages semantics
   \item Adapting and enhancing state-of-the-art compilation techniques
         towards non-functional property and platform awareness
   \item New functional and non-functional property and platform-aware
         compilation techniques
   \item Analyses for non-functional program and system properties
   \item Functional and non-functional property and platform-aware
         code generation techniques
   \item Enabling validation and verification throughout the compilation
         process
   \item Techniques for reducing or eliminating trusted code,
         annotation, etc., bases
   \end{itemize}
   These goals are essential for making the development and the
   compilation of embedded systems software more reliable and
   robust. Moreover, they are the basis for the second 4 years extension
   of the project.
   
   
 \subsubsection*{Work Plan (first 4 years):}  \subsubsection*{Work Plan (first 4 years):}
Line 112 
Line 215 
 %you intend to conduct the actual research during the first 4 years. Be sure  %you intend to conduct the actual research during the first 4 years. Be sure
 %to also describe and (coarsely) quantify the resources (staff, cost of  %to also describe and (coarsely) quantify the resources (staff, cost of
 %special equipment) required for this work in a table. (20-30 lines)}  %special equipment) required for this work in a table. (20-30 lines)}
   Compilation techniques for robust embedded systems comprise different
   areas.  Therefore, the project is divided into three work packages:
   \emph{compilation and simulation techniques for reliability}, \emph{verified
   compilation} and \emph{resource analysis}.
   
   \paragraph*{WP1 - Compilation and Simulation Techniques for Reliability}
   
   In previous work we have developed a processor description language
   with a very concise semantics from where we automatically generate
   optimized compilers \cite{BrEbKr07} and high efficient instruction set
   simulators \cite{BrFeKrRi09}. This environment we use as testbed for
   our compiler optimizations for embedded processors
   \cite{EbBrSchKrWiKa08,PrKrHo06,MeKr07}. We will extend this
   environment to do research on compilation and simulation techniques to
   enhance the reliability of processor/memory systems by mixed
   hardware/software and pure software techniques.
   
   \begin{itemize}
   \item Specification method to specify an energy consumption model in
         a processor specification.
   \item Specification method for redundancy and error correction in the
         processor specification
   \item Specification method for fault injection and fault checking in
         the processor specification
   \item Generation of optimized instruction set simulators from the
         extended processor specification
   \item Generation of optimizing compilers from the extended processor
         specification
   \item Research into new compiler optimizations to increase reliability by
         pure software solutions, mixed hardware/software solutions and
         balancing performance, code space, reliability and energy consumption
   \item Research of correctness proofs and validation of the new optimizations
   
   \end{itemize}
   
 (1) Specification and efficient simulation of reliable processors (partial redundancy,  \paragraph*{WP2 - Verified Compilation}
 ECC, lockstep etc) and compiler optimizations to exploit/balance reliabiliy features.  
 Connection with CESAR NN1  Suitable semantics are necessary which support efficient translation
   validation or support easy verification of a compiler. We will
   research into different semantics and into mappings between the
   semantics of our processor description language \cite{BrEbKr07} and a
   compiler backend semantics, intermediate representation semantics
   (compatible to LLVM) and source language semantics. The main research
   will be on verification and translation validation for all kinds of
   compiler optimizations.
   
   \begin{itemize}
   \item Evaluate different semantics regarding suitability for compiler
         verification and translation validation, eventually develop new
         semantics
   \item Develop a translator for an automatic mapping from our processor
         description language into verification semantics
   \item Develop a validation system from the intermediate representation
         (LLVM) to the processor semantics
   \item Develop a validation system from the source language (C) to the
         intermediate representation (LLVM)
   \item Research into verification and translation validation for different
         frontend and backend optimizations
   \end{itemize}
   
   \paragraph*{WP3 - Resource Analysis}
   For safety-critical real-time embedded sytems resource consumption
   measured in terms of a quantitative aspect of a program execution such
   as execution time, storage use, and power consumption belongs rather
   to the functional properties of an application rather its
   non-functional ones. Formal guarantees on resource consumption are
   thus essential and mandatory to ensure the robustness of such
   systems. This requires new and usually more complex but more
   expressive program analyses and transformations to support the (1)
   programmer during source code development by early and automatically
   providing hints on resource consumption and (2) the compiler to
   optimize for resource consumption. In our previous work we focused on
   compiler support for
   \emph{worst-case execution time analysis $($WCET$)$} \cite{Prantl:WCET2009,Prantl:WLPE2008,prantl_et_al:DSP:2008:1661,kirner_et_al:DSP:2008:1657}. Based on this work we will extend this research towards
   other quantitive aspects of resource consumption, especially storage
   usage, towards these two global objectives, using the programming
   environment used there as testbed for implementation
   \cite{Prantl:WCET2009,Prantl:WLPE2008,prantl_et_al:DSP:2008:1661,kirner_et_al:DSP:2008:1657}.
   
   \begin{itemize}
   \item Research into new program analyses for providing high-quality
         bounds on resourse consumption which are useful for both the
         application programmer and the compiler.
   \item Research new program analyses and static optimizations
         to optimize for resource consumption and to help complying to
         possibly given limits.
   \item Research suitable abstraction levels of interfaces and modes
         of interaction between fully automatic program analysis and
         verification methods and semi-automatic ones relying on
         user-assistance because of undecidability issues
   \item Research the synergies and the trade-off between fully
         automatic program analysis and verification methods and
         semi-automatic ones utilizing user-assistance on high-quality
         resource bounds and the computational costs to compute them.
   \item Research simulation and profiling methods to assess the
         quality of resource consumption analyses and to support
         correctness and security checks at run-time.
   \end{itemize}
   Overall, this WP will contribute to the design, foundations,
   verification, implementation, and application of resource analyses.
   
 (2) translation verification, specification of semantics of IRs solving  
 subproblems. NN1 + NN2  
   
 (3) WCET NN3  
   
   
 \begin{tabular}{llll}  \begin{tabular}{llll}
   \\
 \hline  \hline
 {\bf Pos} & {\bf Type} & {\bf Description}    & {\bf Duration} \\  {\bf Pos} & {\bf Type} & {\bf Description}    & {\bf Duration} \\
 NN1 & PhD & reliable compilation / simulation & 4 years \\  NN1 & PhD & reliable compilation / simulation & 4 years \\
 NN2 & PhD & compiler verificationi            & 4 years \\  NN2 & PhD & verified compilation              & 4 years \\
 NN3 & PhD & WCET                              & 4 years \\  NN3 & PhD & resource analysis                 & 4 years \\
 \hline  \hline
 \end{tabular}  \end{tabular}
   
   
 \subsubsection*{Goals (last 4 years):}  \subsubsection*{Goals (last 4 years):}
 %\emph{Brief description of the  %\emph{Brief description of the
 %eesearch topics to be addressed during the last 4 years. Make sure to  %research topics to be addressed during the last 4 years. Make sure to
 %explicitly stress what the significant additions to the scientific  %explicitly stress what the significant additions to the scientific
 %knowledge are, and why they are important. (20-30 lines)}  %knowledge are, and why they are important. (20-30 lines)}
   
 New programming languages and compilers for RESs  In the last 4 years we will extend the research of the first years into
 Non-functional properties and requirements as first-class language and compiler citizens  some additional directions like
 New compilation techniques enabling a uniform and integrated approach  
   \begin{itemize}
   \item New programming languages and compilers for RESs
   \item Non-functional properties and requirements as first-class language and
         compiler citizens
   \item New compilation techniques enabling a uniform and integrated approach
 for ensuring functional and non-functional program and system requirements  for ensuring functional and non-functional program and system requirements
 Replacing trust by proof  \item Verified compilers, proof-carrying code, verifying compilation for RESs
 Certifying compilation, proof-carrying code, translation validation  \item Making legacy applications fit to and available on RESs
 Verified compilers, verifying compilation for RESs  \item Techniques for adjusting and decompiling legacy applications
 Making legacy applications fit to and available on RESs  \end{itemize}
 Techniques for adjusting and decompiling legacy applications  
   Application of the results of this research reduces the cost of the
   development of reliable and correct embedded systems and makes them
   safer and robust.
   
 \subsubsection*{Collaboration with other PPs:}  \subsubsection*{Collaboration with other PPs:}
 %\emph{List the PPs you are expecting to collaborate with, and describe briefly  %\emph{List the PPs you are expecting to collaborate with, and describe briefly
Line 160 
Line 363 
       Links to specification and modeling of timing properties, to execution        Links to specification and modeling of timing properties, to execution
       models, hardware and software models.        models, hardware and software models.
 \item PP Composition and Predictability in RES Architectures  \item PP Composition and Predictability in RES Architectures
       [E182/Puschner]: Links to hard- and software models for time        [E182.1/Puschner]: Links to hard- and software models for time
       predictable systems, verification of timing behaviour.        predictable systems, verification of timing behaviour.
 \item PP Formal Verification for Robustness [E184/Veith]: Links to software  \item PP Formal Verification for Robustness [E184/Veith]: Links to software
       model checking and testing of code (on source code and intermediate        model-checking and testing of code (on source code and intermediate
       code levels), support for program analysis and transformation.        code levels), support for program analysis and transformation.
 \item PP Modeling \& Analysis of Robust Distributed Systems [E182/Schmid]:  \item PP Modeling \& Analysis of Robust Distributed Systems [E182.2/Schmid]:
       Links to functional and non-functional system requirements,        Links to functional and non-functional system requirements,
       distribution, concurrency.        distribution, concurrency.
 \end{itemize}  \end{itemize}
Line 174 
Line 377 
 %\emph{List envisioned international  and national collaborations, and  %\emph{List envisioned international  and national collaborations, and
 %describe briefly the topic and nature  of such a collaboration. (5-10  %describe briefly the topic and nature  of such a collaboration. (5-10
 %lines)}  %lines)}
   \begin{itemize}
 Aviral Shrivastava, Arizona State University, Tempe, AZ, USA  \item Walter Binder, University of Lugano, Switzerland (resource analysis)
   \item Sabine Glesner, TU Berlin, Berlin, Germany (verified compilation)
 Wolf Zimmermann, Universit\"at Halle, Halle, Germany  \item Aviral Shrivastava, Arizona State University, Tempe, AZ, USA (reliable compilation)
   \item Wolf Zimmermann, Martin-Luther Universit\"at Halle-Wittenberg, Halle, Germany
         (verified compilation)
   \end{itemize}
   
 \begin{comment}  \begin{comment}
 %Bitte hier die Bibtex-Entries  einfuellen, z.B.,  %Bitte hier die Bibtex-Entries  einfuellen, z.B.,

Generate output suitable for use with a patch program
Legend:
Removed from v.1.2  
changed lines
  Added in v.1.16
CVS Admin

Powered by ViewCVS 1.0-dev 		(Powered by ViewCVS)

ViewCVS and CVS Help