Skip to main content
SpringerLink
Log in

Posting Graphs for Finding Non-Terminating Executions in Asynchronous Programs

  • Conference paper
  • First Online:
Computational Science and Its Applications – ICCSA 2017 (ICCSA 2017)

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

Included in the following conference series:

  • 2327 Accesses

Abstract

Asynchronous programming is one of the currently dominant programming techniques. The key idea of asynchronous programming is to use a queue to post computations as tasks (events). This queue is used then by the application to pick events asynchronously for processing. Asynchronous programming was found very convenient for achieving a massive percentage of software systems used today such as Gmail and Facebook which are Web 2.0 JavaScript ones.

This paper presents a novel technique for searching for nonterminating executions in asynchronous programming. The targeted cases of nontermination are those caused by the posting concept. The proposed technique is based on graphical representation for posting behaviours of asynchronous programs. Proofs for termination and correctness of the proposed method is outlined in the paper.

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 EPUB and 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

References

  1. Abe, T., Maeda, T.: Concurrent program logic for relaxed memory consistency models with dependencies across loop iterations. J. Inf. Process. 25, 244–255 (2017)

    Google Scholar 

  2. Andrews, G.R.: Concurrent Programming: Principles and Practice. Benjamin/Cummings Publishing Company, San Francisco (1991)

    MATH  Google Scholar 

  3. Brotherston, J., Bornat, R., Calcagno C.: Cyclic proofs of program termination in separation logic. In: ACM SIGPLAN Notices, vol. 43, pp. 101–112. ACM (2008)

    Google Scholar 

  4. Cantelon, M., Harter, M., Holowaychuk, T.J., Rajlich, N.: Node. js in Action. Manning, Greenwich (2014)

    Google Scholar 

  5. Chadha, G., Mahlke, S., Narayanasamy, S.: Accelerating asynchronous programs through event sneak peek. ACM SIGARCH Comput. Archit. News 43(3), 642–654 (2016)

    Article  Google Scholar 

  6. Colón, M.A., Sipma, H.B.: Practical methods for proving program termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 442–454. Springer, Heidelberg (2002). doi:10.1007/3-540-45657-0_36

    Chapter  Google Scholar 

  7. Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: ACM SIGPLAN Notices, vol. 41, pp. 415–426. ACM (2006)

    Google Scholar 

  8. Cook, B., Podelski, A., Rybalchenko, A.: Proving program termination. Commun. ACM 54(5), 88–98 (2011)

    Article  Google Scholar 

  9. Cousot, P.: Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 1–24. Springer, Heidelberg (2005). doi:10.1007/978-3-540-30579-8_1

    Chapter  Google Scholar 

  10. Cristian, F.: Synchronous and asynchronous. Commun. ACM 39(4), 88–97 (1996)

    Article  Google Scholar 

  11. El-Zawawy, M.A.: Detection of probabilistic dangling references in multi-core programs using proof-supported tools. In: Murgante, B., et al. (eds.) ICCSA 2013. LNCS, vol. 7975, pp. 516–530. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39640-3_38

    Google Scholar 

  12. El-Zawawy, M.A.: An efficient layer-aware technique for developing asynchronous context-oriented software (acos). In: 2015 15th International Conference on Computational Science and Its Applications (ICCSA), pp. 14–20. IEEE (2015)

    Google Scholar 

  13. ElZawawy, M.A.: Finding divergent executions in asynchronous programs. In: Gervasi, O., et al. (eds.) International Conference on Computational Science and Its Applications. LNCS, vol. 9790, pp. 410–421. Springer, Heidelberg (2016). doi:10.1007/978-3-319-42092-9_32

    Google Scholar 

  14. El-Zawawy, M.A., Alanazi, M.N.: An efficient binary technique for trace simplifications of concurrent programs. In: 2014 IEEE 6th International Conference on Adaptive Science & Technology (ICAST), pp. 1–8. IEEE (2014)

    Google Scholar 

  15. Emmi, M., Lal, A.: Finding non-terminating executions in distributed asynchronous programs. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 439–455. Springer, Heidelberg (2012). doi:10.1007/978-3-642-33125-1_29

    Chapter  Google Scholar 

  16. Ganty, P., Majumdar, R.: Algorithmic verification of asynchronous programs. ACM Trans. Program. Lang. Syst. (TOPLAS) 34(1), 6 (2012)

    Article  Google Scholar 

  17. Jhala, R., Majumdar, R.: Interprocedural analysis of asynchronous programs. In: ACM SIGPLAN Notices, vol. 42, pp. 339–350. ACM (2007)

    Google Scholar 

  18. Lucia, B., Ceze, L.: Cooperative empirical failure avoidance for multithreaded programs. In: ACM SIGPLAN Notices, vol. 48, pp. 39–50. ACM (2013)

    Google Scholar 

  19. Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: ACM SIGPLAN Notices, vol. 42, pp. 446–455. ACM (2007)

    Google Scholar 

  20. Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing Heisenbugs in concurrent programs. In: OSDI, vol. 8, pp. 267–280 (2008)

    Google Scholar 

  21. Ousterhout, J.: Why threads are a bad idea (for most purposes). In: Presentation Given at the 1996 Usenix Annual Technical Conference, vol. 5, San Diego, CA, USA (1996)

    Google Scholar 

  22. Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Ausiello, G., Dezani-Ciancaglini, M., Della Rocca, S.R. (eds.) ICALP 1989. LNCS, vol. 372, pp. 652–671. Springer, Heidelberg (1989). doi:10.1007/BFb0035790

    Chapter  Google Scholar 

  23. Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: Proceedings of 13th IEEE Computer Security Foundations Workshop, CSFW-13, pp. 200–214. IEEE (2000)

    Google Scholar 

  24. Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: a dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst. (TOCS) 15(4), 391–411 (1997)

    Article  Google Scholar 

  25. Sui, Y., Di, P., Xue, J.: Sparse flow-sensitive pointer analysis for multithreaded programs. In: 2016 IEEE/ACM International Symposium on Code Generation and Optimization (CGO), pp. 160–170. IEEE (2016)

    Google Scholar 

  26. Syme, D., Petricek, T., Lomov, D.: The f# asynchronous programming model. In: Rocha, R., Launchbury, J. (eds.) PADL 2011. LNCS, vol. 6539, pp. 175–189. Springer, Heidelberg (2011). doi:10.1007/978-3-642-18378-2_15

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. College of Computer and Information Sciences, Al Imam Mohammad Ibn Saud Islamic University (IMSIU), Riyadh, Kingdom of Saudi Arabia

    Mohamed A. El-Zawawy

  2. Department of Mathematics, Faculty of Science, Cairo University, Giza, 12613, Egypt

    Mohamed A. El-Zawawy

Authors
  1. Mohamed A. El-Zawawy
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mohamed A. El-Zawawy .

Editor information

Editors and Affiliations

  1. University of Perugia, Perugia, Italy

    Osvaldo Gervasi

  2. University of Basilicata, Potenza, Italy

    Beniamino Murgante

  3. Covenant University, Ota, Nigeria

    Sanjay Misra

  4. University of Trieste, Trieste, Italy

    Giuseppe Borruso

  5. Polytechnic University of Bari, Bari, Italy

    Carmelo M. Torre

  6. University of Minho, Braga, Portugal

    Ana Maria A.C. Rocha

  7. Monash University, Clayton, Victoria, Australia

    David Taniar

  8. Kyushu Sangyo University, Fukuoka, Japan

    Bernady O. Apduhan

  9. Saint Petersburg State University, Saint Petersburg, Russia

    Elena Stankova

  10. University of Trieste, Trieste, Italy

    Alfredo Cuzzocrea

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

El-Zawawy, M.A. (2017). Posting Graphs for Finding Non-Terminating Executions in Asynchronous Programs. In: Gervasi, O., et al. Computational Science and Its Applications – ICCSA 2017. ICCSA 2017. Lecture Notes in Computer Science(), vol 10409. Springer, Cham. https://doi.org/10.1007/978-3-319-62407-5_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-62407-5_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-62406-8

  • Online ISBN: 978-3-319-62407-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation