知識マップ: Adaのメモリ管理 ── アクセス型・Controlled型・ストレージプールの使い分け

記事「Adaのメモリ管理 ── アクセス型・Controlled型・ストレージプールの使い分け」の主張を、概念と関係(エッジ)に分解した知識グラフの全体です。各関係には根拠・確認日・確度が付いています。

Adaでnewを使うとき、値はアクセス型ごとのストレージプールから確保される。Unchecked_Deallocationで解放すると渡した変数はnullになるが、同じ領域を指すほかのアクセス値は残り、ダングリング参照になる。アクセシビリティ検査は寿命の短い変数を指す値の保存を止め、SPARKは所有権の規則で、確保した領域に読み書きできるアクセス値を同時に1つに限る。Controlled型はFinalizeに解放を書くことでC++のRAIIと同じ役割を担う。GNATは長さの決まらない戻り値をセカンダリスタックに置き、Ada.Containersは要素の確保と解放を引き受ける。ダングリング参照による読み取りとメモリリークは、Valgrindで確かめられる。

flowchart LR
    accTitle: Adaのメモリ管理の知識マップ
    accDescr: アクセス型がストレージプールから領域を確保し、Unchecked_Deallocationによる解放がダングリング参照の原因になりうること、アクセシビリティ検査とSPARKがそれを防ぎ、Controlled型がRAIIの役割を担うこと、ValgrindやGNATのセカンダリスタック、サブプール、Ada.Containersとの関係を示す図。
    ada_access_type["アクセス型"]
    ada_storage_pool["ストレージプール(Ada)"]
    ada_controlled_type["Controlled型(Ada)"]
    gnat["GNAT"]
    ada["Ada(プログラミング言語)"]
    gnat_secondary_stack["セカンダリスタック(GNAT)"]
    ada_unchecked_deallocation["Ada.Unchecked_Deallocation"]
    dangling_pointer["ダングリング参照"]
    ada_accessibility_rules["アクセシビリティ規則"]
    spark["SPARK"]
    gnatprove["GNATprove"]
    valgrind["Valgrind"]
    memory_leak["メモリリーク"]
    raii["RAII(Resource Acquisition Is Initialization)"]
    ada_storage_subpool["サブプール(Ada)"]
    ada_containers["Ada.Containers"]
    gnat -->|"実装を担う"| ada
    gnat -.->|"利用する"| gnat_secondary_stack
    ada_access_type -->|"利用する"| ada_storage_pool
    ada_unchecked_deallocation -->|"前提とする"| ada_access_type
    ada_unchecked_deallocation -->|"原因になり得る"| dangling_pointer
    ada_accessibility_rules -.->|"防止する"| dangling_pointer
    spark -.->|"防止する"| dangling_pointer
    spark -->|"利用する"| gnatprove
    dangling_pointer -.->|"で確認できる"| valgrind
    memory_leak -.->|"で確認できる"| valgrind
    ada_controlled_type -->|"実装を担う"| raii
    ada_controlled_type -.->|"利用する"| ada_unchecked_deallocation
    ada_controlled_type -.->|"軽減する"| memory_leak
    ada_storage_subpool -->|"前提とする"| ada_storage_pool
    ada_containers -.->|"軽減する"| memory_leak

概念間の関係(全15件)

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

GNATはAda(プログラミング言語)の実装を担います。GNATはAda言語のコンパイラとしての実装を担う処理系で、本記事の例はGNAT 13.3.0でコンパイルして実行した。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
GNATはセカンダリスタック(GNAT)を利用します。GNATは、長さの決まっていない値を返す関数の戻り値をセカンダリスタックに置き、呼び出し側のスコープを出ると戻す。pragma Restrictions (No_Secondary_Stack)を付けると、その使用はコンパイルエラーになる。 / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典出典
アクセス型はストレージプール(Ada)を利用します。アクセス型のnewは、そのアクセス型に結び付いたストレージプールから領域を確保する。指定しなければ処理系の既定のプール(GNATではmallocとfreeを使うSystem.Pool_Global)が使われ、Storage_PoolやStorage_Sizeで型ごとに差し替えたり上限を付けたりできる。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典出典
Ada.Unchecked_Deallocationはアクセス型を前提とします。Unchecked_Deallocationは、解放するオブジェクトの型とそれを指すアクセス型を渡してインスタンス化して使う。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
Ada.Unchecked_Deallocationはダングリング参照の原因になることがあります。Free(X)のあとXはnullになるが、同じオブジェクトを指していたほかのアクセス値は元のアドレスを持ったまま残る。それを参照した実行はerroneousで、GNAT 13.3では例外にならなかった。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
アクセシビリティ規則はダングリング参照を防ぎます。寿命の短い変数を指す値を寿命の長いアクセス型に保存することを、静的に分かればコンパイルエラーで、匿名アクセス型の引数のように実行時まで分からなければProgram_Errorで止める。Unchecked_Deallocationで解放した領域を指すアクセス値は、この検査では防げない。 / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典
SPARKはダングリング参照を防ぎます。SPARKはアクセス型に所有権の規則を課し、確保した領域に読み書きできるアクセス値を同時に1つに限る。本記事の例では、所有権がBに移ったAを解放しようとした行を、GNATproveが--mode=check_allの検査でエラーにした。 / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典
SPARKはGNATproveを利用します。SPARKのコードの検査と証明にはGNATproveを使う。本記事ではGNATprove 15.1で所有権の規則を検査した。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
ダングリング参照はValgrindで確認できます。本記事の例では、解放済みの領域をダングリング参照で読んでもGNATは例外を出さず、ValgrindのMemcheckがInvalid readとして報告した。 / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典
メモリリークはValgrindで確認できます。本記事の例では、前の値を指すアクセス値を失うループで確保した領域を、ValgrindのMemcheckがdefinitely lostとして報告した。 / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典
Controlled型(Ada)はRAII(Resource Acquisition Is Initialization)の実装を担います。Controlled型のFinalizeはスコープを出るときや例外で抜けるときにも呼ばれるため、解放をFinalizeに書くと、C++でデストラクタに解放を書くRAIIと同じく、呼び出し側が解放を書かずに済む。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
Controlled型(Ada)はAda.Unchecked_Deallocationを利用します。本記事のBuffer型は、Limited_ControlledのFinalizeの中でUnchecked_Deallocationのインスタンスを呼び、持っている配列を解放する。 / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典出典
Controlled型(Ada)はメモリリークを軽減します。解放をFinalizeに書くと、呼び出し側が解放を書き忘れることがなくなる。本記事の例では、数えるプールを使ったBuffer型でブロックを出ると確保と解放の回数がそろい、使用量が0に戻った。 / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典
サブプール(Ada)はストレージプール(Ada)を前提とします。サブプールは1つのストレージプールを複数に分けたもので、newで確保先のサブプールを指定でき、サブプールごとまとめて解放できる。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典出典
Ada.Containersはメモリリークを軽減します。Ada.Containersは要素の確保と解放をコンテナの側で行うので、利用者がnewや解放を書かずに済む。本記事のIndefinite_Vectorsの例では、Valgrindで終了時の使用量が0バイトだった。 / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典

主要概念の定義

アクセス型: オブジェクトやサブプログラムを指す値を持つAdaの型で、ほかの言語のポインタや参照に当たる。accessだけで宣言するプール固有のアクセス型はその型のnewで作った値だけを指し、access allなどで宣言する汎用のアクセス型はaliasedを付けた変数も指せる。
ストレージプール(Ada): アクセス型のnewが領域を確保する場所。アクセス型ごとにStorage_PoolやStorage_Sizeで指定でき、Root_Storage_Poolを継承してAllocate・Deallocate・Storage_Sizeを上書きすると独自のプールを作れる。
Controlled型(Ada): Ada.FinalizationのControlledまたはLimited_Controlledから派生し、Initialize・Adjust・Finalizeを上書きして、既定の初期化・代入・スコープを出るときの処理を定義できるAdaの型。
GNAT: GCCに含まれる無償のAdaコンパイラで、Adaの代表的な処理系。
Ada.Unchecked_Deallocation: newで確保したオブジェクトを明示的に解放するために、オブジェクトの型とアクセス型を渡してインスタンス化するAdaの標準のジェネリック手続き。解放に渡した変数はnullになるが、同じオブジェクトを指すほかのアクセス値は検査しない。
アクセシビリティ規則: アクセス型と指す先のオブジェクトの寿命(アクセシビリティレベル)を比べ、指す先より長く残るアクセス値を作らせないAdaの規則。静的に違反が分かればコンパイルエラーになり、実行時の検査(accessibility check)に失敗するとProgram_Errorが発生する。
SPARK: プログラムの性質を数学的に証明できるように設計された、Adaのサブセット(部分言語)とそのツール群。
ダングリング参照: すでに存在しないオブジェクトを指すポインタや参照。参照外しすると、意図しないデータを読み書きする。Adaの参照マニュアルは、これを参照した実行をerroneous(結果が規格で定まらない)としている。
メモリリーク: 確保したメモリを解放し忘れ、Private BytesやCommitが増え続ける現象。
サブプール(Ada): Ada 2012で追加された、1つのストレージプールを複数に分ける仕組み。newで確保先のサブプールを指定でき、Unchecked_Deallocate_Subpoolでサブプールごとまとめて解放できる。
Ada.Containers: Ada 2005で標準に加わった、ベクタ・リスト・マップ・集合などの要素の集まりを扱うAdaの標準パッケージ群。

機械可読データ

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

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

作成: 合同会社小村ソフト
ライセンス: CC BY 4.0 ── 出典(合同会社小村ソフト)とライセンスへのリンクを明示し、改変した場合はその旨を示すことを条件に、再配布・改変を含めて再利用できます
最終確認日: 2026-11-01 ── 収録する関係のうち、最後に出典と照合した日

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