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

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

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

В данной работе описывается созданная в ИСП РАН система для автоматической настройки параметров компиляции, разработанная для использования на встраиваемых платформах. Система включает в себя средства анализа полученных результатов. С помощью этих средств были выявлены недочеты в работе компилятора GCC, приводящие к генерации неоптимального кода для платформы ARM. Были выявлены причины генерации неоптимального кода, а также рассмотрены и реализованы различные подходы к улучшению оптимизаций. Также была проведена работа по улучшению других оптимизаций компилятора GCC, недостатки которых были обнаружены при ручном анализе ассемблерного кода. Получено значительное увеличение производительности выбранных тестовых приложений на платформе ARM.

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

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

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

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

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

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

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

В данной работе изучаются перспективы применения технологий виртуализации в области высокопроизводительных вычислений на платформе x64. Рассматриваются основные причины падения производительности при запуске параллельных программ в виртуальной среде. Подробно рассматриваются системы виртуализации KVM/QEMU и Palacios, в качестве тестовых пакетов используются HPC Challenge и NAS Parallel Benchmarks. Тестирование выполняется на современном вычислительном кластере, построенном на базе высокоскоростной сети Infiniband. Результаты проведенного исследования в целом показывают целесообразность применения виртуализации для большого класса высокопроизводительных приложений. Доводка рассматриваемых систем виртуализации позволила снизить накладные расходы с 10-60% до 1-5% на большинстве тестов пакетов HPC Challenge и NAS Parallel Benchmarks. Основными "узкими местами" систем виртуализации являются уменьшенная производительность системы памяти (критично только для узкого класса задач), расходы при виртуализации устройств, а также повышенный уровень "шума", источником которого становятся основная ОС и гипервизор. Шум может оказывать негативное влияние на производительность и масштабируемость "мелкозернистых" приложений (приложений с частыми коммуникациями небольшого объема). При увеличении числа узлов в системе, влияние шума существенно усиливается.

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

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

Работа посвящена исследованию формальных методов тестирования соответствия (конформности) исследуемой системы требованиям, заданным в форме спецификации. Такое тестирование основано на семантике взаимодействия, которая определяет тестовые возможности по управлению (заданный набор тестовых воздействий) и наблюдению действий и отказов (отсутствие действий). Допускаются также ненаблюдаемые (внутренние) действия. Семантика параметризуется семействами наблюдаемых и ненаблюдаемых отказов. Вводится разрушение - запрещённое действие, которого следует избегать при взаимодействии. Определяется понятие безопасного тестирования, при котором не возникают ненаблюдаемые отказы и разрушение, и тестовые воздействия не подаются при дивергенции (бесконечной последовательности ненаблюдаемых действий). На этой основе определяются реализационная гипотеза о безопасности и безопасная конформность, а также генерация полного набора тестов по спецификации. В работе исследуются различные модели для описания спецификационных требований. Наиболее распространенной моделью является система помеченных переходов - LTS (Labelled Transition System). В то же время для рассматриваемой семантики взаимодействия существенны только трассы (последовательности наблюдений), но не состояния LTS. Поэтому естественной оказывается трассовая модель как множество трасс LTS. Такая семантика позволяет определять только конформности типа редукции, в отличие от конформностей типа симуляций, для проверки которых требуется дополнительная тестовая возможность - опрос состояния реализации [10],[11],[12],[19],[22]. При безопасном тестировании тесты генерируются по безопасным трассам спецификации, для прохождения которых используются только безопасные тестовые воздействия. Целью данной работы является выделение подмножества трасс спецификации, достаточного для генерации полного набора тестов. Такое подмножество мы назвали финальной трассовой моделью спецификации. С другой стороны, LTS-модель удобна тем, что является способом конечного представления регулярных множеств трасс. Для представления финальной трассовой модели в работе предлагается разновидность LTS, названная финальной RTS (Refusal Transition System). Переходы по наблюдаемым отказам задаются явно (эти отказы входят в алфавит RTS). Такая модель обладает целым рядом полезных для генерации тестов свойств: 1) она детерминирована, 2) трасса наблюдений безопасна тогда и только тогда, когда она заканчивается в нетерминальном состоянии, где нет разрушения, 3) тестовое воздействие безопасно после трассы тогда и только тогда, когда оно безопасно в конечном состоянии трассы, то есть в этом состоянии нет дивергенции, тестовое воздействие не вызывает разрушения и ненаблюдаемых отказов . В работе предложены алгоритмы преобразования LTS-модели в финальную RTS-модель и определены достаточные условия построения конечной RTS за конечное время.

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

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

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

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

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

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

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

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

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

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

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