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.
-
Our goal is to design and implement tools
for building reactive real-time systems that go beyond
``valid via testing'', toward ``correct by construction'' technology.
Such tools may lead to faster software development and fewer surprises
after deployment.
Publications
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.