Verified integrity properties for safe approximate program transformations
Approximate computations (for example, video, audio, and image processing, machine learning, and many scientific computations) have the freedom to generate a range of acceptable results. Approximate program transformations (for example, task skipping and loop perforation) exploit this freedom to pro...
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | en_US |
| Published: |
Association for Computing Machinery (ACM)
2014
|
| Online Access: | http://hdl.handle.net/1721.1/90624 https://orcid.org/0000-0001-8195-4145 https://orcid.org/0000-0003-0313-9270 https://orcid.org/0000-0001-8095-8523 |
| _version_ | 1811083280186867712 |
|---|---|
| author | Kim, Deokhwan Misailovic, Sasa Rinard, Martin C. Carbin, Michael James |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Kim, Deokhwan Misailovic, Sasa Rinard, Martin C. Carbin, Michael James |
| author_sort | Kim, Deokhwan |
| collection | MIT |
| description | Approximate computations (for example, video, audio, and image processing, machine learning, and many scientific computations) have the freedom to generate a range of acceptable results. Approximate program transformations (for example, task skipping and loop perforation) exploit this freedom to produce computations that can execute at a variety of points in an underlying accuracy versus performance trade-off space. One potential concern is that these transformations may change the semantics of the program and therefore cause the program to crash, perform an illegal operation, or otherwise violate its integrity.
We investigate how verifying integrity properties -- key correctness properties that the transformed computation must respect -- can enable the safe application of approximate program transformations. We present experimental results from a compiler that verifies integrity properties of perforated loops to enable the safe application of loop perforation. |
| first_indexed | 2024-09-23T12:30:33Z |
| format | Article |
| id | mit-1721.1/90624 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T12:30:33Z |
| publishDate | 2014 |
| publisher | Association for Computing Machinery (ACM) |
| record_format | dspace |
| spelling | mit-1721.1/906242022-09-28T08:10:24Z Verified integrity properties for safe approximate program transformations Kim, Deokhwan Misailovic, Sasa Rinard, Martin C. Carbin, Michael James Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Carbin, Michael James Kim, Deokhwan Misailovic, Sasa Rinard, Martin C. Approximate computations (for example, video, audio, and image processing, machine learning, and many scientific computations) have the freedom to generate a range of acceptable results. Approximate program transformations (for example, task skipping and loop perforation) exploit this freedom to produce computations that can execute at a variety of points in an underlying accuracy versus performance trade-off space. One potential concern is that these transformations may change the semantics of the program and therefore cause the program to crash, perform an illegal operation, or otherwise violate its integrity. We investigate how verifying integrity properties -- key correctness properties that the transformed computation must respect -- can enable the safe application of approximate program transformations. We present experimental results from a compiler that verifies integrity properties of perforated loops to enable the safe application of loop perforation. National Science Foundation (U.S.) (Grant CCF-0811397) National Science Foundation (U.S.) (Grant CCF-0905244) National Science Foundation (U.S.) (Grant CCF-1036241) National Science Foundation (U.S.) (Grant IIS-0835652) United States. Defense Advanced Research Projects Agency (Grant FA8650-11-C-7192) United States. Defense Advanced Research Projects Agency (Grant FA8750-12-2-0110) United States. Dept. of Energy (Grant DE-SC0005288) 2014-10-08T14:21:24Z 2014-10-08T14:21:24Z 2013-01 Article http://purl.org/eprint/type/ConferencePaper 9781450318426 http://hdl.handle.net/1721.1/90624 Michael Carbin, Deokhwan Kim, Sasa Misailovic, and Martin C. Rinard. 2013. Verified integrity properties for safe approximate program transformations. In Proceedings of the ACM SIGPLAN 2013 workshop on Partial evaluation and program manipulation (PEPM '13). ACM, New York, NY, USA, 63-66. 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/2426890.2426901 Proceedings of the ACM SIGPLAN 2013 workshop on Partial evaluation and program manipulation (PEPM '13) Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/pdf Association for Computing Machinery (ACM) MIT web domain |
| spellingShingle | Kim, Deokhwan Misailovic, Sasa Rinard, Martin C. Carbin, Michael James Verified integrity properties for safe approximate program transformations |
| title | Verified integrity properties for safe approximate program transformations |
| title_full | Verified integrity properties for safe approximate program transformations |
| title_fullStr | Verified integrity properties for safe approximate program transformations |
| title_full_unstemmed | Verified integrity properties for safe approximate program transformations |
| title_short | Verified integrity properties for safe approximate program transformations |
| title_sort | verified integrity properties for safe approximate program transformations |
| url | http://hdl.handle.net/1721.1/90624 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 kimdeokhwan verifiedintegritypropertiesforsafeapproximateprogramtransformations AT misailovicsasa verifiedintegritypropertiesforsafeapproximateprogramtransformations AT rinardmartinc verifiedintegritypropertiesforsafeapproximateprogramtransformations AT carbinmichaeljames verifiedintegritypropertiesforsafeapproximateprogramtransformations |