Ravenscarプロファイル

動的タスク生成やselect文などを禁止し、Adaのタスク機能を静的解析可能で決定論的なサブセットに制限するプロファイル。

概念URI: https://comcomponent.com/knowledge/ravenscar-profile/
別名・表記: Ravenscar
最終確認日: 2026-08-01
機械可読データ: JSON-LD

この概念が関わる関係

RavenscarプロファイルはAdaのタスク(並行処理)を前提とします。Ravenscarプロファイルは、Adaのタスク機能を静的タイミング解析を行いやすい決定論的なサブセットへ制限する規約である。 / 確度: 確立した関係 / 確認日: 2026-08-01 出典
Annex D(Adaのリアルタイムシステム標準)はRavenscarプロファイルを利用します。Annex Dの枠組みのもとで、安全性が極めて重要なシステム向けにタスク機能を制限するRavenscarプロファイルが定義される。 / 確度: 確立した関係 / 確認日: 2026-08-01 出典
RavenscarプロファイルはAdaのタスク(並行処理)を前提とします。Ravenscarプロファイルは、Adaのタスク機能を静的に解析可能で決定論的なサブセットへ制限する規約である。 / 確度: 確立した関係 / 確認日: 2026-08-01 出典
RavenscarプロファイルはFIFO_Within_Prioritiesを前提とします。Ravenscarプロファイルは、FIFO_Within_Prioritiesを必須のディスパッチポリシーとして要求する。 / 確度: 確立した関係 / 確認日: 2026-08-01 出典
RavenscarプロファイルはCeiling_Lockingプロトコルを前提とします。Ravenscarプロファイルは、Ceiling_Lockingを必須のロッキングポリシーとして要求する。 / 確度: 確立した関係 / 確認日: 2026-08-01 出典
RavenscarプロファイルはGNATで構成できます。GNATを使う場合、Ravenscarプロファイルはgnat.adcファイルにpragma Profile (Ravenscar);を記述することで有効化できる(他のAda処理系では有効化の記述方法が異なる)。 / 確度: 条件付きの関係 / 確認日: 2026-08-01 出典
相対delay(delay文)をRavenscarプロファイルに用いることは推奨されません。相対delayは累積ドリフトを生みやすいため、Ravenscarプロファイルに準拠したコードで用いることは推奨されず、禁止される。 / 確度: 確立した関係 / 確認日: 2026-08-01 出典
SPARKはRavenscarプロファイルを前提とします。SPARKでタスクを扱う場合、並行処理をRavenscar(または後継のJorvik)プロファイルの範囲に限定することを前提とする / 確度: 条件付きの関係 / 確認日: 2026-08-01 出典
Ravenscarプロファイルはデッドロック(deadlock)を軽減します。Ravenscarプロファイルはタスクモデルを制限し、静的なデッドロック解析を可能にすることでデッドロックのリスクを下げる / 確度: 条件付きの関係 / 確認日: 2026-08-01 出典
RavenscarプロファイルはAdaのタスク(並行処理)を前提とします。Ravenscarプロファイルは、通常のAdaのタスクモデルを静的解析しやすい範囲に制限したものである / 確度: 確立した関係 / 確認日: 2026-08-01 出典

この概念を扱う記事

一次資料

https://ada-lang.io/docs/arm/AA-D/

このページはサイトの知識グラフ(_data/knowledge/)から自動生成されています。誤りの指摘はお問い合わせからお願いします。