Resource-Aware Compilation

Jens Palsberg


The project is supported by a National Science Foundation ITR Award, a National Science Foundation Award , and by Intel.

Project Summary

Real-time, reactive and embedded systems are widely and increasingly used throughout society (e.g., flight control, railway signaling, vehicle management systems, medical devices). This trend is likely to continue, as applications that would have been unthinkable only a few years ago come into the reach of ever more complex processors. Many such applications are long lived, interact with their environment continuously, and are under important real-time constraints. As these reactive systems permeate our lives, bringing us everything from intelligent pace-makers to tiny freshness-tracking devices in groceries, the need for cost-effective, confidence-inspiring software engineering techniques grows proportionately.

This project focuses on the challenges faced by compilers for embedded software. For embedded systems, predictability and resource awareness are of greater importance than execution efficiency. For example, if a compiler is not aware of the size of the instruction store for generated code, opportunities to squeeze code into the available space can be lost. A programmer can often hand-optimize generated code, but this is tedious and error-prone, and does not scale to large systems. This project is aimed towards a new generation of resource-aware compilers with solid foundations. Next-generation compilers will lead to increased confidence in a wide variety of embedded systems, including sensor networks, medical implants, engine control, and fly-by-wire/drive-by-wire systems.

We are investigating resource-awareness in several dimensions, including language design, type systems, static analysis, model checking, code generation, and reverse engineering. We are focusing on real-time, interrupt-driven systems and network processors. The resources that we currently consider are code size, stack size, real-time deadlines, bus width, and network-processor packet engines.

Background

Compilers are an important part of today's computational infrastructure because software is ever-increasingly written in high-level programming languages like C, C++, and Java. Early on, compilers were successful for desktop computing, and now they are also used for mission-critical software, trusted mobile code, and real-time embedded systems. The field of compiler design is driven by the advent of new languages, new run-time systems, and new computer architectures, and the need for compilers to be fast, to generate efficient code, and to be correct. Even the smallest of bugs introduced by a compiler can lead to failures, security breaches, and crashes in an otherwise correct system.

Resource-aware compilation is particularly important for embedded systems where economic considerations often lead to the choice of a resource-impoverished processor. A state-of-the-art approach to resource awareness is the use of integer constraints for static analysis and optimization of software. Integer constraints, in the form of integer linear programming (ILP), are particularly well suited for resource issues such as register allocation, instruction scheduling, code-size minimization, energy efficiency, and so forth. The idea is to phrase the static analysis problem as an ILP and then let an off-the-shelf constraint solving tool do the rest. In effect, a compiler writer sees a clean separation of what the analysis is supposed to do'' from how the analysis is done.'' While satisfaction of an ILP is NP-complete, there are many research results and tools concerned with solving ILPs efficiently, making ILP a practical approach for moderately sized programs.

Research Objectives

Our objective is to enable a giant leap forward in the resource-aware compilation technology for embedded systems. We envision an integrated system with (i) a programming language in which a programmer can specify and statically check types that talk about code space, stack size, event-handling time, etc., (ii) a model checking tool that can check resource policies, and (iii) a compiler which generates code that is guaranteed to satisfy all specified resource bounds. We have encouraging preliminary results in all three areas. We have designed a core language in which one can specify types that are annotated with stack-size information [3]. If a program type checks, then it is guaranteed not to cause stack overflow. We have also designed a model checking tool which can analyze machine code for microcontrollers and determine whether all deadlines for event handling will be met [5]. The tool combines static analysis with test oracles in a way that significantly reduces the needed testing effort for the machine code. This is significant because in a time when rapid market cycles in all areas of electronics and communications virtually guarantee design changes in any meaningfully complex project, even the slightest change can invalidate months of comprehensive testing. Finally, we have implemented a compiler which is aware of the size of the available code space; the compiler does ILP-based register allocation and instruction selection so as to squeeze the code into the available space [2].

Future challenges include the composition of ILP-based static analyses, reasoning about the correctness of such analyses, investigating relationships with other approaches, finding ways to handle component-based embedded software, and making approaches scale up to some of the larger processors now used in embedded systems such as Palm Pilots, handheld digital phones, etc.

Expected Impact of Research

While it is unlikely that the need for full-scale testing will ever be completely supplanted by any other methodology, there is great potential for software engineering tools to substantially decrease the cost of building and testing reactive systems, both in time and effort. At the core of such tools is the concept of resource-aware compilation. At the end of the rainbow in this research area lies correct by construction technology, which would allow software to be proven ``correct'' in a wide range of aspects before actual testing even begins. Such tools may lead to faster software development and fewer surprises after deployment.

Publications

  1. Dennis Brylow, Niels Damgaard, and Jens Palsberg. Static Checking of Interrupt-driven Software. In Proceedings of ICSE'01, 23rd International Conference on Software Engineering, pages 47-56, Toronto, May 2001.
  2. Mayur Naik and Jens Palsberg. Compiling with code-size constraints. ACM Transactions on Embedded Computing Systems, 3(1):163-181, 2004. Preliminary version in Proceedings of LCTES'02, Languages, Compilers, and Tools for Embedded Systems joint with SCOPES'02, Software and Compilers for Embedded Systems, pages 120--129, Berlin, Germany, June 2002.
  3. Jens Palsberg and Di Ma. A Typed Interrupt Calculus. In Proceedings of FTRTFT'02, 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems, pages 291--310. Springer-Verlag (LNCS 2469), Oldenburg, Germany, September 2002. Slides.
  4. Krishnendu Chatterjee, Di Ma, Rupak Majumdar, Tian Zhao, Thomas A. Henzinger, and Jens Palsberg. Stack Size Analysis of Interrupt Driven Software, In Proceedings of SAS'03, International Static Analysis Symposium, pages 109-126, San Diego, June 2003.
  5. Dennis Brylow and Jens Palsberg. Deadline Analysis of Interrupt-Driven Software, In Proceedings of FSE'03, ACM SIGSOFT International Symposium on the Foundations of Software Engineering joint with ESEC'03, European Software Engineering Conference, pages 198-207, Helsinki, Finland, September 2003.
  6. V. Krishna Nandivada and Jens Palsberg. Efficient spill code for SDRAM, In Proceedings of CASES'03, International Conference on Compilers, Architecture and Synthesis for Embedded Systems, pages 24-31, San Jose, California, October 2003.
  7. Jens Palsberg and Mayur Naik. ILP-based Resource-aware Compilation. In Ahmed Jerraya and Wayne Wolf, editors, Multiprocessor Systems-on-Chips, Chapter 12. Elsevier, 2004.
  8. Mayur Naik and Jens Palsberg. A type system equivalent to a model checker. In Proceedings of ESOP'05, European Symposium on Programming, Edinburgh, Scotland, April 2005. To appear.