Powered by ViewCVS 1.0-dev
| 1 : | andi | 1.1 | \documentclass[11pt,a4paper]{article} |
| 2 : | %\usepackage{latexsym} | ||
| 3 : | \usepackage{url} | ||
| 4 : | %\usepackage{times} | ||
| 5 : | \usepackage{comment} | ||
| 6 : | \pagestyle{plain} | ||
| 7 : | \setlength{\textwidth}{16truecm} | ||
| 8 : | \setlength{\textheight}{24truecm} | ||
| 9 : | \setlength{\oddsidemargin}{-0.3truecm} | ||
| 10 : | \setlength{\evensidemargin}{-0.3truecm} | ||
| 11 : | \setlength{\topmargin}{0.0truecm} | ||
| 12 : | \setlength{\topskip}{0.0truecm} | ||
| 13 : | \setlength{\headheight}{0.0truecm} | ||
| 14 : | \setlength{\headsep}{0.0truecm} | ||
| 15 : | |||
| 16 : | \newcommand{\emn}[1]{{\em #1\/}} | ||
| 17 : | \newcommand{\NOTE}[1]{{\medskip\bf #1\medskip}} | ||
| 18 : | |||
| 19 : | \title{\bf PP \emph{Compilation Techniques for Robust Embedded Systems}} | ||
| 20 : | |||
| 21 : | knoop | 1.13 | \author{{\sc Jens Knoop and Andreas Krall}\\ |
| 22 : | \{knoop,andi\}@complang.tuwien.ac.at | ||
| 23 : | andi | 1.1 | } |
| 24 : | |||
| 25 : | \bibliographystyle{unsrt} | ||
| 26 : | |||
| 27 : | \begin{document} | ||
| 28 : | \maketitle | ||
| 29 : | |||
| 30 : | knoop | 1.10 | PP leader: \emph{Jens Knoop and Andreas Krall (beide E185.1)} |
| 31 : | andi | 1.1 | |
| 32 : | knoop | 1.10 | Associated researchers: \emph{Anton Ertl (E185.1), Bernhard Gramlich (E185.2)} |
| 33 : | andi | 1.1 | |
| 34 : | |||
| 35 : | |||
| 36 : | \subsubsection*{Motivation:} | ||
| 37 : | %\emph{Informal description of the purpose of the PP (3-5 lines)} | ||
| 38 : | Every embedded system consists of software which is written in a high | ||
| 39 : | level language, compiled to machine language and executed on a | ||
| 40 : | knoop | 1.10 | processor. For robust embedded systems new verified analysis and |
| 41 : | compilation, simulation, and specification methods are necessary to | ||
| 42 : | support the programmer during application development and maintenance | ||
| 43 : | and to optimize for performance, power, space, concurrency and | ||
| 44 : | reliability during compilation. | ||
| 45 : | %for short, new programming and | ||
| 46 : | %compilation techniques for robust embedded systems development and | ||
| 47 : | %deployment. | ||
| 48 : | andi | 1.1 | |
| 49 : | \subsubsection*{State of the art and related work:} | ||
| 50 : | %\emph{Briefly describe the scientific state of the art (20-30 lines)} | ||
| 51 : | |||
| 52 : | andi | 1.2 | %Compilation Techniques for Reliability |
| 53 : | Because of the exponential increase of the number of transistors and | ||
| 54 : | the continuing decrease of the feature sizes of current processors | ||
| 55 : | knoop | 1.10 | \emph{soft errors} mainly caused by energetic particles are becoming an |
| 56 : | andi | 1.2 | important design issue for robust embedded systems. Blome et |
| 57 : | al.~\cite{Blome+06} observed that a majority of faults that affect the | ||
| 58 : | architectural state of a processor come from the register file. Lee | ||
| 59 : | knoop | 1.10 | and Shrivastava \cite{LeeShrivastava09a,LeeShrivastava09c} proposed |
| 60 : | different solutions to cope with this problem. The first assigns | ||
| 61 : | variables depending on their lifetime to either the ECC protected or | ||
| 62 : | the unprotected part of a register file to balance energy consumption | ||
| 63 : | and reliability \cite{LeeShrivastava09a}. The second spills registers | ||
| 64 : | to ECC protected memory if the register contents are not used for a | ||
| 65 : | long period \cite{LeeShrivastava09c}. There exist complete software | ||
| 66 : | solutions which use different forms of code duplications | ||
| 67 : | \cite{Oh+02a,Reis+05}, which do failure virtualization | ||
| 68 : | \cite{WapplerMueller08} or which use techniques like control flow | ||
| 69 : | checking \cite{Oh+02b}. A complete overview of processor description | ||
| 70 : | languages and generation of compilers and simulators from processor | ||
| 71 : | specifications gives the book of Mishra and Dutt \cite{MishraDutt08}. | ||
| 72 : | andi | 1.4 | A good survey of current instruction set simulators gives our chapter |
| 73 : | knoop | 1.10 | in the \emph{Handbook of Signal Processing systems} \cite{BrHoKr09}. A |
| 74 : | famous instruction set simulator with modelling of energy consumption | ||
| 75 : | is \emph{Wattch} \cite{BrooksTiwariMartonosi00}. | ||
| 76 : | |||
| 77 : | Methods for \emph{compiler verification} do exist | ||
| 78 : | \cite{Langmaack97a,Po-lncs124,MMO-lncs1283,Goos:99:verifix,Goos:00:ASM,1328444}. | ||
| 79 : | Most notably are the pioneering approaches of the | ||
| 80 : | \emph{ProCoS} \cite{Langmaack96a} and the \emph{Verifix} | ||
| 81 : | knoop | 1.13 | \cite{Goerigk-et-al:CC96,GlesnerGoosZimmeermann04,GoosZimmermann00} projects, and more recently of |
| 82 : | knoop | 1.10 | the \emph{CompCert} project \cite{CompCert,BDL-fm06,Le-popl06}. There |
| 83 : | is also a rich body of work on the related approaches of | ||
| 84 : | \emph{translation validation} | ||
| 85 : | knoop | 1.14 | \cite{Pnueli98a,Pnueli98b,Ne-pldi00,ZaksPnueli08}, |
| 86 : | knoop | 1.13 | \emph{certifying compilation} |
| 87 : | knoop | 1.10 | \cite{NL-pldi98,Colby-etal-pldi00,BlechPoetzsch07}, and |
| 88 : | \emph{proof-carrying code} \cite{Ne-popl97,AF-popl00,FNSG-tlfi07}. | ||
| 89 : | knoop | 1.13 | However, an integratedly verified compiler, which is optimizing and |
| 90 : | ensures non-functional program properties such as on time and space | ||
| 91 : | knoop | 1.14 | resources required by the compiled program is still |
| 92 : | knoop | 1.13 | missing. Complementary to these approaches are approaches focusing on |
| 93 : | frameworks for verifying compiler optimizations | ||
| 94 : | \cite{781156,1040335,Kundu+09} or the verification of specific | ||
| 95 : | knoop | 1.14 | compiler optimizations, such as the \emph{Lazy Code Motion} |
| 96 : | knoop | 1.13 | \cite{TristanLeroy09} or instruction scheduling |
| 97 : | \cite{TristanLeroy08}. By far more ambitious and a grand challenge for | ||
| 98 : | computing research is Tony Hoare's vision of a \emph{verifying | ||
| 99 : | compiler} which proves properties of the translated program | ||
| 100 : | \cite{Hoare03}. | ||
| 101 : | |||
| 102 : | knoop | 1.14 | \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, |
| 103 : | knoop | 1.10 | especially in the avionics and automotive industry. A survey on |
| 104 : | state-of-the-art tools and methods for WCET analysis has recently been | ||
| 105 : | given by Wilhelm et al.~\cite{Wilhelm:TECS2008}. The outcomes of the | ||
| 106 : | WCET Tool Challenges \cite{Gus:ISoLA2006,Holsti:WCET2008}, however, | ||
| 107 : | demonstrate that all these tools have their own strengths and | ||
| 108 : | limitations. In particular, they all rely to some extent on | ||
| 109 : | user-assistance and thus a \emph{trusted information basis} guiding | ||
| 110 : | the WCET analysis \cite{Prantl:WCET2009}. | ||
| 111 : | |||
| 112 : | andi | 1.1 | |
| 113 : | knoop | 1.13 | %\paragraph{AK} |
| 114 : | %Three aspects of program and compiler correctness exist. The verifying | ||
| 115 : | %compiler proves properties of the translated program and is a grand challenge | ||
| 116 : | %for computing research \cite{Hoare03}. A certified compiler like Verifix is | ||
| 117 : | %proven once to do semantically equivalent optimizations and translations | ||
| 118 : | %\cite{GlesnerGoosZimmeermann04,GoosZimmermann00}. Translation validation proves | ||
| 119 : | %at every compiler run that the translation is correct and was introduced by | ||
| 120 : | %Pnueli et al.\ \cite{Pnueli98a,Pnueli98b} and Necula \cite{Necula00}. Until now | ||
| 121 : | %some optimizations have been verified, recently lazy code motion | ||
| 122 : | %\cite{TristanLeroy09}, instruction scheduling \cite{TristanLeroy08}, or the whole | ||
| 123 : | %code generation phase \cite{BlechPoetzsch07}. Another research direction is the | ||
| 124 : | %construction of general frameworks for validation \cite{ZaksPnueli08} or | ||
| 125 : | %generalizations like parameterized equivalence checking \cite{Kundu+09}. | ||
| 126 : | andi | 1.9 | |
| 127 : | andi | 1.7 | |
| 128 : | knoop | 1.13 | |
| 129 : | |||
| 130 : | andi | 1.1 | \subsubsection*{Previous achievements:} |
| 131 : | %\emph{Brief description of your own contributions to the related | ||
| 132 : | %scientific state-of-the art (5-10 lines)} | ||
| 133 : | knoop | 1.10 | Jens Knoop's research focuses on proven correct and optimal program |
| 134 : | analyses and optimizations \cite{Kn-lncs1428}. He is the co-inventor | ||
| 135 : | of the \emph{Lazy Code Motion} | ||
| 136 : | knoop | 1.13 | \cite{KRS-pldi92,KRS-retrolcm04,XueK06}, and numerous other program |
| 137 : | analyses and optimizations including | ||
| 138 : | \emph{partial dead-code elimination} \cite{KRS-pldi94} and | ||
| 139 : | \emph{partially redundant assignment elimination} \cite{KRS-pldi94}, | ||
| 140 : | which are now part of state-of-the-art compilers. Regarding the | ||
| 141 : | present PP, particularly important are the achievements on | ||
| 142 : | resource-aware program analyes and optimizations including the | ||
| 143 : | code-size sensitive \emph{Sparse Code Motion} \cite{RKS-popl00}, and its | ||
| 144 : | counterpart for \emph{Speculative Code Motion} \cite{scholz04}. | ||
| 145 : | Recent research in the frame of the FWF project CoSTA and the EU FP7 | ||
| 146 : | project ALL-TIMES focuses on compiler support for | ||
| 147 : | knoop | 1.10 | \emph{worst-case execution time analysis} for safety-critical |
| 148 : | real-time embedded systems | ||
| 149 : | knoop | 1.13 | \cite{Prantl:WCET2009,SchrSchoKn09,Prantl:WLPE2008,prantl_et_al:DSP:2008:1661,kirner_et_al:DSP:2008:1657,kirner_et_al:DSP:2007:1197}. |
| 150 : | |||
| 151 : | % He served on $50+$ | ||
| 152 : | %programme committees of international conferences including PLDI, CC, | ||
| 153 : | %TACAS, Formal Methods, and Supercomputing. He was the General Chair of | ||
| 154 : | %PLDI'02 and ETAPS'06, and is Programme Committee Co-Chair of PACT'10. He is the | ||
| 155 : | %iniator and co-founder of the annual workshop series on | ||
| 156 : | %\emph{Compiler Optimization meets Compiler Verification} (since 2002), | ||
| 157 : | %co-organizer of 4 Dagstuhl seminars, most recently on \emph{Verifying | ||
| 158 : | %Optimizing Compilation}, and a member of the European Network of | ||
| 159 : | %Excellence HiPEAC. | ||
| 160 : | knoop | 1.10 | %, and the IFIP WG 2.4 \emph{Software Implementation Technology}. |
| 161 : | andi | 1.1 | |
| 162 : | Andreas Krall does research in the area of architecture description | ||
| 163 : | languages and the automatic generation of highly optimizing compilers, | ||
| 164 : | efficient instruction set simulators and hardware from one single | ||
| 165 : | specification of a processor \cite{BrFeKrRi09,BrEbKr07,FaKrHo07, | ||
| 166 : | FarKrStBrand06,Krall+04micro}. An important focus is on optimization | ||
| 167 : | techniques for embedded processors | ||
| 168 : | knoop | 1.13 | \cite{EbBrSchKrWiKa08,MeKr07,PrKrHo06,HiKr03} as he leads the Christian |
| 169 : | andi | 1.1 | Doppler research laboratory {\em compilation techniques for embedded |
| 170 : | processors} with partners from industry (Infineon, OnDemand | ||
| 171 : | Microelectronics). | ||
| 172 : | |||
| 173 : | knoop | 1.13 | The PP is designed to exploit the synergies of the complementary |
| 174 : | expertise of Jens Knoop on resource-aware program analyses and | ||
| 175 : | optimizations and their verification and of Andreas Krall on | ||
| 176 : | compilation techniques for embedded processors. Their complementary | ||
| 177 : | expertise is essential for the PP. | ||
| 178 : | |||
| 179 : | andi | 1.1 | |
| 180 : | \subsubsection*{Goals (first 4 years):} | ||
| 181 : | %\emph{Description of the research | ||
| 182 : | %topics to be addressed during the first 4 years. Make sure to explicitly | ||
| 183 : | %stress what the significant additions to the scientific knowledge are, | ||
| 184 : | %and why they are important. (30-40 lines)} | ||
| 185 : | knoop | 1.13 | The goals of the first 4 years are as follows: |
| 186 : | andi | 1.1 | |
| 187 : | knoop | 1.13 | \begin{itemize} |
| 188 : | \item New modeling and representation techniques of non-functional | ||
| 189 : | program and system properties on the programming and | ||
| 190 : | intermediate language levels | ||
| 191 : | \item Definitions and measures of non-functional program and system | ||
| 192 : | properties (performance, time, space/memory, power, | ||
| 193 : | concurrency). | ||
| 194 : | \item Modeling and representation of these properties alongside | ||
| 195 : | with the programming languages semantics | ||
| 196 : | \item Adapting and enhancing state-of-the-art compilation techniques | ||
| 197 : | towards non-functional property and platform awareness | ||
| 198 : | \item New functional and non-functional property and platform-aware | ||
| 199 : | compilation techniques | ||
| 200 : | \item Analyses for non-functional program and system properties | ||
| 201 : | \item Functional and non-functional property and platform-aware | ||
| 202 : | code generation techniques | ||
| 203 : | \item Enabling validation and verification throughout the compilation | ||
| 204 : | process | ||
| 205 : | \item Techniques for reducing or eliminating trusted code, | ||
| 206 : | annotation, etc., bases | ||
| 207 : | \end{itemize} | ||
| 208 : | These goals are essential for making the development and the | ||
| 209 : | compilation of embedded systems software more reliable and | ||
| 210 : | robust. Moreover, they are the basis for the second 4 years extension | ||
| 211 : | of the project. | ||
| 212 : | andi | 1.1 | |
| 213 : | |||
| 214 : | \subsubsection*{Work Plan (first 4 years):} | ||
| 215 : | %\emph{Brief description of how | ||
| 216 : | %you intend to conduct the actual research during the first 4 years. Be sure | ||
| 217 : | %to also describe and (coarsely) quantify the resources (staff, cost of | ||
| 218 : | %special equipment) required for this work in a table. (20-30 lines)} | ||
| 219 : | knoop | 1.11 | Compilation techniques for robust embedded systems comprise different |
| 220 : | areas. Therefore, the project is divided into three work packages: | ||
| 221 : | knoop | 1.13 | \emph{compilation and simulation techniques for reliability}, \emph{verified |
| 222 : | compilation} and \emph{resource analysis}. | ||
| 223 : | andi | 1.1 | |
| 224 : | andi | 1.5 | \paragraph*{WP1 - Compilation and Simulation Techniques for Reliability} |
| 225 : | andi | 1.1 | |
| 226 : | andi | 1.6 | In previous work we have developed a processor description language |
| 227 : | with a very concise semantics from where we automatically generate | ||
| 228 : | optimized compilers \cite{BrEbKr07} and high efficient instruction set | ||
| 229 : | simulators \cite{BrFeKrRi09}. This environment we use as testbed for | ||
| 230 : | our compiler optimizations for embedded processors | ||
| 231 : | \cite{EbBrSchKrWiKa08,PrKrHo06,MeKr07}. We will extend this | ||
| 232 : | environment to do research on compilation and simulation techniques to | ||
| 233 : | enhance the reliability of processor/memory systems by mixed | ||
| 234 : | hardware/software and pure software techniques. | ||
| 235 : | andi | 1.1 | |
| 236 : | andi | 1.5 | \begin{itemize} |
| 237 : | \item Specification method to specify an energy consumption model in | ||
| 238 : | a processor specification. | ||
| 239 : | \item Specification method for redundancy and error correction in the | ||
| 240 : | processor specification | ||
| 241 : | \item Specification method for fault injection and fault checking in | ||
| 242 : | the processor specification | ||
| 243 : | \item Generation of optimized instruction set simulators from the | ||
| 244 : | andi | 1.6 | extended processor specification |
| 245 : | \item Generation of optimizing compilers from the extended processor | ||
| 246 : | specification | ||
| 247 : | andi | 1.5 | \item Research into new compiler optimizations to increase reliability by |
| 248 : | pure software solutions, mixed hardware/software solutions and | ||
| 249 : | balancing performance, code space, reliability and energy consumption | ||
| 250 : | \item Research of correctness proofs and validation of the new optimizations | ||
| 251 : | |||
| 252 : | \end{itemize} | ||
| 253 : | |||
| 254 : | \paragraph*{WP2 - Verified Compilation} | ||
| 255 : | |||
| 256 : | andi | 1.8 | Suitable semantics are necessary which support efficient translation |
| 257 : | knoop | 1.11 | validation or support easy verification of a compiler. We will |
| 258 : | research into different semantics and into mappings between the | ||
| 259 : | semantics of our processor description language \cite{BrEbKr07} and a | ||
| 260 : | compiler backend semantics, intermediate representation semantics | ||
| 261 : | (compatible to LLVM) and source language semantics. The main research | ||
| 262 : | will be on verification and translation validation for all kinds of | ||
| 263 : | compiler optimizations. | ||
| 264 : | andi | 1.8 | |
| 265 : | \begin{itemize} | ||
| 266 : | \item Evaluate different semantics regarding suitability for compiler | ||
| 267 : | verification and translation validation, eventually develop new | ||
| 268 : | semantics | ||
| 269 : | \item Develop a translator for an automatic mapping from our processor | ||
| 270 : | description language into verification semantics | ||
| 271 : | \item Develop a validation system from the intermediate representation | ||
| 272 : | (LLVM) to the processor semantics | ||
| 273 : | \item Develop a validation system from the source language (C) to the | ||
| 274 : | intermediate representation (LLVM) | ||
| 275 : | \item Research into verification and translation validation for different | ||
| 276 : | frontend and backend optimizations | ||
| 277 : | \end{itemize} | ||
| 278 : | andi | 1.5 | |
| 279 : | knoop | 1.11 | \paragraph*{WP3 - Resource Analysis} |
| 280 : | For safety-critical real-time embedded sytems resource consumption | ||
| 281 : | measured in terms of a quantitative aspect of a program execution such | ||
| 282 : | as execution time, storage use, and power consumption belongs rather | ||
| 283 : | to the functional properties of an application rather its | ||
| 284 : | non-functional ones. Formal guarantees on resource consumption are | ||
| 285 : | thus essential and mandatory to ensure the robustness of such | ||
| 286 : | systems. This requires new and usually more complex but more | ||
| 287 : | expressive program analyses and transformations to support the (1) | ||
| 288 : | programmer during source code development by early and automatically | ||
| 289 : | providing hints on resource consumption and (2) the compiler to | ||
| 290 : | optimize for resource consumption. In our previous work we focused on | ||
| 291 : | compiler support for | ||
| 292 : | knoop | 1.14 | \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 |
| 293 : | knoop | 1.11 | other quantitive aspects of resource consumption, especially storage |
| 294 : | usage, towards these two global objectives, using the programming | ||
| 295 : | environment used there as testbed for implementation | ||
| 296 : | \cite{Prantl:WCET2009,Prantl:WLPE2008,prantl_et_al:DSP:2008:1661,kirner_et_al:DSP:2008:1657}. | ||
| 297 : | |||
| 298 : | \begin{itemize} | ||
| 299 : | \item Research into new program analyses for providing high-quality | ||
| 300 : | bounds on resourse consumption which are useful for both the | ||
| 301 : | application programmer and the compiler. | ||
| 302 : | \item Research new program analyses and static optimizations | ||
| 303 : | to optimize for resource consumption and to help complying to | ||
| 304 : | possibly given limits. | ||
| 305 : | \item Research suitable abstraction levels of interfaces and modes | ||
| 306 : | of interaction between fully automatic program analysis and | ||
| 307 : | verification methods and semi-automatic ones relying on | ||
| 308 : | user-assistance because of undecidability issues | ||
| 309 : | \item Research the synergies and the trade-off between fully | ||
| 310 : | automatic program analysis and verification methods and | ||
| 311 : | semi-automatic ones utilizing user-assistance on high-quality | ||
| 312 : | resource bounds and the computational costs to compute them. | ||
| 313 : | \item Research simulation and profiling methods to assess the | ||
| 314 : | knoop | 1.13 | quality of resource consumption analyses and to support |
| 315 : | correctness and security checks at run-time. | ||
| 316 : | knoop | 1.11 | \end{itemize} |
| 317 : | Overall, this WP will contribute to the design, foundations, | ||
| 318 : | verification, implementation, and application of resource analyses. | ||
| 319 : | |||
| 320 : | andi | 1.1 | |
| 321 : | andi | 1.2 | |
| 322 : | andi | 1.1 | |
| 323 : | \begin{tabular}{llll} | ||
| 324 : | andi | 1.5 | \\ |
| 325 : | andi | 1.1 | \hline |
| 326 : | andi | 1.2 | {\bf Pos} & {\bf Type} & {\bf Description} & {\bf Duration} \\ |
| 327 : | NN1 & PhD & reliable compilation / simulation & 4 years \\ | ||
| 328 : | andi | 1.5 | NN2 & PhD & verified compilation & 4 years \\ |
| 329 : | knoop | 1.14 | NN3 & PhD & resource analysis & 4 years \\ |
| 330 : | andi | 1.1 | \hline |
| 331 : | \end{tabular} | ||
| 332 : | |||
| 333 : | |||
| 334 : | \subsubsection*{Goals (last 4 years):} | ||
| 335 : | %\emph{Brief description of the | ||
| 336 : | andi | 1.12 | %research topics to be addressed during the last 4 years. Make sure to |
| 337 : | andi | 1.1 | %explicitly stress what the significant additions to the scientific |
| 338 : | %knowledge are, and why they are important. (20-30 lines)} | ||
| 339 : | |||
| 340 : | andi | 1.12 | In the last 4 years we will extend the research of the first years into |
| 341 : | some additional directions like | ||
| 342 : | |||
| 343 : | \begin{itemize} | ||
| 344 : | \item New programming languages and compilers for RESs | ||
| 345 : | \item Non-functional properties and requirements as first-class language and | ||
| 346 : | compiler citizens | ||
| 347 : | \item New compilation techniques enabling a uniform and integrated approach | ||
| 348 : | for ensuring functional and non-functional program and system requirements | ||
| 349 : | \item Verified compilers, proof-carrying code, verifying compilation for RESs | ||
| 350 : | \item Making legacy applications fit to and available on RESs | ||
| 351 : | \item Techniques for adjusting and decompiling legacy applications | ||
| 352 : | \end{itemize} | ||
| 353 : | |||
| 354 : | Application of the results of this research reduces the cost of the | ||
| 355 : | development of reliable and correct embedded systems and makes them | ||
| 356 : | safer and robust. | ||
| 357 : | andi | 1.1 | |
| 358 : | \subsubsection*{Collaboration with other PPs:} | ||
| 359 : | %\emph{List the PPs you are expecting to collaborate with, and describe briefly | ||
| 360 : | %the topic and nature of such a collaboration. (10-20 lines)} | ||
| 361 : | |||
| 362 : | \begin{itemize} | ||
| 363 : | \item PP Composition of Non-functional Requirements [I.S.T.A./Henzinger]: | ||
| 364 : | Links to specification and modeling of timing properties, to execution | ||
| 365 : | models, hardware and software models. | ||
| 366 : | \item PP Composition and Predictability in RES Architectures | ||
| 367 : | knoop | 1.14 | [E182.1/Puschner]: Links to hard- and software models for time |
| 368 : | andi | 1.1 | predictable systems, verification of timing behaviour. |
| 369 : | \item PP Formal Verification for Robustness [E184/Veith]: Links to software | ||
| 370 : | knoop | 1.10 | model-checking and testing of code (on source code and intermediate |
| 371 : | andi | 1.1 | code levels), support for program analysis and transformation. |
| 372 : | knoop | 1.14 | \item PP Modeling \& Analysis of Robust Distributed Systems [E182.2/Schmid]: |
| 373 : | andi | 1.1 | Links to functional and non-functional system requirements, |
| 374 : | distribution, concurrency. | ||
| 375 : | \end{itemize} | ||
| 376 : | |||
| 377 : | \subsubsection*{External Collaborations:} | ||
| 378 : | %\emph{List envisioned international and national collaborations, and | ||
| 379 : | %describe briefly the topic and nature of such a collaboration. (5-10 | ||
| 380 : | %lines)} | ||
| 381 : | knoop | 1.10 | \begin{itemize} |
| 382 : | andi | 1.12 | \item Walter Binder, University of Lugano, Switzerland (resource analysis) |
| 383 : | \item Sabine Glesner, TU Berlin, Berlin, Germany (verified compilation) | ||
| 384 : | \item Aviral Shrivastava, Arizona State University, Tempe, AZ, USA (reliable compilation) | ||
| 385 : | knoop | 1.10 | \item Wolf Zimmermann, Martin-Luther Universit\"at Halle-Wittenberg, Halle, Germany |
| 386 : | andi | 1.12 | (verified compilation) |
| 387 : | knoop | 1.10 | \end{itemize} |
| 388 : | andi | 1.1 | |
| 389 : | \begin{comment} | ||
| 390 : | %Bitte hier die Bibtex-Entries einfuellen, z.B., | ||
| 391 : | |||
| 392 : | |||
| 393 : | ------------------------------------ | ||
| 394 : | |||
| 395 : | @article{Hoare, | ||
| 396 : | author = {Tony Hoare}, | ||
| 397 : | title = {The verifying compiler: A grand challenge for computing research}, | ||
| 398 : | journal = {Journal of the ACM}, | ||
| 399 : | volume = {50}, | ||
| 400 : | number = {1}, | ||
| 401 : | year = {2003}, | ||
| 402 : | issn = {0004-5411}, | ||
| 403 : | pages = {63--69}, | ||
| 404 : | doi = {http://doi.acm.org/10.1145/602382.602403}, | ||
| 405 : | publisher = {ACM}, | ||
| 406 : | address = {New York, NY, USA}, | ||
| 407 : | } | ||
| 408 : | |||
| 409 : | @article{1328444, | ||
| 410 : | author = {Jean-Baptiste Tristan and Xavier Leroy}, | ||
| 411 : | title = {Formal verification of translation validators: a case study on instruction scheduling optimizations}, | ||
| 412 : | journal = {SIGPLAN Not.}, | ||
| 413 : | volume = {43}, | ||
| 414 : | number = {1}, | ||
| 415 : | year = {2008}, | ||
| 416 : | issn = {0362-1340}, | ||
| 417 : | pages = {17--27}, | ||
| 418 : | doi = {http://doi.acm.org/10.1145/1328897.1328444}, | ||
| 419 : | publisher = {ACM}, | ||
| 420 : | address = {New York, NY, USA}, | ||
| 421 : | } | ||
| 422 : | |||
| 423 : | @article{1314860, | ||
| 424 : | author = {Jan Olaf Blech and Arnd Poetzsch-Heffter}, | ||
| 425 : | title = {A Certifying Code Generation Phase}, | ||
| 426 : | journal = {Electron. Notes Theor. Comput. Sci.}, | ||
| 427 : | volume = {190}, | ||
| 428 : | number = {4}, | ||
| 429 : | year = {2007}, | ||
| 430 : | issn = {1571-0661}, | ||
| 431 : | pages = {65--82}, | ||
| 432 : | doi = {http://dx.doi.org/10.1016/j.entcs.2007.09.008}, | ||
| 433 : | publisher = {Elsevier Science Publishers B. V.}, | ||
| 434 : | address = {Amsterdam, The Netherlands, The Netherlands}, | ||
| 435 : | } | ||
| 436 : | |||
| 437 : | @INPROCEEDINGS{LeeShrivastava09, | ||
| 438 : | TITLE = {A Compiler Optimization to Reduce Soft Errors in Register Files}, | ||
| 439 : | AUTHOR = {Jongeun Lee and Aviral Shrivastava}, | ||
| 440 : | BOOKTITLE = {ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems}, | ||
| 441 : | EDITOR = {Mahmut Kandemir}, | ||
| 442 : | PUBLISHER = {ACM}, | ||
| 443 : | PAGES = {??--??}, | ||
| 444 : | ADDRESS = {Dublin}, | ||
| 445 : | MONTH = {June}, | ||
| 446 : | YEAR = {2009}, | ||
| 447 : | } | ||
| 448 : | |||
| 449 : | @BOOK{MishraDutt08, | ||
| 450 : | TITLE = {Processor Description Languages}, | ||
| 451 : | AUTHOR = {Prabhat Mishra and Nikil Dutt (Editor)}, | ||
| 452 : | PUBLISHER = {Morgan Kaufmann}, | ||
| 453 : | YEAR = {2008}, | ||
| 454 : | } | ||
| 455 : | |||
| 456 : | |||
| 457 : | |||
| 458 : | %Eigene Referenzen ab hier. | ||
| 459 : | |||
| 460 : | @InProceedings{SchrSchoKn09, | ||
| 461 : | TITLE = "Adding Timing-Awareness to {AUTOSAR} Basic-Software - A Component Based Approach", | ||
| 462 : | AUTHOR = "Dietmar Schreiner and Markus Schordan and Jens Knoop", | ||
| 463 : | BOOKTITLE = "12th IEEE International Symposium on Object/component/service-oriented | ||
| 464 : | Real-time distributed Computing (ISORC 2009)", | ||
| 465 : | PUBLISHER = "IEEE", | ||
| 466 : | ADDRESS = "Tokyo, Japan", | ||
| 467 : | YEAR = "2009", | ||
| 468 : | MONTH = "March", | ||
| 469 : | PAGES = "288--292", | ||
| 470 : | } | ||
| 471 : | |||
| 472 : | @inproceedings{Prantl:WLPE2008, | ||
| 473 : | Address = {Udine, Italy}, | ||
| 474 : | Author = {Adrian Prantl and Jens Knoop and Markus Schordan and Markus Triska}, | ||
| 475 : | Booktitle = {The 18th Workshop on Logic-based methods in Programming Environments (WLPE 2008)}, | ||
| 476 : | Month = {December 12}, | ||
| 477 : | Title = {Constraint solving for high-level WCET analysis}, | ||
| 478 : | Year = {2008}, | ||
| 479 : | URL = {http://costa.tuwien.ac.at/papers/wlpe08.pdf} | ||
| 480 : | } | ||
| 481 : | |||
| 482 : | @InProceedings{prantl_et_al:DSP:2008:1661, | ||
| 483 : | author = "Adrian Prantl and Markus Schordan and Jens Knoop", | ||
| 484 : | title = "TuBound - {A} Conceptually New Tool for Worst-Case | ||
| 485 : | Execution Time Analysis", | ||
| 486 : | booktitle = "8th Intl. Workshop on Worst-Case Execution Time (WCET) | ||
| 487 : | Analysis", | ||
| 488 : | year = "2008", | ||
| 489 : | editor = "Raimund Kirner", | ||
| 490 : | publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, | ||
| 491 : | Germany", | ||
| 492 : | address = "Dagstuhl, Germany", | ||
| 493 : | URL = "http://drops.dagstuhl.de/opus/volltexte/2008/1661", | ||
| 494 : | annote = "Keywords: Worst-case execution time (WCET) analysis, | ||
| 495 : | Tool Chain, Flow Constraints, Source-To-Source", | ||
| 496 : | ISBN = "978-3-939897-10-1", | ||
| 497 : | note = "also published in print by Austrian Computer Society | ||
| 498 : | (OCG) under ISBN 978-3-85403-237-3", | ||
| 499 : | } | ||
| 500 : | |||
| 501 : | @InProceedings{kirner_et_al:DSP:2008:1657, | ||
| 502 : | author = "Raimund Kirner and Albrecht Kadlec and Adrian Prantl | ||
| 503 : | and Markus Schordan and Jens Knoop", | ||
| 504 : | title = "Towards a Common {WCET} Annotation Language: Essential | ||
| 505 : | Ingredients", | ||
| 506 : | booktitle = "8th Intl. Workshop on Worst-Case Execution Time (WCET) | ||
| 507 : | Analysis", | ||
| 508 : | year = "2008", | ||
| 509 : | editor = "Raimund Kirner", | ||
| 510 : | publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, | ||
| 511 : | Germany", | ||
| 512 : | address = "Dagstuhl, Germany", | ||
| 513 : | URL = "http://drops.dagstuhl.de/opus/volltexte/2008/1657", | ||
| 514 : | annote = "Keywords: Worst-case execution time (WCET) analysis, | ||
| 515 : | annotation languages, WCET annotation language | ||
| 516 : | challenge", | ||
| 517 : | ISBN = "978-3-939897-10-1", | ||
| 518 : | note = "also published in print by Austrian Computer Society | ||
| 519 : | (OCG) under ISBN 978-3-85403-237-3", | ||
| 520 : | } | ||
| 521 : | |||
| 522 : | @InProceedings{kirner_et_al:DSP:2007:1197, | ||
| 523 : | author = "Raimund Kirner and Jens Knoop and Adrian Prantl and | ||
| 524 : | Markus Schordan and Ingomar Wenzel", | ||
| 525 : | title = "{WCET} Analysis: The Annotation Language Challenge", | ||
| 526 : | booktitle = "7th Intl. Workshop on Worst-Case Execution Time (WCET) | ||
| 527 : | Analysis", | ||
| 528 : | year = "2007", | ||
| 529 : | editor = "Christine Rochange", | ||
| 530 : | publisher = "Internationales Begegnungs- und Forschungszentrum | ||
| 531 : | f{"u}r Informatik (IBFI), Schloss Dagstuhl, Germany", | ||
| 532 : | address = "Dagstuhl, Germany", | ||
| 533 : | URL = "http://drops.dagstuhl.de/opus/volltexte/2007/1197", | ||
| 534 : | annote = "Keywords: Worst-case execution time analysis, WCET, | ||
| 535 : | path description, annotation language challenge, | ||
| 536 : | expressiveness, convenience", | ||
| 537 : | } | ||
| 538 : | |||
| 539 : | |||
| 540 : | @InProceedings{knoop:DSP:2008:1575, | ||
| 541 : | author = {Jens Knoop}, | ||
| 542 : | title = {Data-Flow Analysis for Multi-Core Computing Systems: A Reminder to Reverse Data-Flow Analysis}, | ||
| 543 : | booktitle = {Scalable Program Analysis}, | ||
| 544 : | year = {2008}, | ||
| 545 : | editor = {Florian Martin and Hanne Riis Nielson and Claudio Riva and Markus Schordan}, | ||
| 546 : | number = {08161}, | ||
| 547 : | series = {Dagstuhl Seminar Proceedings}, | ||
| 548 : | ISSN = {1862-4405}, | ||
| 549 : | publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany}, | ||
| 550 : | address = {Dagstuhl, Germany}, | ||
| 551 : | URL = {http://drops.dagstuhl.de/opus/volltexte/2008/1575}, | ||
| 552 : | annote = {Keywords: Multi-core computing systems, scalable program analysis, reverse data-flow analysis, demand-driven data-flow analysis} | ||
| 553 : | } | ||
| 554 : | |||
| 555 : | @InProceedings{conf/cc/XueK06, | ||
| 556 : | title = "A Fresh Look at {PRE} as a Maximum Flow Problem", | ||
| 557 : | author = "Jingling Xue and Jens Knoop", | ||
| 558 : | bibdate = "2006-04-05", | ||
| 559 : | bibsource = "DBLP, | ||
| 560 : | http://dblp.uni-trier.de/db/conf/cc/cc2006.html#XueK06", | ||
| 561 : | booktitle = "CC", | ||
| 562 : | booktitle = "Compiler Construction, 15th International Conference, | ||
| 563 : | {CC} 2006, Held as Part of the Joint European | ||
| 564 : | Conferences on Theory and Practice of Software, {ETAPS} | ||
| 565 : | 2006, Vienna, Austria, March 30-31, 2006, Proceedings", | ||
| 566 : | publisher = "Springer", | ||
| 567 : | year = "2006", | ||
| 568 : | volume = "3923", | ||
| 569 : | editor = "Alan Mycroft and Andreas Zeller", | ||
| 570 : | ISBN = "3-540-33050-X", | ||
| 571 : | pages = "139--154", | ||
| 572 : | series = "Lecture Notes in Computer Science", | ||
| 573 : | URL = "http://dx.doi.org/10.1007/11688839_13", | ||
| 574 : | } | ||
| 575 : | |||
| 576 : | @InProceedings{scholz04, | ||
| 577 : | author = "Bernhard Scholz and Nigel Horspool and Jens Knoop", | ||
| 578 : | title = "Optimizing for space and time usage with speculative | ||
| 579 : | partial redundancy elimination", | ||
| 580 : | booktitle = "LCTES '04: Proceedings of the 2004 ACM SIGPLAN/SIGBED | ||
| 581 : | conference on Languages, Compilers, and Tools for Embedded Systems", | ||
| 582 : | year = "2004", | ||
| 583 : | ISBN = "1-58113-806-7", | ||
| 584 : | pages = "221--230", | ||
| 585 : | location = "Washington, DC, USA", | ||
| 586 : | publisher = "ACM Press", | ||
| 587 : | } | ||
| 588 : | |||
| 589 : | @InProceedings{HiKr03, | ||
| 590 : | TITLE = "{VLIW} Operation Refinement for Reducing Energy Consumption", | ||
| 591 : | AUTHOR = "Ulrich Hirnschrott and Andreas Krall", | ||
| 592 : | BOOKTITLE = "International Symposium on System-on Chip", | ||
| 593 : | PUBLISHER = "IEEE", | ||
| 594 : | ADDRESS = "Tampere, Finland", | ||
| 595 : | YEAR = "2003", | ||
| 596 : | PAGES = "131--134", | ||
| 597 : | } | ||
| 598 : | |||
| 599 : | @Article{Krall+04micro, | ||
| 600 : | author = {Andreas Krall and Ulrich Hirnschrott and Christian Panis and Ivan Pryanishnikov}, | ||
| 601 : | title = {x{DSP}core: {A} {C}ompiler-{B}ased {C}onfigureable {D}igital {S}ignal {P}rocessor}, | ||
| 602 : | journal = {IEEE Micro}, | ||
| 603 : | year = {2004}, | ||
| 604 : | OPTkey = {}, | ||
| 605 : | volume = {24}, | ||
| 606 : | number = {4}, | ||
| 607 : | pages = {67-78}, | ||
| 608 : | month = {July/August}, | ||
| 609 : | OPTnote = {}, | ||
| 610 : | OPTannote = {}, | ||
| 611 : | } | ||
| 612 : | |||
| 613 : | @INPROCEEDINGS{FarKrStBrand06, | ||
| 614 : | TITLE = {Effective Compiler Generation by Architecture Description}, | ||
| 615 : | AUTHOR = {Stefan Farfeleder and Andreas Krall and Edwin Steiner and Florian Brandner}, | ||
| 616 : | BOOKTITLE = {ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems}, | ||
| 617 : | EDITOR = {Koen De Bosschere}, | ||
| 618 : | PUBLISHER = {ACM}, | ||
| 619 : | PAGES = {145--152}, | ||
| 620 : | ADDRESS = {Ottawa}, | ||
| 621 : | MONTH = {June}, | ||
| 622 : | YEAR = {2006}, | ||
| 623 : | URL = {http://doi.acm.org/10.1145/1134650.1134671}, | ||
| 624 : | } | ||
| 625 : | |||
| 626 : | @ARTICLE{PrKrHo06, | ||
| 627 : | AUTHOR = {Ivan Pryanishnikov and Andreas Krall and Nigel Horspool}, | ||
| 628 : | TITLE = {Compiler Optimizations for Processors with {SIMD} Instructions}, | ||
| 629 : | JOURNAL = {Software---Practice and Experience}, | ||
| 630 : | PUBLISHER = {Wiley}, | ||
| 631 : | VOLUME = {37}, | ||
| 632 : | NUMBER = {1}, | ||
| 633 : | PAGES = {93--113}, | ||
| 634 : | YEAR = {2007}, | ||
| 635 : | URL = {http://www3.interscience.wiley.com/cgi-bin/fulltext/112783581/PDFSTART}, | ||
| 636 : | } | ||
| 637 : | |||
| 638 : | @ARTICLE{FaKrHo07, | ||
| 639 : | AUTHOR = {Stefan Farfeleder and Andreas Krall and Nigel Horspool}, | ||
| 640 : | TITLE = {Ultra Fast Cycle-Accurate Compiled Emulation of Inorder Pipelined Architectures}, | ||
| 641 : | JOURNAL = {Journal of Systems Architecture}, | ||
| 642 : | PUBLISHER = {Elsevier}, | ||
| 643 : | VOLUME = {53}, | ||
| 644 : | NUMBER = {8}, | ||
| 645 : | PAGES = {501--510}, | ||
| 646 : | YEAR = {2007}, | ||
| 647 : | } | ||
| 648 : | |||
| 649 : | @INPROCEEDINGS{MeKr07, | ||
| 650 : | TITLE = {Instruction Set Encoding Optimization for Code Size Reduction}, | ||
| 651 : | AUTHOR = {Michael Med and Andreas Krall}, | ||
| 652 : | BOOKTITLE = {International Conference on Embedded Computer Systems: Architectures, Modeling, and Simulation}, | ||
| 653 : | ADDRESS = {Samos, Greece}, | ||
| 654 : | PAGES = {9--17}, | ||
| 655 : | MONTH = {July}, | ||
| 656 : | YEAR = {2007} | ||
| 657 : | } | ||
| 658 : | |||
| 659 : | @INPROCEEDINGS{BrEbKr07, | ||
| 660 : | TITLE = {Compiler Generation from Structural Architecture Descriptions}, | ||
| 661 : | AUTHOR = {Florian Brandner and Dietmar Ebner and Andreas Krall}, | ||
| 662 : | BOOKTITLE = {International Conference on Compilers, Architecture, and Synthesis for Embedded Systems}, | ||
| 663 : | ADDRESS = {Salzburg, Austria}, | ||
| 664 : | PAGES = {13--22}, | ||
| 665 : | MONTH = {September}, | ||
| 666 : | YEAR = {2007} | ||
| 667 : | } | ||
| 668 : | |||
| 669 : | @INPROCEEDINGS{EbBrSchKrWiKa08, | ||
| 670 : | TITLE = {Generalized Instruction Selection using {SSA}-Graphs}, | ||
| 671 : | AUTHOR = {Dietmar Ebner and Florian Brandner and Bernhard Scholz and Andreas Krall and Peter Wiedermann and Albrecht Kadlec}, | ||
| 672 : | BOOKTITLE = {ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems}, | ||
| 673 : | EDITOR = {John Regehr}, | ||
| 674 : | PUBLISHER = {ACM}, | ||
| 675 : | PAGES = {31--40}, | ||
| 676 : | ADDRESS = {Tucson}, | ||
| 677 : | MONTH = {June}, | ||
| 678 : | YEAR = {2008}, | ||
| 679 : | } | ||
| 680 : | |||
| 681 : | @INPROCEEDINGS{BrFeKrRi09, | ||
| 682 : | TITLE = {Fast and Accurate Simulation using the LLVM Compiler Framework}, | ||
| 683 : | AUTHOR = {Florian Brandner and Andreas Fellnhofer and Andreas Krall and David Riegler}, | ||
| 684 : | BOOKTITLE = {Rapid Simulation and Performance Evaluation: Methods and Tools (RAPIDO'09)}, | ||
| 685 : | EDITOR = {Smail Niar, Rainer Leupers, Olivier Temam}, | ||
| 686 : | PUBLISHER = {HiPEAC}, | ||
| 687 : | PAGES = {1--6}, | ||
| 688 : | ADDRESS = {Paphos, Cyprus}, | ||
| 689 : | MONTH = {January}, | ||
| 690 : | YEAR = {2009}, | ||
| 691 : | } | ||
| 692 : | \end{comment} | ||
| 693 : | |||
| 694 : | \bibliography{res} % Input von res.bib, kommt dann spaeter dazu ... | ||
| 695 : | |||
| 696 : | \end{document} |
|
CVS Admin Powered by ViewCVS 1.0-dev |
ViewCVS and CVS Help |