Verification of Concurrent Go Programs using Timed Trace Theory

Denduang Pradubsuwun

doi:10.59796/jcst.V15N2.2025.94

Authors

Denduang Pradubsuwun Department of Computer Science, Faculty of Science and Technology, Thammasat University, Pathum Thani 12120, Thailand

DOI:

https://doi.org/10.59796/jcst.V15N2.2025.94

Keywords:

concurrent program, conformance checking, Go program, goroutine, time Petri net, timed trace theory, verify

Abstract

The Go programming language, or Go, plays a critical role in developing concurrent programs because it provides features such as goroutines and channels that support program concurrency. Even though concurrency makes programs efficient, verification is required to ensure their correctness. This paper proposes a novel approach to verifying concurrent Go programs using timed trace theory. The proposed approach is specifically designed to verify concurrent systems. Verifying a Go program using timed trace theory is divided into two tasks: modeling and verification. Modeling involves transforming a Go program into time Petri nets using a proposed algorithm. Verification involves checking the conformance between the Go program and its specification. This can be done automatically by the timed trace theoretic verification tool, which supports a partial order reduction technique to mitigate the state explosion problem. We demonstrate the verification of the Philosopher problem using both the total order method and the partial order reduction method. Experiments with the Go program of the Philosopher problem demonstrate the effectiveness of the proposed method.

References

Dill, D. L. (1988). Trace theory for automatic hierarchical verification of speed-independent circuits. Advanced Research in VLSI: Proceedings of the 5th MIT Conference. MIT Press. https://doi.org/10.7551/mitpress/1102.001.0001

Dilley, N., & Lange, J. (2021). Automated verification of Go programs via bounded model checking [Conference presentation]. 36th IEEE/ACM International Conference on Automated Software Engineering (ASE), November 15-19, 2021, Melbourne, Australia. https://doi.org/10.1109/ASE51524.2021.9678571

Fu, S., & Zhang, K. (2023). Network asset sensitive information management system based on Golang [Conference presentation]. International Conference on Algorithms, Computing and Data Processing (ACDP), June 23-25, 2023, Qingdao, China. https://doi.org/10.1109/ACDP59959.2023.00030

Gabet, J., & Yoshida, N. (2020). Static race detection and mutex safety and liveness for Go programs (extended version) [Conference presentation]. European Conference on Object-Oriented Programming, Online Conference, November 15-17, 2020, Berlin, Germany. https://doi.org/10.48550/arXiv.2004.12859

Gao, C., Lv, H., & Tan, Y. (2023). Multithreading technology based on Golang implementation [Conference presentation]. 3rd Asia-Pacific Conference on Communications Technology and Computer Science (ACCTCS), February 25-27, 2023, Shenyang, China. https://doi.org/10.1109/ACCTCS58815.2023.00116

Ghosh, P., & Karsai, G. (2023). Distributed cyber physical systems software model checking using timed automata [Conference presentation]. IEEE 26th International Symposium on Real-Time Distributed Computing (ISORC), May 23-25, 2023, Nashville, TN, USA. https://doi.org/10.1109/ISORC58943.2023.00030

Go. (2019). Documentation. Retrieved July 2, 2024, from https://go.dev/doc

Hu, J., & Zhang, Y. (2023). Design of remote monitoring system for ventilator based on Golang and MongoDB [Conference presentation]. 6th International Conference on Artificial Intelligence and Big Data (ICAIBD), May 26-29, 2023, Chengdu, China. https://doi.org/10.1109/ICAIBD57115.2023.10206318

Kitahara, Y., Nakamura, M., & Sakakibara, K. (2022). An investigation of formal verification of control policy of multi-car elevator systems using statistical Model checking [Conference presentation]. International Conference on Machine Learning and Cybernetics (ICMLC), September 9-11, 2022, Japan. https://doi.org/10.1109/ICMLCp6445.2022.9941319

Lange, J., Ng, N., Toninho, B., & Yoshida, N. (2018). A static verification framework for message passing in Go using behavioural types [Conference presentation]. IEEE/ACM 40th International Conference on Software Engineering (ICSE), May 27-June 3, 2018, Gothenburg, Sweden. https://doi.org/10.1145/3180155.3180157

Meyerson, J. (2014). The Go Programming Language. IEEE Software, 31(5), 101-104. https://doi.org/10.1109/MS.2014.127

Pang, S., Bian, Z., Zhang, Z., Meng, L., & Jiao, J. (2024). A safety analysis method based on model checking [Conference presentation]. 10th International Symposium on System Security, Safety, and Reliability (ISSSR), March 16-17, 2024, Xiamen, China. https://doi.org/10.1109/ISSSR61934.2024.00014

Pradubsuwun, D., Yoneda, T., & Myers, C. (2005). Partial order reduction for detecting safety and timing failures of timed circuits. IEICE transactions on information and systems, 88(7), 1646-1661. https://doi.org/10.1093/ietisy/e88-d.7.1646

Prasertsang, A., & Pradubsuwun, D. (2016). Formal verification of concurrency in Go [Conference presentation]. 13th International Conference on Computer Science and Software Engineering (JCSSE), July 13-15, 2016, Khonkaen, Thailand. https://doi.org/10.1109/JCSSE.2016.7748882

Zhou, B., Yoneda, T., & Myers, C. (2001). Framework of timed trace theoretic verification revisited [Conference presentation]. Proceedings of the 10th Asian Test Symposium, November 19-20, 2001, Kyoto Japan. https://doi.org/10.1109/ATS.2001.990323

Zhu, W., & Wang, Y. (2023). Model checking for scheduling on flight decks of aircraft carriers [Conference presentation]. IEEE 6th Information Technology, Networking, Electronic and Automation Control Conference (ITNEC), February 24-26, 2023, Chongqing, China. https://doi.org/10.1109/ITNEC56291.2023.10082464