Formal analysis and verification of the PSTM architecture using CSP

Starting with the analysis of the source codes of the Python Software Transactional Memory (PSTM) architecture, this paper applies process algebra CSP to formally verify the architecture at a fine-grained level. We analyze the communication process and components of the architecture from multiple perspectives and establish models describing the communication behaviors of the PSTM architecture. We use model checker PAT to automatically simulate and verify the established model. After adapting the traditional transactional properties to the PSTM architecture, we analyze and verify five properties for the PSTM architecture, including deadlock freeness, atomicity, isolation, consistency and optimism. The verification results indicate that all the properties are valid. Based on the judgement of the execution logic of the communication procedure in the PSTM architecture, we can conclude that the architecture can have a proper communication and can guarantee atomicity, isolation, consistency and optimism. Besides, we also provide a case study with an application scenario and propose a corollary that the value of the shared counter is equal to the number of parallel processes. We verify whether the case study system can satisfy all the conditions of corollary from both positive and negative perspectives. The results show that the corollary is tenable.