Симуляция и верификация распределенных программ при использовании транзакционной памяти. Simulation and verication distributed programs using transactional memory.

Authors

  • А. Т. Бектемесов Казахский национальный университет им. аль-Фараби, Алматы, Казахстан
  • Д. Ж. Ахмед-Заки Казахский национальный университет им. аль-Фараби, Алматы, Казахстан
  • Н. Т. Данаев Казахский национальный университет им. аль-Фараби, Алматы, Казахстан

Keywords:

верификация, кластер, параллельные вычисления, распределенные системы, Spin, Promela, TORQUE, verication, clusters, parallel computing, distributed systems.

Abstract

В данной работе исследована модель симуляции распределенных программ с использованием транзакционной памяти. Показаны особенности модели во время симуляции и дальнейшим этапом верификации. Продемонстрирована модель распределенной системы с использованием WSTM, написанной на языке Promela. Проведен анализ результатов выполнения асинхронных компонентов вычислений. Сделано модельное сравнение распределительной системой TORQUE. При выполнении вычисления задач на кластерных компьютерах проанализирована модель распределения ресурсов между узлами и ее верификация с помощью Spin. In this work, investigate model simulation of distributed programs using transactional memory. Shows the feature of the model during simulation, and proceeds to the next stage of verication. Demonstrated a model of a distributed system using WSTM written in language Promela. The results of the asynchronous computing components has been analyzed. The distribution system TORQUE in model comparison is made. In carrying out computation tasks on clustered computers, the distribution model of the nodes is written and analyzed and verication using Spin.

References

Беляев А.Б Верификация алгоритма поддержки транзакционной памяти.// Научно-технические ведомости, ѕТелематика-2010: телекоммуникации, вебтехнологии, суперкомпьютингї. СПбГУ, Санкт-Петербург  101. 2010. С. 186-192.

Imbs D., Raynal M. Software Transactional Memories: An Approach for Multicore Programming // PaCT 2009. LNCS. 2009. Vol. 5698. P. 2640.

Карпов Ю.Г. Model Checking: Верификация параллельных и распределенных программных систем. // "БХВ-Петербург" 2010. 189 c.

Clarke E. M., Grumberg O., Peled D.A. Model Checking // The MIT Press. London, England, 1999. 330 p.

Torque administrator's guide. www.clusterresources.com (дата обращения 25.07.2014)

М.А. Лукин, А.А. Шалыто Международная научно-практическая конференция: Инструменты и методы анализа программ. // TMPA-2013. 2013. С. 7893.

F.J. Morten Formal Verication of Distributed Programs using Session Types and Coq. // IT University of Copenhagen. 2013. 68 p.

Belyaev À. B. Verication algorithm of the supporting transactional memory. // Technical-science issue, ¾Telematic-2010:telecommunication , web-technology, supercomputing¿. SPbGU, Saint-Petersburg  101. 2010. P. 186-192.

Imbs D., Raynal M. Software Transactional Memories: An Approach for Multicore Programming // PaCT 2009. LNCS. 2009. Vol. 5698. P.2640.

Karpov Y.G. Model Checking: Verication of parallel and distributing software systems. // ¾BHV-Peterburg¿ 2010. 189 p.

Downloads

Issue

Section

Mechanics, Mathematics, Computer Science