@inproceedings{73d01c37417b448b810578edeef145e2,
title = "Verifying opacity of a modified PSTM",
abstract = "Software transactional memory (STM) provides programmers with a high-level programming abstraction for synchronization of parallel processes, allowing blocks of codes that execute in an interleaved manner to be treated as an atomic block. Python Software Transactional Memory (PSTM) is an STM implementation in Python language. Its presentation fills a gap that Python lacks an applicable and reliable software transactional memory. PSTM satisfies the basic transaction properties, however it does not satisfy opacity, which defines conditions for serialising concurrent transaction. To alleviate this issue, we modify the PSTM implementation and present a new PSTM called PSTM-M. Based on PSTM-M, we verify opacity of this implementation. We present the formalization of opacity which is based on the history model of transaction. Further, we explain why PSTM does not satisfy opacity and present a modified PSTM called PSTM-M. Finally, we give a machine-checked proof for the opacity of PSTM-M based on the theorem prover Coq.",
keywords = "Coq, Opacity, PSTM, STM",
author = "Yucheng Fang and Huibiao Zhu and Jiaqi Yin",
note = "Publisher Copyright: {\textcopyright} 2019 IEEE.; 13th International Symposium on Theoretical Aspects of Software Engineering, TASE 2019 ; Conference date: 29-07-2019 Through 31-07-2019",
year = "2019",
month = jul,
doi = "10.1109/TASE.2019.00008",
language = "英语",
series = "Proceedings - 2019 13th International Symposium on Theoretical Aspects of Software Engineering, TASE 2019",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "232--239",
booktitle = "Proceedings - 2019 13th International Symposium on Theoretical Aspects of Software Engineering, TASE 2019",
address = "美国",
}