Работа посвящена моделированию и формальной верификации распределенной транзакционной памяти CUDA-DTM при помощи метода Model Checking. Модель памяти CUDA-DTM является новой, и авторы статьи, описывающие ее, не приводят сведений о формальной верификации модели. В то же время разработка моделей транзакционной памяти является очень сложным процессом, в котором легко допустить ошибку. Цель нашей работы - формально верифицировать модель CUDA-DTM при помощи метода проверки модели. Ключевые особенности CUDA-DTM были выделены после сравнения её с другими моделями транзакционной памяти. Таких особенностей оказалось три: работа в режиме потока управления, использование вложенных транзакций и поддержка MPI. Для верификации при помощи метода Model Checking были выбраны инструменты проверки моделей Spin и TLC Model Checker. Были выделены основные структуры данных и алгоритмы, используемые в CUDA-DTM. Для верификации в Spin была построена модель на языке Promela, а для верификации в TLC Model Checker была построена модель на языке Pluscal. В результате в ходе верификации в Spin было формально доказано, что модель CUDA-DTM для кластеров с 2 узлами и 2,4 и 8 ячейками разделяемой памяти удовлетворяет свойствам отсутствия блокировок и взаимно исключающего доступа. В ходе верификации в TLC Model Checker было формально доказано, что модель CUDA-DTM для кластеров с 2 узлами и 2 ячейками разделяемой памяти удовлетворяет свойству отсутствия блокировок. Верификация моделей CUDA-DTM для кластеров с большим количеством узлов и ячеек общей разделяемой памяти была ограничена ресурсами системы, на которой проводилась верификация. В будущем можно провести верификацию на более производительной системе, увеличив число узлов и ячеек разделяемой памяти. Также в будущем можно формализовать более сложные свойства и проверить, удовлетворяет ли CUDA-DTM этим свойствам.

This thesis is devoted to modeling and formal verification of distributed transactional memory CUDA-DTM using Model Checking method. Memory model CUDA-DTM is new and authors of the article describing this model did not provide information about formal verification of the model. At the same time, the development of transactional memory model is a very complicated process in which it is easy to make a mistake. The objective of this thesis is to highlight the main distinctive features of CUDA-DTM, build a model which will reflect these features and then formally verify it with Model Checking method. The main distinctive features if CUDA-DTM were pointed out after the comparison of CUDA-DTM with other transactional memory models. There are three main distinctive features: the support of MPI, working in control-flow mode and nested transactions support. For verification with Model Checking method, we chose model verification tools Spin and TLC Model Checker. We highlighted the main data structures and algorithms used in CUDA-DTM. For Spin verification we created a model in Promela language and for TLC Model Checker verification we created a model in Pluscal language. During the Spin verification, we formally proved that CUDA-DTM model for clusters with 2 nodes and 2, 4 and 8 shared memory pieces satisfies the requirement of mutual exclusion and being deadlock-free. During the TLC Model Checker verification, we formally proved that CIDA-DTM model for clusters with 2 nodes and 2 shared memory pieces satisfies the requirement of being deadlock-free. The verification of CUDA-DTM model for clusters with bigger number of nodes and shared data objects was limited by the resources of our system where we launched the verification. In the future we will be able to perform the verification on a more productive machine and increase the number of nodes and shared data objects. Also, in the future we will be able to formalize more complicated properties and check if CUDA-DTM satisfies these properties.