Устали от нестабильных ошибок в многопоточном коде? Попробуйте использовать средства проверки моделей! Ведь вам больше не нужно бояться непроверенных средств проверки моделей, которые работают либо в геометрической прогрессии, либо неоптимально.
Все это в прошлом: в Институт программных систем Макса Планка разработали новый алгоритм под названием TruSt, который решает эти проблемы и также проверен на Coq. Меня зовут Владимир Гладштейн.
Этим летом я проходил стажировку в MPI-SWS в группе, которая придумала новый алгоритм проверки моделей для поиска ошибок в многопоточных программах.
Этот алгоритм является оптимальным и действительно не имеет состояния (в результате он работает с линейными затратами памяти).
В этом посте я расскажу, как работают средства проверки моделей, в каких случаях их можно использовать и какой алгоритм придумали мои коллеги.
А также как я проверял доказательство его корректности на Coq. 
Обо мне
Я учусь на 4 курсе программы «Математика, алгоритмы и анализ данных» факультета математики и информатики СПбГУ, а также работаю в Лаборатории языковых инструментов Исследования JetBrains. Я изучаю формальную верификацию программ более двух лет и в основном пишу на языке Coq.О стажировке
Этим летом мне посчастливилось пройти стажировку в Институт Макса Планка программных систем .Я попал туда не случайно.
Дело в том, что Лаборатория языковых инструментов JBR тесно сотрудничает с этим институтом.
В частности, мой руководитель группы Антон Подкопаев был постдоком у профессора MPI Виктор Вафеядис .
Поэтому по рекомендации Антона на меня быстро обратили внимание и договорились об интервью с Виктором.
В итоге меня взяли стажером на два месяца — с июля по август 2021 года.
Стажировка проходила удаленно.
О проекте, над которым я работал
В начале лета команда, к которой я присоединился в MPI-SWS, готовилась представить доклад на конференцию.ПОПЛ .
Короче говоря, они придумали новый алгоритм проверки моделей (MC) для поиска ошибок в многопоточных программах и предложили мне формально проверить доказательство его корректности на Coq. Это то, чем я занимался.
Но давайте обо всем по порядку.
Начнем с Кока.
ОКок
Coq — функциональный язык программирования с очень мощной системой зависимых типов.С ее помощью Переписка Карри-Ховарда Кок способен формулировать и записывать доказательства теорем на специальном языке, который он может проверить.
Примеры формулировок теорем в Coq у нас еще будут, а пока, чтобы получить представление о чем речь, можно прочитать начало нежное введение .
Главное, что здесь нужно понимать, это то, что на этом языке можно написать доказательство теоремы, и он его проверит. В сообществе CS считается, что теоремы, проверенные на Coq, не содержат ошибок в доказательствах.
Об ошибках в многопоточном коде
Думаю, хаброжители знают, что многопоточные программы — штука сложная.Иногда они содержат ошибки, которые очень сложно выявить тестами.
Такие баги могут появляться пару раз на тысячу запусков программы, однако, если каждый день ею пользуется около десяти тысяч человек, то хочется как-то поймать баг и исправить его.
Одним из решений является MC. Давайте рассмотрим пример такой программы.
Пример довольно длинный, но он поможет вам понять, в каких случаях разумно использовать средства проверки моделей.
Если вы хотите пропустить пример, нажмите здесь .
Представьте себе свой любимый банк.
А теперь представьте, что вас назначили программистом в этот банк и попросили написать код для обслуживания очередей.
Человек приходит в банк, берет номер и стоит в очереди.
Традиционно ваша программа должна уметь:
- Сохраните номер билета, который будет выдан следующему человеку;
- Сохраните номер билета человека, обслуживаемого в данный момент;
- Выдавать новые билеты;
- Измените номер обслуживаемого билета.
Для начала давайте создадим структуру, описывающую память нашего автомата по выдаче билетов:
Теги: #ошибки #Алгоритмы #Тестирование ИТ-систем #Функциональное программирование #coq #многопоточность #исследование jetbrains #spbgu #проверка моделей #институт Макса Планкаstruct ticketlock_s {
-
Генерируйте Веб-Трафик – Быстро
19 Oct, 24 -
Интернет-Игры: Рост Мировой Популярности
19 Oct, 24 -
С Новым Простом! Просто Линукс. Выпуск 3
19 Oct, 24 -
Sudo И Другие В .Bashrc
19 Oct, 24 -
Лебедев И Его Ошибка
19 Oct, 24
