GoのMinimal Version Selectionについて

はじめに

2022-01-08、オープンソースのnpmパッケージであるcolors.jsとfaker.jsの作者が、不具合を引き起こす実装を意図的に含めたこれらの最新バージョンを公開した。

それらを利用しているプロジェクトは影響を被り、問題のコードが含まれないバージョンへのダウングレードによって当座の問題を回避したはずだ。

その後、colors.jsは2022-01-11時点で問題を含むバージョン(1.4.1や1.4.2など)はnpmからunpublishされたため、npmの最新は安全なバージョン(1.4.0)へと変更済みだ。ゆえにunpublishまでの数日間において^1.0.0のようにキャレット(^)でバージョン指定していたプロジェクトでは1.4.2が選択されてしまっていた。

本件の教訓として、今後は固定バージョン指定でのパッケージ管理を原則化したプロジェクトも少なくないのではないだろうか。

ところで、GoのパッケージマネージャであるGo Modules(vgo)は、Minimal Version Selection(以下、MVS)というアルゴリズムを採用している。これによって、Goはビルドに関わるパッケージ解決において制約を満たしうる最小バージョンを一意に選択する。そのため、依存パッケージのバージョンをロックファイルによって固定する必要がない。

MVSについて

GoのReferenceにMVSに関する公式ドキュメントが存在し、アルゴリズムが簡潔に説明されている。しかし、今回はRuss Cox氏の”Go & Versioning”における解説を追うことでMVSについて理論的側面から理解を深めてみたい。

MVSというアプローチの特徴は、依存関係解決のためにSAT（SATisfiability、充足可能性）問題を直接解かない点だ。

SAT問題とは、命題変数を含む論理式に対して、その論理式を真にするような命題変数の値への割り当てが存在するかどうかを決定する問題だ。任意の問題（ハノイの塔や数独のような状態空間問題など）をそのまま解かず、SAT問題に変換してSATソルバで解くアプローチが広い分野で採用されており、現代ではパッケージ管理においてSATソルバが使われることがままある。 postd.cc

だがMVSはSAT問題としてバージョン選択問題を解かない。じゃあどうしてるのか。結論から言うと、MVSはSATと正面からぶつからず、問題を変換した上で3つのアルゴリズム（2-SAT, Horn-SAT, Dual-Horn-SAT）を利用して解く。

SATはNP完全問題に属しており、上述したいくつかのパッケージ管理システムはNP完全と向き合っている。しかし実運用における効率的観点から、バージョン選択問題解決にあたってNP完全は避けたい。ところで、Schaefer's dichotomy theoremによって、ある条件を満たすSATはPに属し、効率的な解を持つSATの部分問題としての制限SATは6種類存在することが証明されている。そして、MVSは2-SAT, Horn-SAT, Dual-Horn-SATの中間に位置することが判明したそうだ。計算の複雑度という観点からみれば、NP完全 > Pであるため嬉しい話である。

論理式 $ψ$ を構成する変数 $x$ とその否定 $\overline{x}$ はリテラルと呼ばれ、リテラルの論理和のみで構成される部分は節と呼ばれる。 MVSにおいて、ビルドに対応する論理式は一連の節の論理積である。それぞれの節は、単一の正のリテラル、単一の負のリテラル、一つの負と一つの正のリテラルの論理和のいずれかとなる。

この論理式は、各節が最大2つの変数を持つため、2-CNF式(節の長さが高々2の乗法標準形で表された論理式)である。また、各節は最大1つの正のリテラルを持つから、この式はHorn式でもある。また、各節は最大1つの負リテラルを持つので、この式はDual-Horn式でもある。

つまり、MVSで提起されるすべての充足可能性問題は、3つのアルゴリズムから選択することで解けるそうだ。なるほど……？

おわりに

MVSはビルドにおいて開発者が指定したバージョンを正確に使用し、バージョンアップグレードは自動化せず完全にユーザーに委任している。このアプローチは、ロックファイルを管理せず常に開発時における依存パッケージのバージョンを忠実に再現可能なビルドにつながる。個人的には実運用を意識したアプローチだと感じる。

MVSの理論における記述には筆者による誤解、数学的に不適切な表現が含まれる可能性が多分にあることを留意されたい（すみません……）。下記の参考文献を参照いただければ幸いである。一応アルゴリズムを専門とした研究室で学んで修士出てるのに、SATと言われてもSuchmosしか思い浮かばない体たらくを反省した。今年こそ、まずは「アルゴリズムとデータ構造」を読み通すぞ。