Инструмент формальной проверки интернет-провайдера - ISP Formal Verification Tool

ISP («Частичный заказ на месте») - это инструмент для формальной проверки MPI программы, разработанные в Школе вычислительной техники Университета Юты. подобно модельные шашки, Такие как ВРАЩЕНИЕ, Провайдер проверяет полное пространство состояний системы для набора свойства безопасности. Однако, в отличие от программ проверки моделей, ISP выполняет проверка уровня кода. Это означает, что инструмент проверяет все соответствующие чередования параллельной программы путем воспроизведения реального программного кода без построение верификационных моделей. Эта идея была впервые реализована в ряде инструментов, в частности, Годфроидом в его инструменте VeriSoft.[1]Среди других недавних инструментов этого жанра - Java Pathfinder, инструмент Microsoft CHESS и MODIST. Соответствующие чередования вычисляются с использованием настраиваемого динамическая редукция частичного порядка[2] алгоритм называется POE.[3]

ISP использовался для успешной проверки до 14 000 строк кода MPI / C на наличие взаимоблокировок и нарушений утверждений. В настоящее время он поддерживает более 60 MPI 2.1 функций и был протестирован с MPICH2, OpenMPI,и Microsoft MPI библиотеки.

Интернет-провайдер доступен для загрузки для linux и Mac OS X; как Visual Studio плагин для работы под Windows, и как Затмение плагин ..

Рекомендации

  1. ^ Патрис Годфройд, Проверка моделей для языков программирования с помощью VeriSoft POPL 1997
  2. ^ Кормак Фланаган и Патрис Годфройд, Динамическая редукция частичного порядка для программного обеспечения проверки моделей,, POPL 2005, стр. 110-121, ACM, ISBN  1-58113-830-X
  3. ^ Сарвани Ваккаланка, Ганеш Гопалакришнан и Роберт М. Кирби, Динамическая проверка программ MPI с уменьшением наличия операций разделения и упрощенных порядков, Компьютерная проверка (CAV 2008), стр. 66-79, LNCS 5123.

Ань Во, Сарвани Ваккаланка, Майкл Делиси, Ганеш Гопалакришнан, Роберт М. Кирби и Раджив Тхакур, Официальная проверка практических программ MPI, PPoPP 2009

Сарвани Ваккаланка, Майкл Делиси, Ганеш Гопалакришнан и Роберт М. Кирби, Рекомендации по планированию создания инструментов динамической проверки для MPI, Параллельные и распределенные системы - тестирование и отладка (ПАДТАД-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, Джеффри М. Фолькер, Университет Цинхуа, Microsoft Research Asia, Университет Южной Калифорнии в Сан-Диего - cs.ucsd.edu

Динамическое тестирование параллельных приложений на основе потоковых графов

- epfl.ch [1]

B Schaeli, RD Hersch - Труды 6-го семинара по параллельному и распределенному программированию, 2008 г. - portal.acm.org

Визуальная отладка приложений MPI

- epfl.ch PDF

Б. Шаэли, А. Аль-Шабиби, Р. Д. Херш - Труды 15-й Европейской группы пользователей PVM / MPI…, 2008 - Springer

внешняя ссылка