Complete Formal Verification of the PSTM Transaction Scheduler

Miroslav Popovic1, Marko Popovic1, Branislav Kordic1 and Huibiao Zhu2

  1. University of Novi Sad, Faculty of Technical Sciences, Trg D. Obradovica 6,
    21000 Novi Sad, Serbia
    {miroslav.popovic, marko.popovic, branislav.kordic}@rt-rk.uns.ac.rs
  2. East China Normal University, Shanghai Key Laboratory of Trustworthy Computing,
    Shanghai 200062, China
    hbzhu@sei.ecnu.edu.cn

Abstract

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.

Key words

Formal Verification, Process Algebra, Transaction Scheduling, Python, Software Transactional Memory

Digital Object Identifier (DOI)

https://doi.org/10.2298/CSIS210908058P

Publication information

Volume 20, Issue 1 (January 2023)
Year of Publication: 2023
ISSN: 2406-1018 (Online)
Publisher: ComSIS Consortium

Full text

DownloadAvailable in PDF
Portable Document Format

How to cite

Popovic, M., Popovic, M., Kordic, B., Zhu, H.: Complete Formal Verification of the PSTM Transaction Scheduler. Computer Science and Information Systems, Vol. 20, No. 1, 307–327. (2023), https://doi.org/10.2298/CSIS210908058P