The power consumption of CPUs and memory systems has traditionally been constrained by the need for strict correctness guarantees. Processor voltage, for instance, must be set high enough to prevent even the rarest timing errors. The SRAM cells in registers need a similar margin to prevent unlikely bit flips.
However, some recent work has shown that many modern applications do not require perfect correctness. An image renderer, for example, can tolerate occasional pixel errors without compromising overall quality of service. Applications that output data meant to be seen by humans (audio or video encoders, for example) also deal with inherent imprecision. Programs like this are paying for reliability that they don’t need.
However, programming an architecture that doesn’t give reliable results would be difficult or impossible. EnerJ represents an attempt to make it possible to safely take advantage of energy/reliability trade-offs. It does so by creating a strict separation of approximate (unreliable) and precise (traditional) program parts and only allowing them to interact in controlled ways.
The language is an extension to Java that adds a type system to
distinguish between approximate
and precise types. Precise types are the default, so ordinary Java code
behaves how you expect it to. Approximate variables are distinguished by a
JSR 308 type qualifier,
@Approx. You can write declarations like this:
@Approx int a = ...;
int p = ...; // precise by default
The variable a can be stored in unreliable memory and computations
involving it may be performed approximately, saving energy.
The variable p, however, behaves fully reliably but saves
no energy. Approximate and precise types are incompatible, which means that
EnerJ’s type checker prohibits this assignment:
p = a; // error!
This prevents the approximate part of the program from “leaking” into the precise part unexpectedly. However precise primitive types are subtypes of their approximate counterparts. This allows flow in one direction, like so:
a = p; // OK
There’s no danger in letting precise data affect approximate computation.
Of course, a complete separation of approximate and precise program components
would probably not be very useful. Frequently, the result of an approximate
computation needs to be used in a precise way (for example, to be summarized or
converted for output). For this reason, EnerJ provides an “escape hatch” for
moving from the approximate world to the precise world. The function endorse
acts as a cast that converts approximate values to precise values:
p = endorse(a); // OK
(The terminology comes from previous work on information-flow type systems.) The programmer has to explicitly mark each point where approximate-to-precise flow occurs. Accidental flows are caught and reported by the type checker. In this way, endorsements enforce disciplined violation of the separation EnerJ provides.
Type qualifiers and endorsements form the basis for the EnerJ language. It also provides some checking of implicit flows and object-oriented features that allow you to apply approximation to user-defined classes. Details on these features can be found in the PLDI paper, which I’ll link here when it’s available.
Through some experimentation with existing Java programs, we found EnerJ’s type annotations easy and intuitive to add to the kinds of programs discussed above. We developed a simulation infrastructure to quantify potential energy savings for the programs, and found that our benchmarks could use 10% to 50% less energy than their fully-precise counterparts without compromising too much output quality.
These encouraging results suggest that occasionally-unreliable systems have the potential to provide significant energy savings, especially when used with applications that don’t require perfect reliability—a programming language like EnerJ, however, is necessary to rein in the chaos of approximate computing.