Сборники трудов ИСП РАН


Предисловие.

В.П. Иванников.

Аннотация

25 января 2009 г. Институту системного программирования РАН исполняется 15 лет. Все эти годы основными задачами Института являлись фундаментальные исследования в области системного программирования, прикладные исследования и разработки в интересах различных областей индустрии и образование. Во всех этих областях удалось добиться значительных успехов.

Результаты исследований и разработок освещаются на страницах web-сайта Института, публикуются в регулярных и тематических выпусках Трудов Института системного программирования РАН, ведущем российском журнале «Программирование», авторитетных зарубежных изданиях, докладываются на авторитетных российских и международных конференциях. Проекты, выполняемые специалистами Института, поддерживаются грантами РФФИ, Министерства образования и науки, Президиума РАН и Отделения математики. Прикладные исследования и разработки выполняются на основе контрактов с российскими и зарубежными компаниями.

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

Настоящий юбилейный сборник Трудов института системного программирования РАН полностью состоит из статей, написанных молодыми сотрудниками ИСП РАН и посвященных результатам выполняемых ими исследовательских проектов.

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

Статья А. Белеванцева, Д. Журихина и Д. Мельника «Компиляция программ для современных архитектур» содержит обзор работ по оптимизации программ для современных вычислительных архитектур, проводимых в отделе компиляторных технологий ИСП РАН. Работы включают в себя выявление параллелизма на уровне команд для архитектуры Intel Itanium, исследование и разработку энергосберегающих оптимизаций для архитектуры ARM, а также исследования по динамическим оптимизациям для языков общего назначения, выполняемым на машине пользователя. Большая часть этих работ выполнялось на основе компилятора GCC с открытыми исходными кодами, являющегося стандартным компилятором для Unix-подобных систем.

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

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

В статье В. Мутилина «Метод проверки линеаризуемости многопоточных Java программ» описывается новый метод Sapsan, предназначаемый для функционального тестирования Java-программ с программным интерфейсом (API), процедуры (операции) которого можно вызывать из нескольких потоков одновременно. Метод Sapsan позволяет проверять одно из распространенных требований к таким программам – требование линеаризуемости, заключающееся в том, что параллельное выполнение операций эквивалентно некоторому последовательному выполнению этих же операций, удовлетворяющему спецификации.

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

В статье В. Рубанова «Современная инфраструктура для обеспечения совместимости Linux-платформ и приложений» описывается подход к построению инфраструктуры для эффективной разработки и использования спецификаций Linux-платформ. Подобные спецификации описывают программные интерфейсы (API) для обеспечения совместимости между различными реализациями таких платформ и различными приложениями для них. Задача рассматривается в условиях эволюционирующих версий спецификации платформы и наличия множественных платформенных реализаций и приложений, удовлетворяющих той или иной версии спецификации. Предлагаемый подход основан на использовании централизованной базы данных, содержащей структурированную информацию о различных версиях спецификации и различных реализациях платформ и приложений, а также средств автоматической верификации фактического соответствия реализаций платформ и приложений той или иной версии спецификации. Подход иллюстрируется на примере инфраструктуры для поддержки стандарта Linux Standard Base (LSB), основного промышленного стандарта на интерфейсы базовых библиотек операционной системы Linux.

В статье М. Гринева и И. Щеклеина «Ориентированные на приложения методы хранения XML-данных» утверждается, что единственно возможным подходом, способным обеспечить высокую эффективность управления XML-данными на основе универсальной модели данных XQury, является выбор способов внутреннего представления и методов обработки данных под потребности конкретного приложения. Достаточной информацией для описания потребностей является схема XML-данных и рабочая нагрузка в виде возможных запросов и операций модификации данных. Предлагается выбирать структуры хранения данных, необходимые для эффективного выполнения запросов и модификаций для данного приложения. Такой подход позволит поддерживать модель данных XQuery на логическом уровне, но избежать излишних накладных расходов на физическом уровне хранения данных. Описываются первые результаты по разработке таких методов хранения и обработки XML-данных.

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

Издание

Труды Института системного программирования РАН, том 16, 2009, стр. 5-8.

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

Полный текст статьи в формате pdf Вернуться к содержанию тома