1. ホーム
  2. c++

宇宙・放射線環境下でのC++テンプレート利用が推奨されない理由は?

2023-09-20 22:22:03

質問

読み方 この質問 を読んで、例えば宇宙や原子力発電所のような放射線量が高い環境では動的割り当てや例外処理が推奨されない理由がわかりました。 テンプレートについては、その理由がわかりません。説明していただけませんか?

考慮中 この回答 を考えると、かなり安全に使えると書いてありますね。

注:複雑な標準ライブラリのものではなく、目的に応じて作られたカスタムテンプレートについて話しています。

どのように解決するのですか?

スペース互換性のある ( 放射線硬化 , 航空工学 準拠)コンピューティング・デバイスは非常に高価であり、(その中には 打ち上げ 重量がキログラムを超えるため、宇宙での打ち上げも含む)、1 回の宇宙ミッションにはおそらく数億ユーロまたは数十万米ドルの費用がかかります。ソフトウェアやコンピュータの問題でミッションを失うことは、一般に法外なコストがかかるため受け入れられず、携帯電話のアプレット開発には夢にも思わないような高価な開発手法や手順を正当化することになります。 確率的推論 と工学的アプローチを使用することが推奨されます。 宇宙線 は、まだ何らかの形で異常な出来事であることに変わりはありません。ハイレベルな視点から見ると、宇宙線とそれが生み出すビット反転は、信号や入力の抽象的な形式におけるノイズと考えることができます。この「ランダムなビット反転」の問題は、次のように見ることができます。 信号とノイズの比 の問題として見ることができ、そして ランダム化アルゴリズム は有用な概念的枠組みを提供するかもしれません(特にメタレベル、すなわち を分析する 安全性が重要視されるソース コードやコンパイル済みバイナリを分析するとき、また、重要なシステムのランタイムにおいて、洗練されたカーネルやスレッドで スケジューラー ) を使って 情報理論 の視点に立つ。

<ブロッククオート

なぜ宇宙や放射線環境ではC++テンプレートの使用が推奨されないのでしょうか?

その推奨は 一般化 であり、C++ に対する MISRA C のコーディング規則と 組込みC++の のルール、そして DO178C 推奨事項 で、それは放射線に関係なく、組み込みシステムに関係するものです。放射線や振動の制約があるため、宇宙ロケットのコンピュータの組み込みハードウェアは非常に小さくなければなりません(たとえば 経済的 例えば、経済的かつエネルギー消費の理由から、大きな x86 サーバーシステムよりも Raspberry Pi のようなシステムの方がコンピュータパワーとしては大きくなります)。宇宙用チップは、民生用チップの1000倍もします。そして WCET を計算することは、まだ技術的な課題となっています。 CPUキャッシュ 関連の問題のため)。それゆえ ヒープ割り当て では嫌われます。 セーフティクリティカル のような組み込みソフトウエアを多用するシステムでは嫌われます (これらのシステムでメモリ不足の状態をどう扱うか? あるいは、どのように を証明します。 のために十分な RAM があることをどのように証明するのでしょうか? をすべて に十分な RAM があることを確認してください。)

安全性において クリティカルなソフトウェアの世界では の世界では、あなた自身のソフトウェアの品質を何らかの形で保証するだけでなく、それを構築するために使用するすべてのソフトウェア ツール (特にコンパイラとリンカ) の品質も (多くの場合、巧妙な確率論的推論を用いて) 評価しなければなりません。 GCC クロス コンパイラーのバージョンを変更することはありません。 を書きました。 からの事前の承認なしに 連邦航空局 または DGAC ). ほとんどのソフトウェア ツールは、何らかの形で承認または認定を受ける必要があります。

注意してほしいのは 実際には ほとんどの C++ テンプレートは、内部的にヒープを使用します。また、標準的な C++ の コンテナ は確かにそうです。テンプレートを書くと 決して ヒープを使用しないテンプレートを書くのは難しい作業です。もしそれができれば、テンプレートを安全に使うことができます(C++コンパイラとそのテンプレート展開機構を信頼していることが前提ですが、これは トリッキー のような、最近の C++ コンパイラの C++ フロントエンドの一部です。 GCC または Clang ).

同様の理由(ツールセットの信頼性)で、多くの ソースコード生成 ツール (ある種の メタプログラミング 例えば、C++ や C のコードを出力するなど)。例えば、もしあなたが bison (または RPCGEN によってコンパイルされた) いくつかの安全上重要なソフトウェアに含まれます。 makegcc ) を評価する必要があります (そしておそらく徹底的にテストする必要があります)。 gccmake を含むが、さらに bison . これは工学的な理由であり、科学的な理由ではありません。組み込みシステムの中には ランダム化アルゴリズム を巧みに扱うために、特に 騒がしい 入力信号 (おそらく、ごくまれに発生する宇宙線によるランダムなビット反転でさえも) に巧みに対処します。このようなランダム ベースのアルゴリズムの証明、テスト、または分析 (あるいは単なる評価) は、非常に難しいトピックです。

次の項目も参照してください。 フラマ・クラング 証明書 を追加し、以下を観察してください。

  • C++11 (または以下) は恐ろしく複雑なプログラミング言語です . それは、完全な 形式的意味論 . C++の専門家は C++の専門家は、世界中で数十人しかいません。 そのほとんどは標準化委員会に所属しています)。私は、C++でコーディングすることができます。 C++でコーディングする能力はありますが、手のセマンティクスの微妙なコーナーケースをすべて説明できるわけではありません。 のセマンティクスや、C++の メモリ モデル . また、C++は効率的に使用するために、実際には多くの最適化を必要とします。

  • エラーのないC++コンパイラを作るのは非常に困難です。 特に、C++ は実質的にトリッキーな 最適化 また、C++の仕様が複雑なためです。しかし、現在の 最近のGCCやClangのような)現在のものは、実際には非常に優れていて、コンパイラのバグもほとんどありません(それでもいくつかありますが)。 のコンパイラのバグが残っています。C++のCompCert++はまだなく、作るには数百万ユーロか数千万ドル必要です(でも、もしそのような金額を集められるなら まで電子メールでご連絡ください。 [email protected] , 私の仕事の電子メール)。そして、宇宙ソフトウェア産業は 極めて 保守的です。

  • CやC++のヒープメモリアロケータを作るのは難しい。 . コーディング コーディングはトレードオフの問題です。ジョークとして この C のヒープアロケータ を C++ に適用することを考えてみてください。

  • 安全性の証明 (特に レースコンディション または 未定義の動作 実行時のバッファオーバーフローなど) のテンプレート関連 C++ コードは、2019 年第 2 四半期ではまだ、最先端の技術よりわずかに進んでいます。 静的プログラム解析 を行うことができます。私の Bismon テクニカルレポートのドラフト (これは H2020 の成果物のドラフトなので、ヨーロッパの官僚のためにページを飛ばしてください) には、これをより詳細に説明したページがいくつかあります。 を意識してください。 ライスの定理 .

  • システム全体のC++組込みソフトウェアテスト は、ロケット打ち上げが必要になるかもしれません(la アリアン5試験飛行501 あるいは、少なくとも研究室での複雑で重い実験が必要です)。それは です。 非常に 高い . テストでも、地球上では 火星探査機 たくさん が必要です。

安全性が重要な組み込みソフトウェア (例: 列車のブレーキ、自律走行車、自律型ドローン、大型石油プラットフォームまたは石油精製所、ミサイルなど) をコーディングしている場合を考えてみてください。あなたは素朴にC++の標準コンテナ、例えば、いくつかの std::map<std::string,long> . メモリ不足の場合、どうすればいいのでしょうか?億ユーロの宇宙ロケットに資金を提供する組織で働く人々に、あなたの組み込みソフトウェア(それを構築するために使用したコンパイラを含む)が十分に優れていることをどのように証明し、少なくとも "納得させるのでしょうか? 10 年前のルールでは、あらゆる種類の動的ヒープ割り当てを禁止していました。

複雑な標準ライブラリではなく、意図的に作られたカスタムテンプレートについてです。

これらも証明するのは難しい を証明すること、あるいはより一般的にその品質を評価することは困難です(そしておそらく、あなたは自分自身の アロケータ をその内部で使いたいでしょう)。空間的には、コード空間は強い制約です。だから、例えば、次のようにコンパイルすることになる。 g++ -Os -Wall または clang++ -Os -Wall . しかし、どのように証明したのでしょうか? すべて によって行われる微妙な最適化について -Os (そして、これらはあなたのGCCやClangのバージョンに特有のものです)? 組み込みの C++ 宇宙ソフトウェアの実行時バグがあるとミッションがクラッシュする可能性があるため、宇宙資金提供団体はあなたにこのことを尋ねるでしょう (もう一度 アリアン 5 初飛行 の失敗についてもう一度お読みください)、しかしヨーロッパ人をあまり笑わないでください。 ボーイング 737 MAX とその MACS 類似の混乱 ).


私の個人的な推奨 (ただし、あまり深刻に考えないでください。2019 年は何よりもダジャレです)、空間埋め込みソフトウェアのコーディングについて検討することです。 Rust . なぜなら、C++よりも若干安全だからです。もちろん、宇宙用コンピュータに適した立派なRustコンパイラを手に入れるには、5年か7年で5〜10M€(あるいはMUS$)を費やさなければなりません(繰り返しますが、フリーソフトウェアのCompcert/Rustライクコンパイラにそれだけの費用をかけられるなら、専門的に私にコンタクトをとってください)。しかし、これはソフトウェア工学とソフトウェアプロジェクト管理の問題なのです。 神話上の人月 そして でたらめな仕事 をご覧ください。 ディルバートの原則 これは、宇宙ソフトウェア業界や組み込みコンパイラ業界にも当てはまることです。)

私の強く個人的な意見としては、欧州委員会は(例えば以下のような手段で)資金を提供すべきです。 ホライゾン ヨーロッパ ) a フリーソフト CompCert++ (あるいはもっといいのは Compcert/Rust) のようなプロジェクト (そしてそのようなプロジェクトは 5 年以上と 5 人以上のトップクラスの博士課程の研究者を必要とするでしょう) が必要です。しかし、60 歳になった私は、悲しいかな、それが実現しないことを知っています (なぜなら、E.C. のイデオロギーは - 明白な理由により、ほとんどがドイツの政策に影響されていますが - 今でも、そのイデオロギーは 歴史の終わり そのため、H2020とHorizon Europeは、実際には、欧州の企業に対する税の最適化を、欧州の企業を通じて実施するための方法であることがほとんどです。 タックスヘイブン と、CompCertプロジェクトのメンバー数人と個人的に何度も話し合った結果です。私は悲しいことに DARPA または NASA は、将来の CompCert/Rust プロジェクトに(E.C.が資金を提供するよりも)はるかに多くの資金を提供する可能性があります。


NB。ヨーロッパのアビオニクス産業 (主に Airbus) は、より多くの 形式的な手法 のアプローチを使用しています。したがって いくつかの (に置き換わっているため)ユニットテストは回避されます。 形式的な証明 のようなツールで、ソースコードの Frama-C または アストレ - のみで、どちらも C++ の認証を受けていません。 サブセット を禁止している C の C動的メモリ割り当て およびCの他のいくつかの機能)。そして、これが許されるのは DO-178C で許可されています (前身である DO-178B )であり、フランスの規制当局によって承認されている。 DGAC (というフランスの規制当局の承認を受けています(他のヨーロッパの規制当局も同様と思われます)。

また、多くの SIGPLAN カンファレンスは 間接的に の質問と関連しています。