a22_acl2_01 のバックアップ(No.4)

acl2ライブラリ

acl2ライブラリは、できるだけC言語が使いやすくなるようにするためのライブラリです。このライブラリが提供するマクロや関数などは、すべてAかaで始まる名前が付けられています。

裏方はこうなっています。

#define AClass0(nam)   typedef struct nam##_ nam
#define AClass1(nam)   struct nam##_
#define AClass(nam)    AClass0(nam); AClass1(nam)

構造体の最初のメンバは、デスクトラクタ関数（deinit関数）のポインタが入っていることが望ましいです。この取り決めがあれば、素性のよくわからないオブジェクトであっても、少なくともデストラクタは呼べるということになります。
デストラクタ関数は、第一引数がオブジェクトへのポインタで、第二引数が整数値になっています。この第二引数で、デストラクト処理の状況を知らせます。0なら通常の終了で、1なら緊急の終了です。一般に緊急の終了の場合は、longjmpなどのような正常なネスト処理が行えない状況などに対応していて、それに配慮した処理が期待されます（正しい順序でデストラクタ関数を呼べていなくてもエラーにはしないとか）。ということで、基本的には通常終了を選んでください。
多くのオブジェクトでは、0でも1でも同じ終了処理をしています。

ただまあ、このルールは、acl2ライブラリが提供するオブジェクトが守っているルールであって、acl2ライブラリを使う側のプログラムは、この制約を守る義務はありません。

acl2ライブラリが提供する関数群は、勝手にmallocやfreeを呼び出すことはありません。必ずメモリ管理オブジェクトを経由してメモリ管理を行います（AMC）。これによりライブラリ利用者は、acl2ライブラリが勝手にメモリを確保したり開放したりすることを心配しないで済みます。もし自前のメモリ管理アルゴリズムを使いたい場合は、簡単に適用できます。
この機能のおかげで、オブジェクトごとにメモリ管理の方法を選択することができます。

名称未定#0	標準のmalloc/freeを呼ぶだけのクラスです。主に共通のインタフェースを提供するために用意されています。
名称未定#1	最初にかなり大きなサイズのメモリを親に対して要求します。そしてmalloc要求が来るたびにそのメモリを切り取って渡します。free要求が来てもそれはすべて無視します（！）。
名称未定#2	あらかじめサイズを一つだけ設定しておきます。そのサイズでのmalloc/freeについては、内部で高速に処理します。それ以外のサイズについては、そのまま親に丸投げします。
名称未定#3	名称未定#2を内部に4つもったAMCで、4通りのメモリサイズに対してのみ高速化します。もしもっとたくさんのメモリサイズに特化したければ、このAMCを直列につなげばいいでしょう。

[補足:名称未定#1] メモリが足りなくなればまた親に大きなサイズを要求して補充します。このAMCをdeinitしたときにすべてのメモリを親に返します。
[補足:名称未定#2] 指定されたサイズでのfreeの処理は、返されたメモリを線形リストに接続するだけです（前後の領域とのマージは行いません）。そしてmallocでは、もし線形リストにメモリブロックがあればそれを即座に返します。なければ親にmalloc要求を丸投げします。このAMCをdeinitするか、もしくは専用のリクエストをすれば、線形リスト内に蓄えておいたメモリブロックも親にfreeで返します。・・・このようなAMCは木構造などのクラスがノード用のメモリのmalloc/freeを連発するときに、かなりの高速化を可能にします。

ADbgLvというマクロ定数を定義すると、デバッグ向けの機能が有効になります。定義しないとデフォルト動作になり、ADbgLv=0とみなされます。
ADbgLv=1で、負荷の小さいデバッグ支援機能が有効になります。消費メモリを確認できるようになるのもこのレベルです。
ADbgLv=2で、すべてのデバッグ支援機能が有効になります。
ADbgLv=0でも消費メモリ量くらいは確認できるようにすべきだと思うかもしれませんが、「もうとにかくしてもしなくてもいい処理は全部カットして、速度最優先でやってくれ」というのがADbgLv=0に課された使命ですので、消費メモリレポート機能が動かなくなっても問題はないのです。
なお、デバッグレベルによって、構造体の大きさが変わることはありません。デバッグに必要なメンバ変数はADbgLv=0でも確保されます。・・・たいていはそこはポインタになっていて、ポインタの先でデバッグ情報を管理します。こうすることで、ADbgLv=0時のメモリの無駄使いを小さくしています。また、デバッグ情報のためのAMCと通常のAMCは別々になっているので、デバッグ時の消費メモリ確認において、デバッグ情報のためのメモリが計上されることはありません。