Preview

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

Расширенный поиск
Том 23 (2012)
Скачать выпуск PDF
Аннотация
В работе описывается расширение модели параллельной SPMD программы возможностью использования потоков Java. Использование потоков в программе позволяет лучше утилизировать ресурсы многоядерного процессора. Разработанная модель позволяет оценивать время выполнения параллельной программы с явными обращениями к библиотеке MPI, где в каждом процессе можно использовать параллельные потоки Java. Однако следует учесть трудности, возникающие при использовании потоков в среде Java. В работе приводятся рекомендации призванные улучшить производительность многопроцессно-многопоточной программы связанные с управлением памяти JVM, настройкой сборщика мусора, управлением локальных буферов и.т.д.
Аннотация
Реализация алгоритмов на программируемых логических интегральных схемах с помощью языков описания аппаратуры является сложной задачей. Поэтому, инструмент, позволяющий эффективно транслировать алгоритм с языка высокого уровня в язык описания аппаратуры, был бы очень полезен. В данной статье рассматривается инструмент для трансляции функций языка Си в модули на языке Verilog, процесс трансляции и две реализованных на уровне описания аппаратуры оптимизации: встраивание присваиваний и конвейеризация циклов. Результаты тестирования показывают, что эти оптимизации существенно увеличивают производительность генерируемого кода.
Аннотация
В данной статье приводятся результаты экспериментального исследования по восстановлению графа потока управления, запутанного специализированным компилятором на основе LLVM. Средства запутывания и распутывания бинарного кода независимо разрабатывались двумя коллективами ИСП РАН. Помимо того, для количественной оценки стойкости запутывания были получены метрики сложности кода модельных примеров.
Аннотация
В данной статье приводится обзор запутывающих преобразований программ, сформулированы критерии эффективности методов обфускации. Также предлагается подход к реализации обфусцирующего компилятора на основе инфраструктуры LLVM. Особенность подхода заключается в одновременном применении преобразований, маскирующих различные аспекты работы запутываемого приложения, что обеспечивает стойкую защиту от статического анализа.
Аннотация
В статье описываются маскирующие преобразования, реализованные в ходе разработки обфусцирующего компилятора в ИСП РАН, приводится оценка понижения быстродействия и увеличения объема потребляемой приложением памяти, а также оценка возможности восстановления информации об исходном коде. Реализованные маскирующие преобразования могут быть одновременно применены к запутываемому приложению, что увеличивает степень защиты приложения и обеспечивают стойкую защиту от статического анализа.
Аннотация
Использование динамического анализа для понимания поведения программы является распространенной практикой в наши дни. Одним из видов динамического анализа является анализ трасс выполнения программ. В то же время, трассы выполнения программ, состоящие из последовательности выполненных процессором инструкций, слишком велики для непосредственного восприятия человеком. Поэтому актуальной является задача повышения уровня представления таких трасс. В данной статье предлагается метод повышения уровня представления, предназначенный для построения модели алгоритма по трассе выполнения программы.
Аннотация
В статье рассматривается подход для проведения рефакторинга исходного кода на языках Си/Си++, реализованный в инструменте Klocwork Insight. Приводится подробное описание подхода на примере рефакторинга «Выделение функции». Разбираются способы обработки различных языковых конструкций при проведении рефакторинга, показывается, как структурные изменения в синтаксическом дереве отображаются в изменения исходного кода программы. На основе описанного подхода для проведения рефакторинга предлагается выделить методы для реализации произвольных изменений в программе, выходящих за рамки широко используемых рефакторингов. В конце статьи проводится сравнение с существующими инструментами для проведения рефакторинга.
Аннотация
В статье описывается метод построения синтаксического анализатора, позволяющий существенно сократить требуемые для анализа ресурсы. Метод основан на том факте, что каждый исходный файл подключает множество заголовков, из которых используется лишь небольшое количество определений. Разбор определений из заголовков можно пропускать до момента непосредственного обращения к ним, таким образом, неиспользуемые определения анализироваться не будут. Отличительной особенностью метода является необходимость внесения лишь небольшого количества изменений в существующий парсер. Метод реализован в статическом анализаторе Klocwork Insight.
Аннотация
Большие данные поставили перед традиционными системами хранения и обработки новые сложные задачи. В данной статье анализируются возможные способы их решения, ограничения, которые не позволяют сделать это эффективно, а также приводится обзор трех современных подходов к работе с большими данными: NoSQL, MapReduce и обработка потоков событий в реальном времени.
Аннотация
Сегодня всё чаще звучит утверждение, что универсальных хранилищ данных не существует. Несмотря на то, что SQL-ориентированные системы управления базами данных (СУБД) широко применялись и применяются сегодня, масштабирование приложений при использовании этих систем сильно затруднено. В связи с этим появилось много различных хранилищ данных, стремящихся соответствовать требованиям современных высоконагруженных Web-приложений. В настоящее время наблюдается тенденция к использованию нескольких технологий и систем в рамках одного приложения для решения различных задач. В данной статье рассматриваются основные подходы к реализации доступа к данным и проблемы абстракции от используемых хранилищ, а также предлагаются некоторые принципы организации слоя работы с данными при использовании нескольких хранилищ данных разного типа.
Аннотация
Одним из важнейших механизмов повышения скорости работы современных СУБД является кэширование часто читаемых или записываемых данных в оперативной памяти. Классические алгоритмы замещения страниц БД в кэше стремятся минимизировать промахи буферного пула СУБД. Данный метод оптимизации негласно опирается на тот факт, что скорость записи и чтения данных одинакова. Постепенное совершенствование и удешевление технологии производства флэш-памяти привели к созданию твердотельных накопителей данных(SSD), которые в настоящее время все чаще используются как в персональных компьютерах, так и в системах хранения данных. Флэш-накопители имеют серьезные преимущества по сравнению с традиционными жесткими дисками, главные из которых - более высокая скорость чтения и записи, а также значительно меньшее время доступа к данным. Однако, самые распространенные виды флэш-памяти читают данные с большей скоростью, чем записывают. Из-за данной особенности использование классических алгоритмов замещения страниц при кэшировании дисковых данных неэффективно. В данной статье производится обзор современных алгоритмов управления буферным пулом СУБД, которые предназначены для работы с накопителями на флэш-памяти.
Аннотация
Статья посвящена лексической оптимизации запросов и описывает работы, опубликованные в течение последних четырех десятилетий. Особое внимание уделяется таким подходам к оптимизации как модификация, украшение и сокращение запросов. Обсуждаются алгоритмы оптимизации для реляционных и нереляционных СУБД.
Аннотация
Тематическое моделирование - способ построения модели коллекции текстовых документов, которая определяет, к каким темам относится каждый из документов. Переход из пространства терминов в пространство найденных тематик помогает разрешать синонимию и полисемию терминов, а также эффективнее решать такие задачи, как тематический поиск, классификация, суммаризация и аннотация коллекций документов и новостных потоков. Наибольшее применение в современных приложениях находят подходы, основанные на Байесовских сетях - ориентированных графических вероятностных моделях, позволяющих учитывать авторство документов, связи между словами, темами, документами и авторами, а также другие типы сущностей и метаданных. В статье приведён сравнительный обзор различных моделей, описаны способы оценивания их параметров и качества результатов, а также приведены примеры открытых программных реализаций.
Аннотация
На основе технологической платформы UniHUB (<http://www.unihub.ru>), разработанной в Институте системного программирования РАН, в составе Дата-центра РАН создана веб-лаборатория, нацеленная на интеграцию данных дистанционного зондирования в интересах наук о Земле. . Информационная система ориентирована на научное и образовательное сообщество и предназначена для совместной научной работы ее участников в едином рабочем пространстве, обеспечивая поиск источников пространственных данных, формирование хранилищ данных, доступ к данным, в том числе к ресурсам внешних открытых веб-сервисов, к приложениям и обучающим материалам. Облачная распределенная информационная среда UniHUB использована для решения географических задач, включая обработку космических изображений и цифровых моделей рельефа с использованием методов и технологий пространственного анализа и геомоделирования средствами ГИС с открытым исходным кодом Quantum GIS.
Аннотация
В данной работе предлагается метод для извлечения цепочек семантически близких слов и выражений, описывающих различных участников сюжета – тематических узлов. Предполагается, что выделение основных участников позволит улучшить качество обработки новостного кластера. Метод основан на структурной организации новостных кластеров и анализе контекстов вхождения языковых выражений. Контексты слов используются в качестве базиса для извлечения многословных выражений и построения тематических узлов. Оценка предложенного алгоритма производится в задаче построения обзорных рефератов новостных кластеров.
Аннотация
Статья посвящена разработке системы интеграции данных в пространстве Linked Open Data. Предложено архитектурное решение, осуществляющее весь комплекс задач по публикации данных из множества локальных гетерогенных источников в пространстве Linked Open Data. В системе предлагается применять новый подход исполнения федеративных SPARQL запросов с использованием наборов RDF связей
Аннотация
Для анализа больших объемов данных используются такие методы как параллельные СУБД, парадигма MapReduce, колоночное хранение и различные комбинации этих подходов. В данной работе будут рассмотрены алгоритмы соединения в среде MapReduce. К сожалению, алгоритмы соединения не поддерживаются напрямую в MapReduce . Цель данной работы заключается в том, чтобы обобщить и сравнить существующие алгоритмы соединения по равенству с некоторыми методами оптимизации.
Аннотация
Повторяемость во временных данных это важное свойство, которое может быть использовано во многих приложениях. Такая регулярность исследуется в области интеллектуального анализа периодических шаблонов. В данной работе мы поднимаем проблему обнаружения периодических наборов и предлагаем способ для ее решения. Существующие алгоритмы обнаружения периодических событий и новый подход подробно рассматриваются в статье. Сравнительный анализ алгоритмов и их производительность демонстрируются через серию экспериментов.
Аннотация
Статья посвящена проблеме зависимости между ошибками, определяемыми спецификацией, и связанной с ней проблеме оптимизации тестов. Между ошибками имеется зависимость, если существует такое строгое подмножество ошибок, что любая неконформная реализация (то есть реализация, в которой есть какая-нибудь ошибка) содержит ошибку из этого подмножества. Соответственно, достаточно, чтобы тесты обнаруживали ошибки только из этого подмножества. Предлагается формальная модель тестового взаимодействия самого общего вида и конформность типа редукции, для которых зависимость между ошибками практически отсутствует. Показывается, что многие известные конформности в различных семантиках взаимодействия являются частными случаями этой общей модели. В этой общей модели зависимость между ошибками может возникать, когда в качестве класса тестируемых реализаций выбирается то или иное строгое подмножество класса всех реализаций. Частные семантики взаимодействия и/или различные гипотезы о реализации (в частности, гипотезы о безопасности) как раз и предполагают, что тестируемая реализация не любая, а относится к некоторому подклассу (безопасных) реализаций.
Аннотация
В статье представлен метод генерации тестов для конфигурационного тестирования на основе покрывающих наборов, т.е., обеспечивающая покрытие всех возможных комбинаций пар, троек и т.д., значений параметров конфигурации. Новым элементом в предлагаемом методе является учет условий использования отдельных параметров, который вносит коррективы как в учет покрываемых комбинаций, так и в построение отдельных тестов. Данный метод использован на практике для генерации тестовых программных конфигураций операционной системы реального времени, приведены результаты этого применения.
Аннотация
Запросы по исходному коду программ помогают разработчикам обнаруживать искомые фрагменты кода и определять их взаимоотношения друг с другом. Для выполнения запросов по исходному коду автоматизированным образом существуют различные подходы от достаточно простых, основывающихся на текстовом поиске по шаблонам, до более интеллектуальных, осуществляющих поиск на основе формального представления программ и позволяющих использовать для запросов естественные языки. В статье предлагается подход к выполнению запросов по исходному коду программ на основе аспектно-ориентированного программирования, рассматриваются достоинства и недостатки такого подхода.
Аннотация
Статья посвящена разработке тестового набора для проверки соответствий реализаций узлов Интернет спецификациям протокола безопасности TLS. Для построения тестового набора использовалась технология автоматического тестирования UniTESK и программный пакет JavaTESK, реализующий эту технологию. Работа выполнялась в Институте системного программирования РАН в рамках проекта «Верификация реализаций расширяемых протоколов Интернета» при поддержке гранта РФФИ № 10-07-00145. В ходе ее выполнения были выделены требования к реализациям TLS, разработаны формальные спецификации и прототип тестового набора для верификации реализаций TLS. В статье кратко описаны метод формализации требований TLS, тестовый набор, а также результаты тестирования существующих реализаций сервера TLS. Эти результаты показывают, что предложенный в данной работе метод верификации позволяет эффективно автоматизировать тестирование таких сложных протоколов, как протоколы безопасности.
Аннотация
Верификация драйверов ОС Linux - это широкая область для применения различных методов верификации, в частности, методов проверки свойств безопасности и надежности программ, а также функциональной верификации. Драйверы Linux - это индустриальное программное обеспечение, на стабильность которого полагаются ИТ-инфраструктуры. В силу этого к надежности и корректности их работы предъявляют жесткие требования, в свою очередь, это означает, что если инженер-верификатор обнаружил ошибку в драйвере, он может рассчитывать на быструю реакцию сообщества разработчиков в плане подтверждения и исправления этой ошибки. Драйверы Linux - сложное низкоуровневое системное программное обеспечение, и его характеристики требуют применения различных техник анализа программ: использования SMT-решателей, методов верификации моделей (model checking) и других методов верификации. Точность и эффективность этих методов за последнее время значительно повысилась, и поэтому сложная задача верификации драйверов ОС Linux становится реальной по мере использования этих достижений в инструментах верификации.
Аннотация
В статье исследуется проблема тестирования драйверов файловых систем ОС Linux. По результатам рассмотрения существующих систем тестирования, применимых к драйверам файловых систем, формулируются требования к системе тестирования, способной вывести решение этой задачи на качественно новый уровень. В первую очередь, для этого необходимо помимо проверки стандартной функциональности файловых систем, обеспечить тестирование поведения драйверов в редко встречающихся ситуациях, таких как сбои в нижележащем устройстве хранения, условия нехватки памяти, а также выявлять ошибки, связанные с утечкой ресурсов.
Аннотация
Предложен вариант метода Джентри для построения полного гомоморфного шифрования.
Аннотация
Рассмотрена проблема балансировки нагрузки для множества параллельных задач на группе географически распределенных кластеров уменьшающая количество энергии при вычислениях. Предложены несколько алгоритмов распределения задач и проведена экспериментальная проверка их эффективности.
Аннотация
Предложен онлайновый алгоритм распределения параллельных задач на группе кластеров с различными производительностями процессоров и показано, что он гарантирует для любого потока задач построение расписания, отличающегося от оптимального не более чем в 2e раз.
Аннотация
В данной работе в качестве эквивалентности программ рассматривается отношение логико-термальная эквивалентности, одно из наиболее слабых разрешимых отношений эквивалентности программ, аппроксимирующих отношение функциональной эквивалентности.


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


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