Proving acceptability properties of relaxed nondeterministic approximate programs

Michael Carbin, Deokhwan Kim, Sasa Misailovic, Martin C. Rinard

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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 to be acceptable. Our proof rules work with two kinds of acceptability properties: relational acceptability properties, 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 machinechecked verifications of their relaxed programs.

Original languageEnglish (US)
Title of host publicationPLDI'12 - Proceedings of the 2012 ACM SIGPLAN Conference on Programming Language Design and Implementation
Pages169-180
Number of pages12
DOIs
StatePublished - Jul 9 2012
Externally publishedYes
Event33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI'12 - Beijing, China
Duration: Jun 11 2012Jun 16 2012

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Other

Other33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI'12
CountryChina
CityBeijing
Period6/11/126/16/12

Fingerprint

Semantics
Knobs
Computer programming languages
Synchronization
Acoustic waves
Sampling

Keywords

  • Acceptability
  • Coq
  • Relational hoare logic
  • Relaxed programs

ASJC Scopus subject areas

  • Software

Cite this

Carbin, M., Kim, D., Misailovic, S., & Rinard, M. C. (2012). Proving acceptability properties of relaxed nondeterministic approximate programs. In PLDI'12 - Proceedings of the 2012 ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 169-180). (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)). https://doi.org/10.1145/2254064.2254086

Proving acceptability properties of relaxed nondeterministic approximate programs. / Carbin, Michael; Kim, Deokhwan; Misailovic, Sasa; Rinard, Martin C.

PLDI'12 - Proceedings of the 2012 ACM SIGPLAN Conference on Programming Language Design and Implementation. 2012. p. 169-180 (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Carbin, M, Kim, D, Misailovic, S & Rinard, MC 2012, Proving acceptability properties of relaxed nondeterministic approximate programs. in PLDI'12 - Proceedings of the 2012 ACM SIGPLAN Conference on Programming Language Design and Implementation. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 169-180, 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI'12, Beijing, China, 6/11/12. https://doi.org/10.1145/2254064.2254086
Carbin M, Kim D, Misailovic S, Rinard MC. Proving acceptability properties of relaxed nondeterministic approximate programs. In PLDI'12 - Proceedings of the 2012 ACM SIGPLAN Conference on Programming Language Design and Implementation. 2012. p. 169-180. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)). https://doi.org/10.1145/2254064.2254086
Carbin, Michael ; Kim, Deokhwan ; Misailovic, Sasa ; Rinard, Martin C. / Proving acceptability properties of relaxed nondeterministic approximate programs. PLDI'12 - Proceedings of the 2012 ACM SIGPLAN Conference on Programming Language Design and Implementation. 2012. pp. 169-180 (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).
@inproceedings{5f27f81ceea94048ab77b20c11b89000,
title = "Proving acceptability properties of relaxed nondeterministic approximate programs",
abstract = "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 to be acceptable. Our proof rules work with two kinds of acceptability properties: relational acceptability properties, 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 machinechecked verifications of their relaxed programs.",
keywords = "Acceptability, Coq, Relational hoare logic, Relaxed programs",
author = "Michael Carbin and Deokhwan Kim and Sasa Misailovic and Rinard, {Martin C.}",
year = "2012",
month = "7",
day = "9",
doi = "10.1145/2254064.2254086",
language = "English (US)",
isbn = "9781450312059",
series = "Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)",
pages = "169--180",
booktitle = "PLDI'12 - Proceedings of the 2012 ACM SIGPLAN Conference on Programming Language Design and Implementation",

}

TY - GEN

T1 - Proving acceptability properties of relaxed nondeterministic approximate programs

AU - Carbin, Michael

AU - Kim, Deokhwan

AU - Misailovic, Sasa

AU - Rinard, Martin C.

PY - 2012/7/9

Y1 - 2012/7/9

N2 - 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 to be acceptable. Our proof rules work with two kinds of acceptability properties: relational acceptability properties, 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 machinechecked verifications of their relaxed programs.

AB - 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 to be acceptable. Our proof rules work with two kinds of acceptability properties: relational acceptability properties, 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 machinechecked verifications of their relaxed programs.

KW - Acceptability

KW - Coq

KW - Relational hoare logic

KW - Relaxed programs

UR - http://www.scopus.com/inward/record.url?scp=84863438138&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84863438138&partnerID=8YFLogxK

U2 - 10.1145/2254064.2254086

DO - 10.1145/2254064.2254086

M3 - Conference contribution

AN - SCOPUS:84863438138

SN - 9781450312059

T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

SP - 169

EP - 180

BT - PLDI'12 - Proceedings of the 2012 ACM SIGPLAN Conference on Programming Language Design and Implementation

ER -