Formalization and Verification of the PSTM Architecture

摘要

Python Software Transactional Memory (PSTM), was proposed to break the limiting factors which restrict diffusion of the TM paradigm into more application fields. Since the widespread use of the PSTM, it is of great significance to formally analyze and verify relevant transactional properties of this architecture. In this paper, we apply Communicating Sequential Processes (CSP) to model the PSTM. Moreover, we use the model checker Process Analysis Toolkit (PAT) to automatically simulate the developed model, and verify whether the model caters for some relevant properties, e.g. ACID. Our modeling and verification show that the PSTM can guarantee some transactional properties.