Анализ и верификация задержек в микроархитектуре коммуникационных фабрик

• Автор: Викторов, Юрий Олегович
• Шифр специальности: 05.13.05
• Научная степень: Кандидатская
• Год защиты: 2013
• Место защиты: Санкт-Петербург
• Количество страниц: 142 с. : ил.

Оглавление
ВВЕДЕНИЕ
ГЛАВА 1. ПОДХОДЫ К РЕШЕНИЮ ЗАДАЧИ АНАЛИЗА КАЧЕСТВА ОБСЛУЖИВАНИЯ В КОММУНИКАЦИОННЫХ ФАБРИКАХ

1.1 Понятие коммуникационной фабрики

1.2 ПОНЯТИЯ КАЧЕСТВА ОБСЛУЖИВAI1ИЯ

1.3 Проблемы проектирования коммуникационных фабрик

1.4 Механизмы обеспечения качества обслуживания

1.5 Существующие подходы к анализу производительности

1.6 Промышленные средства формальной верификации

Выводы
ГЛАВА 2. ФОРМАЛИЗАЦИЯ СУЖДЕНИЯ О ЗАДЕРЖКЕ
2.1 . Базовые понятия, используемые в суждении о задержке
2.2 Вычисление задержки для сложных отношений отклика
2.3 Ранжирующие функции и связанные с ними понятая
2.4 Использование ранжирующих функций при доказательстве максимальных
задержек
Выводы
ГЛАВА 3. МОДЕЛИРОВАНИЕ МИКР О АРХИТЕКТУРЫ С ПОМОЩЬЮ
СРЕДСТВ ЯЗЫКА XMAS
3.1 Общее представление о среде моделирования xMAS
3.2 Канальный протокол xMAS и его устойчивость
3.3 Уравнения базовых примитивов xMAS
3.3.1 Исток (source)
3.3.2 Сток (sink)
3.3.3 Очередь (queue)
3.3.4 Преобразование (function)
3.3.5 Форк (fork)

3.3.6 Барьер (join)
3.3.7 Ветвление (switch)
3.3.8 Слияние (merge)
3.4 Расширение xMAS для описания временных характеристик микроархитектуры
3.4.1 Специфические алгоритмы арбитража
3.4.2 Ограниченная задержка (delay)
3.4.3 Формирователь потока (shaper)
3.5 Анализ канальных свойств моделей xMAS
3.5.1 Канальные свойства
3.5.2 Распространение канальных свойств
3.5.3 Алгоритм распространения канальных свойств
3.6 Потоковые инварианты
3.6.1 Базовый принцип
3.6.2 Разделяемые каналы передачи данных
3.6.3 Алгоритм обнаружения потоковых инвариантов.
Выводы
ГЛАВА 4. АНАЛИЗ И ВЕРИФИКАЦИЯ ГРАНИЦ ЗАДЕРЖЕК В МОДЕЛЯХ НА ЯЗЫКЕ XMAS
4.1 Базовая задача анализа задержек в микроархитектурной модели
4.2 Локальные задержки в моделях xMAS
4.3 Использование формализма для суждения о задержке в анализе моделей XMAS
4.4 Распространение локальных задержек и макроправила
4.4.1 Базовый принцип вычисления локальных задержек
4.4.2 Макроправила
4.4.3 Связь макроправил с базовыми правилами вывода для задержки
4.4.4 Абстрагирование макроправил распространения задержек через примитив
слияния от используемого алгоритма арбитража
4.5 Нахождение порядка распространения локальных задержек с помощью макроправил
4.6 Вычисление задержек прохождения пакета по траектории
4.7 Контекст вывода задержки и циклические зависимости
4.7.1 Понятие контекста вывода задержки и его связь с макроправилами
4.7.2 Разделение макроправил распространения задержек на частные случаи в
зависимости от переменных состояния
4.7.3 Вывод задержки для модели, содержащей управляющие циклы

4.7.4 Использование контекста в выводе задержки
4.7.5 Алгоритм вывода задержек при учете контекста
4.8 Верификация выведенных задержек для моделей xMAS
4.9 Дорожная карта анализа и верификации задержек в микроархитектуре
Выводы
ГЛАВА 5. ЭКСПЕРИМЕНТАЛЬНЫЕ РЕЗУЛЬТАТЫ ПРИМЕНЕНИЯ ПРЕДЛАГАЕМОГО ПОДХОДА К АНАЛИЗУ И ВЕРИФИКАЦИИ ЗАДЕРЖЕК
5.1 Методика проведения экспериментов, да1 и 1ые и их анализ..
5.2 Модели малого размера
5.3 Модели большого размера
Выводы
ЗАКЛЮЧЕНИЕ
СПИСОК ЛИТЕРАТУРЫ
ПРИЛОЖЕНИЕ 1. АКТ ВНЕДРЕНИЯ В ПРОИЗВОДСТВО
ПРИЛОЖЕНИЕ 2. АКТ ВНЕДРЕНИЯ В УЧЕБНЫЙ ПРОЦЕСС

В включительно. Целочисленная неотрицательная величина ф называется ранжирующей функцией для отношения отклика А **Е В, если
С((Л: В) ■ -лВ -» ф+ < ф - [Е]), где [Я] - индикатор события Е . Обозначение ф+ соответствует значению величины ф на следующем такте. Условие (А: В) • —В означает, что событие А уже наступило, а событие В - еще нет. Подводя итог, данное выражение требует невозрастания ф при Е = False и строгого убывания ф при Е = True.
Значение ф можно считать “мерой” расстояния от текущего момента времени до наступления события В (по модулю события Е). Пусть дана некоторая замкнутая материальная система, для которой А, В и Е входят во множество наблюдаемых свойств. Причем Lat[/1 В] < к для некоторого к . Тогда утверждается, что среди наблюдаемых свойств такой системы можно найти и такую величину ф, которая будет являться ранжирующей функцией для данного
отношения отклика. Т.е. всякая система с конечными задержками также содержит
• ,. . • ' • * -У-:
(в явной или неявной форме) величину, которую можно интерпретировать как
«счётчик» специального вида, измеряющий число тактов до наступления
постусловия. В случае цифровой схемы, величина ф вычисляется как функция от
текущего состояния элементов памяти. На практике точное нахождение ф требует
учета большого числа подробностей, поэтому находят приближенную функцию
ф, оценивающую сверху время до наступления постусловия.
Вопрос поиска соответствующей функции ф для микроархитектурных моделей коммуникационных фабрик на языке xMAS рассмотрен в главе 4.
Рисунок 2.6 иллюстрирует поведение ранжирующей функции для отношения отклика A 'V'g В.
Как видно на рисунок 2.6, поведение ранжирующей функции за пределами интервала (А: В) может быть произвольным. При этом событие В может наступить раньше, чем согласно ожиданиям. Интервал (Л: 5) разбит на меньшие интервалы, на которых событие модуль Еили появляется на каждом шаге (step)