Computing, Telecommunication and Control Информатика, телекоммуникации и управление 2687-0517 16 Verification the algorithm of transactional memory Верификация алгоритма поддержки транзакционной памяти Belyaev Aleksey elyaevab@gmail.com 10 06 2010 3 101 107 111

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.

 PARALLEL PROGRAMMING VERIFICATION MODEL CHECKING TEMPORAL LOGIC TRANSACTIONAL MEMORY OPACITY