Skip to main content
SpringerLink
Log in

Operational Semantics for the Rigorous Analysis of Distributed Systems

  • Conference paper
  • First Online:
Quality Software Through Reuse and Integration (FMI 2016, IRI 2016 2016)

Part of the book series: Advances in Intelligent Systems and Computing ((AISC,volume 561))

Abstract

The development of distributed systems based on poorly specified abstractions can hinder unambiguous understanding and the creation of common formal analysis methods. In this paper, we outline the design of a system modeling language called DS2, and point out how its primitives are well matched with concerns that naturally arise during distributed system design. We present an operational semantics for DS2 as well as results from an ongoing Scala-based implementation slated to support a variety of state-space exploration techniques. The driving goals of this project are to: (1) provide a prototyping framework within which complex distributed system protocols can be stated and modeled without breaking the primitives down to low level ones, and (2) drive the development of interesting and distributed system-relevant property checking methods (e.g., linearizability).

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

    Domain-Specific/Declarative-Specification of Distributed Systems.

  2. 2.

    Our focus is towards networked, asynchronous, deterministic, and non-Byzantine distributed systems. However, the model is easily extensible to include Byzantine distributed systems, too.

  3. 3.

    e.g. a heart beat sending messages every certain time period.

  4. 4.

    For this base model being discussed in this work, all it has as a state is a queue and a local-state. Implementations, of course, can have more than that.

References

  1. Akka, February 2016. http://akka.io/

  2. Pony - High Performance Actor Programming, November 2016. http://www.ponylang.org/

  3. Agha, G.: Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge (1986)

    Google Scholar 

  4. Al-Mahfoudh, M., Gopalakrishnan, G., Stutsman, R.: Toward rigorous design of domain-specific distributed systems. In: Proceedings of the 4th FME Workshop on Formal Methods in Software Engineering, FormaliSE 2016, pp. 42–48. ACM, New York (2016)

    Google Scholar 

  5. Burckhardt, S.: Principles of eventual consistency. Found. Trends Program. Lang. 1(1–2), 1–150 (2014)

    Google Scholar 

  6. Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: a complete and automatic linearizability checker. SIGPLAN Not. 45(6), 330–340 (2010)

    Article  Google Scholar 

  7. Casanova, H.: SimGrid: a toolkit for the simulation of application scheduling. In: Proceedings First IEEE/ACM International Symposium on Cluster Computing and the Grid, pp. 430–437 (2001)

    Google Scholar 

  8. Clebsch, S., Pony: co-designing a type system and a runtime. SPLASH 2016. ACM, New York, November 2016. Appeared in SPLASH-I, Presentation

    Google Scholar 

  9. DS2 official website (2016). http://formalverification.cs.utah.edu/ds2. Accessed 31 Jan 2016

  10. Haller, P., Miller, H.: Distributed programming via safe closure passing. In: Gay, S., Alglave, J. (eds.) Proceedings Eighth International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES 2015, London, UK, 18 April 2015. EPTCS, vol. 203, pp. 99–107 (2015)

    Google Scholar 

  11. Haller, P., Odersky, M.: Event-based programming without inversion of control. In: Proceedings of the 7th Joint Conference on Modular Programming Languages, JMLC 2006, pp. 4–22. Springer, Heidelberg (2006)

    Google Scholar 

  12. Havelund, K., Pressburger, T.: Model checking java programs using java pathfinder. Int. J. Softw. Tools Technol. Transf. 2(4), 366–381 (2000)

    Article  MATH  Google Scholar 

  13. Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: IronFleet: proving practical distributed systems correct. In: Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, 4–7 October 2015, pp. 1–17 (2015)

    Google Scholar 

  14. Hewitt, C., Bishop, P., Steiger, R.: A universal modular actor formalism for artificial intelligence. In: Proceedings of the 3rd International Joint Conference on Artificial Intelligence, IJCAI 1973, pp. 235–245. Morgan Kaufmann Publishers Inc., San Francisco (1973)

    Google Scholar 

  15. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  16. Holzmann, G.J.: Logic verification of ANSI-C code with SPIN. In: SPIN. Lecture Notes in Computer Science, vol. 1885, pp. 131–147. Springer (2000)

    Google Scholar 

  17. Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 21:1–21:54 (2009)

    Article  Google Scholar 

  18. Junqueira, F.P., Reed, B.C., Serafini, M.: Zab: High-performance broadcast for primary-backup systems. In: 2011 IEEE/IFIP 41st International Conference on Dependable Systems Networks (DSN), pp. 245–256, June 2011

    Google Scholar 

  19. Kuraj, I., Jackson, D.: Exploring the role of sequential computation in distributed systems: motivating a programming paradigm shift. In: Proceedings of the 2016 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2016, pp. 145–164. ACM, New York (2016)

    Google Scholar 

  20. Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)

    Article  MATH  Google Scholar 

  21. Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst. 16(2), 133–169 (1998)

    Article  Google Scholar 

  22. Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co. Inc, Boston (2002)

    Google Scholar 

  23. Leesatapornwongsa, T., Hao, M., Joshi, P., Lukman, J.F., Gunawi, H.S.: SAMC: semantic-aware model checking for fast discovery of deep bugs in cloud systems. In: Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation, OSDI 2014, pp. 399–414. USENIX Association, Berkeley (2014)

    Google Scholar 

  24. McCaffrey, C.: The verification of a distributed system. ACM Queue 13(9), 60:150–60:160 (2015)

    Google Scholar 

  25. Ongaro, D., Ousterhout, J.: In search of an understandable consensus algorithm. In: Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conference, USENIX ATC 2014, pp. 305–320. USENIX Association, Berkeley (2014)

    Google Scholar 

  26. Stoica, I., Morris, R., Karger, D., Kaashoek, M.F., Balakrishnan, H.: Chord: a scalable peer-to-peer lookup service for internet applications. In: Proceedings of the 2001 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications, SIGCOMM 2001, pp. 149–160. ACM, New York (2001)

    Google Scholar 

  27. Strategy design pattern (2017). https://sourcemaking.com/design_patterns/strategy. Accessed 1 Jan 2017

  28. Tasharofi, S., Karmani, R.K., Lauterburg, S., Legay, A., Marinov, D., Agha, G.: TransDPOR: a novel dynamic partial-order reduction technique for testing actor programs. In: Proceedings of the 14th Joint IFIP WG 6.1 International Conference and Proceedings of the 32nd IFIP WG 6.1 International Conference on Formal Techniques for Distributed Systems, FMOODS 2012/FORTE 2012, pp. 219–234. Springer, Heidelberg (2012)

    Google Scholar 

  29. Wilcox, J.R., Woos, D., Panchekha, P., Tatlock, Z., Wang, X., Ernst, M.D., Anderson, T.: Verdi: a framework for implementing and formally verifying distributed systems. ACM SIGPLAN Not. 50(6), 357–368 (2015)

    Article  Google Scholar 

  30. Yang, J., Chen, T., Wu, M., Xu, Z., Liu, X., Lin, H., Yang, M., Long, F., Zhang, L., Zhou, L.: MODIST: transparent model checking of unmodified distributed systems. In: NSDI, pp. 213–228. USENIX Association (2009)

    Google Scholar 

  31. Zave, P.: How to make chord correct (using a stable base). Computing Research Repository (CoRR), abs/1502.06461 (2015)

    Google Scholar 

Download references

Acknowledgments

We acknowledge NSF grant CCF 7298529, and help by Heath French, Jarkko Savela, Zepeng Zhao, and Anushree Singh. This work is, also, supported in part by NSF Award CCF 1346756.

Author information

Authors and Affiliations

  1. School of Computing, University of Utah, Salt Lake City, UT, 84112, USA

    Mohammed S. Al-Mahfoudh, Ganesh Gopalakrishnan & Ryan Stutsman

Authors
  1. Mohammed S. Al-Mahfoudh
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ganesh Gopalakrishnan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ryan Stutsman
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mohammed S. Al-Mahfoudh .

Editor information

Editors and Affiliations

  1. SPAWAR Systems Center Pacific, San Diego, California, USA

    Stuart H. Rubin

  2. Laboratoire de Communication dans les Systèmes Informatiques, Ecole nationale Supérieure d’Informatique, Algiers, Algeria

    Thouraya Bouabana-Tebibel

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this paper

Cite this paper

Al-Mahfoudh, M.S., Gopalakrishnan, G., Stutsman, R. (2018). Operational Semantics for the Rigorous Analysis of Distributed Systems. In: Rubin, S., Bouabana-Tebibel, T. (eds) Quality Software Through Reuse and Integration. FMI IRI 2016 2016 2016. Advances in Intelligent Systems and Computing, vol 561. Springer, Cham. https://doi.org/10.1007/978-3-319-56157-8_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-56157-8_10

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation