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

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

Разработка методов автоматической генерации тестов составляет перспективное направление в области верификации цифровой аппаратуры. На текущий момент большое распространение имеют методы генерации функциональных тестов на основе моделей. В данной работе представлен метод генерации функциональных тестов на основе проверки моделей и результаты его сравнения с существующими решениями. В методе используется автоматическое извлечение моделей из исходного кода HDL-описания аппаратуры. Поддерживаются языки VHDL и Verilog. Метод генерации тестов включает автоматическое построение моделей следующих типов: решающие диаграммы системы охраняемых действий (Guarded Action Decision Diagram,GADD), высокоуровневые решающие диаграммы (High-Level Decision Diagrams, HLDD) и расширенные конечные автоматы (Extended Finite-State Machines, EFSM). HLDD-модель используется в качестве функциональной модели. Модель EFSM используется в качестве модели покрытия. Целью тестирования является покрытие всех переходов расширенного конечного автомата. Выбор такого критерия позволяет получить высокое покрытие исходного кода HDL-описания. Из EFSM-модели извлекаются спецификации, основанные на ограничениях на переходы и состояния. Затем спецификации и функциональная модель автоматически транслируются во входной формат инструмента проверки моделей nuXmv. Инструмент выполняет проверку модели и строит контрпримеры. Контрпримеры транслируются в функциональные тесты, которые могут быть исполнены с помощью HDL-симулятора. Предлагаемый метод был реализован программно в инструменте HDL Rertrascope. Результаты экспериментов показывают, что метод генерирует более короткие тесты, чем методы FATE и RETGA, при обеспечении такого же или лучшего покрытия исходного кода.

В статье представлен метод масштабируемой верификации Promela-моделей протоколов обеспечения когерентности памяти. Под масштабируемостью понимается независимость затрат на верификацию (прежде всего, машинного времени и памяти) от числа процессоров в системе. Метод состоит из трех основных шагов. На первом шаге в модель протокола, созданную для определенной конфигурации системы (для конкретного числа процессоров), вводится параметр, представляющий число процессоров в системе. Для этого используются простые индуктивные правила, что возможно только при определенных допущениях на вид протокола. На втором шаге построенная параметризованная модель абстрагируется от числа процессоров. Для этого над присваиваниями, выражениями и коммуникационными действиями модели совершается ряд синтаксических преобразований. На третьем шаге полученная абстрактная модель верифицируется с помощью инструмента Spin обычным образом. Помимо описания метода, в статье приводится доказательство его корректности: утверждается, что предложенная схема абстракции является консервативной в том смысле, что любой инвариант (свойство истинное во всех достижимых состояниях) абстрактной модели является инвариантом исходной модели (свойства-инварианты - это именно те свойства, которые представляют интерес при верификации протоколов обеспечения когерентности памяти). Предложенный метод был воплощен в прототипе инструмента, который разбирает код на языке Promela, строит дерево абстрактного синтаксиса, преобразует его по заданным правилам и отображает обратно в Promela код. Инструмент (и метод в целом) был успешно использован при верификации протоколов семейства MOSI, разработанных в АО «МЦСТ» и реализованных в вычислительных комплексах «Эльбрус».

Генерация тестовых программ на языке ассемблера и проверка корректности результатов их выполнения является наиболее широко применяемым подходом к функциональной верификации микропроцессоров. Данная задача решается при помощи специальных автоматизированных средств, называемых генераторами тестовых программ. Высокая сложность современных электронных устройств создает потребность в автоматизированных средствах, способных генерировать тестовые программы, покрывающие нетривиальные ситуации в их работе. Большинство таких средств используют в качестве входных данных шаблоны тестовых программ, которые позволяют описывать тестовые сценарии в абстрактном виде. Такой подход предоставляет инженерам-верификаторам возможность описывать широкий спектр задач генерации, затрачивая минимальные усилия. Шаблоны тестовых программ разрабатываются на специальных предметно-ориентированных языках. Такие языки должны удовлетворять следующим требованиям: (1) они должны быть достаточно простыми для использования инженерами-верификаторами, не обладающими серьезными навыками программирования; (2) они должны быть применимы для широкого спектра микропроцессорных архитектур и (3) они должны быть легко расширяемы для поддержки описания новых типов задач генерации. В данной работе рассматривается язык описания шаблонов тестовых программ, который был создан для расширяемой среды генерации тестовых программ MicroTESK, разрабатываемой в ИСП РАН. Это гибкий предметно-ориентированный язык, основанный на языке Ruby, который позволяет описывать широкий набор задач генерации в терминах абстракций цифровой аппаратуры. Среда генерации MicroTESK и язык описания тестовых шаблонов успешно применяются в промышленных проектах по верификации микропроцессоров на базе архитектур MIPS и ARM.

В данной работе описан инструмент автоматической генерации тестовых программ для подсистем управления памятью микропроцессоров с архитектурой MIPS64. Предлагаемое средство базируется на среде MicroTESK, разрабатываемой в Институте системного программирования РАН. Инструмент состоит из двух частей: архитектурно независимого ядра генерации тестовых программ и спецификации подсистемы памяти MIPS64. Такое разделение не является новым - аналогичный подход применяется в промышленных генераторах, в том числе в Genesys-Pro, разрабатываемом в исследовательском подразделении компании IBM. Основные различия между инструментами состоят в форме представления спецификаций, типе извлекаемой из них информации и способах использования этой информации для построения тестов. В предлагаемом подходе спецификации включают в себя описания инструкций доступа к памяти (инструкций чтения и записи) и описания механизмов управления памятью, таких как буфер трансляции адресов, таблица страниц, устройство аппаратного поиска по таблице страниц, кэш-память. Для спецификации такого рода механизмов (устройств) разработан проблемно-ориентированный язык, названный mmuSL. Инструмент анализирует mmuSL-спецификации и извлекает все возможные пути исполнения инструкций (варианты обработки запросов к подсистеме памяти) и все возможные зависимости между этими путями (конфликты использования устройств). Извлеченная информация используется для систематического перебора тестовых программ для заданного пользователем тестового шаблона и позволяет исчерпывающим образом исследовать совместное исполнение группы инструкций, включая разного рода граничные случаи. Тестовые данные для тестовых программ (значения адресов, содержимое буферов и т.п.) генерируются с использованием техник символического исполнения и решения ограничений.

Вложенные сети Петри являются одним из удобных формализмов для моделирования и анализа поведения распределенных мультиагентных систем. Они естественным образом представляют структуру мультиагентных систем, так как фишки в системной сети сами являются классическими сетями Петри и могут иметь автономное поведение. Мультиагентные системы являются системами с высоким уровнем параллелизма. При верификации таких систем методами проверки модели (model checking) возникают серьезные трудности, связанные с взрывным ростом числа промежуточных состояний системы (state-space explosion problem). Для решения этой проблемы в литературе был предложен подход, основанный на построении развертки поведения системы. Ранее была изучена применимость разверток для верификации вложенных сетей Петри и предложен метод построения разверток для безопасных консервативных вложенных сетей Петри. В этой работе предлагается другой метод построения разверток для безопасных консервативных вложенных сетей Петри, основанный на трансляции таких сетей в классические сети Петри. Для классических сетей Петри затем применяются стандартные методы построения разверток. Также в работе обсуждаются сравнительные достоинства двух подходов.

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

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

В статье описывается реализация стандарта OpenMP версии 4.0 для акселераторов NVIDIA PTX в компиляторе GCC. Особое внимание уделяется вопросам генерации корректного и эффективного кода для прагм OpenMP с учетом ограничений архитектуры PTX. Поскольку реализация опирается на существующую в GCC трансляцию OpenMP и интеграцию с библиотекой libgomp, для PTX реализованы вторичные программные стеки, позволяющие организовать общий для синхронной группы стек в глобальной памяти и передавать адреса на данные в таких стеках между нитями. Описывается схема организации выполнения одной OpenMP-нити в 32 синхронных потоках выполнения в PTX вне OpenMP SIMD-регионов за счет легковесной инструментации некоторых инструкций. Представлены результаты тестирования на микротестах и сравнение с реализацией стандарта OpenACC.

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

Одним из наиболее популярных и актуальных подвидов нереляционных баз данных являются графовые базы данных. В данной работе рассмотрены задачи на таких базах данных, которые наиболее часто встречаются в современной литературе. Изучены задачи максимизации влияния, motif mining (MM), задача оценки схожести узлов графа, сопоставление образца в графе. Рассмотрены первичные алгоритмы каждого направления и некоторые промежуточные работы. Проанализированы алгоритмы, соответствующие текущему положению дел.

В последние годы по мере увеличения производительности и роста объема оперативной и внешней памяти производительность СУБД для некоторых классов запросов определяется непосредственно скоростью обработки запросов процессором. В СУБД PostgreSQL для исполнения SQL-запросов традиционно используется механизм интерпретации, который приводит к накладным расходам, например, связанным с множественным ветвлением, неявными вызовами функций-обработчиков и выполнением лишних проверок, которых можно избежать, используя информацию, доступную только во время выполнения запроса. В данной работе рассматривается метод динамической компиляции запросов, в частности, компиляция выражений оператора WHERE и метода последовательного сканирования таблиц SeqScan для СУБД PostgreSQL с помощью компиляторной инфраструктуры LLVM. Рассматривается оптимизация доступа к атрибутам, заключающаяся в вычислении смещений атрибутов кортежа во время компиляции запроса, а также метод автоматической трансляции встроенных функций PostgreSQL во внутреннее представление LLVM IR, что позволяет использовать один и тот же исходный код как для JIT-компилятора, так и для имеющегося интерпретатора. Генерация машинного кода во время выполнения запроса дает возможность избежать накладных расходов традиционной системы интерпретации. Метод реализован в виде расширения к СУБД PostgreSQL и не требует изменения исходного кода СУБД. Результаты проведенного тестирования показывают, что динамическая компиляция запросов с помощью JIT-компилятора LLVM позволяет получить ускорение в несколько раз на синтетических тестах.

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