Skip to main content
SpringerLink
Log in

Diamont: Dynamic Monitoring of Uncertainty for Distributed Asynchronous Programs

  • Conference paper
  • First Online:
Runtime Verification (RV 2021)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 12974))

Included in the following conference series:

  • 733 Accesses

Abstract

Many application domains including graph analytics, the Internet-of-Things, precision agriculture, and media processing operate on noisy data and/or produce approximate results. These applications can distribute computation across multiple (often resource-constrained) processing units. Analyzing the reliability and accuracy of such applications is challenging, since most existing techniques operate on specific fixed error models, check for individual properties, or can only be applied to sequential programs.

We present Diamont, a system for dynamic monitoring of uncertainty properties in distributed programs. Diamont programs consist of distributed processes that communicate via asynchronous message passing. Diamont includes datatypes that dynamically monitor uncertainty in data and provides support for checking predicates over the monitored uncertainty at runtime. We also present a general methodology for verifying the soundness of the runtime system and optimizations using canonical sequentialization.

We implemented Diamont for a subset of the Go language and evaluated eight programs from precision agriculture, graph analytics, and media processing. We show that Diamont can prove important end-to-end properties on the program outputs for significantly larger inputs compared to prior work, with modest execution time overhead: 3% on average and 16.3% at maximum.

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 64.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 84.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

Notes

  1. 1.

    \(++\) denotes adding a element to the end of the message queue.

  2. 2.

    Many popular parallel application patterns (e.g. Map, Reduce, Scatter-Gather, Stencil) exhibit symmetric non-determinism [3, 19]. Further, programs satisfying this property can be less error-prone  [3].

References

  1. Achour, S., Rinard, M.: Energy efficient approximate computation with Topaz. In: OOPSLA (2015)

    Google Scholar 

  2. Ahmad, M., Hijaz, F., Shi, Q., Khan, O.: CRONO: a benchmark suite for multithreaded graph algorithms executing on futuristic multicores. In: IISWC (2015)

    Google Scholar 

  3. Bakst, A., Gleissenthall, K.v., Kici, R.G., Jhala, R.: Verifying distributed programs via canonical sequentialization. In: OOPSLA (2017)

    Google Scholar 

  4. Bornholt, J., Mytkowicz, T., McKinley, K.S.: Uncertain \(<\)T\(>\): a first-order type for uncertain data. In: ASPLOS (2014)

    Google Scholar 

  5. Boston, B., Gong, Z., Carbin, M.: Leto: verifying application-specific hardware fault tolerance with programmable execution models. In: OOPSLA (2018)

    Google Scholar 

  6. Boston, B., Sampson, A., Grossman, D., Ceze, L.: Probability type inference for flexible approximate programming. In: OOPSLA (2015)

    Google Scholar 

  7. Boyapati, R., Huang, J., Majumder, P., Yum, K.H., Kim, E.J.: APPROX-NoC: a data approximation framework for network-on-chip architectures. In: ISCA (2017)

    Google Scholar 

  8. Carbin, M., Kim, D., Misailovic, S., Rinard, M.: Proving acceptability properties of relaxed nondeterministic approximate programs. PLDI 47, 169–180 (2012)

    Google Scholar 

  9. Carbin, M., Kim, D., Misailovic, S., Rinard, M.: Verified integrity properties for safe approximate program transformations. In: PEPM (2013)

    Google Scholar 

  10. Carbin, M., Misailovic, S., Rinard, M.: Verifying quantitative reliability for programs that execute on unreliable hardware. In: OOPSLA (2013)

    Google Scholar 

  11. Chen, Y., Louri, A.: An approximate communication framework for network-on-chips. IEEE Trans. Parallel Distrib. Syst. 31, 1434–1446 (2020)

    Article  Google Scholar 

  12. Darulova, E., Izycheva, A., Nasir, F., Ritter, F., Becker, H., Bastian, R.: Daisy-framework for analysis and optimization of numerical programs. In: TACAS (2018)

    Google Scholar 

  13. Darulova, E., Kuncak, V.: Trustworthy numerical computation in Scala. In: OOPSLA (2011)

    Google Scholar 

  14. Darulova, E., Kuncak, V.: Certifying solutions for numerical constraints. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 277–291. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35632-2_27

    Chapter  Google Scholar 

  15. de Kruijf, M., Nomura, S., Sankaralingam, K.: Relax: an architectural framework for software recovery of hardware faults. ISCA 38, 497–508 (2010)

    Google Scholar 

  16. Dean, J., Ghemawat, S.: MapReduce: simplified data processing on large clusters. OSDI (2004)

    Google Scholar 

  17. Fernando, V., Franques, A., Abadal, S., Misailovic, S., Torrellas, J.: Replica: a wireless manycore for communication-intensive and approximate data. In: ASPLOS (2019)

    Google Scholar 

  18. Fernando, V., Joshi, K., Laurel, J., Misailovic, S.: Appendix to Diamont (2021). https://vimuth.github.io/diamont/appendix.pdf

  19. Fernando, V., Joshi, K., Misailovic, S.: Verifying safety and accuracy of approximate parallel programs via canonical sequentialization. In: OOPSLA (2019)

    Google Scholar 

  20. Golubovic, N., Krintz, C., Wolski, R., Sethuramasamyraja, B., Liu, B.: A scalable system for executing and scoring K-means clustering techniques and its impact on applications in agriculture. Int. J. Big Data Intell. 6, 163–175 (2019)

    Google Scholar 

  21. Joshi, K., Fernando, V., Misailovic, S.: Statistical algorithmic profiling for randomized approximate programs. In: ICSE (2019)

    Google Scholar 

  22. Joshi, K., Fernando, V., Misailovic, S.: Aloe: verifying reliability of approximate programs in the presence of recovery mechanisms. In: CGO (2020)

    Google Scholar 

  23. Lahiri, S., Haran, A., He, S., Rakamaric, Z.: Automated differential program verification for approximate computing. Technical report (2015)

    Google Scholar 

  24. Liu, T.: Datasheet for AM2302 Sensor (2020). https://cdn-shop.adafruit.com/datasheets/Digital+humidity+and+temperature+sensor+AM2302.pdf

  25. Maderbacher, B., Karl, A.F., Bloem, R.: Placement of runtime checks to counteract fault injections. In: Deshmukh, J., Ničković, D. (eds.) RV 2020. LNCS, vol. 12399, pp. 241–258. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-60508-7_13

    Chapter  Google Scholar 

  26. Misailovic, S., Carbin, M., Achour, S., Qi, Z., Rinard, M.: Chisel: reliability- and accuracy-aware optimization of approximate computational kernels. In: OOPSLA (2014)

    Google Scholar 

  27. Page, L., Brin, S., Motwani, R., Winograd, T.: The PageRank citation ranking: bringing order to the web. Technical report (1999)

    Google Scholar 

  28. Panchekha, P., Sanchez-Stern, A., Wilcox, J.R., Tatlock, Z.: Automatically improving accuracy for floating point expressions. In: PLDI (2015)

    Google Scholar 

  29. Paradis, L., Han, Q.: A survey of fault management in wireless sensor networks. J. Netw. Syst. Manag. 15, 171–190 (2007). https://doi.org/10.1007/s10922-007-9062-0

    Article  Google Scholar 

  30. Ranjan, A., Venkataramani, S., Fong, X., Roy, K., Raghunathan, A.: Approximate storage for energy efficient spintronic memories. In: DAC 2015 (2015)

    Google Scholar 

  31. Recht, B., Re, C., Wright, S., Niu, F.: HOGWILD: a lock-free approach to parallelizing stochastic gradient descent. In: Advances in Neural Information Processing Systems (2011)

    Google Scholar 

  32. Ringenburg, M., Sampson, A., Ackerman, I., Ceze, L., Grossman, D.: Monitoring and debugging the quality of results in approximate programs. In: ASPLOS (2015)

    Google Scholar 

  33. Rubio-González, C., et al.: Precimonious: tuning assistant for floating-point precision. In: SC (2013)

    Google Scholar 

  34. Samadi, M., Jamshidi, D.A., Lee, J., Mahlke, S.: Paraprox: pattern-based approximation for data parallel applications. In: ASPLOS (2014)

    Google Scholar 

  35. Sampson, A., et al.: Accept: a programmer-guided compiler framework for practical approximate computing. Technical report (2015)

    Google Scholar 

  36. Sampson, A., Panchekha, P., Mytkowicz, T., McKinley, K., Grossman, D., Ceze, L.: Expressing and verifying probabilistic assertions. In: PLDI (2014)

    Google Scholar 

  37. 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 

  38. Sanchez-Stern, A., Panchekha, P., Lerner, S., Tatlock, Z.: Finding root causes of floating point error. In: PLDI (2018)

    Google Scholar 

  39. Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202–215. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27813-9_16

    Chapter  Google Scholar 

  40. Sidiroglou, S., Misailovic, S., Hoffmann, H., Rinard, M.: Managing performance vs. accuracy trade-offs with loop perforation. In: FSE (2011)

    Google Scholar 

  41. Stanley-Marbell, P., et al.: Exploiting errors for efficiency: a survey from circuits to applications. ACM Comput. Surv. J. 53, 1–39 (2020)

    Article  Google Scholar 

  42. Stevens, J.R., Ranjan, A., Raghunathan, A.: AxBA: an approximate bus architecture framework. In: ICCAD (2018)

    Google Scholar 

  43. TensorFlow Developers: Tensorflow (2021). https://doi.org/10.5281/zenodo.5159865. https://www.tensorflow.org

  44. Yazdanbakhsh, A., Mahajan, D., Esmaeilzadeh, H., Lotfi-Kamran, P.: AxBench: a multiplatform benchmark suite for approximate computing. IEEE Design Test 34(2), 60–68 (2017)

    Article  Google Scholar 

  45. Zhuang, W., Chen, X., Tan, J., Song, A.: An empirical analysis for evaluating the link quality of robotic sensor networks. In: WCSP (2009)

    Google Scholar 

Download references

Acknowledgements

We thank the anonymous reviewers for their useful suggestions. The research presented in this paper was supported in part by NSF Grants No. CCF-1846354, CCF-1956374, CCF-2028861, and CCF-2008883, USDA Grant No. NIFA-2024827, and a gift from Facebook.

Author information

Authors and Affiliations

  1. University of Illinois Urbana-Champaign, Urbana, USA

    Vimuth Fernando, Keyur Joshi, Jacob Laurel & Sasa Misailovic

Authors
  1. Vimuth Fernando
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Keyur Joshi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jacob Laurel
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Sasa Misailovic
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Vimuth Fernando .

Editor information

Editors and Affiliations

  1. University of Virginia, Charlottesville, VA, USA

    Lu Feng

  2. Ben-Gurion University of the Negev, Be'er Sheva, Israel

    Dana Fisman

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Fernando, V., Joshi, K., Laurel, J., Misailovic, S. (2021). Diamont: Dynamic Monitoring of Uncertainty for Distributed Asynchronous Programs. In: Feng, L., Fisman, D. (eds) Runtime Verification. RV 2021. Lecture Notes in Computer Science(), vol 12974. Springer, Cham. https://doi.org/10.1007/978-3-030-88494-9_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-88494-9_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-88493-2

  • Online ISBN: 978-3-030-88494-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation