Ada と Rust の安全性の考え方の違い ── 型・オーバーフロー・所有権・データ競合・形式検証を実際に動かして比べる

Ada と Rust はどちらも「安全な言語」として紹介されることが多い言語です。ただし、何を誤りとみなし、それをどこで止めるかは同じではありません。Rust はメモリの誤用とデータ競合を、所有権と型の規則によってコンパイル時に止めることに重点を置いています。Ada は値の範囲を型に書かせ、範囲外の値を既定で実行時に止める作りです。さらに Ada のサブセットである SPARK を使えば、実行時エラーが起きないことを実行の前に証明できます。

この記事では次の6つの観点で両者を比べます。

• 値の範囲を型でどう表すか
• 整数オーバーフローをどう扱うか
• メモリの誤用をどう止めるか
• データ競合をどう止めるか
• 検査を外す仕組みをどう区切っているか
• 形式検証をどう行うか

それぞれの観点で小さなプログラムを Ada と Rust の両方で書き、実際にコンパイル・実行・証明した結果を載せます。どちらが優れているかを決める記事ではありません。読み終えたときに、自分の要件にとってどちらの守り方が合うかを判断できるようにすることが目的です。

Ada の全体像は「Ada言語の魅力」、SPARK の基本は「SPARKによる形式検証入門」で扱っています。

比べる観点と試した環境

先に、誤りを止める場所の違いを図にまとめます。Rust は型と所有権の検査をコンパイラの中で行い、Ada はコンパイラの検査に加えて実行時の検査を言語の規則として持ちます。SPARK の証明は、コンパイルとは別の段階で GNATprove が行うものです。

flowchart TB
        accTitle: Ada と Rust が誤りを止める場所
        accDescr: Rust はコンパイル時に型と所有権を検査し、Ada はコンパイル時の型検査と実行時の範囲検査を持ち、SPARK は GNATprove による証明で実行前に誤りを止めることを示す。
        SRC["ソースコード"] --> C["コンパイル時の検査"]
        C -->|"Rust"| R1["型・所有権・借用・Send/Sync"]
        C -->|"Ada"| A1["型・アクセシビリティ規則"]
        SRC --> P["GNATprove による証明"]
        P --> S1["SPARK: 実行時エラーと競合の不在"]
        R1 --> RUN["実行時の検査"]
        A1 --> RUN
        RUN -->|"Rust"| R2["パニック"]
        RUN -->|"Ada"| A2["Constraint_Error など"]

図1: Rust はコンパイル時の検査に重点があり、Ada は実行時の検査を規則として持ち、SPARK は実行前の証明を加える。

試した環境は次のとおりです。いずれも Ubuntu Linux（x86_64）上で実行しました。

図の実線は常に成り立つ関係、破線は条件付きの関係です(成立条件は詳細ページの各関係の説明に記載)。関係すべての一覧(全37件、根拠・確度つき)と主要概念の定義は知識マップ詳細ページにまとめています。データ: JSON-LD / Turtle

値の範囲を型で表す: Ada の範囲付き型と Rust の newtype

Ada: 派生型と範囲付きの subtype

Ada では、構造が同じでも別の名前で宣言した型は別の型です。次のプログラムでは、Meters と Feet はどちらも Float から作った型ですが、Feet の値を Meters の引数に渡すとコンパイルエラーになります。

with Ada.Text_IO; use Ada.Text_IO;

procedure Units is
   type Meters is new Float;
   type Feet   is new Float;

   procedure Climb (Height : Meters) is
   begin
      Put_Line ("climb" & Meters'Image (Height));
   end Climb;

   H : constant Feet := 10.0;
begin
   Climb (H);
end Units;

units.adb:14:11: error: expected type "Meters" defined at line 4
units.adb:14:11: error: found type "Feet" defined at line 5

flowchart TB
        accTitle: Ada の派生型と subtype の違い
        accDescr: Float から作った派生型 Meters と Feet は互いに別の型で混ぜるとコンパイルエラーになり、Integer の subtype Percent は Integer と同じ型のまま代入時に範囲を検査されることを示す。
        F["Float"] -->|"type … is new"| M["Meters"]
        F -->|"type … is new"| FT["Feet"]
        M -.->|"混ぜて渡す"| E1["コンパイルエラー"]
        FT -.-> E1
        I["Integer"] -->|"subtype … range"| P["Percent（0〜100）"]
        P --> C1["変換なしで代入できる"]
        C1 --> C2["代入時に範囲を検査"]

図2: 派生型は別の型になり、subtype は元の型のまま範囲の検査だけが加わる。

値の範囲は subtype で型に書けます。次の Percent は Integer の部分型で、0〜100 だけを許します。Integer と同じ型なので変換なしで代入でき、代入のときに範囲だけが検査されるという作りです。このプログラムは後の節でも使うので、mod 型とオーバーフローの行も入れてあります。

with Ada.Command_Line; use Ada.Command_Line;
with Ada.Text_IO;      use Ada.Text_IO;

procedure Checks_Demo is
   type Byte is mod 256;                      --  折り返すと宣言した型
   subtype Percent is Integer range 0 .. 100; --  0〜100 だけを許す型

   N : constant Integer := Integer'Value (Argument (1));
   B : Byte := Byte (N mod 256);
   P : Percent;
begin
   B := B + 1;
   Put_Line ("Byte:    " & Byte'Image (B));
   Put_Line ("N + 1:   " & Integer'Image (N + 1));
   P := N;
   Put_Line ("Percent: " & Percent'Image (P));
end Checks_Demo;

gnatmake checks_demo.adb でビルドし、引数を変えて実行しました。

$ ./checks_demo 50
Byte:     51
N + 1:    51
Percent:  50
$ ./checks_demo 255
Byte:     0
N + 1:    256

raised CONSTRAINT_ERROR : checks_demo.adb:15 range check failed

255 を Percent に代入した15行目で、Constraint_Error が発生して止まりました。範囲は型の宣言に1回書くだけで、その型の変数への代入のたびに検査されます。

Rust: newtype と生成関数

Rust では既存の型を1要素の構造体で包む newtype パターンで、単位の取り違えを型で防ぎます。The Rust Programming Language（以下、Rust Book）は、Millimeters を引数に取る関数に Meters や素の u32 を渡すプログラムはコンパイルできない、と説明しています¹。

struct Meters(f64);
struct Feet(f64);

fn climb(height: Meters) {
    println!("climb {}", height.0);
}

fn main() {
    let h = Feet(10.0);
    climb(h);
}

error[E0308]: mismatched types
  --> units.rs:10:11
   |
10 |     climb(h);
   |     ----- ^ expected `Meters`, found `Feet`

一方、Rust の型には Ada の range のような値の範囲を書く構文がありません。範囲を守らせるには、構造体のフィールドを外から作れないようにしたうえで、検査する生成関数を用意します。

use std::env;

#[derive(Debug, Clone, Copy)]
struct Percent(u8);

impl Percent {
    fn new(value: i32) -> Option<Percent> {
        if (0..=100).contains(&value) {
            Some(Percent(value as u8))
        } else {
            None
        }
    }
}

fn main() {
    let n: i32 = env::args().nth(1).unwrap().parse().unwrap();
    println!("{:?}", Percent::new(n));
}

$ ./percent 42
Some(Percent(42))
$ ./percent 120
None

範囲外のときに例外で止めるのではなく、Option を返して呼び出し側に処理させています。この例は1つのファイルに収めたので main から Percent(…) を直接作れますが、型をモジュールに分けてフィールドを非公開にすれば、外からは Percent::new を通るしかなくなります。なお、Rust の型エイリアス（type Kilometers = i32;）は別の型にならず、混ぜて使ってもコンパイラは誤りにしません¹。Ada の subtype も元の型と混ぜて使えますが、範囲の検査は付いて回ります。

flowchart TB
        accTitle: 範囲の外の値を止める位置
        accDescr: Ada は subtype への代入のたびに範囲を検査して Constraint_Error を出し、Rust は生成関数で範囲を確かめて範囲外なら None を返すことを示す。
        V["範囲の外の値"] --> A["Ada: subtype に代入"]
        V --> R["Rust: 生成関数に渡す"]
        A --> A2["代入ごとに範囲検査"]
        A2 --> A3["Constraint_Error"]
        R --> R2["生成関数の中で確認"]
        R2 --> R3["None を返す"]

図3: Ada は型の宣言に書いた範囲を代入ごとに検査し、Rust は生成関数で確かめて結果を値で返す。

整数オーバーフロー: 例外か、パニックか、折り返しか

Ada: 符号付き整数は Constraint_Error、mod 型は折り返し

Ada の言語仕様では、整数型の定義済みの演算は数学的に正しい結果を返すか、Constraint_Error を発生させます²。符号付き整数型の演算の結果が型の範囲を超えると Constraint_Error になり、mod で宣言したモジュラー型は剰余で折り返します³。GNAT は既定でオーバーフローの検査を有効にしています⁴。

先ほどの checks_demo に Integer'Last（2147483647）を渡すと、14行目の N + 1 で止まりました。同じ実行で、mod 256 の Byte は 255 + 1 が 0 に折り返しています。

$ ./checks_demo 2147483647
Byte:     0

raised CONSTRAINT_ERROR : checks_demo.adb:14 overflow check failed

折り返してよい値は型の宣言の時点で mod 型として区別します。同じ + でも、型によって折り返すか止まるかが決まります。

Rust: ビルドの設定で結果が変わる

Rust の言語仕様はオーバーフローを誤りとし、意図した折り返しとは区別しています。debug_assert! が有効なビルド（最適化しないビルドなど）では、オーバーフローでパニックする検査を入れなければなりません。それ以外のビルドについては、パニックするか黙って折り返すかを実装に任せています。折り返す場合も、結果は2の補数の規則で決まります⁵。Cargo の既定値は、dev プロファイルが overflow-checks = true、release プロファイルが overflow-checks = false です⁶。

次のプログラムで確かめました。checked_add・wrapping_add・saturating_add は、オーバーフローしたときの扱いを呼び出し側で選ぶメソッドです。

use std::env;

fn main() {
    // 実行時の引数から値を読むので、コンパイル時には定数にならない
    let x: u8 = env::args().nth(1).unwrap().parse().unwrap();
    println!("checked_add:    {:?}", x.checked_add(1));
    println!("wrapping_add:   {}", x.wrapping_add(1));
    println!("saturating_add: {}", x.saturating_add(1));
    let y = x + 1;
    println!("x + 1 = {}", y);
}

cargo run（dev プロファイル）では x + 1 の行でパニックしました。終了コードは 101 です。

$ cargo run -q -- 255
checked_add:    None
wrapping_add:   0
saturating_add: 255

thread 'main' (10929) panicked at src/main.rs:9:13:
attempt to add with overflow
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

cargo run --release では、同じ式が 0 に折り返して処理が続きました。終了コードは 0 です。

$ cargo run -q --release -- 255
checked_add:    None
wrapping_add:   0
saturating_add: 255
x + 1 = 0

Cargo.toml に次の設定を足すと、release プロファイルでも dev と同じパニックになりました。rustc を直接使う場合は、rustc -O -C overflow-checks=on で同じ結果になります。

[profile.release]
overflow-checks = true

flowchart TB
        accTitle: 整数オーバーフローの扱いの分かれ方
        accDescr: Ada では符号付き整数型は Constraint_Error になり mod 型は折り返す。Rust では overflow-checks が有効ならパニックし、無効なら手元の rustc では折り返した。
        O["整数オーバーフロー"] --> A["Ada: 型で決まる"]
        O --> R["Rust: ビルド設定で決まる"]
        A -->|"符号付き整数型"| A1["Constraint_Error"]
        A -->|"mod 型"| A2["剰余で折り返す"]
        R -->|"overflow-checks 有効"| R1["パニック"]
        R -->|"overflow-checks 無効"| R2["2の補数で折り返す"]

図4: Ada では型の宣言が、Rust ではビルドの設定が、オーバーフローしたときの結果を決める。

検査を外したときの違い

どちらも検査を外せます。外した結果の扱いは違います。

Ada では pragma Suppress や GNAT の -gnatp（すべての検査を抑止する）で検査を外せます⁴。言語仕様は、検査を抑止した状態でその誤りが起きたときの実行を「誤った実行（erroneous）」としています⁷。gnatmake -gnatp checks_demo.adb でビルドし直すと、次の結果になりました。

$ ./checks_demo 2147483647
Byte:     0
N + 1:   -2147483648
Percent:  2147483647

N + 1 が負の値になり、0〜100 しか許さないはずの Percent に 2147483647 が入っています。この値は手元で観測したものにすぎず、誤った実行では言語仕様が結果を決めていません。

Rust の release ビルドの折り返しは、上で見たとおり2の補数の規則で結果が決まります。言語仕様はこれを誤りとしつつ、「unsafe とみなさない動作」の1つに分類しています⁵。Ada は検査を残すのが既定で、外すと結果は保証されません。Rust はリリースビルドでは検査を外すのが既定で、外しても結果は決まっています。既定の置き方も、外したときの意味も、両者で逆になっています。

flowchart TB
        accTitle: 検査を外したときの結果の扱い
        accDescr: Ada で -gnatp などにより検査を抑止して誤りが起きると実行は誤った実行になり結果は決まらない。Rust で overflow-checks を無効にすると2の補数で折り返した値に決まることを示す。
        A["Ada: -gnatp で検査を抑止"] --> A1["オーバーフローや範囲外"]
        A1 --> A2["誤った実行"]
        A2 --> A3["結果を仕様が決めない"]
        R["Rust: overflow-checks 無効"] --> R1["オーバーフロー"]
        R1 --> R2["2の補数で折り返す"]
        R2 --> R3["結果は決まる"]

図5: 検査を外したとき、Ada では結果が決まらず、Rust では折り返した値に決まる。

メモリの安全性: 所有権とアクセス型

Rust: 所有権と借用チェッカー

Rust Book は所有権の規則を3つにまとめています。値には所有者がいて、所有者は同時に1つだけで、所有者がスコープを出ると値は破棄されます。この規則はコンパイラが検査し、違反するとコンパイルできません⁸。借用の規則では、可変の参照を1つだけか不変の参照をいくつでも、のどちらかしか同時に持てず、参照は常に有効でなければなりません⁹。スコープを比べて借用が有効かを判断するのが借用チェッカーです¹⁰。

所有権を移した後の変数を使うと、コンパイルエラーになります。

fn main() {
    let a = String::from("hello");
    let b = a;
    println!("{} {}", a, b);
}

error[E0382]: borrow of moved value: `a`
 --> moved.rs:4:23
  |
2 |     let a = String::from("hello");
  |         - move occurs because `a` has type `String`, which does not implement the `Copy` trait
3 |     let b = a;
  |             - value moved here
4 |     println!("{} {}", a, b);
  |                       ^ value borrowed here after move

flowchart TB
        accTitle: Rust の所有権の移動
        accDescr: let b = a で String の所有権が a から b に移り、それ以降に a を使うとコンパイルエラーになり、b がスコープを出るときに値が破棄されることを示す。
        A["a が String を所有"] -->|"let b = a"| B["b が所有者になる"]
        B --> U["a を使う"]
        U --> E["E0382: 移動後の使用"]
        B --> D["b がスコープを出る"]
        D --> DR["値が破棄される"]

図6: 代入で所有権が移り、移動元を使うとコンパイルエラーになる。

スコープを出た変数への参照を残す書き方も、借用チェッカーが止めます。

fn main() {
    let r;
    {
        let s = String::from("hello");
        r = &s;
    }
    println!("{}", r);
}

error[E0597]: `s` does not live long enough
 --> dangling.rs:5:13
  |
4 |         let s = String::from("hello");
  |             - binding `s` declared here
5 |         r = &s;
  |             ^^ borrowed value does not live long enough
6 |     }
  |     - `s` dropped here while still borrowed
7 |     println!("{}", r);
  |                    - borrow later used here

Ada: アクセス型とアクセシビリティ規則

Ada のポインタはアクセス型と呼ばれます。言語仕様は、アクセシビリティ規則がダングリング参照を防ぐと定めています¹¹。上の Rust の2つ目の例と同じ形を Ada で書くと、コンパイルエラーになりました。

with Ada.Text_IO; use Ada.Text_IO;

procedure Dangling is
   type Int_Ptr is access all Integer;
   P : Int_Ptr;
begin
   declare
      X : aliased Integer := 1;
   begin
      P := X'Access;
   end;
   Put_Line (Integer'Image (P.all));
end Dangling;

dangling.adb:10:12: error: non-local pointer cannot point to local object

ただし、アクセシビリティ規則が見ているのは、ポインタの型と指す先の寿命の関係です。new で確保した領域を Ada.Unchecked_Deallocation で解放したあとの使用は止めません。

with Ada.Text_IO; use Ada.Text_IO;
with Ada.Unchecked_Deallocation;

procedure Use_After_Free is
   type Int_Ptr is access Integer;
   procedure Free is new Ada.Unchecked_Deallocation (Integer, Int_Ptr);

   X : Int_Ptr := new Integer'(1);
   Y : constant Int_Ptr := X;   --  同じ領域を指す2つ目のポインタ
begin
   Free (X);                    --  X は null になるが Y はそのまま
   Put_Line (Boolean'Image (X = null));
   Put_Line (Integer'Image (Y.all));   --  解放済みの領域を読む
end Use_After_Free;

gnatmake -gnatwa（警告をほぼすべて有効にする）でもエラーも警告も出ずにビルドでき、実行すると次の結果になりました。2行目は実行のたびに違う値でした。

TRUE
 1610868145

言語仕様では、Free(X) のあとで X は null になります。一方、解放済みの領域を指すポインタ（ダングリング参照）を参照外しした実行は誤った実行です¹²。Free は渡した X だけを null にし、同じ領域を指す Y には触れません。

flowchart TB
        accTitle: Free の前後でのポインタの状態
        accDescr: X と Y が同じ領域を指している状態で Free(X) を呼ぶと、X は null になり領域は解放されるが、Y は解放済みの領域を指したまま残ることを示す。
        S["X と Y が同じ領域を指す"] --> F["Free(X) を呼ぶ"]
        F --> XN["X は null になる"]
        F --> HF["領域は解放される"]
        HF --> YD["Y は解放済みを指したまま"]

図7: Free は渡したポインタだけを null にし、同じ領域を指す別のポインタは残る。

flowchart TB
        accTitle: ポインタの誤用を止める位置
        accDescr: Rust は所有権の移動後の使用とスコープ外への参照をコンパイル時に止める。Ada はローカル変数を指すポインタの持ち出しをコンパイル時に止めるが、解放後の使用は止めず、SPARK の所有権ポリシーが証明の段階で止める。
        E["ポインタの誤用"] --> R["Rust のコンパイラ"]
        E --> A["Ada のコンパイラ"]
        R --> R1["移動後の使用を拒否"]
        R --> R2["寿命切れの参照を拒否"]
        A --> A1["ローカル変数の持ち出しを拒否"]
        A --> A2["解放後の使用は通る"]
        A2 -.-> S["SPARK の所有権ポリシー"]

図8: Rust は所有権と借用の規則で、Ada はアクセシビリティ規則で止め、Ada が止めない解放後の使用は SPARK が扱う。

SPARK: Rust にならった所有権ポリシー

SPARK のユーザーガイドは「Rust と同じように、SPARK はメモリの所有権ポリシーを強制する」と書いています。アクセス型の変数を代入すると所有権が左辺に移り、右辺はその領域にアクセスする権利を失います。読み取りだけを共有する観察（observe）と、一時的に所有権を渡す借用（borrow）もあります¹³。

次のコードは所有権を Y に移したあとで X を通して書き込んでいます。

with Ada.Unchecked_Deallocation;

procedure Move_Demo with SPARK_Mode is
   type Int_Ptr is access Integer;
   procedure Free is new Ada.Unchecked_Deallocation (Integer, Int_Ptr);

   X : Int_Ptr := new Integer'(1);
   Y : Int_Ptr;
begin
   Y := X;        --  所有権が X から Y に移る
   X.all := 2;    --  移った後の X を通して書き込む
   Free (Y);
end Move_Demo;

GNAT はこのコードをそのままコンパイルし、実行しても何も起きずに終了しました。GNATprove にかけると、10行目で移動した X を11行目で使っていると報告されます。

move_demo.adb:11:06: error: dereference from "X" is not writable
   11 |   X.all := 2;    --  移った後の X を通して書き込む
      |   ~~^~~
  object was moved at line 10 [E0010]
   10 |   Y := X;        --  所有権が X から Y に移る
      |        ^ here

SPARK はメモリリークも検査します。ユーザーガイドによると、GNATprove は代入のたびに左辺がメモリを漏らしていないか、宣言のたびにその寿命の終わりでメモリを漏らしていないかを確かめます¹³。11行目を Y.all := 2; に直し、Free (Y); を消すと、次の報告が出ました。

move_demo.adb:8:04: medium: resource or memory leak might occur at end of scope

Free (Y); を戻すと、リークがないこととポインタの参照外しの検査がすべて証明されました。

move_demo.adb:7:04: info: absence of resource or memory leak at end of scope proved
move_demo.adb:8:04: info: initialization of "Y" proved
move_demo.adb:8:04: info: absence of resource or memory leak at end of scope proved
move_demo.adb:10:06: info: absence of resource or memory leak proved
move_demo.adb:11:06: info: pointer dereference check proved

ここで Rust との違いが1つあります。Rust の言語仕様はメモリやその他の資源のリークを「unsafe とみなさない動作」に挙げています⁵。つまり Rust の安全なコードはリークがないことまでは約束しません。SPARK はリークを証明の対象にしています。

flowchart TB
        accTitle: SPARK の所有権ポリシーで GNATprove が見るもの
        accDescr: アクセス型の代入で所有権が移り、GNATprove は移動後の使用をエラーにし、寿命の終わりや代入でのメモリリークを検査することを示す。
        AS["アクセス型の代入 Y := X"] --> MV["所有権が Y へ移る"]
        MV --> U["X を使う"]
        U --> E1["エラー: 移動後の使用"]
        MV --> L["Y の寿命が終わる"]
        L -->|"Free しない"| E2["リークの可能性を報告"]
        L -->|"Free する"| OK["リークなしを証明"]

図9: GNATprove は移動後の使用をエラーにし、寿命の終わりで解放されているかも確かめる。

データ競合: Send/Sync と保護オブジェクト

Rust: 借用規則と Send/Sync がコンパイル時に止める

Rust Book は参照の規則によってデータ競合をコンパイル時に防げると説明しています⁹。4つのスレッドが同じ変数を足し続ける次のコードは、可変の借用が重なるのでコンパイルできません。

use std::thread;

fn main() {
    let mut count = 0;
    thread::scope(|s| {
        for _ in 0..4 {
            s.spawn(|| {
                for _ in 0..100_000 {
                    count += 1;
                }
            });
        }
    });
    println!("count = {}", count);
}

error[E0499]: cannot borrow `count` as mutable more than once at a time
 --> race.rs:7:21

スレッドをまたげる型かどうかは、Send と Sync という2つのマーカートレイトで表します。Send はその型の値の所有権をスレッド間で移せること、Sync はその型を複数のスレッドから参照しても安全なことを示します。参照カウントを同期せずに更新する Rc<T> は Send を実装していません¹⁴。

use std::rc::Rc;
use std::thread;

fn main() {
    let shared = Rc::new(5);
    let handle = thread::spawn(move || {
        println!("{}", shared);
    });
    handle.join().unwrap();
}

error[E0277]: `Rc<i32>` cannot be sent between threads safely
 --> rc_send.rs:6:32
  = help: within `{closure@rc_send.rs:6:32: 6:39}`, the trait `Send` is not implemented for `Rc<i32>`

flowchart TB
        accTitle: スレッドに値を渡せるかの判定
        accDescr: thread::spawn に渡すクロージャが持つ値の型が Send を実装していればコンパイルが通り、Rc のように Send を実装していなければ E0277 でコンパイルエラーになることを示す。
        S["thread::spawn に値を渡す"] --> Q["値の型は Send か"]
        Q -->|"実装している"| OK["コンパイルが通る"]
        Q -->|"実装していない"| NG["E0277 で拒否"]
        NG -.-> EX["例: Rc の参照カウント"]

図10: スレッドに渡す値は、型が Send を実装しているかでコンパイル時に判定される。

足す処理を Mutex で包むとコンパイルが通り、結果は 400000 になりました。

use std::sync::Mutex;
use std::thread;

fn main() {
    let count = Mutex::new(0);
    thread::scope(|s| {
        for _ in 0..4 {
            s.spawn(|| {
                for _ in 0..100_000 {
                    *count.lock().unwrap() += 1;
                }
            });
        }
    });
    println!("count = {}", count.into_inner().unwrap());
}

count = 400000

Ada: 保護オブジェクトは用意されているが、使わない書き方も通る

Ada の保護オブジェクトは公開した操作を通じてだけ共有データにアクセスさせ、アクセスを調整します¹⁵。ただし、保護オブジェクトを使わずに共有変数を書き換えるコードもコンパイルできます。言語仕様は、同期されていない2つの動作が同じ共有変数を衝突する形で使う実行を、誤った実行としています¹⁶。

次のプログラムは、4つのタスクが保護されていない Count と保護オブジェクトの Counter の両方を100,000回ずつ増やします。

with Ada.Text_IO; use Ada.Text_IO;

procedure Race is
   Count : Integer := 0;

   protected Counter is
      procedure Increment;
      function Value return Integer;
   private
      N : Integer := 0;
   end Counter;

   protected body Counter is
      procedure Increment is
      begin
         N := N + 1;
      end Increment;

      function Value return Integer is (N);
   end Counter;

   task type Worker;
   task body Worker is
   begin
      for I in 1 .. 100_000 loop
         Count := Count + 1;    --  保護されていない共有変数
         Counter.Increment;     --  保護オブジェクト経由
      end loop;
   end Worker;
begin
   declare
      Workers : array (1 .. 4) of Worker;
   begin
      null;  --  ここで4つのタスクの終了を待つ
   end;
   Put_Line ("Count   =" & Integer'Image (Count));
   Put_Line ("Counter =" & Integer'Image (Counter.Value));
end Race;

GNAT は既定の警告設定で何も警告せずにビルドしました。4コアの環境で3回実行すると、保護オブジェクトの値は毎回 400000 で、保護されていない変数は毎回違う値でした。

Count   = 345849
Counter = 400000
Count   = 348876
Counter = 400000
Count   = 387245
Counter = 400000

保護オブジェクトそのものの使い方は「Adaにおける安全な並行処理」で詳しく扱っています。

SPARK: GNATprove がデータ競合を報告する

SPARK で並行処理を書くには Ravenscar プロファイルが必要で、GNATprove は Jorvik プロファイルにも対応しています。プログラム全体のエラボレーション（elaboration）が終わる前にタスクを動かさないよう、pragma Partition_Elaboration_Policy (Sequential); も求められます。タスクどうしが共有できるのは、保護オブジェクトや atomic オブジェクトのような同期されたオブジェクトだけです¹⁷。構成プラグマのファイルに pragma Profile (Jorvik); とこのプラグマを書き、2つのタスクから保護されていない変数を書き換えるパッケージを GNATprove にかけると、次の報告が出ました。

package Shared with SPARK_Mode is
   Count : Integer := 0;

   task type Worker;
   W1, W2 : Worker;
end Shared;

package body Shared with SPARK_Mode is
   task body Worker is
   begin
      loop
         if Count < Integer'Last then
            Count := Count + 1;
         end if;
      end loop;
   end Worker;
end Shared;

shared.ads:5:04: high: possible data race when accessing variable "shared.count"
    5 |   W1, W2 : Worker;
      |   ^~
  task "shared.w1" accesses "shared.count"
  task "shared.w2" accesses "shared.count"

Count を保護オブジェクトの中に移すと、この報告は消え、オーバーフローの検査とタスクが止まらないことが証明されました。

flowchart TB
        accTitle: 共有変数への同期のないアクセスを止める位置
        accDescr: Rust は借用規則と Send/Sync でコンパイル時に止める。Ada はコンパイルを通し実行は誤った実行になる。SPARK では GNATprove がデータ競合の可能性を報告する。
        W["同期のない共有変数の更新"] --> R["Rust"]
        W --> A["Ada"]
        W --> S["SPARK"]
        R --> R1["コンパイルエラー"]
        A --> A1["コンパイルは通る"]
        A1 --> A2["誤った実行"]
        S --> S1["GNATprove が競合を報告"]

図11: 同期のない共有変数の更新を、Rust はコンパイル時に、SPARK は証明の段階で止め、Ada 本体は止めない。

データ競合がないことは、処理の順序に関する誤りがないことまでは意味しません。SPARK のユーザーガイドも、データ競合のないプログラムに競合状態（race condition）が残る例を挙げています¹⁷。Rust の言語仕様もデッドロックを「unsafe とみなさない動作」に挙げています⁵。

検査を外す出入口: unsafe と Unchecked_

どちらの言語にも、言語の検査を外す仕組みがあります。違うのは、その範囲の区切り方です。

Rust の unsafe で使えるようになるのは5つの操作だけです。生ポインタの参照外し、unsafe な関数やメソッドの呼び出し、可変の static 変数へのアクセスと変更、unsafe なトレイトの実装、union のフィールドへのアクセスです。unsafe ブロックの中でも借用チェッカーやその他の検査は止まりません¹⁸。生ポインタを unsafe の外で参照外しすると、コンパイルエラーになります。

fn main() {
    let x = 5;
    let p = &x as *const i32;
    println!("{}", *p);
}

error[E0133]: dereference of raw pointer is unsafe and requires unsafe function or block
 --> rawptr.rs:4:20
  |
4 |     println!("{}", *p);
  |                    ^^ dereference of raw pointer
  |
  = note: raw pointers may be null, dangling or unaligned; they can violate aliasing rules and cause data races: all of these are undefined behavior

コンパイラの注記にあるとおり、生ポインタは null やダングリング参照になりえます。unsafe の中で参照外しするなら、その正しさは書いた人が保証します。

クレートの先頭に #![forbid(unsafe_code)] を書くと、unsafe ブロックを書いた時点でエラーになりました。

error: usage of an `unsafe` block
 --> forbid.rs:6:5

Ada で検査を外す仕組みは、名前に Unchecked が付く Ada.Unchecked_Deallocation・Ada.Unchecked_Conversion・'Unchecked_Access 属性と、検査を抑止する pragma Suppress です。言語仕様は、Unchecked_Access がアクセシビリティ規則を回避するために使えると書いています¹¹。使ってよい単位を絞るには、言語定義の制限 No_Dependence を使えます¹⁹。次のように書くと、Ada.Unchecked_Deallocation を使う行でコンパイルエラーになりました。

pragma Restrictions (No_Dependence => Ada.Unchecked_Deallocation);

with Ada.Unchecked_Deallocation;

procedure Restricted is
   type Int_Ptr is access Integer;
   procedure Free is new Ada.Unchecked_Deallocation (Integer, Int_Ptr);
   X : Int_Ptr := new Integer'(1);
begin
   Free (X);
end Restricted;

restricted.adb:3:06: error: violation of restriction "No_Dependence => Ada.Unchecked_Deallocation" at line 1

SPARK では、SPARK_Mode => Off を指定した部分が GNATprove の解析から外れます。前の節の Move_Demo を with SPARK_Mode => Off に変えて GNATprove にかけると、移動後の使用は報告されず、解析する本体がないという警告だけが出ました。

warning: no checks generated by GNATprove
possible reason: no bodies have been selected for analysis with SPARK_Mode

flowchart TB
        accTitle: 検査を外す仕組みの区切り方
        accDescr: Rust は unsafe ブロックで5つの操作だけを許し、forbid(unsafe_code) で禁止できる。Ada は Unchecked_ の付く単位と pragma Suppress で検査を外し、Restrictions の No_Dependence で禁止できる。
        U["言語の検査を外す"] --> R["Rust: unsafe ブロック"]
        U --> A["Ada: Unchecked_ と Suppress"]
        R --> R1["5つの操作だけ許可"]
        R --> R2["forbid(unsafe_code) で禁止"]
        A --> A1["名前で使用箇所が分かる"]
        A --> A2["No_Dependence で禁止"]

図12: どちらも検査を外す箇所を名前で探せ、プロジェクト単位で禁止する指定もある。

どちらの言語でも、検査を外す箇所は unsafe や Unchecked という名前で検索できます。レビューではこの箇所を優先して読みます。

形式検証: 言語のサブセットとしての SPARK と、Rust の検証ツール

SPARK は Ada のサブセットで、契約（事前条件・事後条件など）を Ada の構文で書き、GNATprove が証明します。この記事の SPARK の例も Ada のコードに SPARK_Mode を付けたものです。証明の段階の考え方は「SPARKによる形式検証入門」で説明しています。

Rust には言語に組み込まれた形式検証はありませんが、外部のツールがあります。各ツールの公式資料に書かれていることを並べます。この記事の環境ではどのツールも動かしていません。

flowchart TB
        accTitle: 形式検証の道具の位置づけ
        accDescr: SPARK は Ada のサブセットで GNATprove が証明する。Rust では Kani、Verus、Creusot、Prusti などの外部ツールがそれぞれの方式で検証する。
        FV["形式検証"] --> SP["SPARK: Ada のサブセット"]
        FV --> RT["Rust: 外部のツール"]
        SP --> GP["GNATprove"]
        RT --> K["Kani: モデル検査"]
        RT --> V["Verus: Z3 で証明"]
        RT --> C["Creusot: Why3 へ変換"]
        RT --> P["Prusti: Viper 基盤"]

図13: SPARK は言語のサブセットと証明ツールが一体で、Rust では外部のツールがそれぞれの方式で検証する。

どちらの守り方が要件に合うか

ここまでの結果を表にまとめます。

要件と照らすときは、次の点を見ます。

• 値の範囲や単位の誤りが主な心配なら、Ada の範囲付き型は宣言1行で全代入に検査が付きます。SPARK まで使えば、その違反が起きないことを実行前に示せます。
• メモリの誤用とデータ競合をコンパイラだけで止めたいなら、Rust の所有権と Send/Sync は追加の道具なしでそれを行います。Ada 本体では、解放後の使用と同期のない共有はコンパイラが止めないので、SPARK を使うか、No_Dependence などで使える機能を絞ります。
• リリースビルドのオーバーフローの扱いは既定が逆です。Rust で検査を残したいなら overflow-checks = true を明示し、Ada で -gnatp を使うなら、外した検査の誤りが起きないことを別の方法で示す必要があります。
• 証明まで求める場合、SPARK は言語のサブセットと証明ツールがそろっています。Rust では、対象のコードがツールの対応範囲に入るかを先に確かめます。

flowchart TB
        accTitle: 主な心配ごとと合う守り方
        accDescr: 値の範囲や単位の誤りが主な心配なら Ada の範囲付き型、メモリの誤用とデータ競合をコンパイラで止めたいなら Rust、実行前の証明まで求めるなら SPARK が合うことを示す。
        Q["主な心配ごと"] --> V["値の範囲・単位の誤り"]
        Q --> M["メモリ誤用・データ競合"]
        Q --> P["実行前の証明が要る"]
        V --> V1["Ada の範囲付き型"]
        M --> M1["Rust の所有権と Send/Sync"]
        P --> P1["SPARK と GNATprove"]

図14: 主に何を防ぎたいかによって、合う守り方が変わる。

どちらの言語も守り方の違いを知ったうえで不足を補う道具を持っています。AI が書いたコードを SPARK で証明する具体的な手順は「AIが書いたコードを SPARK で証明する」、Ada のポインタと解放の扱いは「Ada のメモリ管理」で扱います。

関連記事

• Ada言語の魅力
• SPARKによる形式検証入門
• Adaにおける安全な並行処理
• AIが書いたコードを SPARK で証明する
• Ada のメモリ管理
• Ada 2022 の新しい機能

参考リンク

関連する記事

同じタグを共有する最新の記事です。さらに近い話題で知識を深められます。

関連トピック

このテーマと近いトピックページです。記事を起点に、関連するサービスや他の記事へ進めます。

このテーマがつながるサービス

この記事は次のサービスページにつながります。近い入口からご覧ください。

よくある質問

この記事のテーマについて、相談時によくある質問をまとめています。

Ada と Rust はどちらが安全ですか？

一言では比べられません。Rust は所有権と借用の規則で、メモリの誤用とデータ競合をコンパイル時に止めます。Ada は値の範囲を型に書き、範囲外の値やオーバーフローを既定で実行時に止めます。Ada のサブセットである SPARK を使えば、実行時エラーが起きないことやデータ競合がないことを、実行する前に証明できます。守りたい性質に合わせて選びます。

Rust の整数オーバーフローはリリースビルドでどうなりますか？

Cargo の release プロファイルは overflow-checks が既定で false なので、手元の rustc 1.97.0 では 255u8 + 1 が 0 に折り返し、パニックしませんでした。Rust の言語仕様は、デバッグ用の検査が無効なビルドではパニックと折り返しのどちらにするかを実装に任せています。Cargo.toml で overflow-checks = true にすれば、リリースビルドでもパニックします。

Ada にも Rust の所有権のような仕組みはありますか？

Ada 本体にはアクセシビリティ規則があり、ローカル変数を指すポインタがその変数より長く生き残る書き方をコンパイル時に止めます。ただし Unchecked_Deallocation で解放したあとの使用は止めません。SPARK には Rust にならった所有権ポリシーがあり、GNATprove がポインタの移動後の使用やメモリリークを検出します。

Rust にも SPARK のような形式検証はありますか？

言語に組み込まれてはいませんが、外部のツールがあります。Kani はモデル検査、Verus は SMT ソルバによる定理証明、Creusot は Why3 を使う演繹的な検証、Prusti は Viper 基盤の検証を行います。対応する Rust の範囲はツールごとに違うので、使う前に各ツールの資料で確かめます。

著者プロフィール

記事の著者プロフィールページです。

小村 豪

合同会社小村ソフト 代表

Windows ソフト開発、技術相談、不具合調査を中心に、既存資産が残る案件や原因が見えにくい障害調査に強みがあります。