Preview

Труды Института системного программирования РАН

Расширенный поиск
Том 27, № 2 (2015)
5-22
Аннотация
В работе описывается подход, применяемый в ParJava по разработке многопроцессно-многопоточных (МПМП) программ. Разработан API и поддерживающая его библиотека, которая позволяет писать параллельные МПМП приложения на языке Java оставаясь в рамках стандарта MPI. Использование потоков в программе позволяет лучше утилизировать ресурсы многоядерного процессора. В рамках работы реализована МПМП программа быстрого преобразования Фурье на языке Java. Проведенные эксперименты показали, что МПМП программа работает быстрее, чем многопроцессная программа.
23-38
Аннотация
Данная статья посвящена вопросам проведения анализа программ интерпретируемых языков программирования. В качестве целевой задачи рассматривается автоматический сбор и обработка статистики использования динамической памяти при выполнении приложений операционной системы Android на виртуальной машине Dalvik. Рассматриваются основные свойства виртуальной машины Dalvik (организация работы с кучей, протоколы отладки) и описывается ряд возможных модификаций Dalvik, позволяющих проводить сбор информации о выполнении программы. Статья завершается обзором результатов применения использованной модифицированной версии Dalvik для анализа ряда стандартных приложений Android.
39-52
Аннотация
В статье рассматривается подход к поиску состояний гонки в многопоточных программах на языке Java при помощи динамического анализа. Преимущества динамического анализа заключаются в отсутствии ложных срабатываний при определённых ограничениях, накладываемых на анализируемую программу. Для проведения анализа используется статическая инструментация байт-кода языка Java при помощи инструмента Coffee Machine, что позволяет избежать накладных расходов, связанных с внедрением инструментационного кода в ходе выполнения программы и проводить анализ программ на виртуальных машинах, не предоставляющих интерфейс для динамической инструментации. Инструментируются инструкции доступа к памяти, вызова методов, работы с потоками и мониторами. Поиск ошибок осуществляется при помощи инструмента ThreadSanitizer Offline на основе построения отношений предшествования на множестве событий, собранных в ходе выполнения программы, и построения множеств блокировок. Наличие связи с исходным кодом для проведения анализа не является необходимым, однако это позволяет более точно определить причины возникновения ошибки. Реализация была проверена на ряде проектов с открытым исходным кодом и продемонстрировала свою эффективность для поиска состояний гонки.
53-64
Аннотация
В статье рассматривается инструмент статического анализа программ, определяющий сущности программы на языке Си или Си++, их метрики и связи между ними. Сущностями программы являются файлы, функции, классы, методы и т.п., а связями - вызовы, наследование, чтение/запись глобальных переменных, включение, агрегация. Описываются методы построения такого инструмента на основе открытой компиляторной инфраструктуры LLVM[1], включая необходимые доработки в компиляторе Clang[2] и разработанный анализатор. Представляются результаты тестирования инструмента на коде ОС Android.
65-92
Аннотация
Технология (детерминированного) воспроизведения вычислительного процесса в виртуальных вычислительных машинах используется для отладки, повышения отказоустойчивости, а также в различных исследованиях программного кода, в том числе, в области информационной безопасности при обратной инженерия вредоносных программ. В данной работе описывается реализация технологии воспроизведения для гостевых машин на базе Intel Architecture 32-bit в программном эмуляторе QEMU, предлагающая минимизацию перечня воспроизводимых устройств. Подробно рассмотрено устройство эмулятора QEMU и обоснованы технические приемы, использованные при реализации. Приводятся экспериментальные оценки ключевых характеристик: объем записываемого журнала недетерминированных событий и замедление.
93-104
Аннотация
В статье предлагается новый метод поиска семантических ошибок, возникающих при неправильном копировании исходного кода в процессе разработки ПО. Метод состоит из двух основных этапов. На первом этапе производится поиск клонов кода на основе лексического анализа программы. Найденные идентичные последовательности лексем фильтруются путем частичного разбора. После чего в них остаются целостные конструкции, допускаемые языком программирования. На втором этапе производится анализ найденных клонов с целью обнаружения допущенных ошибок при копировании. Для этого строится и анализируется граф зависимостей программы (Program Dependence Graph - PDG). Предложенный подход реализован в компиляторной инфраструктуре LLVM/Clang, что позволяет эффективным образом производить анализ, во время компиляции проекта. Найденные ошибки выдаются в виде предупреждений для разработчика. В статье приводится результаты анализа ядра Linux 2.6 и Android 4.3. Инструмент обеспечивает точность выше 65%.
105-126
Аннотация
В статье рассматривается метод выявления ошибок работы с памятью в бинарном коде программ, таких как выход за границы буфера при чтении и записи. Предлагаемый метод основывается на использовании динамического анализа и символьного выполнения. Метод применяется к бинарным файлам программ без дополнительной отладочной информации. Описанный метод был реализован в виде программного инструмента. Возможности инструмента продемонстрированы на примере поиска ошибок в 11 программах, которые работают под управлением ОС Windows и Linux, в 7 из них ошибки не были исправлены на момент написания статьи.
127-144
Аннотация
Обратная отладка - это инструмент разработки ПО, позволяющий более эффективно справляться с ошибками, возникающими при недетерминированном поведении программы. Она позволяет изучать прошедшие состояния программы без ее повторного запуска. В работе описана реализация обратной отладки на основе детерминированного воспроизведения в симуляторе QEMU 2.0. Предлагаются несколько способов повышения производительности отладки за счет сокращения дополнительно записываемых данных, оптимального сохранения снимков системы, индексации и сжатия журнала событий. Симулятор может работать совместно с интерактивным отладчиком GDB, что позволяет использовать команды reverse-continue, reverse-nexti, reverse-stepi и reverse-finish в процессе отладки. Скорость работы этих команд зависит от периода сохранения состояний системы в процессе записи ее работы. В статье представлена оценка наилучшего периода для оптимальной скорости работы команды reverse-continue.
145-160
Аннотация
В данной статье описаны результаты работы по созданию тестового набора для тестирования соответствия реализаций клиента протокола TLS спецификациям Интернета. В качестве базы для построения тестов мы использовали технологию UniTESK и программный пакет JavaTesK, реализующий эту технологию. Для мутационного тестирования протокола были разработаны операторы мутации для некоторых основных типов данных, которые используются в формальной модели протокола. Этот подход доказал свою эффективность, поскольку обеспечил обнаружение отклонений от спецификации и других ошибок во всех выбранных реализациях клиента протокола.
161-172
Аннотация
Рассматриваемые в этой статье алгебраические модели программ являются обобщением двух моделей программ, введенных в работах А.А. Ляпунова и А.А. Летичевского. Центральное место в теории таких моделей занимает проблема эквивалентности схем программ, заменивших формализованные программы. Доказана разрешимость этой проблемы в широком классе алгебраических моделей программ. Методика получения этого результата восходит к разрешимости проблемы эквивалентности конечных автоматов. Задача статьи состоит в выявлении этого обстоятельства.
173-188
Аннотация
В статье рассматриваются алгебраические модели программ с процедурами. Для специфического класса моделей, связанного с изученным классом моделей программ без процедур, строится полная система эквивалентных преобразований, позволяющая проводить структурный анализ формализованных программ.
189-220
Аннотация
Рассматривается задача параллельного вычисления значения функции от мультимножества значений, записанных в вершинах ориентированного сильно-связного графа. Вычисление выполняется автоматами, находящимися в вершинах графа. Автомат имеет локальную информацию о графе: он «знает» только о дугах, выходящих из вершины, в которой он находится, но «не знает», куда (в какие вершины) эти дуги ведут. Автоматы обмениваются сообщениями, передаваемыми по дугам графа, которые играют роль каналов передачи сообщений. Вычисление инициируется сообщением, приходящим извне в автомат выделенной начальной вершины графа. Этот же автомат в конце работы посылает вовне вычисленное значение функции. Для решения этой задачи предлагаются два алгоритма. Первый алгоритм выполняет исследование графа, целью которого является разметка графа с помощью изменения состояний автоматов в вершинах. Такая разметка используется вторым алгоритмом, который и производит вычисление значения той или иной функции. Это вычисление основано на алгоритме пульсации: сначала от автомата начальной вершины по всему графу распространяются сообщения-вопросы , которые должны достигнуть каждой вершины, а затем от каждой вершины «в обратную сторону» к начальной вершине двигаются сообщения-ответы . Алгоритм пульсации, по сути, вычисляет агрегатные функции, для которых значение функции от объединения мультимножеств вычисляется по значениям функции от этих мультимножеств. Однако показано, что любая функция F(x) имеет агрегатное расширение, то есть может быть вычислена как H(G(x)) , где G агрегатная функция. Заметим, что разметка графа не зависит от той функции, которая будет вычисляться. Это означает, что разметка графа выполняется один раз, после чего может многократно использоваться для вычисления различных функций. Поскольку автоматы в вершинах графа работают параллельно, как разметка графа, так и вычисление функции выполняются параллельно. Это первая особенность работы. Вторая особенность - вычисления выполняются на динамически меняющемся графе: его дуги могут исчезать, появляться или менять свои конечные вершины. На изменения графа налагаются такие минимальные ограничения, которые позволяют решать эту задачу за ограниченное время. Приводится оценка времени работы обоих предлагаемых алгоритмов.
221-250
Аннотация
Автоматы-преобразователи с конечным числом состояний над полугруппами могут служить простой моделью последовательных реагирующих программ. Эти программы работают во взаимодействии с окружающей средой, получая на входе поток управляющих сигналов и выполняя последовательности действий. Как только программа достигает определенного состояния управления, она выдает на выходе текущий результат вычисления. Элементарные действия реагирующей программы можно рассматривать как порождающие элементы некоторой полугруппы, а результат последовательного выполнения этих действий расценивается как элемент полугруппы, представляющий собой композицию этих действий. В данной статье предложен общий подход к решению двух задач анализа вычислений преобразователей такого вида - задачи проверки k-значности конечных преобразователей и задачи проверки эквивалентности k-значных преобразователей. Показано, что обе указанные задач можно свести к задаче поиска опровергающих вершин в ограниченных фрагментах размеченных системах переходов. При помощи предложенного подхода показано, что задача проверки эквивалентности детерминированных конечных преобразователей над полугруппами, которые могут быть вложены в конечно порожденные разрешимые полугруппы, и задача проверки k-значности таких преобразователей разрешимы за полиномиальное время. Кроме того, установлено, что задача проверки эквивалентности k-значных преобразователей разрешима за время, экспоненциальное относительно их размеров.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


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