Тестирование на основе спецификации реализованных в акторной модели практических распределенных систем

Илья Всеволодович Кокорин; Евгений Геннадьевич Чернацкий

doi:10.14529/cmse260303

Авторы

Илья Всеволодович Кокорин Университет ИТМО, Санкт-Петербург; vk.com Москва
Евгений Геннадьевич Чернацкий Университет ИТМО, Санкт-Петербург; vk.com Москва

DOI:

https://doi.org/10.14529/cmse260303

Ключевые слова:

распределенные системы, тестирование программного обеспечения, алгоритмы на графах

Аннотация

Корректная реализация распределенной системы может являться очень сложной задачей. Несмотря на то что распределенные системы часто разрабатываются на основе формальных спецификаций, которые верифицируются при помощи техник проверки моделей, существует значимая разница между формальной спецификацией и реализацией распределенной системы: верификация формальной спецификации не может гарантировать отсутствия ошибок в реализации. Для решения этой проблемы можно использовать тестирование на основе спецификации. Для этого будем интерпретировать формальную спецификацию системы как конечный автомат, и на основе этой спецификации генерировать исчерпывающий набор тестов, покрывающий все возможные состояния и переходы распределенной системы. В этой статье обсуждаются способы эффективной генерации такого набора тестов для распределенной системы, реализованной в акторной модели. Разработанный подход не требует модификации кода реализованной в акторной модели распределенной системы или какого-либо вмешательства в работу среды передачи данных. В качестве примера была верифицирована реализация алгоритма репликации, использующаяся в базах данных компании vk.com, основанная на алгоритме Viewstamped Replication.

Библиографические ссылки

Liskov B., Cowling J. Viewstamped Replication Revisited: Technical Report / MIT Computer Science; Artificial Intelligence Laboratory, Cambridge, MA. 2012.. URL: http://pmg.csail.mit.edu/papers/vr-revisited.pdf.

Oki B.M., Liskov B.H. Viewstamped Replication: A New Primary Copy Method to Support Highly-Available Distributed Systems. Proceedings of the Seventh Annual ACM Symposium on Principles of Distributed Computing, PODC’88, Toronto, Ontario, Canada, August 15–17, 1988. New York: ACM, 1988. P. 8–17. DOI: 10.1145/62546.62549.

Costa C.H., Filho J.V.B.M., Maia P.H.M., Oliveira F.C.M.B. Sharding by Hash Partitioning - A Database Scalability Pattern to Achieve Evenly Sharded Database Clusters. Proceedings of the 17th International Conference on Enterprise Information Systems, ICEIS 2015, Barcelona, Spain, April 27–30, 2015. SciTePress, 2015. P. 313–320. DOI: 10.5220/0005376203130320.

Lakshman A., Malik P. Cassandra: a decentralized structured storage system. ACM SIGOPS Operating Systems Review. 2010. Vol. 44, no. 2. P. 35–40. DOI: 10.1145/1773912.1773922.

Baker J., Bond C., Corbett J.C., et al. Megastore: Providing Scalable, Highly Available Storage for Interactive Services. CIDR 2011, Fifth Biennial Conference on Innovative Data Systems Research, Asilomar, CA, USA, January 9–12, 2011, Online Proceedings. www.cidrdb.org, 2011. P. 223–234. URL: http://cidrdb.org/cidr2011/Papers/CIDR11_Paper32.pdf.

Lamport L. The Part-Time Parliament. ACM Transactions on Computer Systems. 1998. Vol. 16, no. 2. P. 133–169. DOI: 10.1145/279227.279229.

Taft R., Sharif I., Matei A., et al. CockroachDB: The Resilient Geo-Distributed SQL Database. Proceedings of the 2020 ACM SIGMOD International Conference on Management of Data, SIGMOD’20, Portland, OR, USA, June 14–19, 2020. New York: ACM, 2020. P. 1493–1509. DOI: 10.1145/3318464.3386134.

Atif M. Analysis and Verification of Two-Phase Commit & Three-Phase Commit Protocols. 2009 International Conference on Emerging Technologies, ICET 2009, Islamabad, Pakistan, October 19–20, 2009. IEEE, 2009. P. 326–331. DOI: 10.1109/ICET.2009.5353152.

Huang D., Liu Q., Cui Q., et al. TiDB: A Raft-based HTAP Database. Proceedings of the VLDB Endowment. 2020. Vol. 13, no. 12. P. 3072–3084. DOI: 10.14778/3415478.3415535.

Ongaro D., Ousterhout J.K. In Search of an Understandable Consensus Algorithm. 2014 USENIX Annual Technical Conference, USENIX ATC’14, Philadelphia, PA, USA, June 19–20, 2014. USENIX Association, 2014. P. 305–319. URL: https://www.usenix.org/conference/atc14/technical-sessions/presentation/ongaro.

Peng D., Dabek F. Large-scale Incremental Processing Using Distributed Transactions and Notifications. 9th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2010, Vancouver, BC, Canada, October 4–6, 2010, Proceedings. USENIX Association, 2010. P. 251–264. URL: https://www.usenix.org/legacy/events/osdi10/tech/full_papers/Peng.pdf.

Corbett J.C., Dean J., Epstein M., et al. Spanner: Google’s Globally Distributed Database. ACM Transactions on Computer Systems. 2013. Vol. 31, no. 3. P. 1–22. DOI: 10.1145/2491245.

Zheng J., Lin Q., Xu J., et al. PaxosStore: High-availability Storage Made Practical in WeChat. Proceedings of the VLDB Endowment. 2017. Vol. 10, no. 12. P. 1730–1741. DOI: 10.14778/3137765.3137778.

Chandra T.D., Griesemer R., Redstone J. Paxos Made Live: An Engineering Perspective. Proceedings of the Twenty-Sixth Annual ACM Symposium on Principles of Distributed Computing, PODC’07, Portland, OR, USA, August 12–15, 2007. New York: ACM, 2007. P. 398–407. DOI: 10.1145/1281100.1281103.

Liang H., Pei X., Jia X., et al. Fuzzing: State of the Art. IEEE Transactions on Reliability. 2018. Vol. 67, no. 3. P. 1199–1218. DOI: 10.1109/TR.2018.2834476.

Lamport L. Specifying Concurrent Systems with TLA+. Calculational System Design, Proceedings of the NATO Advanced Study Institute, Marktoberdorf, Germany, July 28 – August 9, 1998. Vol. 173 / ed. by M. Broy, R. Steinbrüggen. Amsterdam: IOS Press, 1999. P. 183–247. NATO ASI Series, Series F: Computer and Systems Sciences.

Yu Y., Manolios P., Lamport L. Model Checking TLA+ Specifications. Correct Hardware Design and Verification Methods, 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME’99, Bad Herrenalb, Germany, September 27–29, 1999, Proceedings. Vol. 1703 / ed. by L. Pierre, T. Kropf. Springer, 1999. P. 54–66. Lecture Notes in Computer Science. DOI: 10.1007/3-540-48153-2_6.

Wang D., Dou W., Gao Y., et al. Model Checking Guided Testing for Distributed Systems. Proceedings of the Eighteenth European Conference on Computer Systems, EuroSys’23, Rome, Italy, May 8–12, 2023. New York: ACM, 2023. P. 127–143. DOI: 10.1145/3552326.3587442.

Biere A. Bounded Model Checking. Handbook of Satisfiability. Vol. 185 / ed. by A. Biere, M. Heule, H. van Maaren, T. Walsh. Amsterdam: IOS Press, 2009. P. 457–481. Frontiers in Artificial Intelligence and Applications. DOI: 10.3233/978-1-58603-929-5-457.

Goldberg A.V., Tarjan R.E. Finding Minimum-Cost Circulations by Canceling Negative Cycles. Proceedings of the Twentieth Annual ACM Symposium on Theory of Computing, STOC’88, Chicago, IL, USA, May 2–4, 1988. New York: ACM, 1988. P. 388–397. DOI: 10.1145/62212.62250.