Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses
2008
Transactional memory is a programming abstraction intended to simplify the synchronization of conflicting memory accesses (by concurrent threads) without the difficulties associated with locks. In a previous work we presented a formal framework for proving that a transactional memory implementation satisfies its specifications and provided with model checking verification of some using small instantiations. This paper extends the previous work to capture non-transactional accesses to memory, which occurs, for example, when using legacy code. We provide a mechanical proof of the soundness of the verification method, as well as a mechanical verification of a version of the popular tcc implementation that includes non-transactional memory accesses. The verification is performed by the deductive temporal checker tlpvs .
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
14
References
27
Citations
NaN
KQI