Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Testing and Verifying Chain Repair Methods for Corfu Using Stateless Model Checking

  • Conference paper
  • First Online:
Integrated Formal Methods (IFM 2017)

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

Included in the following conference series:

Abstract

Corfu is a distributed shared log that is designed to be scalable and reliable in the presence of failures and asynchrony. Internally, Corfu is fully replicated for fault tolerance, without sharding data or sacrificing strong consistency. In this case study, we present the modeling approaches we followed to test and verify, using Concuerror, the correctness of repair methods for the Chain Replication protocol suitable for Corfu. In the first two methods we tried, Concuerror located bugs quite fast. In contrast, the tool did not manage to find bugs in the third method, but the time this took also motivated an improvement in the tool that reduces the number of traces explored. Besides more details about all the above, we present experiences and lessons learned from applying stateless model checking for verifying complex protocols suitable for distributed programming.

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

Notes

  1. 1.

    @slfritchie: “I was all ready to have a celebratory “New algorithm works!” tweet. Then the DPOR model execution w/Concuerror found an invalid case. Ouch.” (https://twitter.com/slfritchie/status/745863131407220737).

  2. 2.

    More information about Concuerror is at http://parapluu.github.io/Concuerror.

References

  1. Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pp. 373–384. ACM, New York (2014). doi:10.1145/2535838.2535845

  2. Armstrong, J.: Erlang. Commun. ACM 53(9), 68–75 (2010)

    Article  Google Scholar 

  3. Burckhardt, S., Kothari, P., Musuvathi, M., Nagarakatte, S.: A randomized scheduler with probabilistic guarantees of finding bugs. In: Proceedings of ASPLOS, ASPLOS XV, pp. 167–178. ACM, New York (2010). doi:10.1145/1736020.1736040

  4. Christakis, M., Gotovos, A., Sagonas, K.: Systematic testing for detecting concurrency errors in Erlang programs. In: Sixth IEEE International Conference on Software Testing, Verification and Validation (ICST 2013), pp. 154–163. IEEE Computer Society (2013)

    Google Scholar 

  5. Deligiannis, P., Donaldson, A.F., Ketema, J., Lal, A., Thomson, P.: Asynchronous programming, analysis and testing with state machines. In: Proceedings of the 36th PLDI, PLDI 2015, pp. 154–164 (2015). doi:10.1145/2737924.2737996

  6. Emmi, M., Qadeer, S., Rakamarić, Z.: Delay-bounded scheduling. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, pp. 411–422. ACM, New York (2011)

    Google Scholar 

  7. Fritchie, S.L.: Chain replication in theory and in practice. In: Proceedings of the 9th ACM SIGPLAN Workshop on Erlang, Erlang 2010, pp. 33–44. ACM, New York (2010). doi:10.1145/1863509.1863515

  8. Geambasu, R., Birrell, A., MacCormick, J.: Experiences with formal specification of fault-tolerant file systems. In: IEEE International Conference on Dependable Systems and Networks With FTCS and DCC, DSN 2008, pp. 96–101. IEEE (2008)

    Google Scholar 

  9. Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer-Verlag New York Inc., Secaucus (1996)

    Book  MATH  Google Scholar 

  10. Godefroid, P.: Model checking for programming languages using VeriSoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1997, pp. 174–186. ACM, New York (1997). doi:10.1145/263699.263717

  11. Godefroid, P.: Software model checking: the VeriSoft approach. Form. Methods Syst. Des. 26(2), 77–101 (2005). doi:10.1007/s10703-005-1489-x

    Article  Google Scholar 

  12. Gotovos, A., Christakis, M., Sagonas, K.: Test-driven development of concurrent programs using Concuerror. In: Proceedings of the 10th ACM SIGPLAN Workshop on Erlang, Erlang 2011, pp. 51–61. ACM, New York (2011). doi:10.1145/2034654.2034664

  13. Malkhi, D., Balakrishnan, M., Davis, J.D., Prabhakaran, V., Wobber, T.: From Paxos to CORFU: a flash-speed shared log. SIGOPS Oper. Syst. Rev. 46(1), 47–51 (2012). doi:10.1145/2146382.2146391

    Article  Google Scholar 

  14. Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI 2008, pp. 267–280. USENIX Association, Berkeley (2008)

    Google Scholar 

  15. Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31980-1_7

    Chapter  Google Scholar 

  16. van Renesse, R., Schneider, F.B.: Chain replication for supporting high throughput and availability. In: Proceedings of the 6th Conference on Symposium on Operating Systems Design & Implementation, OSDI 2004, pp. 91–104. USENIX, Berkeley (2004)

    Google Scholar 

  17. Schiper, N., Rahli, V., van Renesse, R., Bickford, M., Constable, R.L.: Developing correctly replicated databases using formal tools. In: 2014 44th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 395–406. IEEE (2014)

    Google Scholar 

  18. Thomson, P., Donaldson, A.F., Betts, A.: Concurrency testing using controlled schedulers: an empirical study. ACM Trans. Parallel Comput. 2(4), 23:1–23:37 (2016). doi:10.1145/2858651

    Article  Google Scholar 

Download references

Acknowledgments

This work was supported in part by the Swedish Research Council and carried out within the Linnaeus centre of excellence UPMARC, Uppsala Programming for Multicore Architectures Research Center.

Author information

Authors and Affiliations

  1. Department of Information Technology, Uppsala University, Uppsala, Sweden

    Stavros Aronis & Konstantinos Sagonas

  2. VMware, Cambridge, MA, USA

    Scott Lystig Fritchie

Authors
  1. Stavros Aronis
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Scott Lystig Fritchie
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Konstantinos Sagonas
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Stavros Aronis .

Editor information

Editors and Affiliations

  1. Massachusetts Institute of Technology, Cambridge, Massachusetts, USA

    Nadia Polikarpova

  2. University of Surrey, Guildford, United Kingdom

    Steve Schneider

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Aronis, S., Fritchie, S.L., Sagonas, K. (2017). Testing and Verifying Chain Repair Methods for Corfu Using Stateless Model Checking. In: Polikarpova, N., Schneider, S. (eds) Integrated Formal Methods. IFM 2017. Lecture Notes in Computer Science(), vol 10510. Springer, Cham. https://doi.org/10.1007/978-3-319-66845-1_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66845-1_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66844-4

  • Online ISBN: 978-3-319-66845-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation