Computer Science and Information Systems 2023 Volume 20, Issue 1, Pages: 307-327
https://doi.org/10.2298/CSIS210908058P
Full text (
2828 KB)
Complete formal verification of the PSTM transaction Scheduler
Popović Miroslav 
(University of Novi Sad, Faculty of Technical Sciences, Novi Sad, Serbia), miroslav.popovic@rt-rk.uns.ac.rs
Popović Marko (University of Novi Sad, Faculty of Technical Sciences, Novi Sad, Serbia), marko.popovic@rt-rk.uns.ac.rs
Kordić Branislav (University of Novi Sad, Faculty of Technical Sciences, Novi Sad, Serbia), branislav.kordic@rt-rk.uns.ac.rs
Zhu Huibiao (East China Normal University, Shanghai Key Laboratory of Trustworthy Computing, Shanghai, China), hbzhu@sei.ecnu.edu.cn
State of the art formal verification is based on formal methods and its goal is proving given correctness properties. For example, a PSTM scheduler was modeled in CSP in order to prove deadlock-freeness and starvation-freeness. However, as this paper shows, using solely formal methods is not sufficient. Therefore, in this paper we propose a complete formal verification of trustworthy software, which jointly uses formal verification and formal model testing. As an example, we first test the previous CSP model of PSTM transaction scheduler by comparing the model checker PAT results with the manually derived expected results, for the given test workloads. Next, according to the results of this testing, we correct and extend the CSP model. Finally, using PAT results for the new CSP model, we analyze the performance of the PSTM online transaction scheduling algorithms from the perspective of the relative speedup.
Keywords: Formal Verification, Process Algebra, Transaction Scheduling, Python, Software Transactional Memory
Project of the Serbian Ministry of Education, Science and Technological Development, Grant no. 451-03-68/2020-14/200156
Show references
Xu, C., Wu, X., Zhu, H., Popovic, M.: Modeling and Verifying Transaction Scheduling for Software Transactional Memory using CSP. In Proceedings of the 13th Theoretical Aspects of Software Engineering Symposium. IEEE, Guilin, China, 240-247. (2019)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice/Hall International, New Jersey, USA. (1985)
Si, Y., Sun, J., Liu, Y., Dong J. S., Pang, J., Zhang, S. J., Yang, X.: Model checking with fairness assumptions using PAT. Frontiers of Computer Science, Vol. 8, No. 1, 1-16. (2014)
Marinković, B., Ognjanović, Z., Glavan, P., Kos, A., Umek, A.: Correctness of the Chord Protocol. Computer Science and Information Systems, Vol. 17, No. 1, 141-160. (2020)
Elqortobi, M., El-Khouly, W., Rahj, Amine R., Bentahar, J., Dssouli, R.: Verification and Testing of Safety-Critical Airborne Systems: a Model-based Methodology. Computer Science and Information Systems, Vol. 17, No. 1, 271-292. (2020)
Cheikhrouhou, S., Kallel, S., Guidara, I., Maamar, Z.: Business Process Specification, Verification, and Deployment in a Mono-Cloud, Multi-Edge Context. Computer Science and Information Systems, Vol. 17, No. 1, 293-313. (2020)
Berard, B., Bidoit, J. M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, Ph., McKenzie, P.: Systems and Software Verification. Springer, Berlin, Germany. (1999)
Testing. Cambridge online dictionary. [Online]. Available: https://dictionary.cambridge.org/dictionary/english/testing (current September 2021)
Herlihy, M., Moss, J. E. B.: Transactional memory: Architectural support for lock-free data structures. In Proceedings of the 20th Annual International Symposium on Computer Architecture. ACM, San Diego, CA, USA, 289-300. (1993)
Harris, T., Larus, J. R., Rajwar, R.: Transactional Memory, 2nd edition. Morgan and Claypool, San Rafael, CA, USA. (2010)
Shavit, N., Touitou, D.: Software transactional memory. In Proceedings of the 14th Annual ACM Symposium on Principles of Distributed Computing. ACM, Ottawa, Ontario, Canada, 204-213. (1995)
Popovic, M., Kordic, B.: PSTM: Python software transactional memory. In Proceedings of the 22nd Telecommunications Forum (TELFOR). IEEE, Belgrade, Serbia, 1106-1109. (2014)
Kordic, B., Popovic, M., Popovic, M., Goldstein, M., Amitay, M., Dayan, D.: An Evolutionary Computational System Architecture Based on a Software Transactional Memory. Revue Roumaine des Sciences Techniques. Ser. Electrotechnique et Energetique, Vol. 61, No. 1, 47-52. (2021)
Kordic, B., Popovic, Ghilezan, M., S.: Formal Verification of Python Software Transactional Memory Based on Timed Automata. Acta Polytechnica Hungarica, Journal of Applied Sciences, Vol. 16, No. 7, 197-216. (2019)
Alur, R., Dill, D. L.: A theory of timed automata. Theoretical Computer Science, Vol. 126, No. 2, 183-235. (1994)
Behrmann, G., David, A., Larsen, K. G.: A Tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.): Formal Methods for the Design of Real-Time Systems. Lecture Notes in Computer Science, Vol. 3185. Springer-Verlag, Berlin Heidelberg New York, 200-236. (2004)
Liu, A., Zhu, H., Popovic, M., Xiang, S., Zhang, L.: Formal Analysis and Verification of the PSTM Architecture Using CSP. Journal of Systems and Software, Vol. 165, 1-14. (2020)
Popovic, M., Popovic, M., Ghilezan, S., Kordic, B.: Formal Verification of Local and Distributed Python Software Transactional Memories. Revue Roumaine des Sciences Techniques. Ser. Electrotechnique et Energetique, Vol. 64, No. 4, pp. 423-428. (2019)
Koskinen, E., Parkinson, M.: The Push/Pull Model of Transactions. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation. Morgan Kaufmann, Portland, Oregon, USA, 186-195. (2015)
Yoo R.M., Lee, H.-H.S.: Adaptive transaction scheduling for transactional memory systems. In Proceedings of the 20th annual symposium on Parallelism in algorithms and architectures. ACM, Munich, Germany, 169-178. (2008)
Ansari, M., Luján, M., Kotselidis, C., Jarvis, K., Kirkham, C., Watson, I.: Steal-on-Abort: Improving Transactional Memory Performance through Dynamic Transaction Reordering. In: Seznec, A., Emer, J., O’Boyle, M., Martonosi, M., Ungerer, T. (eds.): High Performance Embedded Architectures and Compilers. HiPEAC 2009. Lecture Notes in Computer Science, Vol. 5409. Springer, Berlin, Heidelberg, 4-18. (2009)
Dolev, S., Hendler, D., Suissa, A.: CAR-STM: scheduling based collision avoidance and resolution for software transactional memory. In Proceedings of the twenty-seventh ACM symposium on Principles of distributed computing. ACM, Toronto, Ontario, Canada, 125- 134. (2008)
Popovic, M., Kordic, B., Popovic, M., Basicevic, I.: Advanced Algorithm for Scheduling TM Transactions with Conflict Avoidance. In Proceedings of the 25th Telecommunications Forum (TELFOR). IEEE, Belgrade, Serbia, 844-847. (2017)
Popovic, M., Kordic, B., Popovic, M., Basicevic, I.: Online Algorithms for Scheduling Transactions on Python Software Transactional Memory. Serbian Journal of Electrical Engineering, Vol. 16, No. 1, 85-104. (2019)
Popovic, M., Popovic, M., Kordic, B., Zhu, H.: PSTM Transaction Scheduler Verification Based on CSP and Testing. In Proceedings of the 7th Conference on the Engineering of Computer Based Systems. ACM, Novi Sad, Serbia, Article No. 10, 1-10. (2021)