PhD Proposal

I finally got my thesis proposal past my advisor and onto my committee. So I also put it up on my web page. You can read it here, or the main point is copied below:

Problem

A straightforward instantiation of traditional dataflow analysis techniques fails to provide adequate precision for aggressive optimization of interrupt-driven MCU systems. These systems contain features which either must be dealt with because they hinder the analysis, or should be leveraged because they represent an untapped potential for information. The pivotal features in interrupt-driven MCU systems are the interrupts and the microcontroller themselves.

An interrupt complicates the dataflow analysis for a given code segment because during the segment it may fire at any time, it may fire repeatedly, or it may never fire at all. To avoid unnecessary degredation of the results, an analysis must have a better coping strategy for multiple flows due to interrupts than just modeling all possible interleavings of the flows. On the other hand, interrupts also provide useful divisions between program elements. Some data and code may be only accessed inside a single interrupt, inside multiple interrupts, or outside of any interrupt. Not capitalizing on the isolation of accesses due to interrupts will unnecessarily reduce analysis precision.

Low-level systems programming on MCUs often involves inline assembly and directly accessing specific parts of the MCU. For example, the status register may be directly read, shifted and masked in order to determine the status of the interrupt bit. Naively and pessimistically analyzing all hardware accesses degrades the analysis of systems code very quickly. Leveraging the information is crucial for the success of
the analysis.

Solution

I am developing a framework to enable sound and accurate dataflow analysis for interrupt-driven microcontroller programs. This framework adapts existing abstract interpretation ideas to system-level C code. My framework integrates several synergistic analyses such as value-flow analysis, pointer analysis, and callgraph construction. Contributions of my work include using pluggable abstract interpretation domains, providing a novel model of interrupt-driven concurrency, allowing dataflow through volatile variables when safe to do so, and tracking interrupt firing dependencies. When compared to a highly optimizing C compiler, my framework improves traditional code optimizations such as conditional constant propagation, dead code elimination, redundant synchronization elimination, and inessential-safety-check removal. It also enables new transformations such as RAM compression, the sub-word packing of statically allocated global variables. These transformations help microcontroller programs meet stringent resource requirements.