nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Exploring Design Alternatives for RAMP Transactions Through Statistical Model Checking

verfasst von : Si Liu, Peter Csaba Ölveczky, Jatin Ganhotra, Indranil Gupta, José Meseguer

Erschienen in: Formal Methods and Software Engineering

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Arriving at a mature distributed system design through implementation and experimental validation is a labor-intensive task. This limits the number of design alternatives that can be explored in practice. In this work we use formal modeling with probabilistic rewrite rules and statistical model checking to explore and extend the design space of the RAMP (Read Atomic Multi-Partition) transaction system for large-scale partitioned data stores. Specifically, we formally model in Maude eight RAMP designs, only two of which were previously implemented and evaluated by the RAMP developers; and we analyze their key consistency and performance properties by statistical model checking. Our results: (i) are consistent with the experimental evaluations of the two implemented designs; (ii) are also consistent with conjectures made by the RAMP developers for other unimplemented designs; and (iii) uncover some promising new designs that seem attractive for some applications.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel A Sliding-Window Algorithm for On-The-Fly Interprocedural Program Analysis

Nächstes Kapitel An Improved Android Collusion Attack Detection Method Based on Program Slicing

“Consistency” in such a non-replicated setting is understood as reads reading the “latest writes.”

We do not show the variable declarations, but follow the Maude convention that variables are written with (all) capital letters.

The variable AS of sort AttributeSet denotes the “other attributes” of the object.

Strong consistency is not evaluated in [5].

Larger versions of our figures can be found in the report [14].

PRISM. http://www.prismmodelchecker.org/

Uppaal SMC. http://people.cs.aau.dk/adavid/smc/

Agha, G.A., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. Electr. Notes Theor. Comput. Sci. 153(2), 213–239 (2006)CrossRef

AlTurki, M., Meseguer, J.: PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386–392. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22944-2_28 CrossRef

Bailis, P., Fekete, A., Ghodsi, A., Hellerstein, J.M., Stoica, I.: Scalable atomic visibility with RAMP transactions. ACM Trans. Database Syst. 41(3) (2016)

Bailis, P., Fekete, A., Hellerstein, J.M., Ghodsi, A., Stoica, I.: Scalable atomic visibility with RAMP transactions. In: Proceedings SIGMOD 2014. ACM (2014)

Barbierato, E., Gribaudo, M., Iacono, M.: Performance evaluation of NoSQL big-data applications using multi-formalism models. Future Gen. Comp. Syst. 37, 345–353 (2014)CrossRef

Benson, T., Akella, A., Maltz, D.A.: Network traffic characteristics of data centers in the wild. In: IMC, pp. 267–280 (2010)

Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.L.: All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007)MATH

10.

Gandini, A., Gribaudo, M., Knottenbelt, W.J., Osman, R., Piazzolla, P.: Performance evaluation of NoSQL databases. In: Horváth, A., Wolter, K. (eds.) EPEW 2014. LNCS, vol. 8721, pp. 16–29. Springer, Cham (2014). doi:10.1007/978-3-319-10885-8_2

11.

Grov, J., Ölveczky, P.C.: Formal modeling and analysis of Google’s Megastore in Real-Time Maude. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol. 8373, pp. 494–519. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54624-2_25 CrossRef

12.

Grov, J., Ölveczky, P.C.: Increasing consistency in multi-site data stores: Megastore-CGC and its formal analysis. In: Giannakopoulou, D., Salaün, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 159–174. Springer, Cham (2014). doi:10.1007/978-3-319-10431-7_12

13.

Liu, S., Ganhotra, J., Rahman, M., Nguyen, S., Gupta, I., Meseguer, J.: Quantitative analysis of consistency in NoSQL key-value stores. Leibniz Trans. Embed. Syst. 4(1), 031–0326 (2017)

14.

Liu, S., Ölveczky, P.C., Ganhotra, J., Gupta, I., Meseguer, J.: Exploring design alternatives for RAMP transactions through statistical model checking. Technical report (2017). https://sites.google.com/site/siliunobi/ramp-smc

15.

Liu, S., Ölveczky, P.C., Rahman, M.R., Ganhotra, J., Gupta, I., Meseguer, J.: Formal modeling and analysis of RAMP transaction systems. In: SAC. ACM (2016)

16.

Liu, S., Rahman, M.R., Skeirik, S., Gupta, I., Meseguer, J.: Formal modeling and analysis of Cassandra in Maude. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol. 8829, pp. 332–347. Springer, Cham (2014). doi:10.1007/978-3-319-11737-9_22

17.

Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoret. Comput. Sci. 96(1), 73–155 (1992)MathSciNetCrossRefMATH

18.

Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 266–280. Springer, Heidelberg (2005). doi:10.1007/11513988_26 CrossRef

19.

Sen, K., Viswanathan, M., Agha, G.A.: VESTA: a statistical model-checker and analyzer for probabilistic systems. In: QEST 2005. IEEE Computer Society (2005)

20.

Younes, H.L.S., Simmons, R.G.: Statistical probabilistic model checking with a focus on time-bounded properties. Inf. Comput. 204(9), 1368–1409 (2006)MathSciNetCrossRefMATH

Titel: Exploring Design Alternatives for RAMP Transactions Through Statistical Model Checking
verfasst von: Si Liu
Peter Csaba Ölveczky
Jatin Ganhotra
Indranil Gupta
José Meseguer
Verlag: Springer International Publishing
Buch: Formal Methods and Software Engineering
Print ISBN: 978-3-319-68689-9

Electronic ISBN: 978-3-319-68690-5

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-68690-5_18

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner