Model-based Testing of Practical Distributed Systems in Actor Model
DOI:
https://doi.org/10.14529/cmse260303Keywords:
distributed systems, software testing, graph algorithmsAbstract
Designing and implementing distributed systems correctly can be quite challenging. Although these systems are often accompanied by formal specifications that are verified using model-checking techniques, a gap still exists between the implementation and its formal specification: there is no guarantee that the implementation is free of bugs. To bridge this gap, we can use model-based testing. Specifically, if the model of the system can be interpreted as a finite-state automaton, we can generate an exhaustive test suite for the implementation that covers all possible states and transitions. In this paper, we discuss how to efficiently generate such a test suite for distributed systems written in the actor model. Importantly, our approach does not require any modifications to the code or interfering with the distributed system execution environment. As an example, we verified an implementation of a replication algorithm based on Viewstamped Replication, which is used in a real-world system.
References
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. Steinbrü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.
