Formal Verification of Python Software Transactional Memory Serializability Based on the Push/Pull Semantic Model
| Autor: | Marko Popovic, Branislav Kordic, Silvia Ghilezan, Miroslav Popovic |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Correctness
010304 chemical physics Computer science Programming language Serialization Transactional memory Python (programming language) 010402 general chemistry Semantic data model computer.software_genre 01 natural sciences 0104 chemical sciences Serializability 0103 physical sciences Software transactional memory computer Formal verification computer.programming_language |
| Zdroj: | ECBS |
| Popis: | The Push/Pull semantic model of transactions has appeared recently as a solution that unifies a wide range of transactional memory algorithms. It has been proved that the push/pull semantic model satisfies serializability, thus one may prove that a given STM satisfies serializability by constructing its push/pull model such that this model satisfies respective correctness criteria. In this paper, we prove that a Python STM implementation is serializable by constructing its Push/Pull model and by showing that the model satisfies the correctness criteria for the relevant push/pull semantic rules. We first identify that modeling Python STM requires only four, out of seven, push/pull operations, namely the operations pull, apply, push, and commit. Next, we introduce the detailed specification of the PSTM transactional algorithm. Then we map the steps of the PSTM transactional algorithm to the respective push/pull semantic rules. Finally, we prove that the PSTM algorithm satisfies the correctness criteria of the respective push/pull semantic rules. We have envisaged this paper to provide interested researchers with a better understanding of PSTM semantics, in order to construct push/pull models of their own STMs more easily. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|