Review of: M. Carbin, D. Kim, S. Misailovic, and M. C. Rinard, “Proving acceptability properties of relaxed nondeterministic approximate programs,” in Proc. of the 33rd ACM SIGPLAN conference PLDI, 2012, pp. 169–180.

1         Identification of the Problem

To achieve performance gains and to enable tradeoffs between performance and the accuracy of programs, there are several program-level parameters that can be controlled, of which skipping tasks, loop perforation, and approximate datatypes are just a few examples. Nondeterministic, approximate, or relaxed programs are a class of programs that enable tradeoffs between performance and program ‘accuracy’ (or semantics), by modification of variables that control execution. Intuitively, there are a number of application domains that can easily tolerate reductions in program accuracy for hopefully disproportionate gains in performance. However, verifying the correctness of programs with relaxed semantics is typically approached in a domain-specific manner, and has not been formalized up to this point. The proposed work formalizes the notion of relaxed dynamic semantics, introduces a program development methodology, and provides associated code for automatically verifying the semantics of relaxed programs with respect to its original counterpart using Coq. The purpose of the proposed work and the way that the work attempts to solve the larger problem of enabling program-level tradeoffs between performance and accuracy is to provide a framework for automatic verification of program semantics after relaxed optimizations have been performed. Guided accuracy-compromising program development expressly for the sake of achieving performance gains is outside the scope of the proposed work.

2         Methods and Assumptions

As part of the solution, the work delivers several contributions:

• A set of language constructs for developing relaxed programs and for stating acceptability properties of relaxed programs
• Proof rules are for reasoning about acceptability properties of relaxed programs
• Proof rules for verifying the stated acceptability properties of relaxed programs
• Machine-checked proofs that the formalized, axiomatic original and relaxed semantics are sound with respect to the dynamic semantics, and provide the stated semantic properties
• A methodology for developing relaxed programs:
  • The developer first develops a standard program and uses standard approaches to reason about this program to determine that it satisfies desired acceptability properties
  • Either the developer or an automated system (such as a compiler that implements loop perforation) then relaxes the program to enable additional nondeterministic executions
  • The developer uses relational reasoning to verify that the relaxation maintains the desired acceptability properties, i.e. the developer specifies and verifies additional relational assertions that characterize the relationship between the original and relaxed semantics

Acceptability properties are expressed by two types of predicates:

• relational properties, which define the relationship between the values of variables in the original program and the relaxed program
• unary properties, which define values that appear exclusively in one or the other version of the program
• Because successful relaxations do not typically interfere with the basic integrity of the original program, the reasoning that establishes the validity of the integrity properties typically transfers directly from the original program over to the relaxed program.
• Accuracy properties formalize how accurate the outputs must be to stay within the acceptable range, and it is often convenient to express accuracy requirements by bounding the difference between results from the original and relaxed executions

Relaxed programming constructs include:

• nondeterministic variable assignments (via the relax statement),
• relational assertions that relate the relaxed semantics to the original semantics (via the relate statement),
• unary assertions (via the assert statement), and
• unary assumptions (via the assume statement)

Relational expressions among values from the original and the relaxed versions of the program, denoted E* for integers and B* for Booleans, are used to formulate predicates that expression relational properties among the respective analogies of the variables. This allows us to develop a new set of predicates (P*) that express conditions that relate values of variables from the original and relaxed versions, for example, “The magnitude of the difference of the value of the variable X in the relaxed program is less than or equal to 2”, i.e. |X<o> – X<r>| ≤ 2. This methodology makes the assumption that both the deterministic and the relaxed nondeterministic versions of the same program are available.

Reading the semantics presented by the paper is nearly identical to the Hoare-style semantics that we had discussed in class. In the paper, for the original semantics, the Hoare-style triple {P} s {Q} is read as, “if the command s is started in any state satisfying precondition P, and if s eventually terminates, then the final state is guaranteed to satisfy the postcondition Q”. The relaxed version of the Hoare triple is a bit different in that it requires the verification of the original and relaxed semantics in lockstep. {P*} s {Q*} is read as, “if the command s is started in any pair of states (σ_o, σ_r) that satisfy precondition P*, and if s eventually terminates, then the final state is guaranteed to satisfy the pair of states (σ_o’, σ_r’), which are subsets of postcondition Q*”. The propositions expressed as the pre- and postconditions reference variables or arguments to commands as part of the command set s, not the commands themselves. The same command is running in both the original and relaxed versions of the program, but the specifications on the values of the variables as arguments are weaker for the relaxed program.

In terms of our class discussion, Carbin’s system of logic allows us to strengthen both precondition and the postcondition predicates for the relaxed version of the program with respect to pre- and postconditions of the original program. For preconditions, this relaxes the notion of correctness, and is opposite of what we had discussed in class, that to prove program equivalence, corresponding preconditions may be weaker, and postconditions may be stronger. For example, if the precondition of an original program states that even(X) must be true, we could create a relaxed version of that program by strengthening the predicate to the condition that X must simply be an integer. Similarly, if a postcondition for a program with original semantics states that X must be less than 4, we could develop a weaker postcondition in the relaxed version of the program that states that X must be prime. The set of valid conditions expressed by the stronger predicate is larger. (Note: I’d like to follow up with you on this)

3         Evaluation Criteria

Since Carbin et. al. are introducing a new system of sentential logic, their evaluation criteria is based on proving properties of logic systems like soundness and completeness, and proving that stated properties for acceptability can be satisfied. While it is mentioned, a proof for completeness is not provided, mostly because it is not quite as important as soundness in order for a derivation system to be useful. Furthermore it is acceptable that the system be relatively complete with respect to the semantics of propositions, as is Hoare logic itself. In essence what this means is that incorrect programs may not be identified as such, but if a program is truly correct with respect to the expressed properties, the derivation system will classify it as such. The authors provide mathematical proof that the proposed system of logic is sound with respect to original dynamic semantics introduced by Floyd and Hoare. In terms of this evaluation criteria, if the proofs of coherence of the proposed system of logic are to be believed, the evidence is irrefutable.

However, we may impose additional evaluation criteria on the paper, which are alluded to at the beginning. For example, the authors state that typical goals of developing approximate programs include:

• Maximizing performance subject to an accuracy constraint,
• maximizing accuracy subject to a performance constraint, or
• dynamically adjusting program behavior to adapt to changes in the characteristics of the underlying hardware platform (such as varying load or clock rate)

To this end, however, the paper does not provide any guidance. While the authors state several times that relaxed programs can be used to trade off between performance and accuracy in the space, they never actually show any results of performance tradeoffs made by applying this methodology.

The framework admittedly does not support relational reasoning about programs for which the control flow of the original and relaxed program versions diverge out of lockstep. The lockstep requirement is restrictive because it requires a high degree of structural similarity between the original program and the relaxed program. Furthermore, the proposed system of verification assumes that both the original and relaxed versions of the program are available to form the basis of reasoning about the relaxed program. The question remains as to whether it is worth the effort of the developer to achieve performance tradeoffs. Ultimately, this question is outside the scope of this work, but a much more powerful system could automatically make inferences about the semantics of an existing original program and would relax them autonomously. However, this would require a formalization of higher-level application requirements, which may not be available or could be hard to formalize. Still, it would be compelling to develop an optimizing compiler that could make suggestions about which regions of programs could be relaxed given some small subset of application specifications.

4         Innovation and Risk

The most innovative part of this work is the concept that approximate program semantics can be formalized in an application-agnostic way. “Application fidelity” has been defined in many different application specific ways, such as mean squared error, structural similarity index (SSIM), or even more dubious metrics as ‘diagnosability’ in biomedical contexts. If anyone tried to formalize such requirements, whatever they could come up with would likely be a subset of the system of logic developed by Carbin et. al., such as for the case of mean squared error, the error could be expressed as the square of the difference between corresponding variables among the original program and the relaxed version. Furthermore, a significant degree of risk is displayed by the researchers in introducing fairly radical concepts such as skipping tasks to a community focused on rigorous program correctness and theorem proving.

5         Discussion

In my interpretation, the essence of this paper reveals that it is possible for the semantics of approximate programs to be proven automatically, subject to some relational properties between the original and relaxed versions of program. The authors don’t just show that it’s possible but provide a rigorously developed proof for the soundness of the method. Taken in reverse, this approach can provide a methodology for systematic development of approximate programs that provably meet their specifications, and that don’t simply run off into the weeds. The process of writing approximate is anything but! The axioms developed here can be taken as a set of principles for what parts of a program can be flexible, and what parts are not. Although the properties provided here are not exhaustive, they provide a functionally complete basis upon which non-trivial, useful, but approximate programs can be built. But why create approximate programs when we have the ability to create exact programs? Hopefully, because there is a way to achieve a disproportionately large gain in terms of some performance metric, e.g. latency or energy or thermal, etc. But what does this mean about equivalence properties?

The proposed framework offers a hardware-independent means of making performance tradeoffs for program accuracy. If a specific target architecture is chosen, the work could be extended to achieve hardware-dependent performance gains, and the specific tradeoff gains can be evaluated depending on the underlying hardware. Ultimately, we are interested in a framework that can allow us to evaluate whether it is more desirable to perform tradeoff optimizations in software or in hardware, and how to combine those optimizations to maximize the benefits of the tradeoff. For example, if we are given an architecture that makes available variable clock rate, or if there is an algorithm with continuously changing load like video compression: how would we make the most of accuracy relaxation to maximize the performance of the application with respect to energy or latency?

Another compelling research question is how do we use notions of relaxed semantics at the program level to design more efficient hardware? While previously we discussed leveraging relaxed semantics of programs to achieve performance gains using existing hardware, would perhaps a new ASIC realization of the program be more efficient than its originally, always correct counterpart?

While admittedly this is outside the scope of this work, the other thing it doesn’t do is guide the development of relaxed semantics: say I have an algorithm that computes the location of a target in a video game. If I want to introduce relaxed semantics into that algorithm, Carbin et. al.’s methodology only shows me how to specify predicates that could be proved to satisfy relaxed predicates, but they don’t tell me what changes I need to make to the algorithm so that it relaxes the accuracy of the final result and actually increases the performance of the algorithm. have an exact video game on a desktop and want to port it to a portable system and trade accuracy for energy performance, wouldn’t know how to actually do it.

Finally, it would be very interesting to compare the runtime characteristics of extracted versions of relaxed programs produced by this framework.

Definitions

relaxed program              A program that may adjust its execution by changing one or more variables subject to a specified relaxation predicate. For example, a perforated program may dynamically choose to skip loop iterations each time it enters a given loop. A relaxed program is therefore a nondeterministic program, with each execution a variant of the original execution. The different executions typically share a common global structure, with local differences at only those parts of the computation affected by the modified variables.

acceptability properties                               Properties that the program must satisfy to be acceptable. Examples include integrity properties and accuracy properties.

integrity properties        An acceptability property that the program must satisfy to successfully produce a result. For example, an integrity property might state that in a relaxed program, a function must return a value greater than zero (otherwise the program might crash) to be acceptable.

accuracy properties        An acceptability property that characterizes how accurate the produced result must be. For example, an accuracy property might state that the relaxed program must (potentially only with high probability) produce a result that differs by at most a specified percentage from the result that the original program produces.

original semantics          Dynamic semantics at the stage of program development in which the developer first develops a standard program and uses standard approaches to reason about this program to determine that it satisfies desired acceptability properties.

relaxed semantics           Dynamic semantics at the stage of program development in which either the developer or an automated system (such as a compiler that implements loop perforation) relaxes the program to enable additional nondeterministic executions

relational assertions      Assertions that characterize the relationship between the original semantics and the relaxed semantics

relational reasoning      Serves as a bridge to transfer properties of the original program over to the relaxed program.