Verification the algorithm of transactional memory

Mathematical Modelling: Methods, algorithms, technologies

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.