Единое окно доступа к образовательным ресурсам

Десятая конференция разработчиков свободных программ: Тезисы докладов

Голосов: 0

В книге собраны тезисы докладов, одобренных Программным комитетом десятой конференции разработчиков свободных программ, которая прошла в городе Калуге 20-22 сентября 2013 года.

Приведенный ниже текст получен путем автоматического извлечения из оригинального PDF-документа и предназначен для предварительного просмотра.
Изображения (картинки, формулы, графики) отсутствуют.
    Утреннее заседание (10.00–13.20)                                          31


device evolution goes quickly and mostly unpredictable this fact plays
significant role.
    There are three valuable components in Luwrain design: Linux kernel,
system services and user environment based on Java as it was mentioned
above. All necessary interaction with system services is performed through
D-Bus activity. Luwrain intents to use udisks for removable media
management, Network Manager for network interfaces operations and so
on. Generally we would like to respect as many relevant freedesktop.org
recommendations as it is possible making Luwrain compatible with usual
Gnu/Linux desktop.
    User interface approach is the most important part of the project.
It is inspired by emacspeak package widely known in community of
blind users of GNU/Linux. Its main advantage is a very high speed of
work usually unapproachable with GUI-based systems in conjunction
with screen reading software. We would like to save all positive parts
of emacspeak experience eliminating its disadvantages. In Luwrain user
interacts with several areas placed on a screen as tiles. Each of them always
has rectangular form and filled with text written using monospaced font.
Font size, font color and background color are defined globally and can
be easily changed to be suitable for needs of a particular user. All areas
are associated with launched applications and not all of them should be
visible on the screen. User has convenient methods for quick applications
and areas switching and that makes Luwrain different than emacspeak
which has no applications at all. In addition Luwrain offers special type of
areas called popup areas and designed for dialogs with a user. Their main
difference is that they can be opened as single method call which does not
return until popup area is closed. A couple of popup areas have system-
wide meaning: main menu and command line prompt. The idea to offer
easily accessible command line evidently was adopted from emacspeak
but there it has slightly different behaviour. It provides the access only
to commands with execution not related to a particular area. Commands
invocation can be done in any time and yields the same result without
dependence what applications are currently opened.
    The standard set of applications includes file manager, mail and
news reading applications, documents reading, text editor, address book,
calendar and so on. Each of this tasks usually implies only creation of
proper interface in terms of Luwrain as real back-ends for them mostly
are available as various libraries for Java. This fact played nearly crucial
role at language choosing decision.


32                                                            21 сентября


   But there are some exceptions from the strategy described above. Web
browser cannot be implemented as text-based application so it should be
available as a separate applications executed outside of Java environment.
There are two possible alternatives for that:
   • Implement AT-SPI-based light screen reader and let users launch
      Firefox as it has proper AT-SPI support.
    • Include Chromium with ChromeVox add-on.
    The former choice is more difficult since creation of libatspi client
requires significant efforts but actually is more preferable because it
allows collecting web-page contents in Java environment for copy-paste
operations. In addition available libatspi client also gives a way for
launching of some closed applications like Skype.
    Luwrain installation program is based on the installation program
previously developed as a part of ALT Linux Homeros project. It uses
livecd-cloning technique and can be done by blind user without any
additional sighted help.

Захаров Илья
Москва, Институт системного программирования РАН
Проект: Linux Driver Verification project
http://linuxtesting.ru/project/ldv, http:
//www.google-melange.com/gsoc/project/google/gsoc2013/glaurung/5001

 Генерация модели окружения для группы модулей
        ядра для статической верификации

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


Утреннее заседание (10.00–13.20)                                      33


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


Система статической верификации драйверов LDV
   Одним из направлений поиска ошибок в драйверах ядра Linux
является применение инструментов статической верификации исход-
ного кода. Инструменты, использующие в своей работе этот подход,
позволяют проверять заданные правила корректности без выполне-
ния программы. Анализ учитывает все возможные пути исполнения
программы и не нуждается в специальном тестовом окружении.
   Система верификации драйверов ядра Linux LDV [5] нацелена
на проверку правил корректности использования интерфейсов яд-
ра Linux драйверами при помощи инструментов статической вери-
фикации верификаторов. В качестве верификаторов используются
такие инструменты, как BLAST [3], CPAchecker [2] и UFO [1]. При-
мерами правил корректности, проверяемых системой LDV, являют-
ся правила вызова драйвером функций ядра module_put/module_get,
spin_lock/spin_unlock и др. Всего система поддерживает проверку
нескольких десятков различных правил корректности.

Верификация модулей ядра
    Система верификации LDV позволяет верифицировать отдельные
модули ядра, так как на сегодняшний день верификаторы не спо-
собны анализировать ядро Linux целиком из-за большого объема и
высокой сложности исходного кода. Модули ядра сильно отличаются
от обычных программ на языке Си. Каждый модуль тесно связан с
остальной частью ядра, поэтому в системе LDV автоматически гене-
рируется модель окружения, имитирующая взаимодействие сердцеви-
ны ядра и модуля [4]. Исходный код модуля анализируется совместно
с такой моделью окружения верификатором.

Верификация группы взаимосвязанных модулей
   В работе [6] драйвером называется код, предназначенный непо-
средственно для работы с конкретным устройством. А часть ядра,
с которой взаимодействует данный драйвер, называется вспомога-


34                                                             21 сентября


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

Литература

[1] A. Albarghouthi, Y. Li, A. Gurnkel, M. Chechik, Ufo: A Framework for
    Abstraction- and Interpolation-Based Software Verication, http://www.cs.
    utoronto.ca/~aws/papers/cav12.pdf

[2] D. Beyer, M. E. Keremoglu, CPAchecker: a tool for configurable software
    verification, http://dl.acm.org/citation.cfm?id=2032305.2032321

[3] D. Beyer, T. Henzinger, R. Jhala, R. Majumdar, The Software
    Model Checker Blast: Applications to Software Engineering,
    http://www.sosy-lab.org/~dbeyer/Publications/2007-STTT.The_
    Software_Model_Checker_BLAST.pdf

[4] I. Zakharov, V. Mutilin, E. Novikov, A. Khoroshilov, Generating
    Environment Model for Linux Device Drivers, http://syrcose.ispras.ru/
    2013/files/SYRCoSE2013_Proceedings.pdf


Утреннее заседание (10.00–13.20)                                           35


[5] M. Mandrykin, V. Mutilin, E. Novikov, A. Khoroshilov, P. Shved, Using
    linux device drivers for static verification tools benchmarking, http://dl.
    acm.org/citation.cfm?id=2387324
[6] Yoann Padioleau, J. L. Lawall, G. Muller, Understanding collateral
    evolution in Linux device drivers, http://coccinelle.lip6.fr/papers/
    RR-5769.pdf


Андрианов Павел
Москва, Институт системного программирования РАН
Проект:   Linux Driver Verification http://linuxtesting.org/project/ldv

   Оценка покрытия кода при статическом анализе


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


36                                                    21 сентября


динамическим анализом применяется и статический. Для этого под-
хода оценка покрытия кода традиционно была высокой, так как ис-
ходный код анализируется весь целиком и без реального выполнения
программы.
   Основным минусом статического анализа всегда оставалось боль-
шое число ложных срабатываний, поэтому много усилий было скон-
центрировано на повышении точности анализа. Учёт возможных зна-
чений переменных позволил не анализировать некоторые ветви усло-
вий. Использование нескольких циклов анализа, а также комбинация
различных алгоритмов с последующим уточнением результатов так-
же помогают исключить из анализа тот код, который при заданных
ограничениях недостижим. При этом становится достаточно сложно
отлаживать инструмент в случае, если он пропустил ошибку. Перед
пошаговой отладкой можно посмотреть покрытие и выяснить, анали-
зировал ли инструмент участок кода, содержащий ошибку. Еще одна
причина, по которой какой-то код может стать недостижимым это
неполнота модели окружения, что является важным моментом для
верификации драйверов. Это означает, что полностью смоделировать
взаимодействие программы с операционной системой, пользователем
и аппаратурой очень сложно, поэтому остается код, который не был
проанализирован в рамках текущей модели. В этом случае нам очень
полезно знать, какие именно функции были вызваны из модельного
окружения. Тогда в случае необходимости можно уточнить модель
или вручную добавить некоторые интересные функции. Таким обра-
зом, становится актуальным вопрос о том, какая же именно часть
исходного кода была проанализирована.
   В проекте LDV [1], целью которого является верификация драй-
веров Linux, используется инструмент статической верификации
CPAchecker [2], который реализует идею адаптивного статического
анализа (Configurable Program Analysis). Этот инструмент на основе
графа потока управления строит граф достижимости и, обходя его в
ходе анализа, собирает информацию о посещённых вершинах. Кроме
того, у него есть информация о том, на в какую строчку исходного
кода отображается каждая вершина. Таким образом, для решения
задачи о поиске проанализированных строк нам необходимо в конце
работы инструмента обойти все вершины и выяснить, каким строкам
они соответствуют.
   Формат вывода был выбран аналогичным утилите gcov, которая
собирает информацию непосредственно во время запуска програм-


Утреннее заседание (10.00–13.20)                                37


мы. Это было сделано для использования графической надстройки
Lcov, которая по выводу gcov генерирует отчет в виде комплекта
html-страниц со сведениями о покрытии в терминах исходного кода
программы. После генерации файла в заданном формате запускается
скрипт Lcov, который создаёт отчет. Gcov может считать, сколько раз
выполнена та или иная строка, а также выводить информацию о по-
крытии ветвей. Ветви возможно выделять при достаточно сложных
алгоритмах анализа, поэтому пока решено было остановиться только
на отображении информация о покрытии строк и функций.
   Инструмент оценки покрытия был использован на практике в про-
екте LDV. Это позволило обнаружить некоторые неточности ошибки
в логике анализа и неточности модели окружения.
   Рассмотрим пример отчета (рис. 1).




                      Рис. 1: Пример отчета



    Темно-серым (в оригинале, красным) цветом подсвечиваются
непосещённые строки, светло-серым (в оригинале синим) посещен-
ные. В данном примере в функции main вызывается функция func
через функциональный указатель. Однако, без детального анализа
верификатор не может понять, какая функция вызывается в строке
10, и функция func остается непокрытой.
    В качестве дальнейших планов по развитию инструмента плани-
руется попробовать реализовать поддержку покрытия ветвей.


38                                                           21 сентября


Литература
[1] M. Mandrykin, V. Mutilin, E. Novikov, A. Khoroshilov, P. Shved, Using
    linux device drivers for static verification tools benchmarking,
    http://dl.acm.org/citation.cfm?id=2387324
[2] D. Beyer, M. E. Keremoglu, CPAchecker: a tool for configurable software
    verification, http://dl.acm.org/citation.cfm?id=2032305.2032321


Игорь Власенко
Киев, ALT Linux
Проект: Облачно-дружественная распределенная инфраструктура для
сервисов автоматизации ALT Linux Team

  Облачный кластер автоматизации сопровождения
                     пакетов


                                Аннотация
         создание программного обеспечения для облачного кластера ав-
     томатизированного импорта, сборки и тестирования программных па-
     кетов из сторонних репозиториев СПО в репозиторий СПО Sisyphus
     и развертывание на базе полученного программного обеспечения об-
     лачного кластера автоматизированного импорта, сборки и тестирова-
     ния программных пакетов для решения задач автоматизации полного
     цикла сопровождения в репозитории СПО для ряда классов пакетов
     программного обеспечения.
   За проcшедшее время наработки по автоматизации цикла со-
провождения пакетов в репозиториях ALT Linux Team преврати-
лись в полноценный SDK для разработки приложений автоматиза-
ции на базе библиотек RPM::Source::Transform, RPM::Source::Editor,
Source::Repository::Mass, RPM::Source::BundleImport.
   На основе этого программного обеспечения разработано или на-
ходится в разработке более 20 приложений автоматизации, т.н.
“роботов”, включая такие, как repocop, watch, cronbuild, croncopy,
cronport, fcimport, mdkimport, mgaimport, pldimport, suseimport,
jppimport, srpmbackport, sugarimport, octave-package-builder, mate-
package-builder, perl-package-builder, nodejs-package-builder, CPAN-
updater, girar-nmu-utils.


Утреннее заседание (10.00–13.20)                                39


   Однако при работе с утилитами автоматизации человеку прихо-
дится выполнять работы по целеуказанию (заданию пакетов, подле-
жащих сборке) и управлять процессом сборки и публикации пакетов.
Для автоматизации и этих процессов было разработано программное
обеспечение autorepo.
   Соединение утилит автоматизации, утилит обслуживания списков
пакетов и программнного обеспечения autorepo позволяет создавать
сборочные узлы, которые под руководством или самостоятельно без
вмешательства человека собирают и публикуют пакеты        автоном-
ные сборочные ноды.
   Программное обеспечение autorepo упаковано в виде набора
пакетов RPM autorepo-altnode-* и пакета autorepo-scripts. Пакеты
autorepo-altnode-* являются служебными и предназначены для раз-
вертывания сборочных нод, нод тестирования и других служебных
нод на кластере автоматизации. Сами же скрипты обслуживания суб-
репозитория находятся в пакете autorepo-scripts.
   Скрипты пакета autorepo-scripts предназначены для обслужива-
ния субрепозитория, т. е. некоторого репозитория, который явля-
ется компонентой другого, большего репозитория, расширяет или
перекрывает этот больший репозиторий. Например, репозиторий
autoimports/Sisyphus расширяет репозиторий Sisyphus, а репозиторий
autoports/p7 перекрывает (предоставляет обновления) репозиторий
p7/branch. Компоненты позволяют логически разделить пакеты на
разные классы (например, по происхождению или по уровням тести-
рования). Мотивацией создания autorepo-scripts послужили генерато-
ры пакетов. Пакеты, созанные автоматически, нужно было вынести
в отдельные репозитории, чтобы отделить их от пакетов, сопровож-
даемых вручную.
   В autorepo-scripts есть 2 основных режима работы: автоматиче-
ский режим работы и полуавтоматический режим работы. В автома-
тическом режиме работы нода может работать полностью самостоя-
тельно: в цикле работы вызывается генератор списков имен на сбор-
ку, затем вызывается генератор пакетов, пакеты собираются и при
успехе и отсутствии проблем (нет unmets, проходит install test) от-
правляются в репозиторий, также происходит уход за репозиторием,
и при необходимости рассылка оповещений.
   В полуавтоматическом режиме работы нода осуществляет уход за
субрепозиторием, но не собирает пакеты. Уход за репозиторием вклю-
чает в себя попытку пересобрать пакеты, в которых возникли unmets


40                                                      21 сентября


(основной репозиторий, например, Sisyphus, не стоит на месте, по-
этому в субрепозитории возникают unmets, даже если субрепозито-
рий не меняется), поиск и удаление устаревших пакетов (в зависи-
мости от настроек для утилиты autorepo-purge), ведение архива ре-
позитория, при необходимости рассылка оповещений. Чтобы собрать
пакеты в субрепозиторий, работающий в полуавтоматическом режи-
ме, нужна инициатива пользователя. Пользователь обновляет списки
и запускает генератор пакетов, или иным образом выкладывает ис-
ходные src.rpm пакеты, которые нужно выложить в субрепозиторий,
в подпапку ./OUT рабочего каталога, после чего запускает скрипт
autorepo-mass-build. Кроме src.rpm пакетов, поддерживаются tar ар-
хивы, в формате, которым gear обменивается с hasher, а также тран-
закции из набора src.rpm или hasher tar архивов.
   Таким образом, autorepo-scripts позволяют организовать свой соб-
ственный небольшой incoming и субрепозиторий.
   Облачный кластер автоматизации предоставляет площадку для
развертывания и администрирования роботов автоматизации. Его
также можно рассматривать как еще одну альтернативу планируе-
мым карманам: можно завести там отдельного псевдопользователя,
развернуть под ним сборочную ноду, дать к ней доступ по ssh, и по-
лучить возможность сопровождать свой субрепозиторий с помощью
autorepo-scripts.
   Публичная страница статуса облачного кластера автоматизации
доступна по адресу http://watch.altlinux.org/pub/monitor/index.htm.
   На момент развертывания облачный кластер автоматизации обес-
печивает работу более 20 роботов. Репозитории, поддерживаемые кла-
стером, содержат более 3 тысяч дополнительных пакетов для плат-
формы “p7” и более 10 тысяч дополнительных пакетов для плат-
формы “Sisyphus”. Учитывая, что в репозитории “Sisyphus” более 4-х
тысяч пакетов сопровождается с применением средств автоматиза-
ции, то уже сейчас число пакетов, сопровождающихся с применением
средств автоматизации превысило число пакетов, сопровождающихся
вручную.
   Из других перспективных направлений автоматизации можно от-
метить автоматизацию портирования под другие архитектуры. Без
автоматизации портирование под другие архитектуры достаточно до-
рогая операция, на примере недавних усилий по созданию armh репо-
зитория.



    
Яндекс цитирования Яндекс.Метрика