場合分けしてみた - Skip Graph の concurrent JOIN を考える - その4

erlang

id:kibayos さんの PDF「構造化オーバレイの一貫性保証」 に書かれている Skip Graph の一貫性保証の例を読み解く。
http://live-e.naist.jp/sensor_overlay/3/doc/yoshida.pdf


その3の続き。
Concurrent Join のアルゴリズムをカジュアルにフォーマライズしたい。拠り所が出来れば実装やテストが安心だし。
不変表明は

  • 「双方向リンクリストがどのステップでも一貫性を保持している事」
    • 右からたどるのと逆からたどるのが全く同じということ。
  • 「双方向リンクリストがどのステップでもソートされている事」

としてみた。


表中の列方向が、Join の各ステップ、行方向が可能性のある状態。


詳しく見ていくと 4 つ目のステップ「change Y->X to Y->A」で不変表明を満たせなくなる。
これは

  • 不変表明がきつすぎる
    • 一貫していなくても、検索、Join、Remove に影響がない？
  • この方法・解釈は間違っている

のどちらかだと思う。難しい。

追記

社内で、バージョンニングして dirty な状態は見せないというのはどうか？という意見をもらった。明日考える。