AI・機械学習
収束だけでは不十分
Convergence Is Not Enough (inkandswitch.com)
要約
Livelymergeプロジェクトは、プログラムのヒープ全体をAutomergeドキュメントとして扱い、リアルタイムでのマージを目指しています。しかし、Automergeの収束保証だけでは、プログラムの不変条件(例: リストの循環がない、各要素が一意である)を満たせない問題が発生します。本稿では、この「意図」ではなく「書き込み」をマージする問題点を具体例で示し、高レベルな操作をマージする「マージ対応型データ構造」という解決策の方向性を提案しています。
全文翻訳
はじめに
Livelymergeプロジェクトにおいて、Dan Ingalls、Peter Van Hardenberg、そして私(Alex Warth)は、Lively Kernelのようなシステムを構築しています。このシステムでは、ヒープ全体、つまり全てのオブジェクト、クラス、メソッドがAutomergeドキュメントとなります。このシリーズの最初のノートでの提案は、これによりマージが「無料」で得られるというものでした。複数のユーザーが同じオブジェクトメモリを共有し、同時に(オフラインでも)作業でき、Automergeが全てを調和させます。また、ライブシステムのステートをマージすることは単純な問題ではなく、オブジェクトの不変条件が侵害されない保証はないとも書きました。このノートでは、具体的な例を用いてその問題に正面から向き合います。まだ解決策はありませんが、有望だと考えている可能性のある解決策の概要をスケッチします。皆さんのアイデアもぜひお聞かせください。
Exhibit A: 連結リスト
Automergeの約束は収束性です。2つのクライアントが変更を交換した後、それらが同じステートに到達することは保証されます。しかし、そのステートがプログラムが維持できるものであるとは限りません。多くのアプリケーション、例えばドキュメントやToDoリストにとっては、Automergeのマージは期待通りに機能します。しかし、LMではもっと奇妙なことを行っています。それは、実行中のプログラムのヒープ、ポインタも含めてマージすることです。これはAutomergeの得意分野を大きく外れており、このノートはその領域で何が起こるかについてです。1 → 2 → 3 → 4という、プログラマーなら誰でもLMで構築するであろう方法で構築された、素朴な連結リストを考えてみましょう。各ノードは別のノードを指すnextプロパティを持っています。ここで、2人のクライアントが同時にそれを変更するとします。
クライアントAは、1.next ← 3、2.next ← 4、3.next ← 2と書き込むことで、2と3をスワップします。彼らのリストは現在 1, 3, 2, 4 となっています。クライアントBは、2.next ← 4、3.next ← null、4.next ← 3と書き込むことで、3と4をスワップします。彼らのリストは 1, 2, 4, 3 となっています。
これらの変更が同期されたときに何が起こるか見てみましょう。Automergeはそれらを次のようにマージします。各クライアントの変更はトランザクションであり、マージは一方のトランザクションの書き込みが適用され、次に他方の書き込みが適用されるかのように動作します。Automergeは決定論的に2つの順序のいずれかを選択し、両方のクライアントが同じ順序を得ます(したがって、個々の書き込みの任意のインターリーブは不可能であり、到達可能なステートの数を制限します)。後続のトランザクションが触れなかった書き込みは、先行するトランザクションから生き残ります。両方のトランザクションが書き込んだ場所では、後続のものが勝ちます。
2つの可能な順序が実際に何を生み出すか見てみましょう。
1.next はどちらの場合もAから来ます(Bはそれを書き込んでいません)。4.next はどちらの場合もBから来ます。しかし、3.next は、両方のトランザクションが書き込んだものですが、後から来た方に属します。
A then B (3.next = null): 1からたどると「1, 3」となります。リストは切り詰められ、ノード2と4は脇に追いやられます。
B then A (3.next = 2): 1からたどると「1, 3, 2, 4, 3, 2, 4, ...」となります。リストにはサイクルができ、それをたどるコードは決して終了しません。
ここで強調したいのは、Automergeはここでは何も間違ったことはしていないということです。両方のクライアントは、約束通り、決定論的に同じ結果に収束します。問題は、Aの書き込みの後にBの書き込みをリプレイすることが、Aの後にBの意図を実行することと同じではないということです。クライアントBは、元のリスト 1 → 2 → 3 → 4 を見て、これらの3つの書き込みを計算しました。マージ後にはもはや存在しないステートです。もしAの変更の後にBの「3と4のスワップ」が実際に実行されていれば、異なる書き込みと完全に正常なリストが生成されていたでしょう。マージは意図ではなく効果をリプレイし、プログラマーの不変条件(各ノードがちょうど1回出現する、サイクルがない、リストが終了する)は、Automergeが見ることができるどこにも書き込まれていませんでした。
収束だけでは不十分です。
これは連結リストだけの問題ではありません
ポインタで連結リストを構築しないことで、この特定の問題を回避できます。Automergeには、うまく機能するマージセマンティクスを持つ組み込みデータ型があります。その配列(私たちのオブジェクトモデルが直接公開しているもの)は、期待通りに同時挿入と削除をマージし、様々な種類のマップも簡単に表現できます。私たちは実際にこれをMorphcで多用しています。Morphcは、私たちのシステムの中心にあるグラフィカルフレームワークです。(MorphcはSelfプログラミング言語に起源を持ち、後にSqueakとDanのLively Kernelで使用されました。Morphcでは、画面上の全てが見えるものはモーフ、つまり他のモーフを含むことができるオブジェクトであり、ボタンやテキストまで全てです。)各モーフのサブモーフリストはAutomerge配列であり、2人のユーザーからの同時追加はうまくインターリーブされます。
しかし、これらのデータ型を組み合わせると、全てが不確実になります。プログラミングではこのようなことが非常に頻繁に起こります!マージはトランザクション全体を順序付けしますが、その書き込みを盲目的にリプレイするため、1つのプロパティまたはオブジェクトを超えるあらゆる不変条件は、マージにとって不可視となります。
双方向連結リスト(nextとprevは互いにミラーリングする必要がある)。
ツリー(Morphc自体:各モーフのオーナーは、そのオーナーのサブモーフと一致する必要がある。同じモーフを同時に再親化する2人のユーザーは、今日これを壊す可能性がある)。
要約するコレクションと一致する必要があるキャッシュされたカウントまたはインデックス。
何らかのものに対する「各要素がちょうど1回出現する」という制約。
LMのようなシステム、つまりヒープがドキュメントであり、ユーザーが好きなデータ構造を構築することが奨励されるシステムでは、これはコーナーケースではありません。これは私たちが積極的に考えている問題です。とはいえ、予想よりも頻繁に私たちを悩ませることはありませんでした。注意深いプログラミングにより、可能な限りAutomergeの組み込みデータ型に依存し、矛盾する可能性のある冗長な表現を避けることで、日常的なマルチユーザー使用に耐えうるシステムを構築することができました。(もちろん、注意深いプログラミングは解決策ではありません。それは、解決策を待っている間に行うことです。)
私たちが好む方向性:マージ対応型データ構造
現在、マージはプログラマーが実際に気にする抽象化の下で、生のオブジェクトグラフのレベルで発生します。上記の診断を踏まえると、自然な動きは、それらがコンパイルされた書き込みではなく、意図をマージすることです。そして、意図は「3.nextをnullに設定する」ではなく、それすらも実装であり、1つ上のレベルに過ぎません。「この値をリストから削除する」「その値の後にこの値を挿入する」といった、抽象型レベルでプログラマーが言うであろうことが意図です。
Automergeはすでに正確にこの方法で動作しますが、組み込み型に対してのみです。Automergeリストへの変更は、ポインタ書き込みではなく、ドキュメントの履歴に挿入および削除操作(これが実際のAutomergeの用語です)として記録されます。そして、まさにこの理由で、それらのリストに対する同時編集はうまくマージされます。
そこで、私たちが興味深いと考えているアイデアがあります。もしAutomergeが、プログラマー定義のデータ構造が自身をリスト型、マップ型、カウンター型などと宣言できるような、型の概念を公開したらどうなるでしょうか?ドキュメント内の表現はプログラマー次第ですが、読み書きはその型のインターフェースを通じて行われ、操作として記録されるのは、その型のより高レベルな語彙となります。マージは、型ごとに定義されたセマンティクスを持つ、それらの操作のマージを意味することになります。プログラマーが組み込み型を採用するだけでなく、全く新しい型を定義できれば、さらに良いでしょう。
nontrivialな型に対して厳密に実行できることには、励みになる先例があります。Kleppmannらによる複製ツリーの移動操作は、「再親化がサイクルを作成しない」ことをマージに直接組み込んでいます。そのアルゴリズムの背後にある技術は驚くほど広く一般化できます。全ての操作を単一の決定論的な順序(例えばタイムスタンプによる)でリプレイし、各操作を不変条件に対してチェックし、違反するものをスキップします。全てのクライアントが同じ順序で同じ操作をリプレイするため、収束は無料で得られ、不変条件は構築によって保持されます。(ECROもこのアイデアに基づいたシステムです。)
しかし、これは完璧な答えではありません。実行時に有効だった操作が、後から到着したより低いタイムスタンプを持つ操作によって、遡って無効になる可能性があるため、ユーザーは以前受け入れられた作業がロールバックされるのを目にすることになります。そして、より広範な未解決の疑問が残ります。