Skip to main content
SpringerLink
Log in

Automatic Verification of Intermittent Systems

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10747))

Abstract

Transiently powered devices have given rise to a new model of computation called intermittent computation. Intermittent programs keep checkpointing the program state to a persistent memory, and on power failures, the programs resume from the last executed checkpoint. An intermittent program is usually automatically generated by instrumenting a given continuous program (continuously powered). The behaviour of the continuous program should be equivalent to that of the intermittent program under all possible power failures.

This paper presents a technique to automatically verify the correctness of an intermittent program with respect to its continuous counterpart. We present a model of intermittence to capture all possible scenarios of power failures and an algorithm to automatically find a proof of equivalence between a continuous and an intermittent program.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Andronick, J.: Formally proved anti-tearing properties of embedded c code. In: Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (isola 2006), pp. 129–136 (2006)

    Google Scholar 

  2. Chen, H., Ziegler, D., Chajed, T., Chlipala, A., Kaashoek, M.F., Zeldovich, N.: Using crash hoare logic for certifying the fscq file system. In: Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, pp. 18–37. ACM, New York (2015). http://doi.acm.org/10.1145/2815400.2815402

  3. Churchill, B., Sharma, R., Bastien, J., Aiken, A.: Sound loop superoptimization for google native client. In: Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2017, pp. 313–326. ACM (2017)

    Google Scholar 

  4. Dahiya, M., Bansal, S.: Black-box equivalence checking across compiler optimizations. In: Chang, B.Y. (ed.) APLAS 2017. LNCS, vol. 10695, pp. 127–147. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-71237-6_7

    Chapter  Google Scholar 

  5. Dahiya, M., Bansal, S.: Modeling undefined behaviour semantics for checking equivalence across compiler optimizations. In: Strichman, O., Tzoref-Brill, R. (eds.) HVC 2017. LNCS, vol. 10629, pp. 19–34. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70389-3_2

    Chapter  Google Scholar 

  6. Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_49

    Google Scholar 

  7. Felsing, D., Grebing, S., Klebanov, V., Rümmer, P., Ulbrich, M.: Automating regression verification. In: Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering, ASE 2014, pp. 349–360. ACM, New York (2014)

    Google Scholar 

  8. 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, pp. 500–517. Springer, Berlin Heidelberg (2001). https://doi.org/10.1007/3-540-45251-6_29

    Chapter  Google Scholar 

  9. Kundu, S., Tatlock, Z., Lerner, S.: Proving optimizations correct using parameterized program equivalence. In: Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, pp. 327–337. ACM, New York (2009)

    Google Scholar 

  10. 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). https://doi.org/10.1007/978-3-642-31424-7_54

    Chapter  Google Scholar 

  11. Lahiri, S.K., Sinha, R., Hawblitzel, C.: Automatic Rootcausing for program equivalence failures in binaries. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 362–379. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_21

    Chapter  Google Scholar 

  12. Lerner, S., Millstein, T., Chambers, C.: Automatically proving the correctness of compiler optimizations. In: PLDI 2003 (2003)

    Google Scholar 

  13. Lerner, S., Millstein, T., Rice, E., Chambers, C.: Automated soundness proofs for dataflow analyses and transformations via local rules. In: Proceedings of the 32Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, pp. 364–377. ACM, New York (2005)

    Google Scholar 

  14. Lopes, N.P., Menendez, D., Nagarakatte, S., Regehr, J.: Provably correct peephole optimizations with alive. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, pp. 22–32. ACM, New York (2015)

    Google Scholar 

  15. Lucia, B., Ransford, B.: A simpler, safer programming and execution model for intermittent systems. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, pp. 575–585. ACM, New York (2015). http://doi.acm.org/10.1145/2737924.2737978

  16. Necula, G.C.: Translation validation for an optimizing compiler. In: Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation, PLDI 2000, pp. 83–94. ACM, New York (2000)

    Google Scholar 

  17. Olivo, J., Carrara, S., Micheli, G.D.: Energy harvesting and remote powering for implantable biosensors. IEEE Sensors Journal 11(7), 1573–1586 (2011)

    Article  Google Scholar 

  18. Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 151–166. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0054170

    Chapter  Google Scholar 

  19. Ransford, B., Sorber, J., Fu, K.: Mementos: system support for long-running computation on rfid-scale devices. In: Proceedings of the Sixteenth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS XVI, pp. 159–170. ACM, New York (2011)

    Google Scholar 

  20. Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press, New York (2011)

    Book  MATH  Google Scholar 

  21. Sharma, R., Schkufza, E., Churchill, B., Aiken, A.: Data-driven equivalence checking. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & #38; Applications, OOPSLA 2013, pp. 391–406. ACM, New York (2013)

    Google Scholar 

  22. Sigurbjarnarson, H., Bornholt, J., Torlak, E., Wang, X.: Push-button verification of file systems via crash refinement. In: Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation, OSDI 2016, pp. 1–16. USENIX Association, Berkeley (2016). http://dl.acm.org/citation.cfm?id=3026877.3026879

  23. Strichman, O., Godlin, B.: Regression verification - a practical way to verify programs. In: Meyer, B., Woodcock, J. (eds.) Verified Software: Theories, Tools, Experiments. LNCS, vol. 4171, pp. 496–501. Springer, Berlin Heidelberg (2008). https://doi.org/10.1007/978-3-540-69149-5_54

    Chapter  Google Scholar 

  24. Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: a new approach to optimization. In: POPL 2009: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 264–276. ACM, New York (2009)

    Google Scholar 

  25. Tristan, J.B., Govereau, P., Morrisett, G.: Evaluating value-graph translation validation for llvm. In: Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp. 295–305. ACM, New York (2011)

    Google Scholar 

  26. Van Der Woude, J., Hicks, M.: Intermittent computation without hardware support or programmer intervention. In: Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation, OSDI 2016, pp. 17–32. USENIX Association, Berkeley (2016)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Indian Institute of Technology Delhi, New Delhi, India

    Manjeet Dahiya & Sorav Bansal

Authors
  1. Manjeet Dahiya
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sorav Bansal
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Manjeet Dahiya .

Editor information

Editors and Affiliations

  1. University of Texas , Austin, Texas, USA

    Isil Dillig

  2. University of California , Los Angeles, California, USA

    Jens Palsberg

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Dahiya, M., Bansal, S. (2018). Automatic Verification of Intermittent Systems. In: Dillig, I., Palsberg, J. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2018. Lecture Notes in Computer Science(), vol 10747. Springer, Cham. https://doi.org/10.1007/978-3-319-73721-8_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-73721-8_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-73720-1

  • Online ISBN: 978-3-319-73721-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation