Формальные модели и анализ корректности параллельных систем и систем реального времени

• Автор: Вирбицкайте, Ирина Бонавентуровна
• Шифр специальности: 05.13.11
• Научная степень: Докторская
• Год защиты: 2001
• Место защиты: Новосибирск
• Количество страниц: 286 с. : ил

Содержание
Введение

1 Формальные модели потоковых вычислений и их автоматическое построение

1.1 Обзор исследований в области потоковой обработки информации .

1.1.1 Архитектуры потоковых вычислительных систем .

1.1.2 Потоковые языки программирования

1.2 Потоковые схемы с тегированными фишками.

1.2.1 Определение потоковой схемы с тегированными фишками псхемы.

1.2.2 Структурированные псхемы

1.2.3 Псхемы с массивами

1.2.4 Псхемы с процедурами

1.3 Автоматическое построение потоковых схем с тегированными фишками
1.3.1 Некоторые атрибуты ссхем
1.3.2 Преобразование ациклических ссхем в потоковый
1.3.3 Преобразование ссхем, содержащих циклические фрагменты. в потоковый вид
1.3.4 Преобразование обогащенных ссхем в обогащенные структурированные псхемы.
2 Сравнительный анализ семантических моделей параллельных процессов и процессов реального времени
2.1 Аксиомы параллельности как базовые свойства параллельных недетерминированных процессов.
2.1.1 Первичные структуры событий и их свойства параллельности .
2.1.2 Локальные структуры событий и их свойства параллельности
2.2 Семантические модели потоковых вычислений с тегированными фишками.
2.2.1 Графы зависимостей.
2.2.2 Семантика структур событий.
2.3 Бисимуляционные эквивалентности параллельных недетерминированных процессов и их логическая характеризация
2.3.1 Бисимуляционные эквивалентности
2.3.2 Логическая характеризация обычных бисимуляций
2.3.3 Логическая характеризация локальных бисимуляций
2.3.4 Разрешимость бисимуляционных эквивалентностей
2.4 Исследование параллельной семантики процессов реального времени.
2.4.1 Временные структуры событий
2.4.2 Интерливинговая семантика
2.4.3 Шаговая семантика .
2.4.4 Семантика временных частично упорядоченных мультимножеств
2.4.5 Сравнение временных эквивалентностей.
Анализ корректности параллельных моделей реального времени
3.1 Верификация временных сетей Петри с использованием аппарата темпоральных логик реального времени
3.1.1 Базовый метод верификации
3.1.2 Метод с использованием техники частичных порядков
3.1.3 Метод с использованием техники временных зон . .
3.1.4 Метод с использованием техники параметризации .
3.2 Верификация временных сетей Петри посредством проверки на поведенческую эквивалентность
3.2.1 Временные процессы и эквивалентностные понятия
временных сетей Петри.
3.2.2 Распознавание временной трассовой и временной тестовой эквивалентностей
3.2.3 Распознавание временной бисимуляции
3.3 Автоматические анализ и верификация сетевых параллельных моделей реального времени .
3.3.1 Обзор инструментальных средств, поддерживающих
сетевые модели
3.3.2 Краткое описание возможностей системы РЕР . . .
3.3.3 Концепции, организация и возможности системы
Заключение
Приложение
Список литературы


Так как в статических ЭВМ только один экземпляр вершины может быть обработан в некоторый момент времени, то возникают препятствия для параллельной реализации различных итераций циклов и вызовов рекурсивных процедур. Такая организация вычислений не позволяет эффективно использовать программный параллелизм, особенно при обработке массивов данных. Однако алгоритмы, в которых преобладает конвейерный тип параллелизма, могут эффективно выполняться на статических машинах с сигналами подтверждений. Динамические ЭВМ за счет возможности эффективного выполнения в них массовых параллельных вычислений способны обеспечивать наибольшее ускорение при достаточном числе ПЭ. В такого типа машинах невозможно определить физический адрес команды в памяти до начала вычислений, а также ПЭ, на который она будет назначена для исполнения. Если память фишек имеет значительные размеры, то программный код и фишки данных целесообразно хранить раздельно. ПЭ. Реентерабельные вычисления поддерживаются механизмами тегирования фишек, копирования кода, организации очередей. Рис. Схема ПЭ потоковой машины с аппаратом обмена тегированными фишками показана на рис. СФ. В устройстве формирования исполнительных команд поступившие из СФ наборы фишек объединяются с копией описания вершины, взятого из памяти команд. Сформированные исполнительные команды передаются в функциональное устройство. В большинстве машин с подобной архитектурой количество входных дуг вершин реализуемых потоковых схем ограничивается двумя. При получении фишки СФ комбинирует ее адрес назначения и тег в некоторый физический адрес и проверяет наличие по этому адресу фишки-партнера, то есть фишки с теми же тегом и адресом назначения. Для сбора фишек-партнеров используется либо динамическое хэширование, либо ассоциативная память. При поступлении в циклические фрагменты и при входе в процедуры фишкам должна быть присвоена уникальная подобласть тега. Обеспечение уникальности в параллельных ЭВМ всегда проблематично. Известно, что при централизованном подходе к решению этой проблемы генерация уникальных тегов становится узким местом машины. При распределенном подходе уникальность тега поддерживается образованием новых подобластей при каждом вызове процедуры. Увеличение размеров тега приводит к значительным накладным расходам, связанными с передачей фишек через коммутационную сеть. Во многих проектах потоковых ЭВМ используется частично распределенный подход. Например, централизованный счетчик ПЭ, который за счет уникальной идентификации процессора обеспечивает уникальность связанной с ним подобласти тега. Для динамических машин с копированием кода характерно отсутствие тегов, а следовательно, готовность вершин к срабатыванию определяется посредством счетчиков входов. При копировании фрагментов потоковых схем необходимо динамическое выделеиие памяти, а также других ресурсов, что приводит к проблемам, сходным с проблемами в тегированных машинах. В некоторых динамических машинах для различия экземпляров вычислений используется механизм очередей. Операнды для текущего экземпляра команды должны быть взяты ‘на фронте’ очередей фишек. Как правило, подобного рода ЭВМ реализуют ациклические рекурсивные потоковые схемы. Достоинством такой организации вычислений является отсутствие накладных расходов на генерацию и модификацию тегов фишек. В следующих разделах дан обзор и анализ наиболее известных потоковых проектов, представленных в классификации рис. Рис. Потоковые ЭВМ с прямой организацией связей. Проект DDM1. Первая действующая потоковая система DDM1 |6], созданная в г. Дэвиса из фирмы Burroughs, является, пожалуй, самым известным представителем класса потоковых машин с прямой организацией связей. Динамические реентерабельные вычисления поддерживаются механизмом FIFO-очередей. Программирование в системе осуществляется на функциональном языке высокого уровня GPL. Генерируемые компилятором потоковые схемы имеют вид иерархически вложенных строковых структур переменной длины. Формат программной команды состоит из полей: кода операции, списка адресов назначения результата, операндов, счетчика готовности. Рис.