Труды института системного программирования РАН
RUS  ENG    ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB  
Общая информация
Последний выпуск
Архив

Поиск публикаций
Поиск ссылок

RSS
Последний выпуск
Текущие выпуски
Архивные выпуски
Что такое RSS


Труды ИСП РАН:
Год:
Том:
Выпуск:
Страница:
Найти




Персональный вход:
Логин:
Пароль:
Запомнить пароль
Войти
Забыли пароль?
Регистрация

Труды института системного программирования РАН, 2015, том 27, выпуск 4, страницы 49–68
DOI: https://doi.org/10.15514/ISPRAS-2015-27(4)-4 (Mi tisp164) 		 
Эта публикация цитируется в 1 научной статье (всего в 1 статье)

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

М. У. Мандрыкинa, А. В. Хорошиловbacd

a Институт системного программирования РАН
b Московский физико-технический институт (государственный университет)
c Московский государственный университет имени М. В. Ломоносова
d НИУ Высшая школа экономики
PDF полного текста (346 kB) Список цитирования (1)
Список литературы:
PDF
HTML
DOI: https://doi.org/10.15514/ISPRAS-2015-27(4)-4
Аннотация: В статье рассматривается задача дедуктивной верификации кода ядра ОС Linux, написанного на языке Си и выполняющегося в окружении с высокой степенью параллелизма. Существенной особенностью этого кода является наличие работы с разделяемыми данными, что не позволяет применять классические методы дедуктивной верификации. Для преодоления этих сложностей в работе представлены предложения по формированию подхода к спецификации и верификации кода, работающего с разделяемыми данными, основанные на доказательстве соответствия этого кода заданной спецификации некоторой дисциплины синхронизации. Подход иллюстрируется примерами упрощенной модели спецификации спин-блокировок и внешнего интерфейса механизма синхронизации RCU (Read-copy-update), широко используемого в ядре ОС Linux.
Ключевые слова: Верификация, параллелизм, владение, инварианты, семантика языка C.
Финансовая поддержка Номер гранта
Министерство образования и науки Российской Федерации RFMEFI60414X0051
Исследование проводилось при финансовой поддержке Министерства образования и науки Российской Федерации (уникальный идентификатор проекта – RFMEFI60414X0051)
Реферативные базы данных:
Тип публикации: Статья
Образец цитирования: М. У. Мандрыкин, А. В. Хорошилов, “О дедуктивной верификации Си программ, работающих с разделяемыми данными”, Труды ИСП РАН, 27:4 (2015), 49–68
Цитирование в формате AMSBIB
\RBibitem{ManKho15}
\by М.~У.~Мандрыкин, А.~В.~Хорошилов
\paper О дедуктивной верификации Си программ, работающих с разделяемыми данными
\jour Труды ИСП РАН
\yr 2015
\vol 27
\issue 4
\pages 49--68
\mathnet{http://mi.mathnet.ru/tisp164}
\crossref{https://doi.org/10.15514/ISPRAS-2015-27(4)-4}
\elib{https://elibrary.ru/item.asp?id=24928723}
Образцы ссылок на эту страницу:
  • https://www.mathnet.ru/rus/tisp164
  • https://www.mathnet.ru/rus/tisp/v27/i4/p49
    • Эта публикация цитируется в следующих 1 статьяx:
    Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    		Труды института системного программирования РАН
    Статистика просмотров:
    Страница аннотации:136
    PDF полного текста:51
    Список литературы:21
     
      Обратная связь:
    		  Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2024