Reasoning about Relaxed Programs
A number of approximate program transformations have recently emerged that enable transformed programs to trade accuracy of their results for increased performance by dynamically and nondeterministically modifying variables that control program execution. We call such transformed programs relaxed pr...
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Published: |
2011
|
| Online Access: | http://hdl.handle.net/1721.1/67031 |
| _version_ | 1811071670524313600 |
|---|---|
| author | Carbin, Michael Kim, Deokhwan Misailovic, Sasa Rinard, Martin C. |
| author2 | Martin Rinard |
| author_facet | Martin Rinard Carbin, Michael Kim, Deokhwan Misailovic, Sasa Rinard, Martin C. |
| author_sort | Carbin, Michael |
| collection | MIT |
| description | A number of approximate program transformations have recently emerged that enable transformed programs to trade accuracy of their results for increased performance by dynamically and nondeterministically modifying variables that control program execution. We call such transformed programs relaxed programs -- they have been extended with additional nondeterminism to relax their semantics and offer greater execution flexibility. We present programming language constructs for developing relaxed programs and proof rules for reasoning about properties of relaxed programs. Our proof rules enable programmers to directly specify and verify acceptability properties that characterize the desired correctness relationships between the values of variables in a program's original semantics (before transformation) and its relaxed semantics. Our proof rules also support the verification of safety properties (which characterize desirable properties involving values in individual executions). The rules are designed to support a reasoning approach in which the majority of the reasoning effort uses the original semantics. This effort is then reused to establish the desired properties of the program under the relaxed semantics. 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-23T08:54:48Z |
| id | mit-1721.1/67031 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T08:54:48Z |
| publishDate | 2011 |
| record_format | dspace |
| spelling | mit-1721.1/670312019-04-10T15:31:51Z Reasoning about Relaxed Programs Carbin, Michael Kim, Deokhwan Misailovic, Sasa Rinard, Martin C. Martin Rinard Computer Architecture A number of approximate program transformations have recently emerged that enable transformed programs to trade accuracy of their results for increased performance by dynamically and nondeterministically modifying variables that control program execution. We call such transformed programs relaxed programs -- they have been extended with additional nondeterminism to relax their semantics and offer greater execution flexibility. We present programming language constructs for developing relaxed programs and proof rules for reasoning about properties of relaxed programs. Our proof rules enable programmers to directly specify and verify acceptability properties that characterize the desired correctness relationships between the values of variables in a program's original semantics (before transformation) and its relaxed semantics. Our proof rules also support the verification of safety properties (which characterize desirable properties involving values in individual executions). The rules are designed to support a reasoning approach in which the majority of the reasoning effort uses the original semantics. This effort is then reused to establish the desired properties of the program under the relaxed semantics. 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. 2011-11-15T18:15:04Z 2011-11-15T18:15:04Z 2011-11-15 http://hdl.handle.net/1721.1/67031 MIT-CSAIL-TR-2011-050 11 p. application/pdf application/octet-stream |
| spellingShingle | Carbin, Michael Kim, Deokhwan Misailovic, Sasa Rinard, Martin C. Reasoning about Relaxed Programs |
| title | Reasoning about Relaxed Programs |
| title_full | Reasoning about Relaxed Programs |
| title_fullStr | Reasoning about Relaxed Programs |
| title_full_unstemmed | Reasoning about Relaxed Programs |
| title_short | Reasoning about Relaxed Programs |
| title_sort | reasoning about relaxed programs |
| url | http://hdl.handle.net/1721.1/67031 |
| work_keys_str_mv | AT carbinmichael reasoningaboutrelaxedprograms AT kimdeokhwan reasoningaboutrelaxedprograms AT misailovicsasa reasoningaboutrelaxedprograms AT rinardmartinc reasoningaboutrelaxedprograms |