Пишем полетный контроллер для квадрокоптера на языке Ada

Контроллер скорости (штука для управления тягой винтов) сыграл мелодию при старте, как это любят делать пилоты дронов, которые часто используют полётный контроллер Betaflight. Неужели там бета-флайт? Похоже, что да. Ну, или какая-то из ее разновидностей — открытых полетных контроллеров всего около полдюжины.

Перед глазами побежали флешбеки, где-то из глубин подсознания всплыла забытая уже информация о прошивках для Тойоты на миллионы тысяч строк Си и 2 тысячи глобальных переменных (Toyota: 81564 ошибки в коде).

После просмотра исходного кода Betaflight на гитхабе стало еще страшнее, и чем дальше, тем хуже. Подозреваем, что и самописный код будет примерно такого же уровня. А значит, отсутствует всякая гарантия и возможность не только обеспечить бессбойное функционирование кода, а и вовсе разобраться до конца в его работе. А это – управляющая программа для тяжелого устройства с острыми винтами, которое летает высоко, быстро. Становится страшно: игрушки это одно, но я бы не хотел летать, на таком такси.

Но ведь можно иначе? Можно, решили мы!

И решили это доказать. На Avito был куплен акробатический FPV-“квадрик” на базе STM32F405, для отладки — Discovery-плата для этого же контроллера, а дальше все как в тумане..

Так как же быть иначе?

После быстрого совещания возникли вот такие мысли:

• нам нужен другой подход
• язык и подход должны друг друга дополнять
• академический подход не подойдет, нужны практические применения.

В качестве нового подхода решили, что лучше всего опираться на возможность верификации ПО — до необходимого уровня, без злоупотреблений. Но для языка типа С доступных промышленных зрелых решений не существует, только прототипы [FC] и рекомендации.

При выборе языка мы поставили себе вот какие требования:

• это должно быть что-то близкое к embedded
• Нам нужен хороший богатый runtime с возможностями RTOS, но при этом брать и интегрировать RTOS не хочется
• Он не должен заметно уступать в производительности тому, что используется сейчас.

Оказалось, что из практических инструментов в эти требования хорошо подходит один очень старый, незаслуженно забытый инструмент. Да, это Ada. А точнее, его модерновое, регулярно обновляемое ядро SPARK. В [SRM] описаны основные отличия SPARK от Ada, их не так много.

Что такое SPARK, будет ясно дальше, мы покажем, как именно оно было применено, почему Ада понравилась больше, чем С, как работает прувер, и почему мы при этом ничего не потеряли, а только приобрели. И почему мы не взяли Rust.

Иной подход

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

Прежде всего, верификация НЕ является гарантией того, что программа не содержит ошибок, а является только проверкой, что программа гарантирует некоторые свойства. А уже дело программиста таким образом обеспечить контроль свойств, чтобы получить нужные результаты.

В случае с SPARK, верификация базово предоставляет нам гарантии:

• отсутствия переполнения массивов и переменных
• отсутствия выхода за границы в типах и диапазонах
• отсутствия разыменования null-указателей
• отсутствие выброса исключений.
• гарантию неприменения инструментов, проверку которых выполнить нельзя.
• гарантию выполнения всех инвариантов, которые мы опишем. А опишем мы много!Круто, да?

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

SPARK также учитывает ограничения на типы, которые описаны в Ada. В случае обычного исполнения ошибка несоответствия типов упадет в Runtime; SPARK же позволяет статически доказать, что ограничения на типы не могут быть нарушены никаким потоком исполнения.

Например:

Или другой пример:

Компилятор и верификатор не дадут создать такой код, который приведет к присвоению значений, нарушающих ограничения и предикаты.

Отдельный плюс SPARK в том, что система позволяет “натягивать” гарантии на программу поэтапно, то есть программа может быть частично верифицированной. То есть часть модулей можно объявить верифицируемыми, а часть — (пока) нет.

Сам SPARK делит верификацию на уровни: от «каменного» (Stone level) через «Бронзовый» и «Серебряный» уровни до «Золотого» (Gold) и «Платинового». Каждый из уровней усиливает гарантии:

Мы остановились на уровне Gold, потому что наш квадрокоптер все-таки не Boing 777 MAX.

Как работает верификация в SPARK: прувер собирает описание контрактов и типов, на их основе генерирует правила и ограничения, и далее передает их в солвер (SMT — Z3), который проверяет выполнимость ограничений. Результат решения прувер привязывает к конкретным строкам, в которых возникает невыполнимость.

Более подробно можно почитать в [SUG]

Иной язык

Несмотря на то, что сейчас «рулят» си-подобные ECMA-языки, мы нормально отнеслись к тому, что от этого придется отказаться. Более того, кажется, что чем больше программа, тем больше вредит укорочение ключевых слов и конструкций. Что касается Rust, то он — субъективно — в отношении минимализма издалека сильно напоминает Perl, к сожалению.

И наоборот, по ощущениям, пространные, многобуквенные конструкции раздражают, когда разум летит вперед, но не мешают, когда во главу угла ставится надежность, понятность, и легкость чтения. В этом смысле Ada (а SPARK это подмножество Ada) вполне хорош. Теперь давайте посмотрим, что же язык Ada может дать embedded-разработчику.

 Профили

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

Мы используем профиль Ravenscar, специально для embedded-разработки. Он включает пару дюжин ограничений, которые делают вашу разработку для микроконтроллеров более удобной и верифицируемой: нельзя на ходу переназначать приоритеты задач-потоков, переключать обработчики прерываний, сложные объекты из stdlib-ы и такое.

Вот ограничения профиля Ravescar, для примера

Runtime

Когда в embedded необходимо создать более-менее сложное приложение, там всегда заводится RTOS, и ее выбор и интеграция это отдельная песня. В случае с Ada с этим больше нет сложностей — сама Ada включает в себя минимальную исполняемую среду с вытесняющим планировщиком потоков (в Ada это tasks, задачи), с интегрированными в сам язык средствами синхронизации (семафоры, рандеву, называются entries) и даже средствами избегания дедлоков и инверсии приоритетов. Это оказалось очень удобно для квадрокоптера, как станет понятно ниже.

Для embedded-разработчика доступны на выбор также разные рантаймы:

• zero-footprint — с минимальными ограничениями и даже без многопоточности; зато минимальная программа не превышает пары килобайт, влезает даже в TO MSP430
• small footprint — доступна большая часть функций Ada, но и требования побольше, несколько десятков килобайт RAM
• full ravenscar — доступны все функции в рамках профиля Ravenscar/Extended Ravenscar

Вот пример описания пустой задачи

Хочется обратить внимание, что эти задачи — это по сути легковесные green threads, так как под ними нет никаких настоящих потоков не существует. Поэтому мы не страдаем от отсутствия корутин, ведь задачи не тяжелее них, зато встроены в язык.

Кроме этого, в Ada есть достаточно мощная stdlib для ядра STM32, включая полную реализацию рантайма. Возможно, и для вашей архитектуры она тоже есть.

Почему не “rustRustRUST”!

Когда мы говорим, про гарантии в языках программирования, сразу вспоминается Rust и его гарантии относительно указателей. Почему тут не он? Нам кажется, что Spark мощнее.

Ada не очень любит указатели — там они называются access types, и в большинстве случаев там они не нужны, но если нужны, то — в Spark также есть проверки владения, как в Rust. Если вы аллоцировали объект по указателю, то простое копирование указателя означает передачу владения (которую проконтролирует компилятор/верификатор), а передачу во временное владение (или доступ на чтение) верификатор также понимает и контролирует.

В общем, концепция владения объектом по указателю, и уровень доступа через этот указатель — есть не только в Rust, и его преимуществами можно пользоваться и в других инструментах, в частности, в Ada/SPARK. Подробно можно почитать в [UPS]

Почему мы пишем, что в Ada/SPARK не нужны указатели? В отличие от Си, где базовым инструментом является указатель (хочешь ссылку — вот указатель, хочешь адрес в памяти — вот указатель, хочешь массив — вот указатель — ну вы поняли?), в Ada для всего этого есть строгий тип. Если не хватает встроенных операций, их допустимо переопределять (например, реализовать инлайновый автоинкремент), аналогично можно создать placement constructor, используя т.н. limited-типы — типы, которые компилятор запрещает копировать.

Если уже и этого мало, есть интероп с СИ – то есть код можно компилировать совместно, и слинковать на этапе сборки. Но в этом случае гарантии поведения модуля как черного ящика остаются на разработчике. Для интеропа используются атрибуты — вот так, например, мы оборачиваем функцию на Си в доступ для Ada.

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

IDE

Для работы доступна вполне приятная и удобная IDE, но всегда можно использовать и VSCode с плагинами, и другие текстовые редакторы.

О производительности и надежности

Вполне валидным аргументом может быть вопрос с эффективностью ПО. Что касается эффективности, то в интернете доступно свежее исследование [EFF], из которого хочется привести табличку, показывающую, что “старичок» Ada еще огого:

Если говорить о надежности, то SPARK/Ada известен как один из языков с наименьшим количеством ошибок. В планируемом на 21 запуске кубсатов [LIC] полетное ПО планируется реализовывать на Ada, предыдущий спутник BasiLEO тоже на Ada был единственным среди 12, кому удалось приступить к планируемой миссии.

А теперь — о самом полетном контроллере

После такого вступления стало понятно, что написать полетный контроллер на таких могучих инструментах — совершенно просто. И действительно, если разобраться, то ничего сложного.

Структурная схема управляющего ПО показана на рисунке