第20章. 時間とメモリの予算

この章の目的

この章を読み終える頃には、すべてのKeleusmaプログラムが「収まる」ことを証明される2つの予算と、それに乗る約束を理解しているはずです。この章を読み終える頃には、すべてのKeleusmaプログラムが「収まる」ことを証明される2つの予算と、それに乗る約束を理解しているはずです。

ティックごとの2つの予算

第19章では検証器がプログラムを却下する姿を見ました。この章では検証器が何を守っているのかを説明します。検証器はすべてのプログラムを2つの予算に従わせ、プログラムが走り出す前にその両方を確認します。第19章では検証器がプログラムを却下する姿を見ました。この章では検証器が何を守っているのかを説明します。検証器はすべてのプログラムを2つの予算に従わせ、プログラムが走り出す前にその両方を確認します。

最初の予算は時間です。プログラムが走り出す前に、言語はプログラムが取りうるすべての経路を考えて、ある1ティックで起こりうる最大の仕事量を割り出し、その量が有限であることを証明します。これが「ワーストケース実行時間」、WCETです。最初の予算は時間です。プログラムが走り出す前に、言語はプログラムが取りうるすべての経路を考えて、ある1ティックで起こりうる最大の仕事量を割り出し、その量が有限であることを証明します。これが「ワーストケース実行時間」、WCETです。

音楽的に読むとそのままです。あるテンポでの一拍には収まる量しかありません。1拍の中に無限の音を詰め込むことはできません。検証器はプログラムの一番忙しいティック、つまり一番仕事量の多いティックでも、その拍に収まることを証明します。音楽的に読むとそのままです。あるテンポでの一拍には収まる量しかありません。1拍の中に無限の音を詰め込むことはできません。検証器はプログラムの一番忙しいティック、つまり一番仕事量の多いティックでも、その拍に収まることを証明します。

予算の単位は「パイプライン化サイクル」です。パイプライン化サイクルは仕事量の単位で、機械の小さなステップを数えるもので、秒数ではありません。言語はその単位での上限を証明します。それを実時間の秒数に変換するには、走る機械によります。言語が保証するのは、ティックあたりの仕事量が有限である、ということです。予算の単位は「パイプライン化サイクル」です。パイプライン化サイクルは仕事量の単位で、機械の小さなステップを数えるもので、秒数ではありません。言語はその単位での上限を証明します。それを実時間の秒数に変換するには、走る機械によります。言語が保証するのは、ティックあたりの仕事量が有限である、ということです。

メモリの予算

2番目の予算はメモリです。言語はあるティックで必要になる最大の作業メモリ量を割り出し、それも有限であることを証明します。これが「ワーストケースメモリ使用量」、WCMUです。それからホストは、その量ぴったりのメモリを「アリーナ」と呼ばれる固定の領域として確保します。2番目の予算はメモリです。言語はあるティックで必要になる最大の作業メモリ量を割り出し、それも有限であることを証明します。これが「ワーストケースメモリ使用量」、WCMUです。それからホストは、その量ぴったりのメモリを「アリーナ」と呼ばれる固定の領域として確保します。

アリーナは決まったサイズの譜面台です。検証器は、プログラムが譜面台に乗る紙より多くを必要とすることが決して無いことを証明します。必要メモリが有限と証明できないプログラム、あるいは証明された必要量がホストの確保したアリーナより大きいプログラムは、走りません。アリーナは決まったサイズの譜面台です。検証器は、プログラムが譜面台に乗る紙より多くを必要とすることが決して無いことを証明します。必要メモリが有限と証明できないプログラム、あるいは証明された必要量がホストの確保したアリーナより大きいプログラムは、走りません。

約束

第15章の関数カテゴリと合わせて、これらの2つの予算は、言語が受け入れるすべてのプログラムについていくつかの約束を支えています。第15章の関数カテゴリと合わせて、これらの2つの予算は、言語が受け入れるすべてのプログラムについていくつかの約束を支えています。

全域性 — すべてのfn関数は終わります。
生産性 — すべてのloop関数はサイクルごとに値を渡します。
時間の有界性 — すべてのティックが時間予算に収まります。
メモリの有界性 — すべてのティックがメモリ予算に収まります。
安全な差し替え — プログラムのコードはRESETの境界で新しいコードに置き換えられて、ホストとの会話を切らずに続けられます。第26章で改めて扱います。安全な差し替え — プログラムのコードはRESETの境界で新しいコードに置き換えられて、ホストとの会話を切らずに続けられます。第26章で改めて扱います。

これらは希望ではありません。受け入れられたすべてのプログラムについて、走り出す前に証明されています。これらは希望ではありません。受け入れられたすべてのプログラムについて、走り出す前に証明されています。

受け入れは証明

このプログラムは受け入れられます。

fn main() -> Word {
    for _b in 0..8 {
        let _beat = 1;
    }
    0
}

keleusma runで実行すると0を返します。劇的なことは何も起こりません。けれど、その0が出てくる前に、検証器はループがちょうど8回走ること、そしてだからプログラムの時間とメモリが両方とも有限であることを証明していました。受け入れは静かですが、受け入れこそが証明です。走るすべてのプログラムがそれを通過しています。keleusma runで実行すると0を返します。劇的なことは何も起こりません。けれど、その0が出てくる前に、検証器はループがちょうど8回走ること、そしてだからプログラムの時間とメモリが両方とも有限であることを証明していました。受け入れは静かですが、受け入れこそが証明です。走るすべてのプログラムがそれを通過しています。

保守的なスタンス

検証器は、有限と証明できないプログラムは、実際には問題なく動いたであろうプログラムでも却下します。安全なプログラムを通さないことを選ぶ方が、危険なプログラムを通してしまうよりマシだ、という選択です。第19章の再帰版count_downが、実際にはゼロで止まっていたであろうにも関わらず却下されたのもそのためです。検証器はそれを事前には知り得ません — 「事前」が要点だからです。検証器は、有限と証明できないプログラムは、実際には問題なく動いたであろうプログラムでも却下します。安全なプログラムを通さないことを選ぶ方が、危険なプログラムを通してしまうよりマシだ、という選択です。第19章の再帰版count_downが、実際にはゼロで止まっていたであろうにも関わらず却下されたのもそのためです。検証器はそれを事前には知り得ません — 「事前」が要点だからです。

これがKeleusmaの取引です。言語は他の言語より小さなプログラムの集合しか受け入れません。その代わり、その集合に入っているすべてのプログラムについて、他の言語が一つのプログラムについても約束できないようなことを約束できます。音飛びしてはいけないオーディオエンジンや、必ず時間内に応答しなければならない制御装置にとって、その取引こそがKeleusmaを選ぶ理由になります。これがKeleusmaの取引です。言語は他の言語より小さなプログラムの集合しか受け入れません。その代わり、その集合に入っているすべてのプログラムについて、他の言語が一つのプログラムについても約束できないようなことを約束できます。音飛びしてはいけないオーディオエンジンや、必ず時間内に応答しなければならない制御装置にとって、その取引こそがKeleusmaを選ぶ理由になります。

この章のまとめ

すべてのプログラムは時間予算とメモリ予算の両方に従わされ、両方とも実行前に確認されます。すべてのプログラムは時間予算とメモリ予算の両方に従わされ、両方とも実行前に確認されます。
時間予算はワーストケース実行時間で、単位はパイプライン化サイクルです。
メモリ予算はワーストケースメモリ使用量で、アリーナの内側に収まります。
言語は、受け入れるすべてのプログラムについて、全域性、生産性、時間の有界性、メモリの有界性、安全な差し替えを約束します。言語は、受け入れるすべてのプログラムについて、全域性、生産性、時間の有界性、メモリの有界性、安全な差し替えを約束します。
検証器は証明できないものをすべて、設計上、却下します。

これで第5部は完了です。言語が何を保証して、引き換えにプログラムに何を求めるのか、両方が分かりました。第6部では言語そのものに戻り、ここまでの全てを土台にする機能をいくつか紹介します。これで第5部は完了です。言語が何を保証して、引き換えにプログラムに何を求めるのか、両方が分かりました。第6部では言語そのものに戻り、ここまでの全てを土台にする機能をいくつか紹介します。

The Keleusma Guide