Advertisement

Verifying Relative Safety, Accuracy, and Termination for Program Approximations

  • Shaobo HeEmail author
  • Shuvendu K. Lahiri
  • Zvonimir Rakamarić
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9690)

Abstract

Approximate computing is an emerging area for trading off the accuracy of an application for improved performance, lower energy costs, and tolerance to unreliable hardware. However, developers must ensure that the leveraged approximations do not introduce significant, intolerable divergence from the reference implementation, as specified by several established robustness criteria. In this work, we show the application of automated differential verification towards verifying relative safety, accuracy, and termination criteria for a class of program approximations. We use mutual summaries to express relative specifications for approximations, and SMT-based invariant inference to automate the verification of such specifications. We perform a detailed feasibility study showing promise of applying automated verification to the domain of approximate computing in a cost-effective manner.

Keywords

Basic Block Satisfiability Modulo Theory Product Program Product Construction Control Flow Graph 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Notes

Acknowledgments

We thank Adrian Sampson for his feedback and for helping out with benchmark selection, and Akash Lal for helping out with Houdini. This work was supported in part by NSF award CCF 1255776 and SRC contract 2013-TJ-2426.

References

  1. 1.
    Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., M. Leino, K.R.: Boogie: a modular reusable verifier for object-oriented programs. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  2. 2.
    Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability (2009)Google Scholar
  3. 3.
    Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: POPL (2004)Google Scholar
  4. 4.
    Boston, B., Sampson, A., Grossman, D., Ceze, L.: Probability type inference for flexible approximate programming. In: OOPSLA (2015)Google Scholar
  5. 5.
    Carbin, M., Kim, D., Misailovic, S., Rinard, M.C.: Proving acceptability properties of relaxed nondeterministic approximate programs. In: PLDI (2012)Google Scholar
  6. 6.
    Carbin, M., Misailovic, S., Rinard, M.C.: Verifying quantitative reliability for programs that execute on unreliable hardware. In: OOPSLA (2013)Google Scholar
  7. 7.
    The Coq proof assistant. http://coq.inria.fr
  8. 8.
    Elenbogen, D., Katz, S., Strichman, O.: Proving mutual termination. FMSD 47(2), 204–229 (2015)zbMATHGoogle Scholar
  9. 9.
    Felsing, D., Grebing, S., Klebanov, V., Rümmer, P., Ulbrich, M.: Automating regression verification. In: ASE (2014)Google Scholar
  10. 10.
    Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, p. 500. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  11. 11.
    Godlin, B., Strichman, O.: Regression verification. In: DAC (2009)Google Scholar
  12. 12.
    Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  13. 13.
    Hawblitzel, C., Kawaguchi, M., Lahiri, S.K., Rebêlo, H.: Towards modularly comparing programs using automated theorem provers. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 282–299. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  14. 14.
    He, S., Lahiri, S.K., Rakamarić, Z.: Verifying relative safety, accuracy, and termination for program approximations. Tech. rep., Microsoft Research (2016)Google Scholar
  15. 15.
    Kugler, L.: Is “good enough” computing good enough? Commun. ACM 58(5), 12–14 (2015)CrossRefGoogle Scholar
  16. 16.
    Lahiri, S.K., Bryant, R.E.: Predicate abstraction with indexed predicates. ACM Trans. Comput. Log. 9(1) (2007)Google Scholar
  17. 17.
    Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Rebêlo, H.: SYMDIFF: a language-agnostic semantic diff tool for imperative programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 712–717. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  18. 18.
    Lahiri, S.K., McMillan, K.L., Sharma, R., Hawblitzel, C.: Differential assertion checking. In: ESEC/FSE (2013)Google Scholar
  19. 19.
    McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 16–30. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  20. 20.
    McMillan, K.L.: Lazy annotation revisited. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 243–259. Springer, Heidelberg (2014)Google Scholar
  21. 21.
    Misailovic, S., Carbin, M., Achour, S., Qi, Z., Rinard, M.C.: Chisel: Reliability- and accuracy-aware optimization of approximate computational kernels. SIGPLAN Not. 49, 309–328 (2014)CrossRefGoogle Scholar
  22. 22.
    Misailovic, S., Sidiroglou, S., Hoffmann, H., Rinard, M.: Quality of service profiling. In: ICSE (2010)Google Scholar
  23. 23.
    Necula, G.C.: Translation validation for an optimizing compiler. In: PLDI (2000)Google Scholar
  24. 24.
    Nelson, J., Sampson, A., Ceze, L.: Dense approximate storage in phase-change memory. In: Ideas and Perspectives session at ASPLOS (2001)Google Scholar
  25. 25.
    Park, J., Esmaeilzadeh, H., Zhang, X., Naik, M., Harris, W.: FlexJava: language support for safe and modular approximate programming. In: ESEC/FSE (2015)Google Scholar
  26. 26.
    Park, J., Ni, K., Zhang, X., Esmaeilzadeh, H., Naik, M.: Expectation-oriented framework for automating approximate programming. In: WACAS (2014)Google Scholar
  27. 27.
    Pnueli, A., Siegel, M.D., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 151–166. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  28. 28.
    Rinard, M.: Acceptability-oriented computing. In: OOPSLA (2003)Google Scholar
  29. 29.
    Ringenburg, M.F., Sampson, A., Ackerman, I., Ceze, L., Grossman, D.: Dynamic analysis of approximate program quality. Tech. Rep. UW-CSE-14-03-01, University of WashingtonGoogle Scholar
  30. 30.
    Ringenburg, M.F., Sampson, A., Ceze, L., Grossman, D.: Profiling and autotuning for energy-aware approximate programming. In: WACAS (2014)Google Scholar
  31. 31.
    Roy, P., Ray, R., Wang, C., Wong, W.F.: ASAC: Automatic sensitivity analysis for approximate computing. In: LCTES (2014)Google Scholar
  32. 32.
    Sampson, A.: Hardware and Software for Approximate Computing. Ph.D. thesis (2015)Google Scholar
  33. 33.
    Sampson, A., Baixo, A., Ransford, B., Moreau, T., Yip, J., Ceze, L., Oskin, M.: ACCEPT: a programmer-guided compiler framework for practical approximate computing. Tech. Rep. UW-CSE-15-01-01, University of WashingtonGoogle Scholar
  34. 34.
    Sampson, A., Bornholt, J., Ceze, L.: Hardware-software co-design: not just a cliché. In: SNAPL (2015)Google Scholar
  35. 35.
    Sampson, A., Dietl, W., Fortuna, E., Gnanapragasam, D., Ceze, L., Grossman, D.: EnerJ: approximate data types for safe and general low-power computation. In: PLDI (2011)Google Scholar
  36. 36.
    Sharma, V.C., Haran, A., Rakamarić, Z., Gopalakrishnan, G.: Towards formal approaches to system resilience. In: PRDC (2013)Google Scholar
  37. 37.
    Thomas, A., Pattabiraman, K.: LLFI: an intermediate code level fault injector for soft computing applications. In: SELSE (2013)Google Scholar
  38. 38.
    Vanegue, J., Lahiri, S.K.: Towards practical reactive security audit using extended static checkers. In: S&P (2013)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • Shaobo He
    • 1
    Email author
  • Shuvendu K. Lahiri
    • 2
  • Zvonimir Rakamarić
    • 1
  1. 1.University of UtahSalt Lake CityUSA
  2. 2.Microsoft ResearchRedmondUSA

Personalised recommendations