Verification the algorithm of transactional memory

Mathematical Modelling: Methods, algorithms, technologies
Authors:
Belyaev Aleksey B.
Abstract:

The paper presents the results of the mechanical verification the algorithm of software transactional memory. Verification has found a subtle error in the algorithm, which may lead to a system failure in some special cases. Then it was corrected.