Top

Published in:

2020 | OriginalPaper | Chapter

Combining State- and Event-Based Semantics to Verify Highly Available Programs

Authors : Peter Zeller, Annette Bieniusa, Arnd Poetzsch-Heffter

Published in: Formal Aspects of Component Software

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Replicated databases are attractive for managing the data of distributed applications that require high availability, low latency, and high throughput. However, these benefits entail weak consistency which comes at a price: it becomes harder to reason about application correctness. We address this difficulty with a verification technique for highly available programs. We augment an existing sequential programming language with primitives for interacting concurrently with a highly available database and extend the state-based operational semantics of that language accordingly. To this end we make use of existing event-based database semantics.

We then present a reduction of the extended semantics to a simpler one, which is again sequential and therefore easier to handle in verification tools. Our verification tool Repliss uses this technique and demonstrates its feasibility.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter State Identification for Labeled Transition Systems with Inputs and Outputs

next chapter Reowolf: Synchronous Multi-party Communication over the Internet

The Isabelle proofs are available at https://github.com/peterzeller/repliss-isabelle/.

Abadi, D.: Consistency tradeoffs in modern distributed database system design: CAP is only part of the story. IEEE Comput. 45(2), 37–42 (2012). https://doi.org/10.1109/MC.2012.33. http://dx.doi.org/10.1109/MC.2012.33CrossRef

Ahamad, M., Neiger, G., Burns, J.E., Kohli, P., Hutto, P.W.: Causal memory: definitions, implementation, and programming. Distrib. Comput. 9(1), 37–49 (1995). https://doi.org/10.1007/BF01784241MathSciNetCrossRef

Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_14CrossRef

Beckert, B., Mostowski, W.: A program logic for handling Java Card’s transaction mechanism. In: Pezzè, M. (ed.) FASE 2003. LNCS, vol. 2621, pp. 246–260. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36578-8_18CrossRef

Bodík, R., Majumdar, R. (eds.): Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, 20–22 January 2016. ACM (2016). http://dl.acm.org/citation.cfm?id=2837614

Burckhardt, S.: Principles of eventual consistency. Found. Trends Program. Lang. 1(1–2), 1–150 (2014). https://doi.org/10.1561/2500000011CrossRef

Burckhardt, S., Gotsman, A., Yang, H., Zawirski, M.: Replicated data types: specification, verification, optimality. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, 20–21 January 2014, pp. 271–284. ACM (2014). https://doi.org/10.1145/2535838.2535848. http://doi.acm.org/10.1145/2535838.2535848

Dongol, B., Derrick, J.: Verifying linearisability: a comparative survey. ACM Comput. Surv. 48(2), 19:1–19:43 (2015). https://doi.org/10.1145/2796550CrossRef

Gilbert, S., Lynch, N.A.: Brewer’s conjecture and the feasibility of consistent, available, partition-tolerant web services. SIGACT News 33(2), 51–59 (2002)CrossRef

10.

Gotsman, A., Yang, H.: Composite replicated data types. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 585–609. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46669-8_24CrossRef

11.

Gotsman, A., Yang, H., Ferreira, C., Najafzadeh, M., Shapiro, M.: ‘Cause I’m strong enough: reasoning about consistency choices in distributed systems. In: Bodík, Majumdar [5], pp. 371–384. https://doi.org/10.1145/2837614.2837625. http://doi.acm.org/10.1145/2837614.2837625

12.

Kaki, G., Earanky, K., Sivaramakrishnan, K., Jagannathan, S.: Safe replication through bounded concurrency verification. In: 32nd ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA) (2018)

13.

Lakshman, A., Malik, P.: Cassandra: a decentralized structured storage system. SIGOPS Oper. Syst. Rev. 44(2), 35–40 (2010). https://doi.org/10.1145/1773912.1773922. http://doi.acm.org/10.1145/1773912.1773922CrossRef

14.

Lesani, M., Bell, C.J., Chlipala, A.: Chapar: certified causally consistent distributed key-value stores. In: Bodík, Majumdar [5], pp. 357–370. https://doi.org/10.1145/2837614.2837622. http://doi.acm.org/10.1145/2837614.2837622

15.

Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18(12), 717–721 (1975). https://doi.org/10.1145/361227.361234MathSciNetCrossRefMATH

16.

Lloyd, W., Freedman, M.J., Kaminsky, M., Andersen, D.G.: Don’t settle for eventual: scalable causal consistency for wide-area storage with COPS. In: Wobber, T., Druschel, P. (eds.) Proceedings of the 23rd ACM Symposium on Operating Systems Principles 2011, SOSP 2011, Cascais, Portugal, 23–26 October 2011, pp. 401–416. ACM (2011). https://doi.org/10.1145/2043556.2043593. http://doi.acm.org/10.1145/2043556.2043593

17.

Nair, S., Petri, G., Shapiro, M.: Invariant safety for distributed applications. CoRR abs/1903.02759 (2019). http://arxiv.org/abs/1903.02759

18.

Najafzadeh, M., Gotsman, A., Yang, H., Ferreira, C., Shapiro, M.: The CISE tool: proving weakly-consistent applications correct. In: Alvaro, P., Bessani, A. (eds.) Proceedings of the 2nd Workshop on the Principles and Practice of Consistency for Distributed Data, PaPoC@EuroSys 2016, London, United Kingdom, 18 April 2016, pp. 2:1–2:3. ACM (2016). https://doi.org/10.1145/2911151.2911160. http://doi.acm.org/10.1145/2911151.2911160

19.

Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9CrossRefMATH

20.

Shapiro, M., Preguiça, N., Baquero, C., Zawirski, M.: A comprehensive study of convergent and commutative replicated data types. Rapport de recherche RR-7506, INRIA, January 2011. http://hal.inria.fr/inria-00555588

21.

Sivaramakrishnan, K.C., Kaki, G., Jagannathan, S.: Declarative programming over eventually consistent data stores. In: Grove, D., Blackburn, S. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, 15–17 June 2015, pp. 413–424. ACM (2015). https://doi.org/10.1145/2737924.2737981. http://doi.acm.org/10.1145/2737924.2737981

22.

Vishnevskiy, S.: How discord stores billions of messages. https://blog.discordapp.com/how-discord-stores-billions-of-messages-7fa6ec7ee4c7. Accessed 16 Nov 2018

23.

Zeller, P., Bieniusa, A., Poetzsch-Heffter, A.: Formal specification and verification of CRDTs. In: Ábrahám, E., Palamidessi, C. (eds.) FORTE 2014. LNCS, vol. 8461, pp. 33–48. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-43613-4_3CrossRef

Title: Combining State- and Event-Based Semantics to Verify Highly Available Programs
Authors: Peter Zeller
Annette Bieniusa
Arnd Poetzsch-Heffter
Publisher: Springer International Publishing
Book: Formal Aspects of Component Software
Print ISBN: 978-3-030-40913-5

Electronic ISBN: 978-3-030-40914-2

Copyright Year: 2020
DOI: https://doi.org/10.1007/978-3-030-40914-2_11

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner