Skip to main content
SpringerLink
Log in
Book cover

International Conference on Computational Science and Its Applications

ICCSA 2016: Computational Science and Its Applications – ICCSA 2016 pp 410–421Cite as

Finding Divergent Executions in Asynchronous Programs

  • Conference paper
  • First Online:

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

Abstract

Developing interactive and distributive softwares is a complicated task for many reasons including the nature of this technique of programming; asynchronous programming. In this style of programming, there is no synchronization between running processes concerning message-posting communications. Therefore the presence of nonterminating executions for asynchronous programs, as a result of simple programming errors, is common.

This paper presents a transformation technique for asynchronous programs to discover their nonterminating (divergent) executions. The proposed technique converts a given asynchronous program P into another form \(P^{\prime }\) such that the nontermination problem of P is equivalent to the state reachability problem of \(P^\prime \). The paper presents the syntax and semantics of source and target languages of the transformation method. Then the transformation is presented using the formal syntax and semantics. The paper also formalizes the relationship between asynchronous programs and their transformations.

This is a preview of subscription content, 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

Learn about institutional subscriptions

References

  1. Arieli, O., Avron, A.: Reasoning with logical bilattices. J. Log. Lang. Inf. 5(1), 25–63 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  2. Atig, M.F., Bouajjani, A., Narayan Kumar, K., Saivasan, P.: Linear-time model-checking for multithreaded programs under scope-bounding. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 152–166. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  3. Atig, M.F., Bouajjani, A., Touili, T.: Analyzing asynchronous programs with preemption. In: LIPIcs-Leibniz International Proceedings in Informatics, vol. 2. Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2008)

    Google Scholar 

  4. Backes, M., Pfitzmann, B., Waidner, M.: The reactive simulatability (RSIM) framework for asynchronous systems. Inf. Comput. 205(12), 1685–1720 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  5. Benveniste, A., Berry, G.: The synchronous approach to reactive and real-time systems. Proc. IEEE 79(9), 1270–1282 (1991)

    Article  Google Scholar 

  6. Berry, G., Gonthier, G.: The esterel synchronous programming language: design, semantics, implementation. Sci. Comput. Program. 19(2), 87–152 (1992)

    Article  MATH  Google Scholar 

  7. Birkhoff, G., Birkhoff, G., Birkhoff, G., Birkhoff, G.: Lattice theory. Am. Math. Soc. 25 (1948). New York

    Google Scholar 

  8. Bouajjani, A., Emmi, M.: Bounded phase analysis of message-passing programs. Int. J. Softw. Tools Technol. Transf. 16(2), 127–146 (2014)

    Article  MATH  Google Scholar 

  9. Strüber, D., Rubin, J., Arendt, T., Chechik, M., Taentzer, G., Plöger, J.: RuleMerger: automatic construction of variability-based model transformation rules. In: Stevens, P., et al. (eds.) FASE 2016. LNCS, vol. 9633, pp. 122–140. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49665-7_8

    Chapter  Google Scholar 

  10. Cristian, F.: Reaching agreement on processor-group membrship in synchronous distributed systems. Distrib. Comput. 4(4), 175–187 (1991)

    Article  MATH  Google Scholar 

  11. Czaplicki, E., Chong, S.: Asynchronous functional reactive programming for GUIs. In: ACM SIGPLAN Notices, vol. 48, pp. 411–422. ACM (2013)

    Google Scholar 

  12. Dakshinamurthy, S., Narayanan, V.K.: A component-based approach to verification of formal software models to check safety properties of distributed systems. Lect. Notes Softw. Eng. 1(2), 186 (2013)

    Article  Google Scholar 

  13. Deligiannis, P., Donaldson, A.F., Ketema, J., Lal, A., Thomson, P.: Asynchronous programming, analysis and testing with state machines. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 154–164. ACM (2015)

    Google Scholar 

  14. Desai, A., Garg, P., Madhusudan, P.: Natural proofs for asynchronous programs using almost-synchronous reductions. In: ACM SIGPLAN Notices, vol. 49, pp. 709–725. ACM (2014)

    Google Scholar 

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

  16. El-Zawawy, M.A.: A robust framework for asynchronous operations on a functional object-oriented model. In: 2015 International Conference on Cloud Computing (ICCC), pp. 1–6. IEEE (2015)

    Google Scholar 

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

  18. Emmi, M., Ganty, P., Majumdar, R., Rosa-Velardo, F.: Analysis of asynchronous programs with event-based synchronization. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 535–559. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  19. 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)

    Chapter  Google Scholar 

  20. Fitting, M.: Bilattices and the semantics of logic programming. J. Log. Program. 11(2), 91–116 (1991)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  Google Scholar 

  22. Ganty, P., Majumdar, R., Rybalchenko, A.: Verifying liveness for asynchronous programs. In: ACM SIGPLAN Notices, vol. 44, pp. 102–113. ACM (2009)

    Google Scholar 

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

    Google Scholar 

  24. Jung, A., Rivieccio, U.: Kripke semantics for modal bilattice logic. In: 2013 28th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS), pp. 438–447. IEEE (2013)

    Google Scholar 

  25. Kelley, J.L.: General Topology. Springer Science & Business Media, New York (1975)

    MATH  Google Scholar 

  26. Kopetz, H.: Real-Time Systems: Design Principles for Distributed Embedded Applications. Springer Science & Business Media, New York (2011)

    Book  MATH  Google Scholar 

  27. Liskov, B., Shrira, L.: Promises: linguistic support for efficient asynchronous procedure calls in distributed systems. In: ACM Proceedings, vol. 23 (1988)

    Google Scholar 

  28. Pfitzmann, B., Waidner, M.: A model for asynchronous reactive systems and its application to secure message transmission. In: Proceedings of 2001 IEEE Symposium on Security and Privacy S&P 2001, pp. 184–200. IEEE (2001)

    Google Scholar 

  29. Stone, M.H.: Applications of the theory of Boolean rings to general topology. Trans. Am. Math. Soc. 41(3), 375–481 (1937)

    Article  MathSciNet  MATH  Google Scholar 

  30. Wilson, R.P., Lam, M.S.: Efficient context-sensitive pointer analysis for C programs. In: ACM Proceedings, vol. 30 (1995)

    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 Minho, Braga, Portugal

    Ana Maria A.C. Rocha

  5. Polytechnic University, Bari, Italy

    Carmelo M. Torre

  6. Monash University, Clayton, Victoria, Australia

    David Taniar

  7. Kyushu Sangyo University, Fukuoka, Japan

    Bernady O. Apduhan

  8. Saint Petersburg State University, Saint Petersburg, Russia

    Elena Stankova

  9. Beijing University of Posts and Telecommunications, Beijing, China

    Shangguang Wang

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

El-Zawawy, M.A. (2016). Finding Divergent Executions in Asynchronous Programs. In: Gervasi, O., et al. Computational Science and Its Applications – ICCSA 2016. ICCSA 2016. Lecture Notes in Computer Science(), vol 9790. Springer, Cham. https://doi.org/10.1007/978-3-319-42092-9_32

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-42092-9_32

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-42091-2

  • Online ISBN: 978-3-319-42092-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation