Principal Investigator Michael Carbin
Approximate program transformations such as task skipping, loop perforation, approximate function memoization, and approximate data types produce programs that can execute at a variety of points in an underlying performance versus accuracy tradeoff space. Namely, these transformed programs trade accuracy of their results for increased performance by dynamically and nondeterministically modifying variables that control their execution. I have defined such transformed programs as relaxed programs -- they have been extended with additional nondeterminism to relax their semantics and enable greater flexibility in their execution.
This project provides programming language constructs for developing relaxed programs. It also provides proof rules for reasoning about acceptability properties, which are the key correctness properties of relaxed programs that enable them to have a range of acceptable executions. Specifically, these proof rules enable programmers to directly specify and verify relational properties that characterize the desired correctness relationships, such as accuracy, between the values of variables in a program's original semantics (before the transformation) and its relaxed semantics. Moreover, these rules enable programmers to reuse correctness properties that hold for the original program to efficiently verify the relaxed.