TY - GEN
T1 - Formal Analysis and Verification of DPSTM v2 Architecture Using CSP
AU - Li, Peimu
AU - Yin, Jiaqi
AU - Zhu, Huibiao
AU - Xiao, Lili
AU - Popovic, Miroslav
N1 - Publisher Copyright:
© 2022 IEEE.
PY - 2022
Y1 - 2022
N2 - Transactional memory is designed for developing parallel programs and improving the efficiency of parallel pro-grams. PSTM (python software transactional memory) mainly supports multi-core parallel programs based on the python language. In order to better adapt to the developing requirements of distributed concurrent programs and enhance the safety of the system, DPSTM (distributed python software transactional memory) was developed. Compared with PSTM, DPSTM has the advantages of higher operating efficiency and stronger fault tolerance. In this paper, we apply CSP (Communicating Sequential Processes) to formally analyze the components of DPSTM v2 architecture, the data exchange process between components, and two different transaction processing modes. We use the model checker PAT (Process Analysis Toolkit) to model the DPSTM v2 architecture and verify eight properties, including deadlock freedom, ACI (atomicity, isolation, and consistency), sequential consistency, data server availability, read tolerance, and crash tolerance. The verification results show that the DPSTM v2 archi-tecture can guarantee all of the above properties. In particular, the normal operation of the system can be maintained when some of the data servers are crashed, ensuring the safety of a distributed system.
AB - Transactional memory is designed for developing parallel programs and improving the efficiency of parallel pro-grams. PSTM (python software transactional memory) mainly supports multi-core parallel programs based on the python language. In order to better adapt to the developing requirements of distributed concurrent programs and enhance the safety of the system, DPSTM (distributed python software transactional memory) was developed. Compared with PSTM, DPSTM has the advantages of higher operating efficiency and stronger fault tolerance. In this paper, we apply CSP (Communicating Sequential Processes) to formally analyze the components of DPSTM v2 architecture, the data exchange process between components, and two different transaction processing modes. We use the model checker PAT (Process Analysis Toolkit) to model the DPSTM v2 architecture and verify eight properties, including deadlock freedom, ACI (atomicity, isolation, and consistency), sequential consistency, data server availability, read tolerance, and crash tolerance. The verification results show that the DPSTM v2 archi-tecture can guarantee all of the above properties. In particular, the normal operation of the system can be maintained when some of the data servers are crashed, ensuring the safety of a distributed system.
KW - CSP
KW - DPSTM v2
KW - Modeling
KW - Verification
UR - https://www.scopus.com/pages/publications/85136956686
U2 - 10.1109/COMPSAC54236.2022.00138
DO - 10.1109/COMPSAC54236.2022.00138
M3 - 会议稿件
AN - SCOPUS:85136956686
T3 - Proceedings - 2022 IEEE 46th Annual Computers, Software, and Applications Conference, COMPSAC 2022
SP - 872
EP - 877
BT - Proceedings - 2022 IEEE 46th Annual Computers, Software, and Applications Conference, COMPSAC 2022
A2 - Va Leong, Hong
A2 - Sarvestani, Sahra Sedigh
A2 - Teranishi, Yuuichi
A2 - Cuzzocrea, Alfredo
A2 - Kashiwazaki, Hiroki
A2 - Towey, Dave
A2 - Yang, Ji-Jiang
A2 - Shahriar, Hossain
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 46th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2022
Y2 - 27 June 2022 through 1 July 2022
ER -