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

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

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

В настоящее время SDN-технология активно используется в виртуальных сетях для реализации различных служебных сервисных функций. В основе сети лежит связный неориентированных граф физических связей (англ. Resource Network Connectivity Topology, RNCT), вершинами которого являются сетевые коммутаторы (switches) и хосты (hosts). В настоящей работе рассматривается топология, когда каждый хост соединен ровно с одним коммутатором. Коммутаторы работают по таблицам правил, которые настраиваются централизованно с помощью контроллера, работающего независимо от сетевого оборудования. Настройка коммутаторов сети предназначена для обеспечения передачи пакетов из начальных хостов в конечные хосты в зависимости от значений параметров пакетов. В статье обсуждается связь настроек коммутаторов и множества реализуемых ими путей передачи пакетов в зависимости от свойств графа физических связей. Исследуется задача тестирования настройки коммутаторов. Под целью тестирования понимается подача пакетов, позволяющих «пройти» по каждому правилу каждого коммутатора хотя бы один раз, подав пакет с необходимыми параметрами. Показывается, что в общем случае не любая настройка любого коммутатора проверяема. Возможности тестирования зависят от принимаемых гипотез о работе коммутатора. В статье рассматриваются две гипотезы: гипотеза о коммутаторе предполагает, что работа коммутатора не зависит от настроек других коммутаторов; более сильная гипотеза о правиле, кроме этого, предполагает, что работы коммутатора по данному правилу не зависит от других правил в настройке этого коммутатора. После введения, в разд. 2 вводятся необходимые определения и обозначения. Раздел 3 посвящен взаимосвязи путей в сети и правил в коммутаторах. В разд. 4 рассматривается тестирование на основе гипотезы о правиле, доказываются необходимые и достаточные условия возможности проверки заданного правила заданного коммутатора. В разд. 5 рассматривается тестирование на основе гипотезы о коммутаторе и доказывается необходимое (но не достаточное) условие и достаточное (но не необходимое) условие проверяемости любой настройки коммутатора. В заключении обсуждаются проблемы, возникающие при установлении необходимого и достаточного условия проверяемости любой настройки коммутатора, а также ставится задача определения таких условий для заданной настройки коммутатора.

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

В работе рассмотрена задача построения расписаний выполнения параллельных вычислительных задач на группах кластеров с одинаковым числом w одинаковых процессоров, производительность которых для разных кластеров различная. Проведён вероятностный анализ задачи. Получены нижние оценки. Показано, что если число процессоров, необходимых для решения любой задачи имеет равномерное распределение на отрезке [o,w] для любого алгоритма составления расписаний величина математического ожидания свободного объёма вычислений равна Ω(w√N). Получены верхние оценки. Был предложен онлайновый алгоритм построения расписаний с распределением задач в ограниченные области Limited Hash Scheduling для задачи построения расписаний, работающий в режиме closed-end, с математическим ожиданием свободного объёма вычислений, равным O(w√(N ln N)).

В настоящее время такие компании как Amazon, Google, Facebook, Microsoft, Yahoo! и другие управляют огромными дата-центрами из десятков тысяч узлов. Эти кластеры используются одновременно многими организациями и пользователями (облачная модель вычислений). Пользователи запускают задания, каждое из которых может состоять из одной или нескольких параллельных задач. Поток задач обычно представляет собой смесь: коротких, долгих, интерактивных, пакетных, и задач с различным приоритетом. Планировщик кластера решает, как разместить эти задачи на узлах, где они запускаются в виде процессов, контейнеров или виртуальных машин. Оптимизация размещения задач планировщиком позволяет улучшить степень использования узлов (machine utilization), сократить время отклика, сбалансировать нагрузку на части кластера, получить предсказуемую производительность приложений, повысить отказоустойчивость. Получить оптимальное размещение сложно. Для этого требуется решить задачу многокритериальной оптимизации, что требует времени. Это приводит к задержке при размещении очередной задачи, негативно сказывается на времени отклика и пропускной способности. С ростом размеров кластера и потока задач удовлетворить оба данных критерия становится сложным, и необходимо отдавать приоритет только одному. В данной статье мы рассмотрим архитектуру современных планировщиков и математические постановки задачи оптимизации.

Ошибки использования памяти в модулях ядра операционной системы Linux сложно обнаружить, но они могут привести к серьезным последствиям. В данной статье мы описываем метод статической верификации, позволяющий обнаруживать все ошибки в рамках предположений метода. Статическая верификация крупных пректов таких, как ядро ОС Linux, требуют дополнительных усилий. Современные инструменты статической верификации не позволяют анализировать ядро как единое целое, поэтому мы используем упрощенную автоматически генерируемую модель окружения. Эта модель вносит некоторую неточность, но позволяет проводить статическую верификацию. Также мы допускаем отсутствие тела некоторых функций, что приводит к неполным программам, написанных на языке ANSI C. В данной работе предлагается подход к обнаружению ошибок использования памяти в таких неполных программах. Наша техника статической верификации основана на теории символических графов памяти и ее расширении для снижения количества ложных срабатываний. Мы ввели концепцию памяти по требованию для упрощения моделей интерфейсов ядра ОС и реализовали ее в фреймворке статической верификации CPAchecker. Также мы изменили точность модели памяти CPAchecker с байтов на поддержку отдельных битов и добавили поддержку выравнивания структур, аналогичное использованому в компиляторе. Для повышения точности анализа мы реализовали предикатное расширение состояния символического графа памяти. Мы провели проверку модулей ядра ОС Linux для версий 4.11.6 и 4.16.10 с помощью фреймворка статической верификации Klever с инструментом верификации CPAchecker, что позволило проанализировать 6224 и 5215 модулей соответствующих версий. Ручной анализ предупреждений от фреймворка Klever выявил 78 реальных ошибок в модулях ядра. Мы сделали патчи для исправления 33 из них.

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

В этой статье мы анализируем современные работы, посвященные поисковому поведению ученых, и работы, посвященные методам исследовательского поиска. Мы показываем, что четыре вида поиска из шести, характерных для ученых (в том числе самый субъективно сложный - исследование новых направлений и самый часто возникающий - поиск для поддержания осведомленности), можно с достаточной степенью уверенности считать исследовательским поиском. Таким образом, поисковые системы, предназначенные для поиска научных данных, должны реализовывать специфичные для исследовательского поиска инструменты. Чтобы проверить это, мы анализируем семнадцать специализированных поисковых систем: от встроенных в электронные библиотеки Scopus и WoS до Google Scholar и социальных сетей для ученых, таких как ResearchGate и Academia.edu. Мы приходим к выводу, что степень их адаптации к специфике исследовательского поиска оставляет простор для улучшений и обсуждаем возможные направления их развития.

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

Поиск и классификация текстовых документов применяются во многих практических приложениях и являются одними из ключевых задач информационного поиска. Методы поиска и классификации текстов находят применение в поисковых системах, электронных библиотеках и каталогах, системах сбора и обработки информации, платформах для онлайн-обучения и многих других. Существует большое количество частных применений указанных методов, однако каждая подобная практическая задача отличается, как правило, слабой формализуемостью, узкой предметностью и, следовательно, требует индивидуального изучения и собственного подхода к решению. В данной работе рассматривается задача автоматического поиска и типизации текстовых фрагментов, содержащих биографическую информацию. Ключевой проблемой при решении указанной задачи является проведение мультиклассовой классификации текстовых фрагментов в зависимости от наличия и типа содержащейся в них биографической информации. Проведя обзор научной литературы по рассматриваемому вопросу, авторы сделали вывод о перспективности и широте применения нейросетевых методов для решения подобных задач. Исходя из данного вывода, в работе проведено сравнение различных архитектур нейросетевых моделей, а также основных способов представления текстов (Bag-of-Words, Bag-of-Ngrams, TF-IDF, Word2Vec) на предварительно собранном и размеченном корпусе биографических текстов. В статье описываются этапы подготовки обучающего множества текстовых фрагментов для обучения моделей, способы представления текстов и методы классификации, выбранные для решения задачи. Также приводятся результаты мультиклассовой классификации текстовых фрагментов и показаны примеры автоматического поиска фрагментов, содержащих биографическую информацию, в текстах, не участвовавших в процессе обучения моделей.

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

В статье рассматриваются возможности открытой библиотеки SOWFA. Проблемно-ориентированная библиотека, работающая в составе открытого пакета OpenFOAM v.2.4.0, предназначена для решения задач ветроэнергетики. В связи со строительством новых ветропарков на территории РФ (Ульяновская область, республика Адыгея) вопросы проектирования, моделирования работы ветропарков и ветроустановок являются актуальными в настоящее время. В статье приводится описание структуры библиотеки SOWFA и некоторых ее классов. Изучение динамики самоорганизованных турбулентных вихревых структур и оценка их размеров важны с точки зрения максимизации вырабатываемой мощности ветроэлектрическими установками (ВЭУ), для анализа оптимального расположения ВЭУ в ветропарке. При этом необходимо детально изучать процесс эжекции воздуха, процесс смещения двух сред, в котором одна среда, находясь под давлением, оказывает воздействие на другую и увлекает ее в требуемом направлении, в районе ветропарке. Явление эжекции играет положительную роль и позволяет восстановить дефицит скорости в следе за ВЭУ, следовательно повлиять на вырабатываемую мощность ветропарка. Явление эжекции можно изучать с помощью движения твердых частиц. В статье описывается пример добавления нового класса KinematicCloud в решатель ABLSolver, который описывает кинематическое облако частиц и пример решения прикладной задачи ветроэнергетики для модельного ветропарка. Расчетная область для модельного ветропарка имела форму параллелепипеда с заданными размерами. Неструктурированная сетка содержала 6 миллионов ячеек. Для определения начального распределения параметров использовалось приближение нейтрального атмосферного пограничного слоя, рассчитанное с применением Precursor метода, реализованного в решателе ABLSolver. Математическое моделирование параметров течения в ветропарке было проведено с использованием решателя pisoFoamTurbine и метода Actuator Line Model. В ходе расчета для случая модельного ветропарка с 12 ветроустановки были получены поля осредненных и пульсационных величин для скорости, для давления, подсеточная вязкость, тензор напряжени, завихренность. В статье выполнено сравнение значения безразмерной горизонтальной скорости в двух различных сечениях со значениями, полученными в эксперименте. Вычисления проведены с использованием ресурсов вычислительного кластера web-лаборатории UniCFD ИСП РАН.

В работе приводится описание многомасштабного подхода для моделирования процессов течений двухфазных сред в сложных технических системах. В основе многомасштабного подхода лежит как разделение расчетной области на подобласти с собственной системой уравнений, так и расщепление исходной системы уравнений на несколько подсистем для каждого из рассматриваемого масштабов. В качестве примера возможного применения многомасштабной модели рассматривается задача определения акустического шума в дальнем поле при старте ракеты-носителя с учетом подачи воды в газовые струи двигательной установки. Другими областями применения многомасштабной модели можно указать задачи нефтегазовой отрасли: глушение газодобывающих скважин, расположенных на большой глубине, глушение нефтяных скважин с высоким газовым фактором на месторождениях. Предлагаемая многомасштабная математическая модель включает в себя 5 подмоделей: 1) подмодель газодинамики высокоскоростных многокомпонентных течений смеси газов; 2) подмодель гидродинамики течения двухфазной смеси в гомогенном приближении с учетом сжимаемости газовой фазы и обмена массой между фазами; 3) подмодель переноса межфазной границы; 4) подмодель переноса облака капель и его взаимодействия с газожидкостной средой; 5) подмодель оценки шума в дальнем поле на основе акустической аналогии Ффоукс Вильямса-Хоукинга. Предложенная в рамках многомасштабного подхода модель может быть расширена для включения дополнительных моделей - таких, например, как Эйлерова-Лагранжева модель атомизации струй на основе уравнения эволюции плотности межфазной поверхности. Реализация подмоделей может быть выполнена на основе пакетов с открытым исходным кодом: OpenFOAM, Nektar++, ITHACA-FV. Подмодели акустики и гибридный алгоритм решения уравнений сжимаемой гомогенной двухфазной среды реализованы в виде модулей libAcoustics и hybridCentralSolvers на базе открытого пакета OpenFOAM. Использование платформы OpenFOAM в качестве базы для реализации программы позволяет получить архитектуру со взаимозаменяемыми элементами. Исходный код разрабатываемой модели свободно доступен через проект GitHub https://github.com/unicfdlab.

Системы полиномиальных уравнений - один из наиболее универсальных математических объектов. Почти все задачи криптографического анализа можно свести к поиску решений систем полиномиальных уравнений. Соответствующее направление исследований принято называть алгебраическим криптоанализом. С точки зрения вычислительной сложности, системы полиномиальных уравнений охватывают весь диапазон возможных вариантов, от алгоритмической неразрешимости диофантовых уравнений до хорошо известных эффективных методов решения линейных систем. Метод Бухбергера приводит систему алгебраических уравнений к системе специального вида, определяемой базисом Гребнера исходной системы уравнений, позволяющему использовать исключение зависимых переменных. Фундаментом определения базиса Гребнера является допустимое упорядочение на множестве термов. Множество допустимых упорядочений на множестве термов бесконечно и даже континуально. Наиболее трудоемким этапом при нахождении базиса Гребнера с помощью алгоритма Бухбергера является доказательство приводимости к нулю всех S-многочленов. Известно, что достаточно провести такую проверку только для любого подмножества таких многочленов, представляющих систему образующих K[X]-модуля S-многочленов. Возникает естественная задача нахождения такой минимальной системы образующих. Существование такой системы образующих следует из теоремы Накаямы. Предложен алгоритм построения такого базиса для любого упорядочения.

Рассматривается задача использования процессоров с архитектурой ARMv8 для ускорения работы алгоритмов мультимедиа и цифровой обработки при решении задач восстановления сигналов в процессе фильтрации. В качестве примера рассмотрена реализация алгоритма работы цифрового КИХ-фильтра с линейной фазо-частотной характеристикой. Предложены формулы расчета фильтра. Алгоритм оптимизирован с использованием векторных SIMD-инструкций архитектуры ARMv8. Представлена реализация алгоритма обработки сигнала на языке Cи на чипе BCM2837 с процессором ARM Cortex-A53. Решение обеспечило эффективное восстановление частот, искаженных при передаче сигналов в звуковом диапазоне, и доказывает эффективность использования мобильных многоядерных процессоров ARMv8 для параллельной обработки данных в процессе решения сложных вычислительных задач. Результаты эксперимента показывают, что использование процессоров с архитектурой ARMv8 при решении задач фильтрации сигналов позволяет существенно ускорить работу мультимедиа и алгоритмов обработки сигналов, таких как видеокодер/декодер, 2D/3D графика, игры, обработка звука и речи, обработка изображений, телефония и звук

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

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

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

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