Анализ и верификация задержек в микроархитектуре коммуникационных фабрик тема диссертации и автореферата по ВАК РФ 05.13.05, кандидат наук Викторов, Юрий Олегович

• Викторов, Юрий Олегович
• кандидат наук
• 2013

Оглавление диссертации кандидат наук Викторов, Юрий Олегович

Оглавление

ВВЕДЕНИЕ

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

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

1.2 понятия качества обслуживания

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 Барьер Coin)

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 Использование формализма для суждения о задержке в анализе моделей XMAS73

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 Методика проведения экспериментов, данные и их анализ

5.2 Модели малого размера

5.3 Модели большого размера

Выводы

ЗАКЛЮЧЕНИЕ

СПИСОК ЛИТЕРАТУРЫ

ПРИЛОЖЕНИЕ 1. АКТ ВНЕДРЕНИЯ В ПРОИЗВОДСТВО

ПРИЛОЖЕНИЕ 2. АКТ ВНЕДРЕНИЯ В УЧЕБНЫЙ ПРОЦЕСС

Введение диссертации (часть автореферата) на тему «Анализ и верификация задержек в микроархитектуре коммуникационных фабрик»

Введение

Актуальность работы. Рост сложности микропроцессорной архитектуры и требований к её производительности и масштабируемости привел к отказу от общей шины как средства коммуникации между узлами микропроцессора и переходу на использование так называемых коммуникационных фабрик (Communication Fabrics).

Коммуникационные фабрики - это современные системы межсоединений узлов системы на кристалле, для которых характерна одновременная обработка множества запросов, за счет глубокого параллелизма и конвейеризации.

Архитектура коммуникационных фабрик может быть самой разнообразной, в зависимости от области применения. Для северного комплекса микросхем потребительской электроники (исторически «северный мост» - контроллер-концентратор памяти) характерна централизованная структура. Южный комплекс (исторически «южный мост» — контроллер-концентратор " ввода-вывода) традиционно имеет древовидную иерархическую структуру. Для серверов применяют распределенные архитектуры типа «сеть на кристалле» (Network on Chip, NoC), такие как кольца и решетки.

Ресурсы в системах на кристалле (размеры очередей, разрядности шин, и т.д.), как правило, ограничены, а производительность и корректность работы системы сильно зависят от эффективности их разделения конкурирующими процессами. Поэтому при проектировании коммуникационных фабрик требуется учитывать минимальный уровень качества обслуживания. Несоблюдение требуемого уровня качества обслуживания приводит к разнообразным последствиям. Например, выпадение кадров при проигрывании видео, или прерывистое воспроизведение звука. Попытка же решить данную проблему увеличением количества ресурсов приводит к удорожанию системы.

В контексте анализа качества обслуживания в коммуникационных фабриках наибольший интерес представляют следующие характеристики:

• форма потока - объем данных, переданных потоком, начиная с некоторого момента времени t0; для описания формы потока часто используют показатели средней плотности (rate, bandwidth) и величины всплеска (burst);

• задержка передачи (latency) - интервал времени между отправлением данных источником и их получением в точке назначения;

• вариация задержки (jitter) — разница между максимальным и минимальным значениями задержки в потоке данных.

Данная работа посвящена анализу задержек передачи.

Существуют две категории подходов к проектированию коммуникационных фабрик, призванных обеспечить гарантии качества обслуживания "по построению": подходы на основе дифференциации потоков (traffic differentiation) и на основе передачи данных без конкуренции (contention-free transmisson). Задача выполнения требований качества обслуживания не может быть в полной мере решена использованием этих подходов. Указанные подходы не предлагают ни эффективного способа борьбы с проблемой истощения ресурсов, ни способов оценки задержек на этапе резервирования ресурсов. Требуются надежные и эффективные методы оценки гарантий качества обслуживания, предоставляемых коммуникационной фабрикой, применимые на ранних этапах разработки микроархитектуры, т.к. обнаруженные на поздних стадиях ошибки не всегда могут быть эффективно исправлены. Это приводит к удорожанию и срыву сроков разработки, что неприемлемо в условиях жестких временных ограничений. Проектирование системы на кристалле для потребительской электроники (мобильные устройства и т.д.) не должно занимать более полугода и малейшие срывы сроков являются фатальными. Практически каждое такое решение

ориентировано на конкретный конечный продукт, который безнадежно устареет к моменту появления на рынке при больших сроках проектирования.

В настоящее время для анализа производительности систем на кристалле используют имитационное моделирование и набор формальных методов. Однако все существующие на данный момент методы имеют ряд серьезных недостатков: либо не дают никаких гарантий, кроме статистических (имитационное моделирование), либо требуют нереалистичных упрощений исходной задачи (аналитические методы), либо не масштабируются на объекты размеров коммуникационной фабрики (формальная верификация), либо требуют чрезмерных усилий и затрат для их применения (методы доказательства теорем).

Жесткие требования к срокам разработки на практике означают, что этап разработки микроархитектуры системы на кристалле не может занимать более месяца. Соответственно, на первый план выходит получение как можно более оперативного ответа, как изменения микроархитектуры отражаются на её характеристиках. Традиционный подход, когда одна итерация верификации выполняется неделями, здесь неприемлем.

Анализ качества обслуживания тесно связан с подходом к моделированию микроархитектуры коммуникационных фабрик, в качестве которого предлагается использовать среду моделирования xMAS. Среда моделирования xMAS (executable Microarchitecture Specification) была специально разработана для высокоуровневого моделирования микроархитектуры в простой и наглядной форме.

Модели xMAS конструируются из небольшого числа параметризованных стандартных блоков (примитивов), соединенных каналами в синхронную сеть передачи пакетов. Примитивы выполняют простые операции над пакетами данных. Например, queue (очередь) выполняет буферизацию пакетов, сохраняя порядок их следования, а примитивы join и fork играют роль барьеров, синхронизируя передачи на входных и выходных каналах.

Для верификации моделей xMAS используются как специализированные алгоритмы, так и средства верификации моделей общего назначения. Модель xMAS всегда может быть автоматически представлена в виде эквивалентного описания на языке Verilog, к которому применимы методы символьной верификации, такие как ограниченная верификация (bounded model checking, ВМС), интерполяция, k-индукция и т.д. Область применения средств верификации общего назначения можно существенно расширить, используя структурный анализ модели для автоматического порождения вспомогательных лемм.

Модели xMAS успешно применялись для обнаружения тупиковых ситуаций (deadlocks) и формального доказательства их отсутствия. Однако моделирование качества обслуживания требует учета большего числа деталей и требует расширения набора примитивов xMAS.

Цель исследования. Цель диссертационной работы состоит в разработке метода автоматического вывода верхней границы на задержку передачи данных в микроархитектурных моделях коммуникационных фабрик, формальной верификации этой границы за время, не превышающее несколько часов. А также в исследовании возможностей, ограничений и области возможного применения разработанного метода.

Для достижения данной цели в диссертационной работе решаются следующие задачи:

• расширение языка моделирования xMAS для представления в моделях временных характеристик микроархитектуры коммуникационных фабрик, в частности, введение в язык новых примитивов;

• построение математического аппарата для описания задержки передачи данных и формализация суждения о задержке в моделях xMAS;

• разработка алгоритмов для автоматического анализа структуры модели, получения оценки сверху на задержку передачи данных и верификации этой оценки за малое время (<24 часов);

• проведение серии экспериментов над моделями коммуникационных фабрик и их частей, имеющих разные размеры, с целью изучения возможностей разработанного подхода.

Научная новизна работы. Научная новизна данной диссертационной работы заключается в следующем:

• предложена математическая модель для описания задержки между событиями и формализовано суждение о задержке;

• разработан алгоритм, позволяющий автоматически получить верхнюю границу задержки передачи данных, анализируя структуру микроархитектурной модели, представленной на языке xMAS;

• предложен новый подход, позволяющий в процессе вывода верхней

н ( [f

границы задержки сконструировать её доказательство с помощью метода k-индукции, при использовании которого глубина индукции не зависит от величины доказываемой задержки.

Методы исследования. Для решения поставленных задач использовались:

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

• язык линейной темпоральной логики (LTL) - как удобное средство спецификации свойств модели xMAS, относящихся к задержке, и построения суждений о задержке;

• сторонние инструментальные средства: ABC Berkeley [1] - для ограниченной верификации моделей и доказательства утверждений методом k-индукции, Synopsis VCS - для имитационного моделирования описаний на языке Verilog;

• подход на основе ранжирующих функций для построения эффективно проверяемых доказательств границы на задержку передачи.

Программная реализация. На базе предложенных алгоритмов создан программный прототип для автоматического анализа микроархитектурных моделей, записанных на языке хМАЗ, получения оценки сверху на задержку передачи данных и её верификации. Верификация осуществляется путем конструирования вывода для задержки, каждый шаг которого проверяется с помощью методов к-индукции для малых значений к, не зависящих от величины доказываемой задержки.

Основные положения и результаты, выносимые на защиту. На защиту выносятся следующие результаты, полученные автором в процессе проведения исследований:

• расширение языка хМА8 для представления в микроархитектурных моделях свойств, связанных с временными характеристиками;

• математическое описание понятия задержки между событиями и формализация процесса суждения о задержке;

• алгоритмическая схема анализа моделей хМАБ для получения оценок сверху на задержку передачи данных из одной точки в другую;

• подход к построению доказательств полученных временных оценок для широкого класса моделей, использующий метод к-индукции;

• ограничение глубины индукции доказательства малым значением к за счет использования ранжирующих функций;

• продемонстрировано сокращение времени верификации задержек на несколько порядков, при допустимом уровне консервативности получаемых оценок.

Практическая значимость работы заключается в предложенном новом подходе к анализу микроархитектурных моделей, позволяющем получить оценки сверху на задержку передачи данных и эффективно верифицировать данные

оценки, используя стандартные средства формальной верификации. Экспериментально подтверждена применимость нового подхода к анализу моделей реальных коммуникационных фабрик, используемых в современных микропроцессорах, в то время, как традиционные подходы к верификации оценок не позволяют получить ответ в течение недели на моделях подобных размеров (так для модели, состоящей из ~400 примитивов и ~50 очередей, с оценкой на пространство состояний ~10Л500, предлагаемый подход позволяет провести доказательство за ~30 сек., а стандартными средствами доказательство не удаётся выполнить за неделю).

Апробация работы. Основные теоретические и практические результаты работы были представлены на конференциях:

• V Всероссийская научно-техническая конференция "Проблемы разработки перспективных микро- и наноэлектронных систем" МЭС-2012, ИППМ РАН, 1 доклад (2012);

? ^' [ I

• 37-ая международная научная конференция «Гагаринские чтения», МАТИ, 1 доклад (2011).

Публикация результатов исследования. Результаты диссертации отражены в 5 публикациях, в том числе 3 входят в перечень научных журналов и изданий, рецензируемых ВАК.

Структура и объем работы. Диссертационная работа состоит из введения, 5 глав, заключения и списка литературы. Работа содержит 140 страниц машинного текста, 33 графика и рисунка, 17 таблиц, список литературы из 111 наименований и 2 приложения.

В первой главе описываются проблемы, с которыми разработчики сталкиваются при проектировании коммуникационных фабрик, и объясняется необходимость обеспечения определенных гарантий производительности. Рассматриваются существующие подходы к обеспечению таких гарантий, и

обосновывается необходимость разработки нового метода для анализа качества обслуживания.

Во второй главе изложен подход к формализации понятия задержки, анализу которых посвящена данная работа, и построению доказательств границы задержки, которая может быть эффективно верифицирована.

В третьей главе приводится описание среды моделирования хМАБ, используемой для моделирования микроархитектуры коммуникационных фабрик, и её инфраструктурных расширений.

В четвертой главе описывается алгоритм, разработанный для анализа моделей на языке хМАБ, и вывода оценки сверху на задержку передачи данных.

В пятой главе приводятся результаты экспериментов с разработанным алгоритмом и их интерпретация.

Глава 1. Подходы к решению задачи анализа качества обслуживания в коммуникационных фабриках

В данной главе вводятся понятия коммуникационной фабрики и качества обслуживания. Описываются проблемы, с которыми разработчики сталкиваются при проектировании коммуникационных фабрик, и объясняется необходимость обеспечения фабрикой определенных гарантий производительности для узлов системы на кристалле. Рассматриваются существующие механизмы обеспечения качества обслуживания и, на основе их недостатков, утверждается, что эта задача не может быть эффективно решена «по построению» для архитектуры общего вида.

Приводится обзор существующих подходов, применяемых для анализа качества обслуживания, описываются их достоинства и недостатки. Утверждается, что ни один из существующих подходов в полной мере не удовлетворяет требованиям разработчиков, и обосновывается необходимость разработки нового метода анализа.

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

Исторически отдельные узлы и устройства внутри интегральных схем микропроцессоров взаимодействовали друг с другом через общую (широковещательную) шину. Однако при числе устройств достигающем десятков и сотен [2], шинная архитектура соединений становится непригодной из-за ограниченной пропускной способности и масштабируемости (использование одной и той же архитектуры межсоединений в системах с разным числом процессорных ядер и разным составом других функциональных блоков). Рост степени интеграции полупроводниковых кристаллов, сложности микропроцессорной архитектуры и требований к производительности системы межсоединений привел к тому, что практика использования общей шины как

средства коммуникации между узлами микропроцессора осталась в прошлом, уступив место коммуникационным фабрикам (Communication Fabrics).

Коммуникационные фабрики — это современные системы межсоединений узлов системы на кристалле, для которых характерны хранение и параллельная обработка множества запросов [40].

Архитектура коммуникационных фабрик может существенно различаться, в зависимости от области применения. Для северного комплекса микросхем потребительской электроники (исторически «северный мост» - контроллер-концентратор памяти) характерна централизованная структура. Южный комплекс (исторически «южный мост» - контроллер-концентратор ввода-вывода) традиционно имеет древовидную иерархическую структуру [4]. Для серверов применяют распределенные архитектуры типа «сеть на кристалле» (Network on Chip, NoC), такие как кольца и решетки [16].

1.2 Понятия качества обслуживания ?

Для понятия качества обслуживания существуют различные формулировки, привязанные к разным предметным областям [107]. В наиболее общем виде, качество обслуживания (англ. Quality of Service, QoS) — это способность системы обеспечивать своим агентам определенные измеряемые гарантии по обработке потоков данных, касающиеся производительности, надежности, безопасности и т.д.

Для описания уровня качества обслуживания существует большое разнообразие метрик. Некоторые метрики качества обслуживания тесно связаны друг с другом или могут быть выражены друг через друга. Например, нулевая вероятность потери данных эквивалентна требованию гарантии доставки [107]. Для каждой конкретной цели выбирается определенный базис метрик, исходя из свойств предметной области, задач и предполагаемых методов их решения.

Потоком данных мы будем называть совокупность сообщений, обладающих каким-либо общим признаком, например, сообщения от одного источника. В контексте анализа качества обслуживания в коммуникационных фабриках наибольший интерес представляют следующие характеристики:

• форма потока - объем данных, переданных потоком, начиная с некоторого момента времени t0; для описания формы потока часто используют показатели средней плотности (rate, bandwidth) и величины всплеска (burst) [8, 20];

• задержка передачи (latency) - интервал времени между отправлением данных источником и их получением в точке назначения;

• вариация задержки (jitter) - разница между максимальным и минимальным значениями задержки в потоке данных.

Данная работа посвящена анализу задержек передачи сообщений из одной точки в другую.

(

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

Аппаратные ресурсы в системах на кристалле (такие как: размеры очередей, разрядности шин, и т.д.), как правило, ограничены, так как увеличение количества таких ресурсов, приводит к увеличению площади, занимаемой устройством на кремнии, а площадь является критическим ресурсом. При этом производительность и корректность работы системы сильно зависят от эффективности разделения общих аппаратных ресурсов конкурирующими процессами. Для коммуникационных фабрик такими процессами являются одновременно протекающие транзакции обмена данными между узлами системы [41]. Поэтому при проектировании коммуникационных фабрик требуется учитывать минимальный уровень обслуживания, который система на кристалле должна гарантировать своим агентам для их корректной работы (уровень качества обслуживания) [103].

Несоблюдение требуемого уровня качества обслуживания приводит к разнообразным негативным для работы системы последствиям. Из них для конечного пользователя наиболее заметны такие проблемы, как выпадение кадров при проигрывании видео, прерывистое воспроизведение звука или зависание системы, в случае возникновения тупикового состояния (deadlock). Попытка же решить проблему качества обслуживания необоснованным увеличением количества ресурсов приводит к серьезному удорожанию системы.

Некорректное взаимодействие агентов и фабрики может приводить к нарушению целостности памяти, возникновению тупиковых ситуаций, истощению ресурсов и другим проблемам, которые не могут быть обнаружены при анализе частей системы по отдельности [88]. А поскольку полностью система доступна лишь на поздних стадиях разработки, то и многие ошибки можно обнаружить лишь на этапе системной интеграции или даже отладки изготовленного кристалла (Post-Si) (отладки, связаной с анализом процессов, протекающих в тестовых образцах полупроводниковых кристаллов^ изготавливаемых перед запуском серийного производства). На данных стадиях ошибки уже невозможно быстро и эффективно исправить. Это приводит к удорожанию проекта, срыву сроков разработки или даже отзыву готовой продукции, что неприемлемо в условиях современной экономики.

Экономическая сторона проблем заключается в следующем.

С одной стороны, себестоимость полупроводникового кристалла пропорциональна его площади. Каждый последующий технологический процесс, по сравнению с предыдущим, имеет более высокую себестоимость на единицу площади [2]. При этом скорость уменьшения транзисторов с переходом на каждую последующую технологию замедляется, а масштабирование межсоединений после технологии 32нм практически остановилось.

С другой стороны, за годы стремительного и дешевого масштабирования техпроцесса у потребителей сформировалось ожидание, что каждое следующее поколение микросхем оказывается дешевле предыдущего.

В итоге, сейчас ценовой диапазон между себестоимостью и рыночной ценой сокращается с двух сторон, вынуждая при разработке систем на кристалле решать задачу оптимизации — минимизации занимаемой на кристалле площади при сохранении допустимой производительности.

Сроки устаревания устройств потребительской электроники, планирование производства конечной продукции и сроки выхода новых продуктов на рынок приводят к появлению жестких временных рамок и общему сокращению сроков проектирования систем на кристалле. Проектирование системы на кристалле (на основе готовых 1Р ядер и подсистем), ориентированной на потребительскую электронику (мобильные устройства и т.д.), не должно занимать более полугода и малейшие срывы сроков являются фатальными. Практически каждая система на кристалле для потребительской электроники ориентирована на конкретный конечный продукт, который, при больших сроках проектирования, окажется неконкурентоспособным к моменту появления на рынке.

На сегодняшний день на рынке потребительской электроники наблюдается широчайшее разнообразие устройств. Современный подход к проектированию таких устройств, основанный на интеграции 1Р, и сроки их разработки указывают на необходимость стандартизации используемых подсистем. При этом важно сохранение гибкости таких подсистем и возможность их применения в широком диапазоне различных устройств. Как правило такие системы имеют большое количество настраиваемых параметров, напрямую влияющих на их характеристики. Конфигурирование подсистемы превращается в отдельную сложную задачу, решение которой напрямую влияет на производительность, корректность и другие аспекты функционирования устройства. Задача оптимизации размера очередей достаточно успешно решается для асинхронных

[77] и эластичных синхронных [23, 24] спецификаций. Но это только небольшая часть структур используемых в современных коммуникационных фабриках.

Жесткие требования к срокам разработки означают, что этап разработки микроархитектуры системы на кристалле не может занимать более месяца. Соответственно, на первый план выходит получение как можно более оперативного ответа, какими характеристиками (в том числе и с точки зрения качества обслуживания) обладает микроархитектура и как вносимые в микроархитектуру изменения отражаются на её характеристиках. Ускорение получения подобных оценок позволяет перебрать большее количество конфигураций и получить более качественное решение задачи оптимизации. Традиционный подход, когда одна итерация верификации выполняется неделями, здесь неприемлем.

Требования качества обслуживания далеко не всегда достаточно формализованы [107]. Проектные спецификации часто составляют в виде текстового описания на естественном языке и без использования ясных метрик, что затрудняет их анализ. Принят подход описания требований качества обслуживания на основе примеров, когда вместо формальной спецификации требований, приводится ряд типовых сценариев работы системы и желаемое поведение. Формализация такого описания требует значительных усилий по его уточнению.

Проектирование коммуникационных фабрик осложняется большим числом второстепенных факторов. Например, обработка конкурирующих запросов и динамическое управление энергопотреблением может приводить к неравномерному использованию ресурсов и большому разбросу значений задержки. Грубая оценка по наихудшему случаю часто оказывается чрезмерно консервативной и недостижимой на практике, а получение точных оценок связано с большой вычислительной сложностью.

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

Механизмы обеспечения качества обслуживания можно условно разделить на категории: дифференциация потоков, статическое и динамическое резервирование ресурсов, статическая и динамическая приоритетизация [65].

За последнее десятилетие были предложены различные подходы к проектированию коммуникационных фабрик, призванные обеспечить гарантии качества обслуживания "по построению". Подходы на основе дифференциации потоков решают проблему конкурирующих запросов введением уровней приоритета, соответствующих разным классам трафика [18]. Однако для сложной системы бывает затруднительно определить необходимое количество уровней приоритетов и избежать проблем «инверсии приоритета» (в частности, ситуаций, когда низкоприоритетный запрос блокирует выполнение высокоприоритетного, что переводит первый в категорию высокоприоритетных запросов) и «истощения ресурсов» (starvation).

Подходы на основе передачи данных без конкуренции основывается на той или иной схеме резервирования ресурсов перед началом передачи [75]. Используя статические схемы резервирования, несложно добиться определенных гарантий производительности. Такой подход позволяет оптимизировать архитектуру под конкретную задачу, и пригоден для встраиваемых узкоспециализированных систем, но приводит к низкой загрузке ресурсов в системах на кристалле широкого спектра применения [68]. При использовании динамического резервирования ресурсов, трудно оценить задержки на стадии резервирования, т.к. имеет место конкуренция за право зарезервировать ресурс. Использование механизмов управления приоритетами сталкивается с теми же проблемами. Затруднительно определить необходимое количество уровней приоритетов. Использование статической схемы управления приоритетами приводит к низкому использованию ресурсов, а динамическое управление приоритетами привносит труднопредсказуемую задержку на фазе определения приоритетов.

Список литературы диссертационного исследования кандидат наук Викторов, Юрий Олегович, 2013 год

Список Литературы

1. ABC Berkeley - A System for Sequential Synthesis and Verification. (http://www.eecs.berkeley.edu/~alanmi/abc/). Проверено 15.09.2013.

2. International technology roadmap for semiconductors: Executive Summary 2011, Semiconductor Industry Association, 2011.

(http://www.itrs.net/Links/2011ITRS/2011 Chapters/201 lExecSum.pdf). Проверено 17.09.2013.

3. JasperGold® Product page. (http://jasper-da.com/products/jaspergold_apps). Проверено 17.09.2013.

4. PCI-Express base specification rev. 1.1, PCI-SIG, 28 March 2005. (http://www.pcisig.com/specifications/pciexpress/base). Проверено 06.09.2013.

5. Гетманов А., Кишиневский M., Галсеран-Омс М. Технология построения синхронных эластичных схем и её применение к оптимизации производительности аппаратного декодера Н.264 CAB АС // МЭС 2010. - М: 2010.-С. 8-13.

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

7. Azimi М. et al. Experience with Applying Formal Methods to Protocol Specification and System Architecture //in proc. Formal Methods in System Design 22. - 2003. - P. 109-116.

8. Bakhouya M., Suboh S. et al. Analytical Modeling and Evaluation of On-Chip Interconnects Using Network Calculus //in proc. NoCS 3rd ACM/IEEE International Symposium. - 2009. - P. 74-79.

9. Barkaoui K., Dutheillet C., Haddad S. An efficient algorithm for finding structural deadlocks in colored Petri nets //in proc. ICATPN 1993. LNCS, V. 691. - Springer, Heidelberg 1993. - P. 69-88.

10. Baumgartner J. et al. Scalable conditional equivalence checking: An automated invariant-generation based approach //in proc. FMCAD'09. - 2009. - P. 120-127.

11. Beers R. Pre-RTL formal verification: an Intel experience //in proc. DAC'08. -2008.-P. 806-811.

12. Benveniste A. et al. The Synchronous Language Twelve Years Later //in proc. of the IEEE, V. 91(1). - 2003. - P. 64-83.

13. Berry G., Gonthier G. The ESTEREL Synchronous Programming Language: Design, Semantics, Implementation //Science of Computer Programming, V. 19(2).-1992.-P. 87-152.

14. Biere A., Artho C., Schuppan V. Liveness checking as safety checking

//Electronic Notes in Theoretical Computer Science 66(2). - 2002. - P. 160-177.

15. Biere A., Cimatti A. et al. Symbolic Model Checking without BDD //in proc. TACAS'99. - 1999. — P. 193-207.

16. Bjerregaard T., Mahadevan S. A survey of research and practices of network-on-chip //ACM Computing Surveys, V. 38(1). - 2006. - P. 1-51.

17. Black D.C. et al. SystemC: From the Ground Up. - Springer, 2nd edition. - 2010.

18. Bolotin E., Cidon I., Ginosar R., Kolodny A. QNoC: QoS architecture and design process for network on chip //The Journal of Systems Architecture. - 2003. -P. 105-128.

19. Borrione D., Helmy A. et al. A formal approach to the verification of Networks on Chip, EURASIP Journal on Embedded Systems, V. 2009. - 2009. - P. 299-304.

20. Boudec J.Y.L., Thiran P. Network Calculus: A Theory of Deterministic Queuing Systems for the Internet //LNCS, V. 2050. - Springer, Heidelberg 2001. - 276 p.

21. Bradley A. SAT-based model checking without unrolling //in proc. VMCAI'l 1. -2011.-P. 70-87.

22. Brayton R., Mishchenko A. ABC: An Academic Industrial-Strength Verification Tool // in proc. CAV'10, LNCS, V. 6174. - 2010. - P. 24-40.

23. Bufistov D., Jrulvez J., Cortadella J. Performance optimization of elastic systems using buffer resizing and buffer insertion //in proc. ICCAD'08. - 2008. -P. 442-448.

24. Bufistov D.E., Cortadella J., Galceran-Oms M., Jrulvez J., Kishinevsky M.

Retiming and recycling for elastic systems with early evaluation // in proc. DAC'09. - ACM, New York, 2009. - P. 288-291.

25. Burns S.M., Hulgaard H., Amon Т., Borriello G. An algorithm for exact bounds on the time separation of events in concurrent systems //IEEE Trans. Comput. 44. - 1995.-P. 1306-1317.

26. Carloni L.P., McMillan K.L. and Sangiovanni Vincentelli A.L. Theory of Latency-Insensitive Design //IEEE Transactions on CAD, V. 20(9). - 2001. - P. 1059-1076.

27. Chandy K.M., Misra J. Parallel Program Design: A Foundation. - Addison-Wesley, 1988.-516 p.

28. Chatterjee S., Kishinevsky M. Automatic generation of inductive invariants from high-level microarchitectural models of communication fabrics //in proc. CAV 2010, LNCS, V. 6174. - Springer, Heidelberg, 2010. - P. 321-338.

29. Chatterjee S., Kishinevsky M., Ogras U.Y. Quick formal modeling of communication fabrics to enable verification //in proc. IEEE High Level Design Validation and Test Workshop (HLDVT). - 2010. - P. 42-49.

30. Chaudhuri K., Doligezet D. et al. A TLA+ Proof System. - 2008. (http://hal.inria.fr/inria-00338299/en/). Проверено 10.01.2013.

31. Chawdhary A., Cook В., Gulwani S., Sagiv M., Yang H. Ranking Abstractions //in proc. ESOP. - 2008. - P. 148-162.

32. Chen Т., Raghavan R., Dale J. N., Iwata E. Cell Broadband Engine Architecture and its first implementation-A performance view //IBM Journal of Research and Development, V. 51(5). - 2007. - P. 559-572.

33. Clarke E., Grumberg O., Jha S., Lu Y. Counterexample-guided abstraction refinement //CAV'OO. - 2000.

34. Cohen I., Rottenstreich O., Keslassy I. Statistical Approach to NoC Design //in proc. Second ACM/IEEE Int. Symposium on NoC. - 2008. - P. 171-180.

35. Colom J.M., Silva M. Convex geometry and semiflows in P/T nets //in proc. of Appl. and Theory of Petri Nets. - 1991. - P. 79-112.

36. Cook B. Principles of Program termination // Notes from the 2008 Marktoberdorf summer school. (http://research.microsoft.com/en-us/um/cambridge/projects/terminator/principles.pdf). Проверено 17.09.2013.

37. Corman Т.Н. et al. Introduction to Algorithms, Second Edition. MIT Press, 1990.

38. Cortadella J., Kishinevsky M., Grundmann B. Synthesis of Synchronous Elastic Architectures //in proc. DAC'06. - 2006. - P. 657-662.

39. Cruz R. L. A calculus for network delay, part I. Network elements in isolation

//IEEE Transactions on Information theory, V.37(l).- 1991.-P. 114-131.

40. Dally W. J., Towles B. Principles and Practices on Interconnection Networks. -Morgan Kaufmann Publishers, 2004. - 550 p.

41. Dally W. J., Towles B. Route packets, not wires: On-chip interconnection networks //in proc. Design Automation Conference. - 2001. - P. 684-689.

42. Das R., Mutlu O. et al. A Network-on-Chip Exploiting Packet Latency Slack //IEEE Micro, Jan/Feb, V. 31(1). -2001. -P. 29-41.

43. Dill D. L. The Murphi Verification System //in proc. CAV'96. - 1996. - P. 390393.

44. Dill D. L., Drexler A. J., Hu A. J., Han Yang C. Protocol Verification as a Hardware Design Aid //in proc. IEEE International Conference on Computer Design: VLSI in Computers and Processors, IEEE Computer Society. — 1992. - P. 522-525.

45. Duato J. A necessary and sufficient condition for deadlock-free adaptive routing in wormhole networks //IEEE Trans. Paral. Distrib. Syst., V.6(10). - 1995. - P. 1055-1067.

46. Een N., Mishchenko A. Efficient implementation of property directed reachability //in proc. FMCAD'l 1. - 2011. - P. 125-134.

47. Emer J. et al. Asim: A Performance Model Framework //IEEE Computer, V. 35(2).-2002.-P. 68-76.

48. Engberg U., Grenning P., Lamport L. Mechanical Verification of Concurrent Systems with TLA //in proc. CAV'93. - 1993. - P. 44-55.

49. Galceran-Oms M. et al. Speculation in Elastic Systems //in proc. DAC'09. - 2009. -P. 292-295.

50. Galton A. et al. Temporal Logic. (http://plato.stanford.edu/entries/logic-temporal/). Проверено 15.12.2011.

51. Garver S., Crepps B. The new era of Tera-scale computing. (http://software.intel.com/en-us/articles/the-new-era-of-tera-scale-computing). Проверено 11.10.2011.

52. Gebremichael В., Vaandrager F.W., Zhang M., Goossens K.G.W., Rijpkema E., Radulescu A. Deadlock prevention in the athereal protocol //in proc. CHARME 2005, LNCS, V. 3725. - Springer, Heidelberg 2005. - P. 345-348.

53. Ghafari N., Gurflnkel A., Klarlund N., Trefler R.J. Algorithmic analysis of piecewise FIFO systems //in proc. FMCAD. - 2007. - P. 45-52.

54. Goossens K., Dielissen J., Radulescu A. Ethereal network on chip: concepts, architectures, and implementations //Design Test of Computers, IEEE, V. 22(5). -2005.-P. 414-421.

55. Goossens K. et al. A Design Flow for Application-specific Networks on Chip with Guaranteed Performance to Accelerate SoC Design and Verification //in proc. DATE.-2005.-P. 1182-1187.

56. Gotmanov A., Chatterjee S., Kishinevsky M. Verifying deadlock-freedom of communication fabrics //in proc. VMCAI 2011. - LNCS, V. 6538. - Springer, Heidelberg 2011. - P. 214-231.

57. Gotsman A., Cook B., Parkinson M., Vafeiadis V. Proving that non-blocking algorithms don't block //in proc. POPL 2009. -ACM, New York 2009. - P. 16-28.

58. Hansson A., Goossens K., Radulescu, A. Avoiding message-dependent deadlock in network-based systems on chip //VLSI Design 2007. - 2007.

59. Hansson A. et al. Enabling Application-Level Performance Guarantees in Network-Based Systems on Chip by Applying Dataflow Analysis //Computers & Digital Techniques, IET. - 2009. - P. 398-412.

60. Hoare. C.A.R. An axiomatic basis for computer programming. //Comm. of the ACM, 12(10):576580,583 1969.

61. Hoe J.C., Arvind J.C. Synthesis of Operation-Centric Hardware Descriptions //in proc. ICCAD. - 2000. - P. 511-518.

62. Holcomb D.E., Brady B.A., Seshia S.A. Abstraction-Based Performance Analysis of NoCs //in proc. DAC' 11. - 2011. - P. 492-497.

63. Holcomb D., Gotmanov A., Kishinevsky M., Seshia S. Compositional Performance Verification of NoC Designs //in proc. MEMOCODE. - 2012.

64. Holzmann G. J. The SPIN Model Checker. - Addison Wesley, 2003. - 236 p.

65. Jantsch A., Lu Z. Networks on Chip: Theory and Practice, chapter Resource allocation for quality of service on-chip communication. - Taylor & Francis Group LLC - CRC Press, 2009.

66. Jhala R., McMillan K.L. Microarchitecture Verification by Compositional Model Checking //in proc. CAV. - 2001. - P. 396-410.

67. Kaivola R. et al. Replacing Testing with Formal Verification in Intel Core i7 Processor Execution Engine Validation, //in proc. CAV'09. - 2009. - P. 414-429.

68. Kishinevsky M., Gotmanov A., Viktorov Y. Challenges in Verifying Communication Fabrics //in proc. ITP' 11. - 2011. - P. 18-21.

70. Krishna B. A., Michelson J., Singhal V., Jain A. Liveness vs Safety-A Practical Viewpoint //in proc. 7th international Haifa Verification conference on Hardware and Software. - 2011.

71. Kupferman O., Piterman N., Vardi M. Y. From liveness to promptness //in proc. Formal Methods in System Design 2009. - Jan. 2009.

72. Lamport L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. - Addison Wesley, 2002. - 384 p.

73. Lee E., Parks T. Dataflow Process Networks //in proc. IEEE, V. 83. - 1995. - P. 1-63.

74. Long J., Ray S., Sterin B., Mishchenko A., Brayton R. K. Enhancing ABC for LTL Stabilization Verification of SystemVerilog/VHDL Models //International Workshop on Design and Implementation of Formal Tools and Systems. - 2011.

75. Lu Z., Jantsch A. TDM virtual-circuit configuration for network-on-chip //IEEE Transactions on Very Large Scale Integration (VLSI) Systems, V. 16(8). - 2008. -P. 1021-1034.

76. Mahajan Y. et al. Verification driven Formal Architecture and Microarchitecture Modeling //in proc. MEMOCODE, 2007.

77. Manohar R., Martin A.J. Slack elasticity in concurrent computing //in proc. MPC 1998. LNCS, V. 1422. -Springer, Heidelberg 1998. - P. 272-285.

78. Manolios P., Srinivasan S.K. Automatic verification of safety and liveness for pipelined machines using web refinement //ACM Trans. Des. Autom. Electron. Syst. V. 13(3).-2008.-P. 1-19.

79. Marescaux T., Brick'el B. et al. Dynamic Time-Slot Allocation for QoS Enabled Networks on Chip //in proc. Embedded Systems for Real-Time Multimedia 3rd workshop. - 2005. - P. 47-51.

80. Matthews J., Launchbury J. Elementary Microarchitecture Algebra //in proc. CAV'99. - 1999. - P. 288-300.

81. Micheli G., Benini L. Networks on Chips, Morgan Kaufmann. - 2006. - 408 p.

82. McMillan K.L. Circular compositional reasoning about liveness //in proc. CHARME 1999. LNCS, V. 1703. - Springer, Heidelberg 1999. - P. 342-345.

83. McMillan K.L. Interpolation and SAT-based Model Checking //in proc. CAV'03. -2003.-P. 1-13.

84. McMillan K.L. The SMV Language. - 1998. (http://santos.cis.ksu.edu/smv-doc/language/language.html). Проверено 15.09.2013.

85. McMillan K.L. The SMV system. Cadence Berkeley Labs. - 1999.

86. Mony H. et al. Exploiting Suspected Redundancy without Proving it //in proc. DAC'05. — 2005.

87. Murata T. Petri Nets: Properties, Analysis and Applications //in proc. IEEE, 77(4):541580. -1989.

88. Ogras U., Hu J., Marculescu R. Key research problems in NoC design: A holistic perspective //In Proc. of the Intl. Conf. on Hardware/Software Codesign and System Synthesis. - 2005. - P. 69-74.

89. O'Leary J., Talupur M., Tuttle M. Protocol Verification using Flows: An Industrial Experience //in proc. FMCAD'09. - 2009.

90. Pinto A. et al. COSI: A Framework for the Design of Interconnection Networks //IEEE Design and Test of Computers, V. 25(5). - 2008. - P. 402-415.

91. Qian Y., Lu Z., Dou W. Analysis of communication delay bounds for networks on chip //in proc. ASPDAC'09. - 2009. - P. 7-12.

92. Rahmati D., Murali S. et al. A Method for Calculating Hard QoS Guarantees for Networks-on-Chip //in proc. ICCAD'09. - 2009. - P. 579-586.

93. Ray S., Bray ton R. K. Well-foundedness in Credit-Based Flow-Control Systems

//in proc. IWLS. - 2012. - P. 1-8.

94. Sanguinetti J., Pursley D. High-Level Modeling and Hardware Implementation with General-Purpose Languages and High-level Synthesis. - April. 2002. (http://www.cynapps.com/products/paper_0402_highlevelmodeling.pdf) Проверено 17.09.2013.

95. Seiler L., Carmean D. et al. Larrabee: A Many-Core x86 Architecture for Visual Computing //Micro, IEEE, V. 29(1). - 2009. - P. 10-21.

96. Seshia S.A. 2011 Berkeley class on FV engine techniques. (http://www.eecs.berkeley.edu/~sseshia/219c/sprl 1/index.html). Проверено 17.09.2013.

97. Sheeran M. et al. Checking Safety Properties Using Induction and a SAT-Solver //FMCAD'OO, LNCS V. 1954. - 2000. - P. 108-125.

98. Shi Z., Burns A. Real-Time Communication Analysis for On-Chip Networks with Wormhole Switching //in proc. Second ACM/IEEE Int. Symposium on NoC. — 2008.-P.161-170.

99. Soteriou V., Wang H., Peh Li-Shiuan. A statistical traffic model for on-chip interconnection networks //in proc. MASCOTS '06. - 2006. - P. 104-116.

100. Taktak S., Desbarbieux J.L., Encrenaz E. A tool for automatic detection of deadlock in wormhole networks on chip //ACM Trans. Design Autom. Electr. Syst. V. 13(1).-1995.

101.Talupur M., Tuttle M. Going with the flow: Parameterized verification using message flows //in proc. FMCAD'08. - 2008.

102. Turing A. Checking a large routine //Conference on High Speed Automatic Calculating Machines. - 1949.

103. Varatkar G., Marculescu R. Traffic analysis for on-chip networks design of multimedia applications //in proc. ACM/IEEE Design Automation Conference. -2002.-P. 510-517.

104. Varshavsky V. Time, Timing and Clock in Massively Parallel Computing System //in proc. International Conference Massively Parallel Computing Systems. - 1998.

105. Verbeek F., Schmaltz J. Formal specification of networks-on-chips: deadlock and evacuation //DATE'10. - 2010. - P. 1701-1706.

106. Verbeek F., Schmaltz J. Hunting deadlocks efficiently in microarchitectural models of communication fabrics //in proc. FMCAD' 11.-2011.

107. Wang G., Wang C. et al. Quality of Service (QoS) Contract Specification, Establishment, and Monitoring for Service Level Agreement //in proc. EDOCW'06. -2006. - P. 49-49.

108. Wang H. et al. A power-performance simulator for interconnection networks

//in proc. Int. Symp. Microarchitecture. - 2002. - P. 294-305.

109. Wentzlaff D., Griffin P., Hoffmann H. et al. On-chip interconnection architecture of the tile processor //Micro. - 2007.

110. Wiggers M., Bekooij M., Smit G. Modelling run-time arbitration by latency-rate servers in dataflow graphs//10th Workshop on Software & Compilers for Embedded Systems. - New York, NY, USA, 2007. - P. 11-22.

111. Wilhelm R. Timing analysis and timing predictability //FMCO 2004. LNCS, V. 3657. - Springer, Heidelberg 2005. - P. 317-323.

Приложение 1. Акт внедрения в производство

«Утверждаю»

Директор по обеспечения

корп^юНдии Интел в России [ШЛ^Хчсттшшов В. В. ШУГ» 2013г.

Акт внедрения

результатов диссертационной работы Викторова ЮршГЛЗлеговича «Анализ и верификация задержек в микроархитектуре коммуникационных фабрик», представленной на соискание учёной степени кандидата технических наук по специальности 05.13.05.

Комиссия в составе к.т.н. A.B. Жмурина - председателя, членов комиссии: к.т.н. Д,А. Плоткина, к.ф-м.н. К.К. Малинаускаса настоящим актом подтверждает, что результаты диссертационной работа Ю.О. Викторова;

• алгоритмическая схема анализа моделей xMAS для получения оценок сверху на задержку передачи данных в системе на кристалле;

• математическое описание понятия задержки между событиями и формализация процесса суждения о задержке;

• доказательство полученных временных оценок для широкого класса моделей с помощью метода k-индукции при малых значениях к:

реализованы в экспериментальном программном комплексе для анализа микроархитектурных спецификаций коммуникационных фабрик для систем на кристалле для технологии 14нм в ЗАО «Интел А/О» в 2013 году. Эксперименты на мнкроархитсктурных моделях коммуникационных фабрик и их отдельных узлов показали перспективность предложенных решений для анализа качества

.«Hlipuup.lJIiVKlJf уишл 1Л.ШИШЙ 11U |ЯШШЛ JtUllUÄ JJUJpuCviWn ;«Н»|Л>«РЛ1!ИМЛДДДМ.

Продемонстрированно радикальное увеличение надежности оценок и скорости их получения с соблюдением приемлемой точности оценок.

к.т н. А.П Жмурин

к.т.н. Д.А. Плоткин к.ф-м.н. К.К. Малинаускас

Приложение 2. Акт внедрения в учебный процесс

«УТВЕРЖДАЮ»

Дпрскто ~ " ' ■

результатов диссертационной работы Викторова Юрия Олеговича «Анализ и верификация задержек в микроархитектуре коммуникационных; фабрик», представленной на соискание учёной степени кандидата технических наук но специальности 05.13.05.

Комиссия в составе профессора. д.т.н. А.Л. Пяоткина - председателя, членов комиссии: к.ф-мл1. К.К. Малииаускаса, к.т.н. А.Ф. Мелик-Адамяна настоящим актом подтверждает, что результаты диссертационной работы Ю. О. Викторова:

• математическое описание понятия задержки между событиями и формализация процесса суждения о задержке;

• алгоритмическая схема анализа моделей хМАБ для получения оценок сверху на задержку передачи данных в системе на кристалле;

• доказательство полученных временных оценок для широкого класса моделей с помощью метода к-индукции при малых значениях к;

внедрены в учебный процесс в курсе ««Математические основы САПР», который читается в МФТИ на базовой кафедре ЗАО «Интел А/О» «Микропроцессорные технологии»

Председатель комиссии.

Акт внедрения

профессор, д.т.н. А.Л. Плоткин

Члены комиссии:

дет. *

к.ф-м.н. К.К. Малинаускас

к.т.н. А.Ф. Мелик-Адамян