Обратите внимание, что совместимые с космосом ( радиационно-стойкие , аэронавтики совместимые) вычислительные устройства очень дороги (включая запуск в космосе, поскольку их вес превышает килограммы), и что одна космическая миссия стоит, возможно, сто миллионов евро или долларов США. Потеря миссии из-за проблем с программным обеспечением или компьютером обычно сопряжена с непомерными затратами, поэтому является неприемлемой и оправдывает дорогостоящие методы и процедуры разработки, о которых вы даже не мечтаете использовать для разработки апплета мобильного телефона и использования вероятностных рассуждений и инженерные подходы рекомендуются, поскольку космические лучи все еще являются каким-то "необычным" событием. С точки зрения высокого уровня, космический луч и перевернутый бит могут рассматриваться как шум в некоторой абстрактной форме сигнала или входа. Вы можете рассматривать эту проблему "случайного переворота битов" как проблему отношение сигнал / шум , тогда рандомизированные алгоритмы могут обеспечить полезную концептуальную основу (особенно на мета-уровне, то есть, когда анализирует ваш критический для безопасности исходный код или скомпилированный двоичный файл, а также во время работы критической системы, в каком-то сложном ядре или потоке планировщик ), с теория информации точка зрения.
Почему использование шаблона C ++ не рекомендуется в космической / излучаемой среде?
Эта рекомендация представляет собой обобщение для C ++ правил кодирования MISRA C и правил Embedded C ++ и DO178C рекомендации , и это связано не с излучением, а со встроенными системами. Из-за радиационных и вибрационных ограничений встроенное аппаратное обеспечение любого ракетно-космического компьютера должно быть очень небольшим (например, по экономичным и по причинам, связанным с энергопотреблением, оно больше - по мощности компьютера - система Raspberry Pi-like чем большая система сервера x86). Космические закаленные чипы стоят в 1000 раз дороже, чем их гражданские аналоги. А вычисление WCET на компьютерах со встроенным пространством все еще остается технической проблемой (например, из-за проблем, связанных с кэш-памятью ЦП ). Следовательно, выделение кучи не одобряется в критически важных для безопасности встроенных программно-интенсивных системах (как бы вы справились с условиями нехватки памяти в этих? Или как бы вы доказали что у вас достаточно ОЗУ для всех случаев реального времени выполнения?)
Помните, что в мире критически важного программного обеспечения вы не только каким-то образом «гарантируете» или «обещаете», и, конечно, оцениваете (часто с некоторыми умными вероятностными рассуждениями) качество вашего собственного программного обеспечения, но также и всех программных инструментов, использованных для его создания (в частности: ваш компилятор и ваш компоновщик; Boeing или Airbus не будут менять свою версию кросс-компилятора GCC , используемого для компиляции их программного обеспечения для управления полетом без предварительного письменное утверждение, например, FAA или DGAC ). Большинство ваших программных инструментов должны быть как-то одобрены или сертифицированы.
Помните, что на практике , большинство шаблонов C ++ (но, конечно, не все) внутренне используют кучу. И стандартные контейнеры C ++ , безусловно, делают. Написание шаблонов, которые никогда не используют кучу, - трудное упражнение. Если вы способны на это, вы можете безопасно использовать шаблоны (при условии, что вы доверяете своему компилятору C ++ и его механизму расширения шаблонов, который является хитрой частью внешнего интерфейса C ++ большинства последних компиляторов C ++, например, как GCC или Clang ).
Я полагаю, что по аналогичным причинам (надежность набора инструментов) неодобрительно использовать множество инструментов генерации исходного кода (при выполнении какого-либо метапрограммирования , например, испускающего код C ++ или C),Обратите внимание, например, что если вы используете bison (или RPCGEN ) в некоторых критически важных для безопасности программах (скомпилированных make и gcc), вам необходимо оценить (и, возможно, исчерпывающий тест) не только gcc и make, но также bison.Это инженерная, а не научная причина.Обратите внимание, что некоторые встраиваемые системы могут использовать рандомизированные алгоритмы , в частности, для умной работы с шумными входными сигналами (возможно, даже случайными скачками битов из-за достаточно редких космических лучей).Проверка, тестирование или анализ (или просто оценка) таких случайных алгоритмов - довольно сложная тема.
Посмотрите также на Frama-Clang и CompCert и наблюдайтеследующее:
C ++ 11 (или далее) - ужасно сложный язык программирования .Он не имеет полной формальной семантики .Людей, достаточно опытных в C ++, всего несколько десятков во всем мире (вероятно, большинство из них в своем стандартном комитете).Я способен кодировать на C ++, но не объяснять все тонкие угловые случаи семантики перемещения или модели памяти C ++ .Кроме того, C ++ требует на практике многих оптимизаций для эффективного использования.
Очень трудно создать безошибочный компилятор C ++ , в частности, потому что C ++ практически требуетхитрые оптимизации , и из-за сложности спецификации C ++.Но текущие (такие как недавние GCC или Clang) на практике довольно хороши, и у них есть немного (но все еще некоторые) остаточных ошибок компилятора.CompCert ++ для C ++ пока не существует, и для его создания требуется несколько миллионов евро или долларов США (но если вы можете собрать такую сумму, пожалуйста, свяжитесь с me по электронной почте, например, с basile.starynkevitch@cea.fr, мойрабочий email).А индустрия космического программного обеспечения крайне консервативна.
Трудно сделать хороший распределитель памяти кучи на C или C ++ .Кодирование - это вопрос компромиссов.В качестве шутки рассмотрите возможность адаптации этого распределителя кучи C к C ++.
доказательство безопасности (в частности, отсутствие гонкиусловия или неопределенное поведение (например, переполнение буфера во время выполнения) кода C ++, связанного с шаблоном, во 2кв2019 все еще немного опережает современное состояние из статический анализ программы кода C ++.Мой черновой технический отчет Бисмона (это черновой вариант H2020, поэтому пропустите страницы для европейских бюрократов) содержит несколько страниц, объясняющих это более подробно. Помните о Теорема Райса .
для теста встроенного программного обеспечения всей системы C ++ может потребоваться запуск ракеты (la Ariane 5, испытательный полет 501 , или, по крайней мере, сложные и тяжелые эксперименты в лаборатории).Это это очень дорого .Даже тестирование на Земле марсохода требует много денег.
Подумайте об этом: вы кодируете какое-то критически важное для безопасностивстроенное программное обеспечение (например, для торможения поездов, автономных транспортных средств, автономных беспилотников, большой нефтяной платформы или нефтеперерабатывающего завода, ракет и т. д ...).Вы наивно используете какой-то стандартный контейнер C ++, например, std::map<std::string,long>.Что должно произойти из-за нехватки памяти?Как вы «докажите» или, по крайней мере, «убедите» людей, работающих в организациях, финансирующих космическую ракету стоимостью 100 миллионов евро, в том, что ваше встроенное программное обеспечение (включая компилятор, использованный для его сборки) достаточно хорошо?Правило десятилетней давности заключалось в том, чтобы запрещать любое динамическое выделение кучи.
Я не говорю о сложных стандартных элементах библиотеки, а о специально созданных пользовательских шаблонах.
Даже это трудно доказать , или, в более общем смысле, оценить их качество (и вы, вероятно, захотите использовать свой собственный allocator внутри них).В пространстве кодовое пространство является сильным ограничением.Таким образом, вы должны скомпилировать, например, g++ -Os -Wall или clang++ -Os -Wall.Но как вы доказали - или просто протестировали - все тонкие оптимизации, выполненные -Os (и они специфичны для вашей версии GCC или Clang)?Ваша организация, финансирующая космос, попросит вас об этом, поскольку любая ошибка во время выполнения во встроенном космическом программном обеспечении C ++ может привести к сбою миссии (прочитайте еще раз о сбое Ariane 5 first flight - закодировано на некотором диалекте Ады, который был при этомвремя «лучшая» и «более безопасная» система типов, чем C ++ 17 сегодня), но не смейтесь слишком над европейцами. Boeing 737 MAX с MACS - похожий беспорядок ).
Моя личная рекомендация (но, пожалуйста, не принимайте ееслишком серьезно. В 2019 году это больше каламбур, чем что-либо еще) было бы рассмотреть кодирование вашего встроенного программного обеспечения в Rust .Потому что это немного безопаснее, чем C ++.Конечно, вам придется потратить от 5 до 10 млн. Евро (или MUS $) через 5 или 7 лет, чтобы получить прекрасный компилятор Rust, подходящий для космических компьютеров (опять же, пожалуйста, свяжитесь со мной профессионально, если вы способны потратить этомного на свободном программном обеспечении Compcert / Rust как компилятор).Но это всего лишь вопрос разработки программного обеспечения и управления программными проектами (подробнее см. Мифический человеко-месяц и Чушь заданий Также следует помнить о принципе Дильберта : он применим как к индустрии космического программного обеспечения, так и к индустрии встроенных компиляторов, как и ко всему прочему.следует финансировать (например, через Horizon Europe ) бесплатное программное обеспечение CompCert ++ (или даже лучше, Compcert / Rust), подобный проекту (и такой проект потребует более 5 лет и более5 топ-класса, PhD исследователи).Но в возрасте 60 лет, к сожалению, я знаю, что этого не произойдет (потому что идеология ЕС - главным образом вдохновленная политикой Германии по очевидным причинам - все еще является иллюзией Конца истории , поэтому H2020 и Horizon Europe на практике представляют собой в основном способ реализации налоговых оптимизаций для корпораций в Европе через европейские налоговые убежища ), и это после нескольких частных обсуждений с несколькими участниками проекта CompCert.К сожалению, я ожидаю, что DARPA или NASA * 1230 * с гораздо большей вероятностью будут финансировать какой-либо будущий проект CompCert / Rust (чем финансирует его ЕС).
NB.Европейская индустрия авионики (в основном Airbus) использует гораздо больше формальных методов , чем североамериканская (Boeing).Следовательно, некоторые (не все) модульные тесты исключаются (поскольку заменены формальными доказательствами исходного кода, возможно, такими инструментами, как Frama-C или Astrée - ни один из них не был сертифицирован для C ++, только для подмножества C, запрещающего C динамического выделения памяти и некоторых других функций C).И это разрешено DO-178C (не предшественником DO-178B ) и одобрено французским регулятором, DGAC (и, я полагаю, другими европейскимирегуляторы).
Также обратите внимание, что многие SIGPLAN конференций косвенно связаны с вопросом ОП.