автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Моделирование, сбор и анализ количественных характеристик функционирования распределенных разнородных аппаратно-программных комплексов

Учреждение Российской академии наук Научно-исследовательский институт системных исследований РАН

На правах рукописи УДК 004.416.2

Шмырёв Николай Владимирович

МОДЕЛИРОВАНИЕ, СБОР И АНАЛИЗ КОЛИЧЕСТВЕННЫХ ХАРАКТЕРИСТИК ФУНКЦИОНИРОВАНИЯ РАСПРЕДЕЛЁННЫХ РАЗНОРОДНЫХ АППАРАТНО-ПРОГРАММНЫХ КОМПЛЕКСОВ

05.13.11 - Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

003470660

Москва 2009

003470660

Работа выполнена в учреждении Российской академии наук научно-исследовательском институте системных исследований РАН

Научные руководители: академик РАН, профессор

Бетелин Владимир Борисович, кандидат физико-математических наук Костюхин Константин Александрович.

Официальные оппоненты: доктор физико-математических наук

Петренко Александр Константинович, кандидат физико-математических наук Эйсымонт Леонид Константинович.

Ведущая организация: Институт прикладной математики

им. М. В. Келдыша РАН

Защита состоится 17 июня 2009 г. в 16 часов на заседании диссертационного совета Д 002.265.01 при НИИСИ РАН по адресу 117218, Москва, Нахимовский пр-т, д. 36, корп. 1, конференц-зал.

С диссертацией можно ознакомиться в библиотеке НИИСИ РАН (комн. 13-12)

Автореферат разослан 15 мая 2009 г.

Ученый секретарь диссертационного совета, кандидат физико-математических наук, доцент В. Б. Демидович

Общая характеристика работы

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

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

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

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

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

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

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

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

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

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

• Предложены средства построения моделей распределённых разнородных аппаратно-программных комплексов с учётом количественных характеристик их функционирования.

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

Апробация. Основные положения диссертационной работы докладывались на III международной конференции «Параллельные вычисления и задачи управления», Москва, ИПУ РАН, 2006; на VI международной конференции «Идентификация систем и задачи управления», Москва, ИПУ РАН, 2007; на III международной научной конференции по проблемам безопасности и противодействия терроризму, Москва, МГУ им. М.В. Ломоносова, 2007; на международной научной конференции «Моделирование-2008», Киев, ИП-МЕ им. Г.Е. Пухова HAH Украины, 2008; на IV международной конференции

«Параллельные вычисления и задачи управления», Москва, ИПУ РАН, 2008; на IV международной научной конференции по проблемам безопасности и противодействия терроризму, Москва, МГУ им. М.В. Ломоносова, 2008; на VIII международной конференции «Идентификация систем и задачи управления», Москва, ИПУ РАН, 2009; на семинаре «Современные сетевые технологии», МГУ им. М.В. Ломоносова, 2007; на научно-исследовательском семинаре «Проблемы проектирования и реализации базового аппаратно-программного обеспечения» в НИИ системных исследований РАН.

Публикации. По теме диссертации опубликовано 11 печатных работ, из них 10 в соавторстве, 3 в изданиях по перечню ВАК.

Объем и структура работы. Диссертация состоит из введения, четырёх глав и заключения. Список использованной литературы содержит 105 наименований. Текст диссертации содержит 112 страниц машинописного текста, включая 7 рисунков.

Содержание работы

Во введении сформулированы цели диссертационной работы, обоснованы ее актуальность и научная новизна.

Первая глава представляет собой анализ существующих средств и методов профилирования и моделирования производительности.

Рассмотрены современные методы и средства диагностики производительности как локальных приложений (gprof, oprofile), так и распределённых и параллельных систем (TAU, Kojak, SvPablo и другие). Наличие широкого спектра средств обуславливает появление стандартов в области профилирования и измерения производительности. Приведён обзор существующих стандартов, таких как стандарт Open Trace Format (OTF), описывающий формат общей трассы событий для средств профилирования, и программный интерфейс Perfomance Application Programming Interface (PAPI), специфицирующий доступ к аппаратным счётчикам платформы. Большое внимание в настоящее время уделяется средствам и механизмам автоматического использования данных профилирования с целью оптимизации работы приложений и использования ими целевых ресурсов, например, оптимизации приложения по профилю на этапе компиляции.

Далее рассматриваются различные подходы к построению моделей распределённых приложений (гибридные автоматы, сети Петри, логики переходов, алгебры процессов и другие), в том числе и моделей ресурсов. Даётся анализ существующих средств построения моделей (SMV, SPIN, JML). Приводится обзор различных механизмов верификации моделей (автоматическое и ручное доказательство утверждений, симуляция, статистическое тестирование). К сожалению, чем шире класс описываемых моделью систем, тем сложнее осуществить верификацию моделей. Одним из наиболее гибких инструментов моделирования является логика Temporal Logic of Actions (TLA), которая задаёт распределённую систему с помощью множества переменных и множества разрешённых действий над этими переменными. Отмечаются преимущества моделей TLA, такие как возможность учёта использования ресурсов, отказов, внешних воздействий и так далее.

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

При анализе проблем соответствия модели и приложения и методов их решения отмечаются недостатки существующих средств проверки, таких как генерация исходного кода из модели, тестирование, автоматическое извлечение модели из исходного кода. Подробно описывается подход к извлечению моделей из аннотаций исходного кода на языке С, язык спецификации ACSL и средство статического анализа Frama-C. Этот инструмент позволяет извлекать из аннотированного исходного кода приложения набор утверждений, необходимых для проверки корректности спецификаций, и доказывать его с помощью средств автоматического доказательства утверждений, таких как Alt-Ergo, или средств проверки доказательств, таких как CoQ. Существенным недостатком инструментария Frama-C является его ориентация на последовательные приложения и упор на проверку таких низкоуровневых свойств, как корректность использования указателей в языке С.

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

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

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

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

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

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

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

• временных требований для узлов реального времени;

• требований отказоустойчивости и самовосстановления узлов в результате возникших сбоев;

• требований информационной безопасности;

• требований по использованию доступных ресурсов.

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

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

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

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

В следующем разделе второй главы формулируется понятие контролируемого выполнения, основанного на моделировании и верификации. Фор-

мальные методы верификации программ, основанные на статической проверке соответствия модели, доказательстве теорем не позволяют в полной мере решить задачи, связанные с контролем количественных характеристик выполнения приложений. В данной работе предлагается подход, включающий как статический анализ программного кода на соответствие модели, так и динамическую верификацию программы в ходе ее выполнения. В качестве средства описания модели выбран язык ACSL (ANSI/ISO С Specification Language), который позволяет описывать поведение программ на языке С в виде аннотаций.

Механизм динамической верификации основан на парадигме программирования, ориентированного на мониторинг (Monitor-Oriented Programming, МОР). В данной работе механизмы наблюдения и верификации МОР рассматриваются как компоненты среды контролируемого выполнения. Механизм наблюдения включает средства мониторинга и реализованные в рамках данной работы средства профилирования, позволяющие отслеживать использование приложением целевых ресурсов. Механизм верификации реализован как сопоставление результатов наблюдения с моделью на основе средств самоконтроля.

Таким образом, понятие контролируемого выполнения расширено введением в его состав:

• инструментов построения моделей;

■ инструментов измерения и анализа характеристик эффективности и корректности функционирования систем и их элементов.

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

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

В третьей главе приводится математическая модель вычислений, описывающая основные аспекты контролируемого выполнения распределённых ответственных приложений реального времени:

• отказоустойчивость;

• потребление ресурсов;

• результативность оптимизаций программы.

Моделирование приложений основано на системе переходов, в качестве общей спецификации используется логика TLA. Кроме того, для описания исходного кода приложения используется формализм логики Хоара.

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

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

Определение 1. Состояние - отображение множества переменных V на множество значений V:

в : V V.

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

Определение 2. Действие - это формула исчисления предикатов первого порядка. Она может содержать исходные значения переменных и их изменённые значения, обозначаемые штрихом:

х' = х + у

Для каждого действия г на множестве состояний определено бинарное отношение [г](5, в'), где 5 и я' - пред состояния и постсостояния действия т. Формула для вычисления [т](в, получается из формулы г путем подстановки нештрихованных значений из я и штрихованных значений из й'. Если имеет место [-г](в, в'), то пара состояний в, э' называется т-шагом вычисления.

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

Над бесконечными последовательностями состояний можно рассматривать временные формулы, которые составлены из булевых операторов и операторов линейной временной логики. Например, для бесконечной последовательности сг = со, с1!,..., выражение [□</>](а) истинно тогда и только тогда, когда ф(а) истинно для любого суффикса 7] последовательности а.

Определение 3. Программа - это система действий (или система переходов) Р = &,А), описываемая следующими компонентами:

• Конечное непустое множество V переменных;

• Подмножество внутренних переменных х, возможно пустое;

• Начальные условия - формула 0, включающая только переменные из V (без штрихов), описывающая множество допустимых начальных состояний программы;

• Конечный набор А атомарных действий, которые могут включать переменные только из V и у'.

Определение 4. Вычисление программы Р = (у,х,&,А) - это последовательность состояний а = оо^ъ • • • такая, что выполняются два условия:

• «То удовлетворяет 0;

• сг*+1 = Яг или найдётся такое т £ А, что ^,04+1 является т-шагом. Для программы Р = рассмотрим

ЯР=\/т,

теЛ

тогда Ир - отношение возможности переходов между состояниями для действий программы Р. Точная спецификация программы Р определяется в виде

п(р) = елп[#р]„.

Она описывает множество всех возможных последовательностей состояний (вычислений) программы. Внешняя спецификация программы задаётся в виде:

Ф (Р) = Эя.П(Р).

Она описывает все возможные последовательности внешних состояний программы.

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

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

механизмов выделения следует учитывать характеристики этих механизмов, такие как фрагментация памяти. Течение времени описывается переменной now:

now = 0 G 0 П[пспю' £ (now, оcOJnou, (1)

Vi G R+,o(now > t)

Описание ресурса позволяет говорить о профиле модели - среднем потреблении ресурса в течение некоторого значительного промежутка времени и распределении потребления ресурса с течением времени. Подобная высокоуровневая информация полезна при оценке результативности оптимизаций.

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

Определение 5. Программа описывается следующими сущностями:

• программа без времени P(v,x,Q,A);

• набор отказов F и соответствующая программа с условиями выполнения отказов F(P, F);

• счётчик времени now со свойствами (1);

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

• функции расхода ресурсов Li(r) и Ui(r), задающие границы потребления ресурсов для действий из А.

Классический подход к описанию программы на императивном языке состоит в использовании логики Хоара, утверждения которой состоят из формул вида {P}S{Q}, где S - часть последовательной программы S на языке С, предусловие Р и постусловие Q - формулы исчисления высказываний, зависящие от переменных, входящих в S. Если Q истинно после исполнения S в состоянии, где истинно Р, то такая тройка считается истинной.

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

Для того чтобы построить спецификацию TLA по набору последовательных программ, опишем множество переменных, действий и свойств. В качестве множества переменных возьмём v - множество переменных программы § и х - множество логических переменных, используемых только в предусловиях, постусловиях и в дополнительных формулах ф{, а также набор переменных рс[г\, описывающих текущий оператор выполнения в каждом из процессов.

Зададим множество действий программы как одно общее действие, представляющее комбинацию действий операторов последовательной программы

Next 3 = f\Pred{Sij)

Sij

где условия Pred(Sij) для каждого из операторов состоят из условий нахождения процесса выполнения в некотором операторе последовательной программы и из предусловий и постусловий этого оператора

Pred(Sij) : \pc[i] = j Аре'[г] = j + 1 Л Рц Л Qij]pc]i}-

Внутренняя спецификация набора программ определяется начальными условиями и условием действия

Spec = Init A D[\/ Nextj]y j

Теорема. Пусть § = USj - распределённая программа, состоящая из последовательных программ, Р§ - TLA-программа, построенная для § как описано выше, ф - формула временной логики, включающая переменные из §. Тогда если Ф(Р§) ф, тоф истинна для всех возможных трасс выполнения

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

• аннотации функций самоконтроля, реализующих динамическую верификацию;

• аннотации к системным функциям взаимодействия потоков и процессов;

• спецификации поддержки моделирования.

Для того чтобы облегчить применение вышеописанных средств динамического и статического анализа, система моделирования и анализа количественных характеристик интегрирована в среду разработки программного обеспечения Eclipse. Реализованы следующие возможности:

• верификация совокупности аннотаций и сохранение результатов;

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

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

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

1. Сбор следующих количественных характеристик:

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

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

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

• объём сетевого трафика.

2. Использование аппаратных средств профилирования.

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

4. Контроль параметров модели.

Система профилирования представляет собой распределённое приложение, состоящее из ряда основных компонентов. На целевых ЭВМ это:

• компонент профилирования в ядре профилируемой ОС, называемый драйвером профилирования;

• агент профилирования, передающий драйверу профилирования управляющие запросы, поступающие от менеджера профилирования;

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

• библиотека контроля параметров модели. На инструментальной ЭВМ это:

• менеджер профилирования и контроля модели;

• база данных для хранения собранной информации (БД событий);

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

Архитектура системы профилирования представлена на рисунке 1. Механизм построения профиля выполнения программы основан на событиях профилирования. Различают простые и составные события профилирования. Простое событие содержит информацию ровно об одном атомарном событии профилирования. Атомарными событиями являются: аппаратное событие профилирования, отправка/получение одного сетевого пакета,

Рис. 1: Архитектура системы профилирования

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

В рамках данной работы был осуществлён перенос библиотеки PAPI, предоставляющей стандартный интерфейс для работы с аппаратными счётчиками событий, в целевую среду, состоящую из операционной системы реального времени «ОС РВ Багет 2.0», выполняющейся на отечественных микропроцессорах Комдив32 и Комдив64, и программируемого процессора сигналов (ППС) многопроцессорной ЭВМ, состоящей из отдельных плат - модулей обработки сигналов (МОС). На каждом модуле обработки сигналов распо-

латается 4 или 8 микропроцессоров цифровой обработки сигналов, имеющих как локальную, так и общую память.

6,054,540 Ьуйа I ;оссгк)5

[3 ¡ЛЮОЮИНЕДОеаТОс

кмвимтвюмлч §3 чмюпоооыомг« ■ вдэнаатсм« [1] «=93010011 аиотвмо !?! МгвКПОООаЭИсЬЬИ В киваПМОаЫЕска«

В ы>'ЗК>1га№!с1«1аоэьс

млпммоит

К»!98010в0ас4всав1:

кьвэоюрнижоюо» сМЭОКНЬхЧИМЗс

кквЭ01000кс41 )а»Эс

■ьеэаюоиям 1эяз= имзлмгоеюдом ¡3.93010011*>тетвй

¡сЬЭтОМ&МОавСкх

кмяошакнаака

Рис. 2: Диаграмма использования динамической памяти

На инструментальной ЭВМ управление сбором событий профилирования осуществляет менеджер профилирования и контроля модельных параметров. Менеджер профилирования является стандартным компонентом комплекса «СОМ». Он взаимодействует с остальными компонентами комплекса (таблицей имён, компонентами сред выполнения). Менеджер профилирования передаёт агенту пользовательские запросы на запуск/останов/сброс профилирования, а также на изменение маски событий профилирования. Также менеджер профилирования сохраняет полученную информацию в БД событий и обрабатывает сигналы о несоответствии параметров производительности параметрам, заложенным в модель,

В качестве программ-анализаторов используются как компоненты комплекса «СОМ», так и внешние компоненты. На рисунке 2 приведена диаграмма использования динамической памяти потоками «ОС РВ Багет 2.0»,

построенная при помощи программы hp2ps инструмента Massif, входящего в состав программного комплекса Valgrind. На этой диаграмме по вертикали откладывается количество байтов, по горизонтали - время, в которое производился очередной срез профилирования (время отсчитывается от момента запуска сбора информации драйвером профилирования на целевой ЭВМ).

Далее в четвёртой главе приводится описание оптимизации по профилю, реализованное в кросс-компиляторе GK PB Багет 3.0 (разработке НИИСИ РАН). Необходимая поддержка со стороны целевой ОС была выполнена автором данной работы.

В заключении приводятся результаты работы.

Основные результаты работы

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

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

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

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

4. На основании выполненных теоретических и практических разработок произведено расширение инструментального комплекса контролируемого выполнения «СОМ», обеспечена интеграция средств управления и отладки со средствами моделирования, сбора и анализа количественных характеристик функционирования распределённых разнородных аппаратно-программных комплексов.

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

Работы автора по теме диссертации

[1] Вьюкова Н.И., Галатенко В.А., Малиновский A.C., Шмырев Н.В. Адаптивная компиляция на основе данных профилирования. - Информационная безопасность. Технологии программирования // под ред. В.Б. Бетелина. - М.: НИИСИ РАН, 2007. - С. 109-124.

[2] Вьюкова Н.И., Галатенко В.А., Малиновский A.C., Шмырев Н.В. Адаптивная компиляция на основе данных профилирования. - Программные продукты и системы, 2007, N3. - С. 5-8.

[3] Вьюкова Н.И., Шмырев Н.В. и др. Описание отладочного комплекса «СОМ» - Инструментальные средства программирования // под ред.

B.Б. Бетелина. - М.: НИИСИ РАН, 2006. - С. 4-50.

[4] Галатенко В.А., Костюхин К.А., Малиновский A.C., Шмырев Н.В. Моделирование распределенных систем реального времени. - Труды IV международной конференции «Параллельные вычисления и задачи управления». - М.: ИПУ РАН, 2008. - С. 1349-1355.

[5] Галатенко В.А., Костюхин К.А., Малиновский A.C., Шмырев Н.В. Модели систем реального времени, ориентированные на контроль количественных параметров работы системы. - Труды международной конференции «Моделирование-2008». - Киев: ИПМЕ HAH Украины, 2008. -

C. 423-428.

[6] Галатенко В.А., Костюхин К.А., Малиновский A.C., Шмырев Н.В. Организация профилирования распределенных программно-аппаратных

комплексов. - Труды IV международной конференции «Параллельные вычисления и задачи управления». - М.: ИПУ РАН, 2008. - С. 1183-1191.

[7] Галатенко В.А., Костюхин К.А., Малиновский A.C., Шмырев Н.В. Построение системы профилирования в рамках концепции контролируемого выполнения. - Технологии программирования. Учетные системы. Ортонормированные системы // под ред. В.Б. Бетелина. - М.: НИИСИ РАН, 2008. - С. 4-12.

[8] Шмырев Н.В. Формальная модель контролируемого выполнения. - Технологии программирования. Учетные системы. Ортонормированные системы / под ред. В.Б. Бетелина. - М.: НИИСИ РАН, 2008. - С. 141-148.

[9] Галатенко В.А., Костюхин К.А., Малиновский A.C., Шмырев Н.В. Моделирование и верификация программ как элемент контролируемого выполнения. - «Программные продукты и системы», 2008, N 4. - С. 1417.

[10] Костюхин К.А., Малиновский A.C., Шмырев Н.В. Организация профилирования сложных систем в условиях дефицита ресурсов. - «Программные продукты и системы», 2008, N 4. - С. 17-20.

[11] Галатенко В.А., Костюхин К.А., Малиновский A.C., Шмырев Н.В. Учет и анализ количественных характеристик встраиваемых систем в условиях дефицита ресурсов. - Труды VIII международной конференции «Идентификация систем и задачи управления». - М.: ИПУ РАН, 2008. -С. 684-691.

Подписано в печать: 13.05.2009

Заказ № 2034 Тираж - 100 экз. Печать трафаретная. Типография «11-й ФОРМАТ» ИНН 7726330900 115230, Москва, Варшавское ш., 36 (499) 788-78-56 www.autoreferat.ru

Введение

1 Обзор методов профилирования и моделирования производительности

1.1 Диагностика производительности.

1.2 Направления развития средств профилирования.

1.3 Автоматическое использование данных профилирования

1.4 Управление производительностью.

1.5 Моделирование производительности.

1.6 Проблемы соответствия модели и приложения.

1.7 Программирование, ориентированное на мониторинг.

1.8 Выводы.

2 Моделирование, сбор и анализ количественных характеристик функционирования как аспекты контролируемого выполнения

2.1 Расширение понятия контролируемого выполнения аппаратно-программных комплексов.

2.2 Особенности целевых аппаратно-программных комплексов

2.3 Контролируемое выполнение, основанное на моделировании и верификации.

2.4 Сбор и анализ информации средствами контролируемого выполнения

2.5 Выводы.

3 Моделирование систем и количественных характеристик их функционирования

3.1 Модель распределённых вычислений.

3.1.1 Моделирование разных аспектов вычисления.

3.1.2 Моделирование ресурсов.

3.1.3 Полная модель приложения.

3.2 Моделирование последовательных распределённых приложений

3.3 Автоматизация описания приложения

3.4 Использование ACSL.

3.5 Библиотека моделирования и самоконтроля.

3.5.1 Аннотированная библиотека самоконтроля.

3.5.2 Аннотации к системным функциям взаимодействия потоков и процессов.

3.5.3 Вспомогательные утверждения

3.6 Интеграция со средой разработки приложений

3.7 Выводы.

4 Сбор и анализ количественных характеристик функционирования

4.1 Сбор количественных характеристик.

4.1.1 Архитектура системы профилирования.

4.1.2 Описание компонентов системы профилирования

4.2 Поддержка оптимизации по профилю в компиляторе СКРВ Багет 3.0.

4.3 Выводы.

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

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

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

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

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

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

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

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

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

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

• Предложены средства построения моделей распределённых разнородных аппаратно-программных комплексов с учётом количественных характеристик их функционирования.

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

Апробация. Основные положения диссертационной работы докладывались на 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 глав, заключения и списка литературы.

4.3 Выводы

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

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

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

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

Заключение

В диссертационной работе получены следующие основные результаты:

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

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

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

4. На основании выполненных теоретических и практических разработок произведено расширение инструментального комплекса контролируемого выполнения «СОМ», обеспечена интеграция средств управления и отладки со средствами моделирования, сбора и анализа количественных характеристик функционирования распределённых разнородных аппаратно-программных комплексов.

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

1. Вьюкова Н. И., Галатенко В. А., Малиновский А. С., Шмырев Н. В. Адаптивная компиляция на основе данных профилирования // Информационная безопасность. Технологии программирования / Под ред. Бетелина. — М.: НИИСИ РАН, 2007. — С. 109-124.

2. Вьюкова Н. И., Галатенко В. А., Малиновский А. С., Шмырев Н. В. Адаптивная компиляция на основе данных профилирования // Программные продукты и системы. — 2007. — № 3. — С. 5-8.

3. Вьюкова Н. И., Шмырев Н. В. и др. Описание отладочного комплекса СОМ // Инструментальные средства программирования / Под ред. Бетелина. М.: НИИСИ РАН, 2006. - С. 4-50.

4. Галатенко В. А., Костюхин К. А., Малиновский А. С., Шмырев Н. В. Моделирование и верификация программ как элемент контролируемого выполнения // Программные продукты и системы. — 2008. — № 4. — С. 14-17.

5. Годунов А. Н. и др. Введение в ос2000 // Вопросы кибернетики / Под ред. Бетелина. — М.: НИИСИ РАН, 1999.

6. КБ Корунд-М.— Семейство ЭВМ для специализированных применений, 1997.

7. Костюхин К. А. Организация контролируемого выполнения для разнородных распределенных программно-аппаратных комплексов: Ph.D.thesis / Научно-исследовательский институт системных исследований. — 2006.

8. Костюхин К. А., Малиновский А. С., Шмырев Н. В. Организация профилирования сложных систем в условиях дефицита ресурсов // Программные продукты и системы. — 2008. — № 4. — С. 17-20.

9. Шмырев Н. В. Формальная модель контролируемого выполнения // Технологии программирования. Учетные системы. Ортонормирован-ные системы / Под ред. Бетелина. — М.: НИИСИ РАН, 2008. — С. 141148.

10. Anand М., Kim J., , Lee I. Code generation from hybrid systems models for distributed embedded systems // ISORC. — 2005. — Pp. 28-36.

11. Baudm P., Filliatre J.-C., Marche G. et al— ASCL: ANSI/ISO С Specification Language, 2008.

12. Auguston M., Jeffery C., Underwood S. A framework for automatic debugging // Automated Software Engineering. — 2002. — Pp. 217-222.

13. Auguston M., Jeffery C., Underwood S. A monitoring language for run time and post-mortem behavior analysis and visualization // AADEBUG. — 2003.

14. Benini S. L., Micheli G. D., Hans M. Source code optimization and profiling of energy consumption in embedded systems //In International Symposium on System Synthesis. — 2000. — Pp. 193-198.

15. Beyer D., Henzinger T. A., Jhala R., Majumdar R. Checking Memory Safety with BLAST // FASE'05. — 2005. Pp. 2-18.

16. Beyer D., Henzinger Т., Jhala R., Majumdar R. The Software Model Checker BLAST: Applications to Software Engineering // Int. Journal on Software Tools for Technology Transfer2007.— no. 9(5-6).— Pp. 505525.

17. Binkley D. Source code analysis: A road map // Future of Software Engineering (FOSE). — 2007. — Pp. 104-119.

18. Boldo S., Filliatre J.-G. Formal verification of floating-point programs // CF. 2008.

19. Boronat A., Meseguer J. An Algebraic Semantics for MOF // FASE. — 2008.

20. Brunst H., Knupfer A. — Open Trace Format API Specification. Version 1.1. — http://www.paratools.com/otf/specification.pdf.

21. Burger R. G., Dybvig R. K. An infrastructure for profile-driven dynamic recompilation // In ICCL'98, the IEEE Computer Society International Conference on Computer Languages. — IEEE, 1998.— Pp. 240-251.

22. Carloni L., Benedetto M. D. D., Pinto A., Sangiovanni-Vincentelli A. — Modeling Techniques, Programming Languages, Design Toolsets and Interchange Formats for Hybrid Systems, 2004.

23. Chaki S., Clarke E., Sharygina N. Sinha N. Dynamic component substi-tutability analysis //In Proc. of Conf. on Formal Methods.— Springer Verlag, 2005.-Pp. 512-528.

24. Chanda A., Cox A. L., Zwaenepoel W. Whodunit: transactional profiling for multi-tier applications // SIGOPS Oper. Syst. Rev. — 2007. — Vol. 41, no. 3. Pp. 17-30.

25. Chang P., Mahlke S., Hwu W. Using profile information to assist classic code optimizations I j Software: Practice and Experience. — 1991. — December. — no. 21(12). — Pp. 1301-1321.

26. Chen F., Rosu G. MOP: Reliable Software Development using Abstract Aspects: Tech. rep.: Dept. of Computer Science, University of Illinois, 2006.

27. Chen W. Y. et al. Profile-assisted instruction scheduling // International Journal of Parallel Programming. — 1994. — Vol. 22, no. 2. — Pp. 151-181

28. Compositional quantitative reasoning / K. Chatterjee, L. de Alfaro, M. Faella et al. // ACM. 2007.

29. Cox J., Howel D., Conte T. Commercializing Profile-Driven Optimization // Proceedings of the 28th Annual Hawaii lntemotional Conference on System Sciences. — 1995.

30. Dauphin P. Combining functional and performance debugging of parallel and distributed systems based on model-driven monitoring //In 2nd Eu-romicro Workshop on Parallel and Distributed Processing. — IEEE Computer Society Press, 1994. — Pp. 463-470.

31. Efficient Verification of Sequential and Concurrent С Programs / S. Chaki, E. Clarke, A. Groce et al. // Formal Methods in System Design. — 2004.— Vol. 25, no. 2-3. — Pp. 129-166.

32. End-user tools for application performance analysis using hardware counters / K. London, J. Dongarra, M. S. et al. // International Conference on Parallel and Distributed Computing Systems. — 2001.

33. Espinoza H., Servat D., Gerard S. Leveraging Analysis-Aided Design Decision Knowledge in UML-Based Development of Embedded Systems // SHARK. — 2008.— Pp. 55-62.

34. Experiences and lessons learned with a portable interface to hardware performance counters / J. Dongarra, K. London, S. Moore et al. // IPDPS 2003.— 2003.

35. Filliatre J.-C- Verification of nun-functional programs using interpretations in type theory // J. Functional Programming. — 2003.— Vol. 13, no. 4.— Pp. 709-745.

36. Filliatre J.-C., Marche C. The Why/Krakatoa/Caduceus Platform for Deductive Program Verification // OOPSLA. — 2004.

37. GCC: the GNU Compiler Collection. —http://gcc.gnu.org.

38. Gherbi A., Khendek F. Timed-automata Semantics and Analysis of UML/SPT Models with Concurrency // Proceedings of the 10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing. — 2007. — Pp. 412-419.

39. GNU binutils home page, — http://www.gnu.org/software/bmutils/binutils.html.

40. Gunter R. Profile driven loop transformations // GCC Developers Summit Procedings. — Ottawa, Ontario, Canada: 2006.— June.

41. Gu G. P., Petriu D. C. From UML to LQN by XML algebra-based model transformations // Proceedings of the 5th international workshop on Software and performance. — 2005. — Pp. 99 110.

42. Hammond K., Ferdinand C., Heckmann R. Towards formally verifiable resource bounds for real-time embedded systems // SIGBED Rev. — 2006. — Vol. 3, no. 4. Pp. 27-36.

43. Havelund К. Run-Time Verification of С Programs // 1st Int. TEST-COM/FATES Conference on Testing of Communicating Systems (TEST-COM) and Formal Approaches to Testing of Software (FATES). — 2008.

44. Havelund K., Wyk E. V. Aspect-Oriented Monitoring of С Programs // EUROMICRO'tM. 2008.

45. Heath M. Т., Malony A. D., Rover D. T. Parallel performance visualization: From practice to theory // IEEE Parallel Distrib. Technol. —1995. — Vol. 3, no. 4. — Pp. 44-60.

46. Henzinger T. A., Alur R. Logics and models of real time // Real Time: Theory in Practice, Lecture Notes in Computer Science.— 1992.— Vol. 600.

47. Henzinger T. A., Horowitz В., Majumdar R., Wong-toi H. Beyond HYTECH: Hybrid systems analysis using interval numerical methods // in HSCC. Springer, 2000. — Pp. 130-144.

48. Henzinger T. A., Sifakis J. The embedded systems design challenge // 14th International Symposium on Formal Methods (FM). — 2006. — Pp. 1-15.

49. Henzinger Т., Kirsch C., Sanvido M., Pree W. From control models to real-time code using Giotto // IEEE Control Systems Magazine. — 2003.— Vol. 23(1).-Pp. 50-64.

50. Herzinger Т., R.Jhalla, R.Majumdar, G.Sutre. Lazy abstraction, principles of programming languages // ACM. — 2002. — Pp. 58-70.

51. Hoare C. A. R. An axiomatic basis for computer programming // Communications of ACM.— 1969. — Vol. 12(10).—Pp. 576-583.

52. Hoskins D. S., Colbourn C. J., Montgomery D. C. Software performance testing using covering arrays // WOSP. — 2005.

53. Hubicka J. Profile driven optimizations in gcc // GCC Developers Summit Procedings. — Ottawa, Ontario, Canada: 2005. — June.

54. Jantsch A., Sander I. Models of computation and languages for embedded system design // IEE Proceedings on Computers and Digital Techniques. — 2005. Pp. 114-129.

55. Jayaputera J., Poernomo I., Schmidt H. Runtime Verification of Timing and Probabilistic Properties using WMI and .NET // EUROMICRO'04. -2004.

56. Jejjry T Russell M. F. J. Scenario-based software characterization as a contingency to traditional program profiling // CASES. — 2002.

57. JML: notations and tools supporting detailed design in Java / G. T. Leavens, K. Rustan, M. Leino et al. // OOPSLA. — 2000. — Pp. 105-106.

58. Jones J., Harrold M. Empirical evaluation of the tarantula automatic fault-localization technique // Proc. of the 20th IEEE/ACM International Conference on Automated Software Engineering.— 2005.

59. JozefH. Extending Hoare logic to Real-Time // Formal aspects of computing. — 1995.

60. Kistler Т., Franz M. Continuous program optimization: A case study // ACM Transactions on Programming Languages and Systems.— 2003.— July. Vol. 25, no. 4. — Pp. 500-548.

61. Lamport L. The temporal logic of actions // ACM Transactions on Programming Languages and Systems. — 1994. — Vol. 16(3). — Pp. 872-923.

62. Lattner C. LLVM: An Infrastructure for Multi-Stage Optimization: Ph.D. thesis / University of Illinois at Urbana-Champaign. — 2002.

63. Lavagno L., Sangiovanni-vincentelli A., Sentovich E. Models of computation for embedded system design //in NATO ASI Proc. on System Synthesis. — Kluwer Academic Publishers, 1998. — Pp. 45-102.

64. Liu Z., Joseph M. Real-Time and Fault-Tolerant Systems. Specification, verification, refinement and scheduling. — UUNU/IIST, 2005.

65. Maier-Komor T.} von Bulow A., Farber G. MetaC and its Use for Automated Source Code Instrumentation of С Programs for Real-Time Analysis // Euromicro Conference on Real-Time Systems. — 2003.

66. Malony A. D., Helm B. R. A theory and architecture for automating performance diagnosis // Future Gener. Comput. Syst.— 2001.— Vol. 18, no. 1.—Pp. 189-200.

67. Malony A. D., Shende S. The TAU Parallel Performance System // International Journal of High Performance Computing Applications. — 2006. — Vol. 20, no. 2.- Pp. 287-311.

68. Management O. — UML Profile for Schedulabibity, Performance and Time Specification, 2005.

69. Manna Z., Pnueli A. The Temporal Logic of Reactive and Concurrent Systems: Specification. — Springer-Verlag, 1991.

70. Modular Verification of Software Components in С // Transactions on Soft-ware Engineering (TSE).— 2004. — Vol. 30, no. 6. — Pp. 388-402.

71. Monate В., Signoles J. Slicing for Security of Code // Trust '08: Proceedings of the 1st international conference on Trusted Computing and Trust ini Information Technologies. — Berlin, Heidelberg: Springer-Verlag, 2008.— Pp. 133-142.

72. Moseley P., Debray S., Andrews G. Checking program profiles // Third IEEE International Workshop of Source Code Analysis and Manipulation. — 2003.

73. Nicolau A. Run-time disambiguation: coping with statically unpredictable dependencies // ieeetc. — 1989. — May. — Vol. 38. — Pp. 663-678.

74. Object Management Group: Meta Object Facility (MOF) 2.0 Core Specification:. — http://www.omg.org/docs/formal/06-01-01.pdf.85. oprofile home page. — http://oprofile.sourceforge.net.

75. PAPI User's Guide.—http://icl.cs.utk.edu/projects/papi.

76. Parallel Tools Consortium. — http://www.ptools.org.

77. Performance technology for parallel and distributed component software: Research articles / A. Malony, S. Shende, N. Trebon et al. // Concurr. Comput. : Pract. Exper. — 2005. — Vol. 17, no. 2-4. — Pp. 117-141.

78. Pnueli A. The temporal logic of programs // 18th Annual Symposium on Foundations of Computer Science. — 1977. — Pp. 46-57.

79. Profiling tools for hardware/software partitioning of embedded applications // LCTES. — 2003.91. iSchneider F. В., Bloom В., Marzullo K. Putting time into proof outlines // Real-Time: Theory in Practice. — 1992. — Pp. 618-639.

80. Smith C. The evolution of software performance engineering: A survey // IEEE. — 1986.

81. Smith C., Williams L. QSEM: Quantitative Scalability Evaluation Method // IEEE. — 2005.

82. Spear W., Malony A. D., Morris A., Shende S. Integrating TAU With Eclipse: A Performance Analysis System in an Integrated Development Environment // High Performance Computing and Communications.— 2006.- Pp. 230-239.

83. System level performance analysis the SymTA/S approach / R. Henia, A. Hamann, M. Jersak et al. // Computers and Digital Techniques, IEE. — 2005. - Vol. 152. — Pp. 148 - 166.

84. The Coq Proof Assistant. — http://coq.inria.fr.

85. The Frama-C framework for analysis of С code. — http://frama-c.cea.fr/.

86. Truong H.-L., Fahringer T. Self-managing sensor-based middleware for performance monitoring and data integration in grids //19 IEEE International Parallel and Distributed Processing Symposium (IPDPS 2005). — IEEE, 2005.

87. Truong H.-L., Fahringer T. Soft computing approach to performance analysis of parallel and distributed programs // Euro-Par 2005 Parallel Processing. — 2005. — Pp. 50-60.

88. Valgrind home page. — http://valgrind.org.

89. Vetter J. S., Worley P. H. Asserting performance expectations // Super-computing '02: Proceedings of the 2002 ACM/IEEE conference on Su-percomputing. — Los Alamitos, CA, USA: IEEE Computer Society Press, 2002.-Pp. 1-13.

90. Weiss A. R. — Dhrystone Benchmark. White Paper, 2002. — October. — http://www.ebenchmarks.com.

91. Woodside M., Franks G., Petriu D. C. The future of software performance engineering // FOSE '07: 2007 Future of Software Engineering.— Washington, DC, USA: IEEE Computer Society, 2007. — Pp. 171-187.

92. Yi J., Woo H., Browne J. С., Мок A. K. Runtime Verification of Timing and Probabilistic Properties using WMI and .NET // IEEE Real-Time and Embedded Technology and Aplication Symposium. — 2008.