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...
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | en_US |
| Published: |
Association for Computing Machinery (ACM)
2012
|
| Online Access: | http://hdl.handle.net/1721.1/72437 https://orcid.org/0000-0001-8195-4145 https://orcid.org/0000-0003-0313-9270 https://orcid.org/0000-0001-8095-8523 |
| _version_ | 1826203708336111616 |
|---|---|
| author | Carbin, Michael James Kim, Deokhwan Misailovic, Sasa Rinard, Martin C. |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Carbin, Michael James Kim, Deokhwan Misailovic, Sasa Rinard, Martin C. |
| author_sort | Carbin, Michael James |
| collection | MIT |
| description | 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 properties [28] which the program must satisfy to be acceptable. Our proof rules work with two kinds of acceptability properties: acceptability properties [28], which characterize desired relationships between the values of variables in the original and relaxed programs, and unary acceptability properties, which involve values only from a single (original or relaxed) program. The proof rules support a staged reasoning approach in which the majority of the reasoning effort works with the original program. Exploiting the common structure that the original and relaxed programs share, relational reasoning transfers reasoning effort from the original program to prove properties of the relaxed program.
We have formalized the dynamic semantics of our target programming language and the proof rules in Coq and verified that the proof rules are sound with respect to the dynamic semantics. Our Coq implementation enables developers to obtain fully machine-checked verifications of their relaxed programs. |
| first_indexed | 2024-09-23T12:41:49Z |
| format | Article |
| id | mit-1721.1/72437 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T12:41:49Z |
| publishDate | 2012 |
| publisher | Association for Computing Machinery (ACM) |
| record_format | dspace |
| spelling | mit-1721.1/724372022-10-01T10:33:04Z Proving acceptability properties of relaxed nondeterministic approximate programs Carbin, Michael James Kim, Deokhwan Misailovic, Sasa Rinard, Martin C. Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Rinard, Martin C. Carbin, Michael James Kim, Deokhwan Misailovic, Sasa Rinard, Martin C. 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 properties [28] which the program must satisfy to be acceptable. Our proof rules work with two kinds of acceptability properties: acceptability properties [28], which characterize desired relationships between the values of variables in the original and relaxed programs, and unary acceptability properties, which involve values only from a single (original or relaxed) program. The proof rules support a staged reasoning approach in which the majority of the reasoning effort works with the original program. Exploiting the common structure that the original and relaxed programs share, relational reasoning transfers reasoning effort from the original program to prove properties of the relaxed program. We have formalized the dynamic semantics of our target programming language and the proof rules in Coq and verified that the proof rules are sound with respect to the dynamic semantics. Our Coq implementation enables developers to obtain fully machine-checked verifications of their relaxed programs. National Science Foundation (U.S.). (Grant number CCF-0811397) National Science Foundation (U.S.). (Grant number CCF-0905244) National Science Foundation (U.S.). (Grant number CCF-1036241) National Science Foundation (U.S.). (Grant number IIS-0835652) United States. Defense Advanced Research Projects Agency (Grant number FA8650-11-C-7192) United States. Defense Advanced Research Projects Agency (Grant number FA8750-12-2-0110) United States. Dept. of Energy. (Grant Number DE-SC0005288) 2012-08-29T19:37:17Z 2012-08-29T19:37:17Z 2012-06 Article http://purl.org/eprint/type/ConferencePaper 978-1-4503-1205-9 http://hdl.handle.net/1721.1/72437 Michael Carbin, Deokhwan Kim, Sasa Misailovic, and Martin C. Rinard. 2012. Proving acceptability properties of relaxed nondeterministic approximate programs. In Proceedings of the 33rd ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI '12). ACM, New York, NY, USA, 169-180. https://orcid.org/0000-0001-8195-4145 https://orcid.org/0000-0003-0313-9270 https://orcid.org/0000-0001-8095-8523 en_US http://dx.doi.org/10.1145/2254064.2254086 Proceedings of the 33rd ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI '12) Creative Commons Attribution-Noncommercial-Share Alike 3.0 http://creativecommons.org/licenses/by-nc-sa/3.0/ application/pdf Association for Computing Machinery (ACM) MIT web domain |
| spellingShingle | Carbin, Michael James Kim, Deokhwan Misailovic, Sasa Rinard, Martin C. Proving acceptability properties of relaxed nondeterministic approximate programs |
| title | Proving acceptability properties of relaxed nondeterministic approximate programs |
| title_full | Proving acceptability properties of relaxed nondeterministic approximate programs |
| title_fullStr | Proving acceptability properties of relaxed nondeterministic approximate programs |
| title_full_unstemmed | Proving acceptability properties of relaxed nondeterministic approximate programs |
| title_short | Proving acceptability properties of relaxed nondeterministic approximate programs |
| title_sort | proving acceptability properties of relaxed nondeterministic approximate programs |
| url | http://hdl.handle.net/1721.1/72437 https://orcid.org/0000-0001-8195-4145 https://orcid.org/0000-0003-0313-9270 https://orcid.org/0000-0001-8095-8523 |
| work_keys_str_mv | AT carbinmichaeljames provingacceptabilitypropertiesofrelaxednondeterministicapproximateprograms AT kimdeokhwan provingacceptabilitypropertiesofrelaxednondeterministicapproximateprograms AT misailovicsasa provingacceptabilitypropertiesofrelaxednondeterministicapproximateprograms AT rinardmartinc provingacceptabilitypropertiesofrelaxednondeterministicapproximateprograms |