Sciweavers

Share
PLDI
2012
ACM

Proving acceptability properties of relaxed nondeterministic approximate programs

8 years 2 months ago
Proving acceptability properties of relaxed nondeterministic approximate programs
Approximate program transformations such as skipping tasks [29, 30], loop perforation [21, 22, 35], reduction sampling [38], multiple selectable implementations [3, 4, 16, 38], dynamic knobs [16], synchronization elimination [20, 32], approximate function memoization [11], and approximate data types [34] produce programs that can execute at a variety of points in an underlying performance versus accuracy tradeoff space. These transformed programs have the ability to trade accuracy of their results for increased performance by dynamically and nondeterministically modifying variables that control their execution. We call such transformed programs relaxed programs because they have been extended with additional nondeterminism to relax their semantics and enable greater flexibility in their execution. We present language constructs for developing and specifying relaxed programs. We also present proof rules for reasoning about acceptability properties [28], which the program must satisfy ...
Michael Carbin, Deokhwan Kim, Sasa Misailovic, Mar
Added 27 Sep 2012
Updated 27 Sep 2012
Type Journal
Year 2012
Where PLDI
Authors Michael Carbin, Deokhwan Kim, Sasa Misailovic, Martin C. Rinard
Comments (0)
books