知識マップ: 取りこぼさない取り込み処理をAdaのタスクで作る ── 保護オブジェクトのリングバッファと優先度

記事「取りこぼさない取り込み処理をAdaのタスクで作る ── 保護オブジェクトのリングバッファと優先度」の主張を、概念と関係(エッジ)に分解した知識グラフの全体です。各関係には根拠・確認日・確度が付いています。

カメラの取り込みを、周期タスクと処理タスクと、スロットの番号を入れる保護オブジェクトの有限バッファーで組み立てる。保護オブジェクトのエントリはバリアで呼び出し側を待たせ、周期タスクはdelay untilで予定時刻を保つ。保護オブジェクトの優先度上限はPriorityアスペクトで設定し、呼ぶタスクの優先度が上限より高いとProgram_Errorになる。JorvikプロファイルはFIFO_Within_PrioritiesとCeiling_Lockingを含み、SPARKで並行処理を扱うにはRavenscarかJorvikが要る。GNATproveはタスクが同期されていないものを共有するとデータ競合として報告する。GNATのLinux版はFIFO_Within_PrioritiesのタスクをSCHED_FIFOのスレッドで動かすが、その権限がなければ優先度は効かない。バッファーがあふれるとフレームは捨てられる。

flowchart LR
    accTitle: Adaのタスクで作るカメラの取り込み処理の知識マップ
    accDescr: 保護オブジェクトが有限バッファーを実装してバリアを使い、Adaのタスクがdelay untilで周期を保ち、保護オブジェクトの優先度上限をPriorityで設定すること、JorvikプロファイルがFIFO_Within_PrioritiesとCeiling_Lockingを前提とすること、SPARKが並行処理にJorvikプロファイルを前提とし、GNATproveでデータ競合を確かめること、GNATのLinux版がFIFO_Within_PrioritiesにSCHED_FIFOを使うこと、満杯の有限バッファーがフレームドロップの原因になり得ることを示す図。
    ada_task["Adaのタスク(並行処理)"]
    protected_object["保護オブジェクト(protected object)"]
    frame_drop["フレームドロップ"]
    bounded_buffer["有限バッファー"]
    barrier["バリア(保護エントリのwhen条件)"]
    ada_delay_until["delay until(絶対時刻の遅延)"]
    task_priority["タスク優先度(pragma Priority)"]
    jorvik_profile["Jorvikプロファイル"]
    fifo_within_priorities["FIFO_Within_Priorities"]
    ceiling_locking["Ceiling_Lockingプロトコル"]
    spark["SPARK"]
    data_race["データ競合(data race)"]
    gnatprove["GNATprove"]
    sched_fifo["SCHED_FIFO"]
    gnat["GNAT"]
    protected_object -.->|"実装を担う"| bounded_buffer
    protected_object -.->|"利用する"| barrier
    ada_task -->|"利用する"| ada_delay_until
    protected_object -->|"で構成できる"| task_priority
    jorvik_profile -->|"前提とする"| fifo_within_priorities
    jorvik_profile -->|"前提とする"| ceiling_locking
    spark -.->|"前提とする"| jorvik_profile
    data_race -.->|"で確認できる"| gnatprove
    fifo_within_priorities -.->|"利用する"| sched_fifo
    gnat -.->|"実装を担う"| ceiling_locking
    bounded_buffer -.->|"原因になり得る"| frame_drop

概念間の関係(全11件)

図と同じ関係を文章でも列挙します。表示している文と機械可読な意味データ(RDFa)は同じ要素に載っています。確度が「確立した関係」のものは直接の関係として、「条件付きの関係」のものは成立条件つきの言明(rdf:Statement)として表現しています。

• 保護オブジェクト(protected object)は有限バッファーの実装を担います。記事の Slot_Queue は容量8の保護型で、スロットの番号をモジュラー型の添字で循環させて入れる。カメラのタスクは満杯でも待たない手続きだけを呼び、処理タスクはエントリで待つ。 / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典 出典 出典
• 保護オブジェクト(protected object)はバリア(保護エントリのwhen条件)を利用します。Slot_Queue のエントリ Take は、バリア when Count > 0 が真になるまで呼び出し側を待たせる。Ravenscar ではバリアが静的な式か保護オブジェクトの成分を指す名前1つに限られ、Jorvik は保護オブジェクトの成分と静的な式を比較演算や論理演算で組み合わせた式を許す。 / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典 出典 出典
• Adaのタスク(並行処理)はdelay until(絶対時刻の遅延)を利用します。カメラを模したタスクは、前回の予定時刻に周期を足した絶対時刻まで delay until で待ち、10ミリ秒ごとの到着を模す。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典
• 保護オブジェクト(protected object)はタスク優先度(pragma Priority)で構成できます。保護オブジェクトの優先度は Priority アスペクトで設定し、Ceiling_Locking では優先度上限になる。保護された操作を呼ぶタスクの優先度が上限より高いと Program_Error になる。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典
• JorvikプロファイルはFIFO_Within_Prioritiesを前提とします。Jorvik プロファイルは、Task_Dispatching_Policy (FIFO_Within_Priorities) を含むプラグマの組と同じである。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典
• JorvikプロファイルはCeiling_Lockingプロトコルを前提とします。Jorvik プロファイルは、Locking_Policy (Ceiling_Locking) を含むプラグマの組と同じである。 / 確度: 確立した関係 / 確認日: 2026-11-10 出典
• SPARKはJorvikプロファイルを前提とします。SPARK でタスクと保護オブジェクトを扱うには、Ravenscar か Jorvik のプロファイルと Partition_Elaboration_Policy (Sequential) が要る。記事では Jorvik を使った。 / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典
• データ競合(data race)はGNATproveで確認できます。GNATprove は、タスクが保護オブジェクトやアトミックな変数のような同期されたもの以外を共有するとデータ競合の可能性として報告する。本体を SPARK の外に置いた状態に Synchronous を付けると、それは確かめられない前提になる。 / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典
• FIFO_Within_PrioritiesはSCHED_FIFOを利用します。GNAT の Linux 版は、FIFO_Within_Priorities のタスクのスレッドに pthread_setschedparam で SCHED_FIFO を設定し、権限がなくて失敗しても続ける。記事の環境（RLIMIT_RTPRIO は0）では root で動かすと SCHED_FIFO になり、一般のユーザーでは SCHED_OTHER のままで優先度は効かなかった。 / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典 出典
• GNATはCeiling_Lockingプロトコルの実装を担います。GNAT の Linux 版は、優先度上限つきのミューテックスで Ceiling_Locking を実装し、ロックが EINVAL を返すと上限の違反とする。root でなく、libcap で CAP_SYS_NICE を判定できなければ Ceiling_Locking の指定を無視する。記事の環境では、CAP_SYS_NICE を持たない root で正しいプログラムが上限の違反で止まった。 / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典
• 有限バッファーはフレームドロップの原因になることがあります。バッファーが満杯になるとフレームは捨てられる。バッファーを増やすと一時的な遅れには耐えられるが、処理が平均して到着より遅いと増やしても捨てる割合は変わらない。 / 確度: 条件付きの関係 / 確認日: 2026-11-10 出典

主要概念の定義

Adaのタスク(並行処理)

スレッドをOSのAPIやライブラリに頼らず、言語仕様に組み込む形で提供するAdaの並行実行単位。

保護オブジェクト(protected object)

procedure・function・entryの3種の操作を通じてのみ内部データへアクセスさせ、排他制御を言語が保証するAda 95で導入された機構。

フレームドロップ

カメラが撮影・送信した画像(フレーム)の一部またはすべてが、受信側のアプリに正しく届かないこと。

Jorvikプロファイル

Ravenscarプロファイルから6つの制限を外し、Simple_BarriersをPure_Barriersに置き換えた、Ada 2022で標準に加わったタスク機能のプロファイル。

SPARK

プログラムの性質を数学的に証明できるように設計された、Adaのサブセット(部分言語)とそのツール群。

データ競合(data race)

複数のタスクが同じメモリ位置に同時アクセスし、少なくとも一方が書き込みであるために結果が未定義になる状態である。

FIFO_Within_Priorities

同一優先度内はFIFOで実行し、より高い優先度のタスクが低い優先度のタスクをプリエンプトする、Annex Dが定める標準的なタスクディスパッチポリシー。

GNAT

GCCに含まれる無償のAdaコンパイラで、Adaの代表的な処理系。

有限バッファー

容量に上限を設けたキュー・循環バッファー。満杯になったら生産側を待たせることが自然な背圧になる。

機械可読データ

• JSON-LD / Turtle ── この記事の知識グラフ全体
• 概念一覧 / 語彙(述語)の定義

このデータセットについて

作成

合同会社小村ソフト

ライセンス

CC BY 4.0 ── 出典(合同会社小村ソフト)とライセンスへのリンクを明示し、改変した場合はその旨を示すことを条件に、再配布・改変を含めて再利用できます

最終確認日

2026-11-10 ── 収録する関係のうち、最後に出典と照合した日

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