|Title:||Formal Verification of Local and Distributed Python Software Transactional Memories||Journal:||Revue roumaine des sciences techniques Série Électrotechnique et Énergétique||Volume:||64||Issue:||4||First page:||423||Last page:||428||Issue Date:||14-Oct-2019||Rank:||M23||ISSN:||0035-4066||URL:||http://revue.elth.pub.ro/viewpdf.php?id=880||Abstract:||
Both local and distributed Python STMs are targeting a wide range of application domains, including critical infrastructures, such as cyber-physical systems, internet of things, etc., and formal verification of such software components is considered mandatory. Recently, the push/pull semantic model of transactions has appeared as a solution that unifies a wide range of transactional memory algorithms. In this paper, we formally prove that both local and distributed Python STM implementations are serializable by constructing their push/pull model and by showing that the push/pull model satisfies the correctness criteria for the relevant push/pull semantic rules. The main contributions of the paper are the following: (i) the PSTM and DPSTM push/pull semantic model, (ii) the proofs of the relevant push/pull semantic rules, and (iii) the way how the model and the proofs have been constructed.
|Keywords:||Formal verification | Push/pull semantic model | Serializability | Python | Software transactional memory (STM)||Publisher:||Editura Academiei Romane|
Show full item record
checked on Mar 27, 2023
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.