ISP («Частичный порядок на месте») - это инструмент для формальной проверки программ MPI , разработанных в Школе вычислительной техники Университета Юты. Подобно программам проверки моделей , таким как SPIN , ISP проверяет полное пространство состояний системы на наличие набора свойств безопасности . Однако, в отличие от программ проверки моделей, провайдер выполняет проверку на уровне кода . Это означает, что инструмент проверяет все соответствующие чередования параллельной программы, воспроизводя реальный программный код без построения моделей проверки. Эта идея была впервые реализована в ряде инструментов, в частности, Годфроидом в его инструменте VeriSoft. [1]Другие недавние инструменты этого жанра включают Java Pathfinder, инструмент Microsoft CHESS и MODIST. Соответствующие перемежения вычисляются с использованием настраиваемого алгоритма динамического сокращения частичного порядка [2] , называемого POE . [3]
ISP использовался для успешной проверки до 14 000 строк кода MPI / C на наличие взаимоблокировок и нарушений утверждений. В настоящее время он поддерживает более 60 функций MPI 2.1 и был протестирован с библиотеками MPICH2 , OpenMPI и Microsoft MPI .
ISP доступен для загрузки для Linux и Mac OS X ; как подключаемый модуль Visual Studio для работы под Windows и как подключаемый модуль Eclipse ..
Рекомендации
- ^ Патрис Годфроид, Проверка моделей для языков программирования с использованием VeriSoft POPL 1997
- ^ Кормак Фланаган и Патрис Годфруа, Динамическое уменьшение частичного порядка для проверки модели программного обеспечения, , POPL 2005 , стр. 110-121, ACM, ISBN 1-58113-830-X
- ^ Сарвани Ваккаланка, Ганеш Гопалакришнан и Роберт М. Кирби, Динамическая проверка программ MPI с уменьшением наличия операций разделения и упрощенного упорядочения, Компьютерная проверка (CAV 2008) , стр. 66-79, LNCS 5123.
Анх Во, Сарвани Ваккаланка, Майкл Делиси, Ганеш Гопалакришнан, Роберт М. Кирби и Раджив Такур, Официальная проверка практических программ MPI, PPoPP 2009
Сарвани Ваккаланка, Майкл Делиси, Ганеш Гопалакришнан и Роберт М. Кирби, Рекомендации по планированию для создания инструментов динамической проверки для MPI, параллельных и распределенных систем - тестирование и отладка (PADTAD-VI) , Сиэтл, Вашингтон, июль 2008 г.
Сарвани Ваккаланка, Майкл Делиси, Ганеш Гопалакришнан, Роберт М. Кирби, Раджив Такур и Уильям Гропп, « Внедрение эффективных динамических формальных методов проверки для программ MPI, последние достижения в области параллельных виртуальных машин и интерфейса передачи сообщений» (EuroPVM / MPI 2008) , Дублин, Ирландия, 2008 г., LNCS 5205, стр. 248–256.
Сарвани Ваккаланка, Субодх Шарма, Ганеш Гопалакришнан и Роберт М. Кирби, ISP: Инструмент для проверки моделей программ MPI, принципов и практик параллельного программирования (PPoPP 2008) , Солт-Лейк-Сити, февраль 2008 г., стр. 285–286.
Салман Первез, Роберт Палмер, Ганеш Гопалакришнан, Роберт М. Кирби, Раджив Такур и Уильям Гропп, Практические методы проверки моделей для проверки правильности программ MPI, Последние достижения в области параллельных виртуальных машин и интерфейса передачи сообщений (PDF) (EuroPVM / MPI) , Париж, 344–353, LNCS 4757, Франция, 30 сентября - 3 октября 2007 г.
Процитировано
Объединение символьного выполнения с проверкой модели для проверки параллельных числовых программ , umass.edu PDF С.Ф. Сигель, А. Миронова, Г.С. Аврунин, Л.А. Кларк - Транзакции ACM по программной инженерии и методологии - portal.acm.org
Проверка свойств остановки для программ MPI с использованием неблокирующих операций
- psu.edu PDF
С.Ф. Сигель, Г.С. Аврунин - Конспект лекций по информатике, 2007 - Springer
MPIWiz: воспроизводимое воспроизведение подгруппы приложений MPI R Xue, X Liu, M Wu, Z Guo, W Chen, W Zheng, Z Zhang, Geoffrey M. Voelker Tsinghua University, Microsoft Research Asia, University of Southern California San Diego - cs.ucsd .edu
Динамическое тестирование параллельных приложений на основе потоковых графов
- epfl.ch [1]
B Schaeli, RD Hersch - Труды 6-го семинара по параллельному и распределенному программированию, 2008 г. - portal.acm.org
Визуальная отладка приложений MPI
- epfl.ch PDF
Б. Шаэли, А. Аль-Шабиби, Р. Д. Херш - Труды 15-й Европейской группы пользователей PVM / MPI…, 2008 г. - Springer