Содержание к диссертации
Введение
1 Обзор методов профилирования и моделирования произво дительности 9
1.1 Диагностика производительности 10
1.2 Направления развития средств профилирования 13
1.3 Автоматическое использование данных профилирования . 14
1.4 Управление производительностью 16
1.5 Моделирование производительности 18
1.6 Проблемы соответствия модели и приложения 22
1.7 Программирование, ориентированное на мониторинг 24
1.8 Выводы 26
2 Моделирование, сбор и анализ количественных характеристик функционирования как аспекты контролируемого выполнения 27
2.1 Расширение понятия контролируемого выполнения аппаратно-программных комплексов 27
2.2 Особенности целевых аппаратно-программных комплексов . 29
2.3 Контролируемое выполнение, основанное на моделировании и верификации 30
2.4 Сбор и анализ информации средствами контролируемого выполнения 32
2.5 Выводы 34
3 Моделирование систем и количественных характеристик их функционирования 35
3.1 Модель распределённых вычислений 35
3.1.1 Моделирование разных аспектов вычисления 40
3.1.2 Моделирование ресурсов 41
3.1.3 Полная модель приложения 43
3.2 Моделирование последовательных распределённых приложений 48
3.3 Автоматизация описания приложения 53
3.4 Использование ACSL 55
3.5 Библиотека моделирования и самоконтроля 64
3.5.1 Аннотированная библиотека самоконтроля 64
3.5.2 Аннотации к системным функциям взаимодействия потоков и процессов 69
3.5.3 Вспомогательные утверждения 70
3.6 Интеграция со средой разработки приложений 74
3.7 Выводы 76
4 Сбор и анализ количественных характеристик функционирования 77
4.1 Сбор количественных характеристик 77
4.1.1 Архитектура системы профилирования 78
4.1.2 Описание компонентов системы профилирования . 82
4.2 Поддержка оптимизации по профилю в компиляторе СКРВ Багет 3.0 94
4.3 Выводы 98
Заключение 100
Литература 102
- Направления развития средств профилирования
- Особенности целевых аппаратно-программных комплексов
- Сбор и анализ информации средствами контролируемого выполнения
- Моделирование последовательных распределённых приложений
Введение к работе
Актуальность темы. Контроль использования ресурсов - важный фактор обеспечения надёжности специализированных распределённых систем, предназначенных для решения ответственных задач. Примером подобной системы может служить бортовой аппаратно-программный комплекс, состоящий из различных специализированных вычислительных блоков и управляющих узлов, соединённых аппаратными шинами. Контроль использования ресурсов в простейшем случае может заключаться в том, чтобы для каждого компонента системы проверять соблюдение явно заданных ограничений по различным видам ресурсов, таких как процессорное время, память, пропускная способность коммуникационных каналов. В более сложных случаях ограничения по ресурсам для различных узлов могут изменяться со временем, но так, чтобы их потребление системой в целом оставалось в заданных пределах.
Для решения проблем надёжности при разработке ответственных систем применяются модели — формальные спецификации различных аспектов поведения системы. Полное описание поведения серьёзной современной системы в виде единой «монолитной» модели оказывается слишком сложным для разработки и сопровождения. Кроме того, модели систем обычно развиваются эволюционно, путём последовательного уточнения общих описаний вплоть до разработки детальных реализаций (в частности, исходный текст системы на языке высокого уровня может рассматриваться как её модель). Поэтому более практичным представляется подход, при котором описание системы задаётся в виде совокупности моделей, описывающих различные аспекты её поведения, в том числе, потребление ресурсов.
Существует широкий спектр программных пакетов, которые позволяют
создавать модели, использовать их на этапе проектирования и реализации. Например, модели, представленные в виде конечных автоматов, применяются для симуляции системы и для последующей генерации исходного кода; алгебры процессов позволяют доказывать свойства моделей распределённых систем. Недостаток большинства подходов заключается в том, что они не ставят и не решают проблему соответствия модели и фактического поведения системы.
Значимость этой проблемы обусловлена тем, что современные системы подвержены постоянным изменениям; изменяется внешняя среда, в которой они работают, модифицируется исходный код, адаптируясь к новым требованиям. При этом могут возникнуть расхождения между различными моделями или между моделями и фактическим поведением системы, что делает результаты моделирования бесполезными. Поэтому актуальной является задача создания методики моделирования и средств верификации, позволяющих эффективно контролировать соответствие моделей системы, её исходного кода и поведения в процессе выполнения.
При создании моделей распределённой системы, описывающих использование ресурсов, необходимо отталкиваться от точных измерений количественных характеристик её функционирования; поэтому, важной является задача создания инструментов для таких измерений. Для систем, работающих в условиях дефицита ресурсов, особую значимость приобретает также проблема разработки средств для диагностики производительности, помогающих выдвигать и проверять гипотезы о причинах перерасхода ресурсов на основе анализа результатов измерений.
Сложность задачи обеспечения надёжности аппаратно-программных комплексов, многообразие факторов, которые необходимо при этом учитывать, требуют создания целостных подходов к её решению. Таким подходом является концепция контролируемого выполнения, которая направлена на выполнение системой её миссии, несмотря на наличие ошибок, сбоев аппаратуры, уязвимостей и т.п. Достижение этой цели обеспечивается применением целого спектра средств, таких как мониторинг, интерактивная отладка, детерминированное воспроизведение ошибочных ситуаций в распределённых системах, самоконтроль и др. на протяжение всего жизненного цикла систе-
мы, включая этап эксплуатации. Среда контролируемого выполнения, поддерживающая указанные средства, реализована в инструментальном комплексе «СОМ». В контексте данной работы актуальной представляется задача расширения и обобщения концепции контролируемого выполнения путём включения в неё методики контроля за использованием ресурсов, а также реализация соответствующих средств в рамках инструментального комплекса «СОМ».
Цель диссертационной работы. Основной целью диссертационной работы является разработка методов и программных средств, позволяющих решать задачи диагностики производительности и контроля за использованием ресурсов в рамках аппаратно-программных комплексов и их компонентов в процессе работы.
Для достижения указанной цели необходимо разработать средства сбора и анализа количественных характеристик функционирования распределённых аппаратно-программных комплексов, а также методику моделирования и верификации специализированных приложений, выполняющихся на этих комплексах, на основе построенной модели.
Научная новизна. Основные результаты работы являются новыми и заключаются в следующем:
Концепция контролируемого выполнения существенно расширена и обобщена за счет включения в неё разработанных автором методик моделирования и верификации распределённых разнородных аппаратно-программных комплексов, а также средств сбора и анализа количественных характеристик функционирования таких комплексов.
Предложены средства построения моделей распределённых разнородных аппаратно-программных комплексов с учётом количественных характеристик их функционирования.
Практическая ценность. Реализованы новые компоненты инструментального комплекса контролируемого выполнения, осуществляющие моделирование, сбор и анализ количественных характеристик приложений реального времени, функционирующих на отечественных ЭВМ серии Багет.
Апробация. Основные положения диссертационной работы докладывались на III международной конференции «Параллельные вычисления и задачи управления», Москва, ИПУ РАН, 2006; на VI международной конференции «Идентификация систем и задачи управления», Москва, ИПУ РАН, 2007; на III международной научной конференции по проблемам безопасности и противодействия терроризму, Москва, МГУ им. М.В. Ломоносова, 2007; на международной научной конференции «Моделирование-2008», Киев, ИП-МЕ им. Г.Е. Пухова НАН Украины, 2008; на IV международной конференции «Параллельные вычисления и задачи управления», Москва, ИПУ РАН, 2008; на IV международной научной конференции по проблемам безопасности и противодействия терроризму, Москва, МГУ им. М.В. Ломоносова, 2008; на VIII международной конференции «Идентификация систем и задачи управления», Москва, ИПУ РАН, 2009; на семинаре «Современные сетевые технологии», МГУ им. М.В. Ломоносова, 2007; на научно-исследовательском семинаре «Проблемы проектирования и реализации базового аппаратно-программного обеспечения» в НИИ системных исследований РАН.
Публикации. По теме диссертации опубликовано 11 печатных работ: [4], [2], [3], [7], [9], [15], [8], [6], [5], [14], [10] из них 10 в соавторстве, 3 в изданиях по перечню ВАК.
Объем и структура работы. Диссертация состоит из введения, 4 глав, заключения и списка литературы.
Первая глава представляет собой обзор имеющихся средств и методов профилирования, построения моделей и верификации приложений. Подробно рассматриваются средства статического и динамического моделирования, обосновывается их недостаточность для решения поставленных в работе задач.
Во второй главе формулируется обобщение концепции контролируемого выполнения, приводится обоснование необходимости такого обобщения для задачи моделирования и верификации выполнения приложений.
В третьей главе подробно рассматриваются средства и методы моделирования, предложенные и реализованные автором в рамках инструментального комплекса «СОМ» (Система Отладки/Мониторинга).
Четвёртая глава посвящена средствам сбора и анализа количественных
характеристик аппаратно-программных комплексов. Рассматривается механизм адаптивной компиляции, реализованный для разработанного в НИИСИ РАН компилятора. Приводится описание архитектурных и технологических решений, которые позволили интегрировать разработанные автором средства в инструментальный комплекс «СОМ». Рассматриваются механизмы взаимодействия разработанных средств со средствами сторонних производителей.
В заключении излагаются основные результаты диссертационной работы.
Список литературы насчитывает 105 названий.
Направления развития средств профилирования
Для больших распределённых систем становится важной задача децентрализованного профилирования, хранения, сбора и обработки информации о производительности. Эта проблема рассмотрена, например, в статье [99], в которой описывается автономная система сбора информации, ориентированная на сбор данных о производительности приложений и вспомогательного ПО (middleware).
Задачу измерения производительности с вносимыми погрешностями, неточностями измерения можно рассматривать как проблему постановки эксперимента. С этой точки зрения измерение производительности представлено в [62]. Естественно рассматривать полученные данные о производительности как некоторую статистическую выборку и анализировать её методами статистики, нечётких множеств [100]. В статье [82] рассмотрено программное обеспечение для проверки соответствия данных профилирования инструментованного приложения и данных приложения без инструментовки.
Задача обработки, визуализации информации о производительности параллельных систем рассмотрена в [55].
Развитие компонентного программного обеспечения, сервис-ориентированных архитектур требует создания компонентов производительности для распределённых научных высокопроизводительных вычислений. Оценки производительности на этом уровне помогают создать компонентную среду, предоставляющую сервисы производительности [88].
В настоящее время существуют два крупных проекта по интеграции средств профилирования и оценки производительности в платформу для средств разработки Eclipse - ТРТР (Trace and Profiling Tools Project) и РТР (Performance Tools Project) [94].
Более точное моделирование распределений событий - периодических и спорадических - позволяет увеличить точность профиля, снизить затраты на профилирование [95].
Оценивать производительность приложения можно и статически. В [66] рассматривается экспертная методика, позволяющая оценивать производительность приложения. Часто это полезно на ранних стадиях разработки, когда аппаратная часть системы.не работает, или для встраиваемых систем, профилирование которых затруднено.
В распределённых системах важно отслеживать межузловые вызовы, представляя профиль всей системы в целом [31].
Использование симуляторов может значительно увеличить объём, степень анализа и детализации собираемой информации. К сожалению, при этом увеличивается время работы приложения (до 20 раз). Примеры симуляторов - Valgrind [101] и SIMICS. С помощью Valgring можно профилировать не только время выполнения приложения, но и память, использование системы ввода-вывода, кэша процессора.
Средства профилирования программ изначально разрабатывались как инструменты, позволяющие разработчику изучать профиль выполнения про-граммы, с тем чтобы вручную оптимизировать наиболее часто выполняемые (критические) фрагменты кода. Например, в критических участках кода программист мог вручную выполнить развёртку (или конвейеризацию) циклов, подстановку коротких функций вместо их вызовов и др. Современные компиляторы способны автоматически выполнять подобные оптимизации с учётом данных профилирования [32], оставляя разработчику содержательную работу по совершенствованию алгоритмических решений. Более того, компиляторы выполняют с учётом профиля множество оптимизаций, недоступных программисту на уровне исходного кода, таких как глобальное планирование команд, распределение регистров и др. По результатам различных работ (см., например, [36], [63]) повышение эффективности кода в результате применения оптимизаций по профилю может составлять 10 - 20 и более процентов.
Существуют различные виды профилей, которые могут быть полезны для тех или иных оптимизаций. Профиль потока управления (control flow profile) может быть представлен с различной степенью детализации: как профиль функций (function profile), профиль базовых блоков (basic block profile), профиль переходов (edge profile), профиль конечных путей в графе потоков управления (path profile). Другой вид профиля - профиль значений - содержит информацию о значениях, принимаемых некоторыми программными выражениями, например, в виде гистограмм.
Процедура для применения оптимизаций по профилю включает 3 шага: компиляцию с инструментовкой программы для сбора профиля; сбор профиля путём выполнения инструментованной программы с типичными входными данными; компиляцию с использованием профиля для оптимизации кода.
Помимо специальных оптимизаций, ориентированных на применение профиля, таких как глобальное планирование потока команд, компилятор может использовать профиль для повышения эффективности многих традиционных оптимизаций ([32], [90], [50], [34], [83]).
Хотя оптимизация по профилю может давать значительный прирост производительности и способствовать сокращению размера кода, с её применением связан ряд проблем. Необходимость двукратной компиляции, а также разработки,и сопровождения достаточно представительных тестовых задач для сбора профиля усложняет процесс разработки и сопровождения программ. Не всегда возможно предугадать, с какими входными данными приложение будет работать в производственных условиях (возможно, разные группы пользователей будут использовать приложение по-разному). Как показывает практика, оптимизация по профилю может приводить к деградации производительности каких-то частей программы, т.е. необходимо анализировать результаты оптимизации по профилю и, возможно, применять её избирательно.
Особенности целевых аппаратно-программных комплексов
Сложность разработки и сопровождения приложений для рассматриваемых в данной работе аппаратно-программных комплексов связана с их особенностями, которые перечислены далее. 1. Разнородность. В состав целевых комплексов входят разнородные аппаратные платформы. Способы учёта ресурсов на каждой из платформ, управляющие интерфейсы и способы взаимодействия могут значительно различаться. 2. Изменяемость. Целевоії комплекс может поддерживать несколько режимов работы, которые характеризуются разными системными конфигурациями, например, разными политиками безопасности, разными политиками планирования потоков и процессов узлов реального времени и так далее. Каждый режим обладает собственным профилем использования ресурсов. 3.
Ограничения, накладываемые требованиями соблюдения определённого уровня качества обслуживания. Компоненты, осуществляющие контроль выполнения целевых комплексов, должны поддерживать требуемый уровень качества обслуживания в автоматическом режиме, без участия оператора. В частности, эти компоненты должны одновременно обеспечивать соблюдение временных требований для узлов реального времени; требований отказоустойчивости и самовосстановления узлов в результате возникших сбоев; требований информационной безопасности; требований по использованию доступных ресурсов. 4. Сложность структуры. Комплекс может представлять собой метасистему, то есть систему, компонентами которой являются системы. Разработчики отдельных компонентов комплекса далеко не всегда имеют полное представление о нем в целом. В результате могут быть приняты неоптимальные решения, приводящие, например, к повышенному потреблению ресурсов или нарушающие базовые принципы построения системы, например, из-за использования узкоспециализированных протоколов. 5. Динамически изменяемые условия функционирования. Условия функционирования аппаратно-программных комплексов могут изменяться в ходе выполнения, например, из-за дефицита ресурсов или выявленной угрозы информационной безопасности комплекса.
Средства контролируемого выполнения должны обеспечивать своевременное реагирование на подобные ситуации. С учётом указанных особенностей, при разработке подобного рода аппаратно-программных комплексов целесообразным представляется построение модели, на которой можно проверить выполнение необходимых требований соблюдения определённого уровня качества обслуживания как всего комплекса в целом, так и отдельных его компонентов. В соответствии с этим подходом, в качестве отправной точки контролируемого выполнения предлагается использовать построение формальной модели системы и верификацию свойств, относящихся к обеспечению надлежащего уровня качества функционирования. Формальные методы верификации программ, основанные на статической проверке соответствия модели, доказательстве теорем в силу отмеченных в предыдущей главе ограничений, не позволяют в полной мере решить задачи, связанные с контролем количественных характеристик выполнения приложений.
В данной работе предлагается подход, включающий как статическую, так и динамическую верификацию программы в ходе ее выполнения. В качестве средства описания модели выбран язык С ACSL (ANSI/ISO С SPECIFICATION LANGUAGE, [17]), который позволяет описывать поведение программ на языке С в виде аннотаций. Инструмент Why [45] вместе со средствами для доказательства утверждений используется для проверки свойств, которые можно проверить статически. Свойства, задающие количественные характеристики выполнения приложения, описываются с использованием средств профилирования инструментального комплекса СОМ и проверяются динамически в ходе выполнения программы. Динамически могут проверяться также заданные в модели функциональные свойства программ, статическая проверка которых невозможна. Идеи динамической верификации программ близки к парадигме программирования, ориентированного на мониторинг МОР, [33]). Механизм наблюдения включает средства мониторинга и реализованные в рамках данной работы средства профилирования, позволяющие отслеживать использование приложением целевых ресурсов. Механизм верификации реализован как сопоставление результатов наблюдения с моделью на основе средств самоконтроля ([13]).
Сбор и анализ информации средствами контролируемого выполнения
Действие может включать условие применимости Q - логическая формула, содержащая только нештрихованные переменные; действие г применимо к состоянию s, только если s удовлетворяет Q. Например, условие применимости для действия з; ОЛа/ = 1-1 задаётся формулой х О, то есть данное действие применимо только к состояниям, в которых значение х положительно.
Над бесконечными последовательностями состояний можно рассматривать временные формулы, которые составлены из булевых операторов и операторов линейной временной логики. Для бесконечной последовательности а тогда Np - отношение возможности переходов между состояниями для действий программы Р. Точная спецификация программы Р определяется в виде
Она описывает множество всех возможных последовательностей состояний (вычислений) программы. Внешняя спецификация программы задаётся в виде: Она описывает все возможные последовательности внешних состояний программы.
Верификация некоторого свойства ф программы Р, выраженного формулой временной логики, не содержащей внутренних переменных, заключается в доказательстве импликации Ф(Р) = ф. Обычно требуется доказать свойства безопасности (safety properties), означающие, что некоторые нежелательные состояния никогда не будут достигнуты, свойства живучести (liveness properties), означающие, что некоторые требуемые состояния когда-либо будут достигнуты. Интерес могут также представлять свойства стабильности (persistence properties), означающие, что любое вычисление рано или поздно достигнет состояния, удовлетворяющего требуемому условию, и это условие далее всегда будет соблюдаться, а также свойства справедливости (fairness properties), означающие, что в ходе вычисления гарантируется, что некоторое условие будет выполнено бесконечное число раз.
Верификация может также заключаться в доказательстве того, что некоторая программа Pj является уточнением программы Р.
Определение 5. Отношение уточнения Pi С Ph означает что Pi корректно реализует Ph, то есть для внешних спецификаций выполнено отношение На основе понятия уточнения можно определить отношение частичного порядка на множестве программ и использовать его для построения семейства моделей, представляющих выполнение приложения с разной степенью детализации.
В работах [79] и [74] описываются дальнейшие расширения предложенных определений и возможности вывода теорем. Например, для того, чтобы описать отказы, вводится множество действий F и понятие внешних и внутренних спецификаций, отказопорождающего вычисления T(P,F) = (v, х, Q, A U F) (где F - программа порождения отказов), отказоустойчивого уточнения и т.д.
Рассмотрим расширения представленного метода описания вычислений, обеспечивающие возможности задания различных аспектов вычисления, оценки оптимизаций и учёта ресурсов.
Естественно описывать вычисление несколькими моделями, отражающими различные аспекты приложения, например, модель памяти и модель занимаемой пропускной способности сети могут быть различными, дополняя-основную модель вычислений. Разнородным может быть и набор проверяемых утверждений. Например, доказательство корректности использования ограниченных ресурсов памяти может проводиться средствами статического анализа и использовать только данные о потоке управления приложения, для доказательства корректности может использоваться представление приложения в виде конечного автомата. Корректность взаимодействия с внешним источником данных может определяться функцией распределения поступления данных и описываться статистической моделью.
Понятие композиции программ Pi Р2 соответствует их совместному выполнению и позволяют изучать свойства комбинации двух моделей.
Определение 6. Композицией программ Р\ и Р2, представляемых наборами (vi,xi,Qi,Ai) и (у 2,Х2,@2,А2), называется программа с набором пере-менных v\\Jv2, набором внутренних переменныхx\\Jx2, начальным состо-01 Л 02, и набором действий А\ U А2.
Подмножество внутренних переменных может быть определено и иначе, в зависимости от потребностей анализа программы. Например, можно определить множество внешних переменных как объединение соответствующих множеств программ Р\,Ро, а остальные переменные считать внутренними. Внутренняя и внешняя спецификации композиции программ Pj определяются как
Моделирование последовательных распределённых приложений
Рассмотрим системы, состоящие из набора обменивающихся сообщениями процессов, каждый из которых описан программой на языке С. Классический подход к описанию программы на императивном языке состоит в использовании логики Хоара [61], утверждения которой состоят из формул специфического вида {P}S{Q}, где S - часть программы на языке С, предусловие Р и постусловие Q - формулы исчисления высказываний, зависящие от переменных, входящих в S. Если Q истинно после исполнения S в состоянии, где истинно Р, такая тройка считается истинной. В логике Хоара для языка программирования семантика этого языка задаётся в виде правил вывода, которые позволяют выводить шаг за шагом истинные тройки из тавтологий. На практике при последовательном применении правил вывода возникают проблемы, связанные со сложностью точного описания операторов приложения. Часто система предусловий и постусловий реализуется в неформальном виде: Автоматический анализ приложения с целью выявления предусловий и постусловий затруднён необходимостью использования дополнительных утверждений для различных конструкций языка. В частности для операторов цикла необходимо использовать вариант цикла, позволяющий доказать его завершимость. Использование логики Хоара позволяет установить соответствие между семантикой приложения и его исходным кодом, но ограничивает спектр выводимых утверждений только утверждениями о состоянии последовательного приложения. В некоторых работах изучались расширения логики Хоара, позволяющие описывать и доказывать свойства приложений реального времени.
В работе [69] предложено использовать в тройках Хоара выражения следующего вида. имена локальных переменных; специальные логические переменные Vi,v2,... и специальные логические переменные времени ti, І2, ; специальную переменную now, содержащую значение времени в текущий момент; выражение о at t, говорящее о том, что событие о должно произойти в момент времени t; выражения (с\\,ехр) at і, обозначающие отсылку сообщения ехр в момент времени t по каналу с; выражения с? at t, обозначающие ожидание сообщения ехр в момент времени t по каналу с; выражения (с, ехр) at , обозначающие приём сообщения ехр в момент времени t по каналу с. В основе использования логики Хоара и производных логик лежит применение определённых правил вывода для доказательства свойства приложения в целом, причём это свойство подразумевает наличие точки завершения приложения, и, следовательно, не настолько широко, чтобы позволить рассматривать временные формулы. В настоящей работе предлагается подход, основанный на трансформации троек Хоара, заданных аннотированным исходным кодом, в модель TLA и в последующей проверке этой модели. Рассмотрим распределённую программу S, состоящую из последовательных процессов j.
Для простоты будем считать, что процессы , состоят из последовательности операторов без передач управления. Для каждого из операторов заданы предусловия и постусловия, часть из которых представлена в виде аннотаций, а остальные определяются семантикой языка. где предусловия и постусловия представляют собой логические формулы, в которые могут входить переменные приложения и логические переменные. Кроме того, может быть определено множество дополнительных временных формул - аксиом и свойств: Примерами таких формул могут служить свойства времени 3.1. Формула Init задаёт начальное состояние приложения. Преобразование набора последовательных программ в модель TLA следует принципам, применённым ранее в примере использования модели TLA для спецификации алгоритма Фишера 3.1.3. Для того чтобы построить спецификацию TLA, опишем множество переменных, действий и свойств. В качестве множества переменных возьмём
