Proceedings of ISP RAS


Introduction.

V.P. Ivannikov.

Abstract

В 22-м томе Трудов ИСП РАН публикуются статьи сотрудников Института (главным образом, молодых специалистов), в которых описываются результаты научных исследований, полученные в конце 2011-го – начале 2012 гг.

Том открывается двумя статьями А.И. Аветисяна. Первая из них называется «Двухэтапная компиляция для оптимизации и развертывания программ на языках общего назначения» и содержит описание метода двухэтапной компиляции программ на языках общего назначения (Си/Си++), основанного на компиляторной системе LLVM и позволяющего проводить оптимизации программ с учетом профиля пользователя и особенностей его целевой машины, а также организовывать развертывание программ в облачном хранилище с дополнительной оптимизацией и поиском дефектов программ.

Во второй статье А.И. Аветисяна – «Планирование команд и конвейеризация циклов на современных архитектурах» – предлагается метод планирования команд и конвейеризации циклов, основанный на расширяемой архитектуре планировщика, содержащей компоненты выявления и использования параллелизма на уровне команд.

В статье Романа Жуйкова, Дмитрия Мельника и Рубена Бучацкого «Программная конвейеризация циклов на платформе ARM» описывается адаптация для архитектуры ARM алгоритма поворотного модульного планирования, используемого в компиляторе GCC. Для обеспечения поддержки архитектуры ARM были в этот алгоритм были внесены значительные изменения, которые позволили ускорить ряд тестовых приложений на 3-4%.

Статья Романа Жуйкова, Дмитрия Плотникова и Мамикона Варданяна «Автоматическая настройка оптимизационных преобразований компилятора GCC для платформы ARM» посвящена описанию системы для автоматической настройки параметров компиляции, предназначенной для использования на встраиваемых платформах. С использованием этой системы, в частности, были выявлены недочеты в работе компилятора GCC, приводящие к генерации неоптимального кода для платформы ARM.

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

К. Батузов, П. Довгалюк, В. Кошелев и В. Падарян в своей статье «Два способа организации механизма полносистемного детерминированного воспроизведения в симуляторе QEMU» предлагают два подхода к реализации полносистемного детерминированного воспроизведения в симуляторе QEMU, которые отличаются тем, какие компоненты виртуальной машины включаются в воспроизведение. Оцениваются достоинства и недостатки этих подходов, оценивается уровень накладных расходов при записи журнала невоспроизводимых событий..

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

Статью «Инкрементальный анализ исходного кода на языках C/C++» написали В.О. Савицкий и Д.В. Сидоров. В статье описывается метод построения статического анализатора кода, позволяющий существенно сократить время повторного поиска дефектов для языков С\С++. Используется свойство малого отношения количества лексем из исходного файла к количеству лексем из заголовочных файлов. Метод реализован в программном продукте для среды разработки MS Visual Studio.

Статья А.Ю.Тихонова и А.И. Аветисяна «Комбинированный (статический и динамический) анализ бинарного кода» посвящена обсуждению проблем анализа программ в бинарном коде для распознавания алгоритмов составляющих их функций, выяснения особенностей реализации алгоритмов, обнаружения недокументированных возможностей. В ряде случаев статический анализ может не дать результатов. Предлагается использовать в таких случаях в дополнение к статическому анализу динамический анализ (анализ трасс программы). Описывается разработанная и реализованная авторами среда динамического анализа бинарного кода TrEx и ее интеграция с известной средой статического анализа Ida Pro.

И.Н.Ледовских и М.Г.Бакулин являются авторами статьи «Подход к восстановлению потока управления запутанной программы». В статье описывается подход к восстановлению потока управления программы, запутанного комбинацией различных преобразований – от вставки недостижимого кода с помощью непрозрачных предикатов до виртуализации. Приводятся результаты тестирования прототипной реализации данного подхода на модельном примере, запутанном с применением различных инструментальных средств защиты.

В статье В.Н. Игнатьева «Использование легковесного статического анализа для проверки настраиваемых семантических ограничений языка программирования» отмечается, что для достижения переносимости, надёжности и безопасности программ на С и С++ могут вводиться дополнительные ограничения на язык и стиль программирования. Предлагается новый метод формализации и классификация таких ограничений, описывается система их автоматической проверки, основанная на применении статического анализа, а также способ интеграции с распространёнными системами сборки проектов.

А.О. Кудрявцев, В.К. Кошелев и А.И. Аветисян в статье «Перспективы виртуализации высокопроизводительных систем архитектуры x64» исследуют перспективы применения технологий виртуализации в области высокопроизводительных вычислений на платформе x64. Рассматриваются основные причины падения производительности при запуске параллельных программ в виртуальной среде. Подробно рассматриваются системы виртуализации KVM/QEMU и Palacios. В качестве тестовых пакетов используются HPC Challenge и NAS Parallel Benchmarks.

Статья Андрея Белеванцев, Алексея Меркулова и Владимира Платонова «Использование стандарта OpenCL для программирования ПЛИС» посвящена использованию стандарта OpenCL для облегчения программирования логических интегральных схем (ПЛИС), применяемых в качестве акселератора в гетерогенной вычислительной системе. Описывается схема реализации подмножества стандарта, обеспечивающая обмен памятью и управление выполнением задач на ПЛИС в предположении, что ПЛИС связана с центральным процессором через шину PCI-express.

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

Целью статьи Игоряь Бурдонова и Александра Косачева «Финальные модели спецификации» является выделение подмножества трасс спецификации, достаточного для генерации полного набора тестов. Такое подмножество авторы назвали финальной трассовой моделью спецификации. Традиционная LTS-модель удобна тем, что является способом конечного представления регулярных множеств трасс. Для представления финальной трассовой модели в работе предлагается разновидность LTS, названная финальной RTS (Refusal Transition System). Такая модель обладает целым рядом свойств, полезных для генерации тестов.

В статье С. П. Вартанова и Д.В. Сидорова «Оптимизация задачи проверки выполнимости булевских ограничений при помощи кэширования промежуточных результатов» предложена оптимизация алгоритма проверки выполнимости булевых формул DPLL (Davis — Putnam — Logemann — Loveland) с помощью кэширования промежуточных результатов при решении задачи нахождения входных данных для неинтерактивных программ. Дополнительная информация для оптимизации алгоритма запоминается на одном из предыдущих запусков алгоритма. Возможность подобного рода модификации алгоритма основана на особенности последовательностей проверяемых формул.

Мандрыкин М.У., Мутилин В.С., Новиков Е.М. и Хорошилов А.В. – авторы статьи «Обзор инструментов статической верификации Си программ в применении к драйверам устройств операционной системы Linux». В работе анализируются методы, используемые в современных инструментах статической верификации Си программ. Представлен обзор текущих возможностей инструментов в части поддержки конструкций языка Си, масштабируемости, видов проверяемых свойств и достоверности результатов анализа. Рассмотрены особенности применения инструментов статической верификации для анализа исходного кода драйверов устройств операционных систем и описаны существующие системы верификации драйверов, построенные на основе таких инструментов.

Статья В.С. Мутилина и М.У. Мандрыкина «Интерполяция формул с кванторами в CSIsat на основе инстанцирования» посвящена реализации на основе инструмента CSIsat интерполяции Крейга для формул с кванторами, заданных в рамках комбинации теорий вещественной линейной арифметики и неинтерпретируемых функций. Предложен способ реализации интерполирования таких формул с помощью инстанцирования подкванторных выражений с использованием внешнего SMT-решателя CVC3. Описываются изменения, которые были внесены в интерполятор и решатель для реализации поддержки кванторной интерполяции. Приводятся результаты тестирования модифицированного интерполятора как на задачах, полученных из набора SMTLIB, так и на тестах, специально сгенерированных для этих целей.

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

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

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

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

В статье В.А.Захарова и Т.А. Новиковой «Полиномиальный по времени алгоритм проверки логико-термальной эквивалентности программ» описывается новая модификация алгоритма проверки логико-термальной эквивалентности программ, основанной на операции вычисления точной нижней грани в решетке конечных подстановок. Показано, что трудоемкость предложенного алгоритма оценивается величиной , где - размер анализируемых программ.

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

В статье А. В. Шокурова «Сравнение сложностей задач нахождения базиса Гребнера идеала и решений этого идеала» сравниваются сложности задач нахождения решения системы алгебраических уравнений и базисов Гребнера идеалов этих систем.

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

Edition

Proceedings of the Institute for System Programming, vol. 22, 2012, pp. 5-10.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2012-22-0

Full text of the paper in pdf (in Russian) Back to the contents of the volume