Добавление спецификаций тестируемого кода в Linux Ke... Чак Волбер, Габриэле Паолони и Кейт Стюарт

Добавление тестируемых спецификаций кода в ядро ​​Linux — Чак Волбер, Габриэле Паолони (Red Hat) и Кейт Стюарт (Linux Foundation)

В ядре Linux замысел проектирования является эмергентным свойством. Этому есть ряд хорошо понятных причин, наиболее важными из которых являются меняющиеся потребности пользовательского пространства и распределенный характер его разработки. Также разумно предположить, что, несмотря на свою исключительную сложность, замысел проектирования ядра можно сформулировать в довольно простых высокоуровневых терминах: действовать как арбитражный слой между аппаратным обеспечением и прикладным программным обеспечением. Поэтому на практике ядро ​​Linux считается «работоспособным», когда пользовательское пространство ведет себя ожидаемым образом как в заданных (например, POSIX), так и в неопределенных (например, поведение планировщика) режимах.

Хотя это разумное объяснение пути, пройденного от скромных начинаний до того, где мы находимся сегодня, процесс разработки ядра Linux испытывает напряжение под тяжестью своего успеха. Сообщество отреагировало, создав такие инструменты, как syzkaller, kselftest, KUnit и наборы тестов, специфичные для каждого поставщика, чтобы помочь ядру соответствовать ожиданиям. Кроме того, существует обширная документация и большой архив знаний сообщества, документирующих проектирование и использование ядра Linux. Несмотря на всё это, сохраняется разрыв между детальным замыслом проектирования и всеми формами тестирования. Это важно, потому что тесты рискуют привести к несоответствию без явного одобрения разработчика.

Возможно, в очень узких ситуациях можно найти подтверждение от сопровождающего, что тест точно отражает детали его предполагаемого проекта. Но в широком смысле нет никаких доказательств того, что замысел разработчика можно однозначно отследить с помощью какой-либо формы воспроизводимого тестирования. Даже среди сопровождающих ядра это так, например, разработчикам PREEMPT_RT, как известно, приходится проводить обратное проектирование поведения планирования ядра, чтобы определить его свойства справедливости и задержки. По сути, всё тестирование ядра в значительной степени основано на системе фрагментарного обратного проектирования и обоснованных предположений. Это не умаляет значительной ценности тестирования, проводимого сообществом, но важно признать, что ни один репозиторий, содержащий тестовый код, не может претендовать на использование метафорического (или буквального) тега «Проверено сопровождающим».

Отложив на мгновение в сторону огромный размер ядра Linux, мы можем поразмышлять над решением этой проблемы, а затем проложить путь к разумному подходу. Выражение проектных решений встречается на многих уровнях, некоторые из которых становятся непрактичными для анализа на уровне исходного кода ядра, поскольку они основаны на сложных предположениях об использовании. Поэтому мы ограничиваемся самым низким разумным уровнем проектного замысла, описанным в RTCA DO-178C как «требования к программному обеспечению, из которых исходный код может быть непосредственно реализован без дополнительной информации». Лучшие практики разработки этих требований, которые мы будем называть «проверяемыми ожиданиями», выходят за рамки этой презентации. Достаточно сказать, что создание проверяемых ожиданий — это специализированный навык, который заставляет очень глубоко размышлять о замысле кода.

Имея на руках проверяемые ожидания, мы получаем необходимый уровень ясности для применения замкнутого цикла к коду ядра Linux, который однозначно связывает код с проектным замыслом отслеживаемым образом. При согласии сопровождающих (своеобразном «подписании»), тестовый пример может быть получен из проверяемого ожидания. Когда тестовый пример проходит успешно, можно использовать инструменты анализа покрытия кода, такие как llvm-cov и gcov, чтобы убедиться, что соответствующий код не был упущен. Согласовав ожидания, тесты и покрытие, мы можем подтвердить, что код точно отражает проектный замысел, достигая цели верификации программного обеспечения.

В заключение мы рассмотрим «слона в комнате» — огромный размер ядра Linux и потенциальную дополнительную нагрузку на сообщество сопровождающих. Как известно любому сопровождающему, сортировка ошибок — огромная часть работы, и хотя ошибки никогда не исчезнут, этот замкнутый цикл перенесет нагрузку с верификации («правильно ли код делает то, что нужно») на валидацию («правильно ли код делает то, что нужно»). Как верификация, так и валидация являются необходимыми составляющими работы сопровождающего, но этот подход обещает значительно облегчить аспект верификации. Таким образом, «сок стоит того», но необходим значительный скептицизм, и для уточнения подхода требуется обратная связь от сообщества разработчиков ядра.

В этом докладе будут рассмотрены следующие темы:
1) текущие ограничения рекомендаций по низкоуровневому проектированию ядра Linux (как в Documentation/doc-guide/kernel-doc.rst)

2) Подробные примеры поведения в рамках замкнутого ...