Think Stitch
PRINCIPIA  最近の更新


ロックフリーアルゴリズム:キュー 2

ロックフリーアルゴリズム:キューへの追加の続きです。 まず最初にお詫びをさせてください。キューへの追加のモデルにバグがありました。ごめんなさい。 詳細は後ほど説明しますが、結論としては論文にある E7 という行を省略してはいけないということです。 とんだ勘違いをしてしまいました。

今回はまず、前回の続きとしてキューからの取り出し部分を考えます。 次に、キューへの追加を行うプロセスと、キューからの取り出しを行うプロセスを複数並行に走らせた場合について検査を行います。 追加モデルのバグは、前回の検査では発見できませんでしたが、取り出すプロセスと並行に走らせると現れます。 さらに ABA 問題にも挑戦します。

キューからの取り出し操作

キューからの取り出し操作について復習します。 追加に比べて取り出しの方が少し簡単です。ダミーのノードがあるおかげでもあります。

キューにデータが入っている一般的な状況は以下のようになります。

まず head が指しているノードの next ポインタを取り出します。 もし next ポインタが空リスト () だったらキューは空です。 そうでなければ next ポインタが指すノードからデータを取り出します。 今回のモデルでもデータは無視するので、このステップはありません。 次に head を next ポインタの値で更新します。 つまりダミーを飛ばします。 すると、いまデータを取り出したノードが新しいダミーになります。

そうしたら、古いダミーを解放すれば取り出しの操作は終わりです。

QUE プロセス

キューを表すプロセス QUE に2つ修正をほどこします。

1つは head ポインタを追加することです。 プロセスパラメータとして head を追加します。 さらに、head のための rd-head, wr-head, cas-head を追加します。 コードは名前を除いて tail と全く同じです。

もう1つの修正は未使用ノードの管理を行っていたプロセス MM を QUE に統合・吸収することです。 主な理由は2つで、1つはモデルの状態数を減らすため、もう1つは未使用ノードに特別なマークをつけて、誤り検出の機会を増やすためです。 ノードを解放するためのインターフェイス free も追加します。

(define-process (QUE c head tail ns)
  (alt
    (! rd-head (head)
       (QUE c head tail ns))
    (? wr-head (p)
       (QUE (consistent p tail ns) p tail ns))
    (! rd-tail (tail)
       (QUE c head tail ns))
    (? wr-tail (p)
       (QUE (consistent head p ns) head p ns))
    (? rd-next (k p) (eqv? (ref ns k) p)
       (QUE c head tail ns))
    (? wr-next (k p)
       (let ((ns-u (update ns k p)))
         (QUE (consistent head tail ns-u)
              head tail ns-u)))
    (? cas-head (q r b)
       (eqv? (eqv? head q) b)
       (if b
           (QUE (consistent r tail ns) r tail ns)
           (QUE c head tail ns)))
    (? cas-tail (q r b)
       (eqv? (eqv? tail q) b)
       (if b
           (QUE (consistent head r ns) head r ns)
           (QUE c head tail ns)))
    (? cas-next (p q r b)
       (eqv? (eqv? (ref ns p) q) b)
       (if b
           (let ((ns-u (update ns p r)))
             (QUE (consistent head tail ns-u)
                  head tail ns-u))
           (QUE c head tail ns)))
    (let ((k (list-index not ns)))
      (if k
          (! alloc (k)
             (let ((ns-u (update ns k '())))
               (QUE (consistent head tail ns-u)
                    head tail ns-u)))
          (! empty (QUE c head tail ns))))
    (? free (p)
       (let ((ns-u (update ns p #f)))
         (QUE (consistent head tail ns-u)
              head tail ns-u)))
    (! terminate
       (if (= c 1) ; consistent
           SKIP
           STOP))))

未使用ノードに対応するスロットには #f を入れることにします。 ノードの割り当てを行うインターフェイス alloc では、リスト ns をスキャンして未使用ノードを求めます。 もし未使用のノードがなければ empty を発行します。 割り当てるノードの next ポインタを空リスト () で初期化する作業も QUE へ移しました。

ノードの解放 free は簡単で、指定されたノードに対応するスロットに #f を入れるだけです。

整合性を検査する関数 consistent は、連結の検査を head が指し示すノードから行うように修正します。

プロセス MM の場合は、未使用ノードのインデックスのリストがあったので、その並び方の場合の数、つまり順列の数だけ状態がありました。 今回はリストを廃止したので、状態数をだいぶ減らすことができたと思います。

取り出し操作を行うプロセス C1

取り出し操作を行うプロセス C1 を定義します。 今回は最初から CAS 操作を使います。 CAS が必要であることは明らかでしょうから。

(define-process C1
  (? rd-head (head)
     (? rd-next (p next) (eqv? p head)
        (if (null? next)
            SKIP
            (? cas-head (q r b)
               (and (eqv? q head)
                    (eqv? r next))
               (if b
                   (! free (head) C1)
                   C1))))))

まず head を読み出し、次に next ポインタを読み出します。 もし next ポインタが空リスト () だったらキューは空ですから終了します。 そうでなければ CAS を使って head を更新します。 CAS に失敗したらリトライします。 最後に古いダミーノードを free を使って解放します。

システムプロセス

取り出し操作を検査するためのシステムプロセスを定義します。 取り出しを検査するので、キューの初期状態はすべてのノードが連結されている状態とします。 今回追加したチャネル rd-head, wr-head, cas-head, free を同期リストに追加します。

(define-process (SYS2 C nc)
  (par (list rd-head wr-head cas-head
             rd-tail wr-tail cas-tail
             rd-next wr-next cas-next 
             empty alloc free
             terminate)
    (QUE 1 (- N 1) 0 (cons '() (interval 0 (- N 1))))
    (seq
      (if (= nc 1)
          C
          (xpar k (interval 0 nc) '() C))
      (! terminate SKIP))))

検査 C1

C1 を1つだけ走らせると、当然のことながら問題は起こりません。 こういう簡単な場合でモデルを検査しておくことには意味があります。 単純な間違いを見つけることができますから。

次に C1 を2つ走らせると、デッドロックが見つかります。 N = 2 の場合でも見つかるので、これを分析することにします。 できるだけ簡単な場合から調べるほうが楽だし、問題の部分が詳細に隠れずに済みます。

デッドロックへ至るパスは次のとおりです。

わかりやすいようにポイントを図解しました。

まず初期状態はすべてのノード、といっても2個だけですが、つながっています。 1つはダミーです。

2つのプロセスがそれぞれ head = 1 を読み取った後、一方が next ポインタを取得して空リストでないことを見出し、head を更新します。

さらに旧ダミーノードを解放します。

ここでもう1つのプロセスが next ポインタを読み取ります。 ところが、ノード 1 はすでに解放されていますから、#f が返ってきます。 これはゴミを読み出しているということです。 このアルゴリズムは、ゴミを読んでしまうことを避けられません。 例えばですが、解放されたノードのあるページが無効になるような場合があるプログラムでは使用することができません。

ゴミを読み出したプロセスは、それが空リストでないことからデータがあると勘違いして、head を CAS で更新しようとします。 しかし、CAS の定義域には #f を入れていないので、デッドロックします。 実は CAS の定義域に #f を入れていないのは、このように検査で見つけられるようにするためです。 実際のプログラムでいえば assert を入れておくことに相当します。 定義域に入れておく代わりにガードで制限して同様の効果を得ることもできます。 こちらの方が、より assert に近いでしょう。 しかし定義域を大きくすると状態数が増える場合があるので、できるだけ必要なものだけに限ったほうが得です。

やや脱線しました。 問題は何かというと、head を読んでから next ポインタを読むまでの間に構造が書き変えられてしまったため、next ポインタが無効であるという点です。 プロセスはこれを検出できなければなりません。 ゴミを参照してしまうことは避けられませんし、ゴミが偶然有効な値に一致することもありますから、ゴミに基づいて判断することはできません。 そこで、next ポインタを読んだあとで、もう1度 head を読み、前に読んだ値と比べて変わっていなかったら next ポインタの値が有効であると判断することにします。 (ここで、前回間違いをおかしたことに気が付いたのです。)

プロセス C2

次のように、head をもう1度チェックするプロセス C2 を定義します。

(define-process C2
  (? rd-head (head)
     (? rd-next (p next) (eqv? p head)
        (? rd-head (head2)
           (if (not (eqv? head head2))
               C2
               (if (null? next)
                   SKIP
                   (? cas-head (q r b)
                      (and (eqv? q head)
                           (eqv? r next))
                      (if b
                          (! free (head) C2)
                          C2))))))))

このプロセスで検査を行うと、プロセス3個、N=4 としてもデッドロックしないことがわかりました。 また、前回のようにすべてのイベントを隠蔽して発散するかどうか調べたところ、発散もないことがわかりました。

追加と取り出しを同時に行う検査

つづいて、追加と取り出しを行うプロセスを並行に走らせる場合について検査します。 以下のように、追加プロセス P を np 個、取り出しプロセス C を nc 個並行に走らせるシステムプロセスを定義します。 キューの初期値は空としました。

(define-process (SYS3 P C np nc)
  (par (list rd-head wr-head cas-head
             rd-tail wr-tail cas-tail
             rd-next wr-next cas-next 
             empty alloc free
             terminate)
    (QUE 1 0 0 (cons '() (map (lambda (p) #f) (cdr I))))
    (seq
      (par '()
        (if (= np 1)
            P
            (xpar k (interval 0 np) '() P))
        (if (= nc 1)
            C
            (xpar k (interval 0 nc) '() C)))
      (! terminate SKIP))))

検査 P2 x C2

追加プロセス P2 と取り出しプロセス C2 を選びます。 まず1つずつ動かした場合は問題ありません。しかしどちらを2個にしてもデッドロックが見つかります。

P2 が2個、C2 が1個の場合

デッドロックに至るパスは次のようになります。 パスは長いですけれども、問題は早い段階、7行目で発生します。

まず初期状態は空ですから次のようになっています。 斜線1つは空リスト (), ×印は未使用ノードを示します。値は #f です。

2つの追加プロセスを P0, P1 とします。 まず P1 がノード 1 を alloc で取得します。 next ポインタはプロセス QUE によって空リスト () に初期化されます。

P1 は割り当てたノードを連結します。 tail の更新はまだです。

ここで取り出しプロセス C が動きます。 C は head の指すノードの next ポインタが空リストでないことからデータがあると判断し、head を更新して、ダミーを解放します。

この時点ですでに派手に壊れていますけれども、面白いので(バグですから面白くないですが、現象として興味深いという意味です^^;)もう少し見ていきます。

もう1つの追加プロセス P0 はがノード 0 を割り当てます。 さらに tail を読み、0 を得ます。 そこ後再び P1 に制御が移り、tail が更新されて次のようになります。

プロセス P0 は tail が 0 だと思っていて、同時に割り当てた新しいノードも 0 だと思っています。 さらに 0 の next ポインタは空リストですから追加が可能であると判断し、新しいノードへのポインタ、つまり 0 を書き込みます。 結果は次のように循環ができてしましました。

問題はどこにあるかというと、キューが壊れる直前の操作、つまり head の更新です。 プロセス C は next ポインタが空リストでないことからデータがあると判断しました。 しかしこの時点ではまだ tail が更新されていないので、head を先に更新するとキューが不整合になってしまうわけです。 これを避けるには、head と tail が一致している場合には head を更新しないようにします。

プロセスを修正する前に、もう1つの場合を見てみます。

P2 が1個の場合、C2 が2個の場合

デッドロックに至るパスは次のとおりです。

追加プロセスを P, 取り出しプロセスを C0, C1 とします。 初期状態は次のとおりです。

まず追加プロセス P が追加を行います。

次にプロセス C1 が取り出しを行います。 この途中、head が更新される前に、C0 が head=0 を読み出します。

C0 は次に 0 の next ポインタを読むわけですが、解放されたあとのゴミ #f を読み出してしまいます。 これは避けられないことなので、これ自体は問題ではありません。

再びプロセス P が追加を行います。

それを C1 が取り出します。

この途中で C0 が再び head=0 を読みました。 すると、C0 の立場から見ると、まず head=0 を読み、次に next ポインタを得て、それが有効であることを確認するために再度 head を読んだら 0 でした。 head が変化していないので、next ポインタが有効であると考え、しかもゴミ #f は空リストでないことから head を更新しようとしてデッドロックしています。

上の過程を見るとわかるように、C0 が最初に読んだ head=0 と2回目に読んだ head=0 は異なるノードです。一度解放されたノードが再割り当てされ、偶然ポインタ値が一致してしまったために変化していないと勘違いしたのでした。 これを ABA 問題というのだそうです。 A が一度 B になって、そのあとまた A に戻ったのだけれど、最初と最後しか見ていなかった人には変化がなかったように見えるという意味だそうです。

この問題への対処はちょっと後に回して、先の問題に対する修正を行うことにします。

プロセス C3

追加途中のデータを早まって取り出してしまわないように、tail も取得して head と一致しているかどうかチェックすることにします。

(define-process C3
  (? rd-head (head)
     (? rd-tail (tail)
        (? rd-next (p next) (eqv? p head)
           (? rd-head (head2)
              (if (not (eqv? head head2))
                  C3
                  (if (eqv? head tail)
                      (if (null? next)
                          SKIP
                          C3)
                      (? cas-head (q r b)
                         (and (eqv? q head)
                              (eqv? r next))
                         (if b
                             (! free (head) C3)
                             C3)))))))))

検査 P2 x C3

C3 を使って検査を行うと次のような結果になりました。

期待通り、追加プロセスが2つある場合のデッドロックは解消しました。 取り出しプロセスが2つある場合はまだデッドロックがあります。 これも分析しておきましょう。 デッドロックに至るパスは次のようになります。

まず追加プロセス P がノードを追加します。

この状態でプロセス C0 は head=0, tail=1 を読み出します。 その後で、C1 が取り出しを行います。

P がノード 0 を割り当てます。next ポインタは空リストに初期化されます。 なんとそのタイミングで C0 が next ポインタを読み、空リストを取得します。

P が追加します。

C1 が取り出します。

ここで C0 が2度目の head = 0 を読み出します。 これも典型的な ABA 問題でした。 なぜデッドロックしたかというと、head と tail が異なるので、データを取り出せると思っているのですが、取得した next ポインタは空リストなので、head には格納できないからです。 ここでも定義域を厳しく制限しておいたおかげで問題を見つけることができました。

ここまでについての補足

C2 については2つの問題を見つけました。 この2つは、どちらも初期状態から似たような距離のところにデッドロックをもっているので、モデルをちょっと変えたり、検査の順序を変えたりすると、一方しか見つからないことがあります。

ABA 問題への対処

ABA 問題が発生する原因は、ノードのポインタ値が偶然一致したことでした。 メモリ管理のアルゴリズムによって頻度は異なるでしょうが、実際に問題になることがあるそうです。 特にマルチスレッドのプログラムで、スピードを上げるためにメモリブロックのプールを持っておき、使いまわすような場合には発生する危険が高まるでしょう。

これに対処する1つの方法は、ポインタ値とは別にもう1つ、区別するための値を持つ方法です。 先の論文では unsigned integer 型の count という値を持たせていました。 ノードを割り当てるたびに count をインクリメントすれば、偶然一致する可能性を大いに減らすことができます。 ここでは同じ方法を使って ABA 問題に対処することにします。

変更はかなり大規模かつ複雑になるので、概要だけ説明することにします。 まずポインタ値として、いままではリスト ns のインデックスを使っていましたが、代わりに、インデックスとカウント値のペア (k . j) を使うことにします。 カウント値は割り当てのたびにインクリメントします。

このようなカウンタをシーケンサと呼ぶことがあります。 実はシーケンサはモデル検査にとって困った存在なのです。 なぜかというと、状態数をとてつもなく増やすからです。 だからといって、実際のプログラムのようにカウンタ値を再利用すると、すべての場合を調べるモデル検査では、かならず値が一巡したあとの衝突を見つけてしまうのです。 この問題を避けるために、ここでは追加プロセスが追加を行う回数に上限を設けることにしました。

ABA 問題に対処したキュープロセス QUE2

ポインタをインデックスとカウンタのペアに変更したプロセス QUE2 を作ります。 詳細な説明は省略しますが、重要な点だけ書いておきます。

まずリスト ns の要素は、((k . j) . ptr) と形にします。ここで k はスロットのインデックスそのもの、j はカウンタです。 k を入れるのはやや冗長ですけど、特に問題というわけでもありません。 ptr は next ポインタの値です。空リスト、または (k' . j') という形になります。 未使用ノードには (#f . #f) を入れておきます。

もう1つの大きな変更は rd-next にあります。 何度かいいましたように、このアルゴリズムではゴミを参照することを避けられません。 したがって例えば、(k . j) というポインタを持っているプロセスが rd-next を要求したとき、ノードはすでに再利用されていて (k . j') になっているかもしません。 この場合でもきちんと(?)ゴミが読めるようにガードを調整してあります。

(define-process (QUE2 c head tail ns j)
  (alt
    (! rd-head (head)
       (QUE2 c head tail ns j))
    (? wr-head (p)
       (QUE2 (consistent2 p tail ns) p tail ns j))
    (! rd-tail (tail)
       (QUE2 c head tail ns j))
    (? wr-tail (p)
       (QUE2 (consistent2 head p ns) head p ns j))
    (? rd-next (p q) (or (equal? (ref ns (car p)) (cons p q))
                         (and (not (equal?
                                    (car (ref ns (car p)))
                                    p))
                              (not q)))
       (QUE2 c head tail ns j))
    (? wr-next (p q) (equal? (car (ref ns (car p))) p)
       (let ((ns-u (update ns (car p) (cons p q))))
         (QUE2 (consistent2 head tail ns-u)
              head tail ns-u j)))
    (? cas-head (q r b)
       (eqv? (equal? head q) b)
       (if b
           (QUE2 (consistent2 r tail ns) r tail ns j)
           (QUE2 c head tail ns j)))
    (? cas-tail (q r b)
       (eqv? (equal? tail q) b)
       (if b
           (QUE2 (consistent2 head r ns) head r ns j)
           (QUE2 c head tail ns j)))
    (? cas-next (p q r b)
       (eqv? (equal? (ref ns (car p)) (cons p q)) b)
       (if b
           (let ((ns-u (update ns (car p) (cons p r))))
             (QUE2 (consistent2 head tail ns-u)
                  head tail ns-u j))
           (QUE2 c head tail ns j)))
    (let ((k (list-index (lambda (p.q) (not (car p.q))) ns)))
      (if k
          (! alloc ((cons k j))
             (let ((ns-u (update ns k (cons (cons k j) '()))))
               (QUE2 (consistent2 head tail ns-u)
                    head tail ns-u (+ j 1))))
          (! empty (QUE2 c head tail ns j))))
    (? free (p)
       (let ((ns-u (update ns (car p) (cons #f #f))))
         (QUE2 (consistent2 head tail ns-u)
              head tail ns-u j)))
    (! terminate
       (if (= c 1)
           SKIP
           STOP))))

ABA 問題の検査

この QUE2 および同様の対処を行った追加プロセス P2 と取り出しプロセス C3 について検査を行うと、P2 が2個、C3 が1個の場合でデッドロックが見つかります。 パスは次のとおりです。

初期状態は次のとおりです。 図ではポインタ (k . j) を k.j と表しました。

まず2つの追加プロセス P0, P1 がそれぞれノードを割り当てます。 カウンタがインクリメントされていることがわかります。

P0 が tail = 0.0 を読んだ後で、P1 が追加を行います。

これをプロセス C が取り出します。ノード 0 は未使用状態になりました。

ここで P0 が next ポインタを読みに行きます。指定のポインタは 0.0 ですが、対応するノードはありませんからゴミ #f が返ります。 これは偶然空リストではありませんから、P0 は更新されていない tail の後ろにノードがあると勘違いして、tail を更新しようとします。 例の、発散を回避している tail 更新です。 しかし tail に #f は格納できませんからデッドロックしてしまいます。

この原因は、tail を読んでから next ポインタを読むまでの間に構造が改変されたことにあります。 これは上で取り出しプロセスに起こったことと同じ問題です。 したがってこれに対処するには、もう1度 tail ポインタを読んで、変わっていないことを確認する必要があります。 これが論文のコードにある E7 で、省略してはいけないものでした。

tail を再度チェックする追加プロセス P3

tail の再チェックを加えたプロセス P3 を定義します。プロセスパラメータ c はシーケンサ対策のカウンタです。

(define-process P3 (P3L 2))

(define-process (P3L c)
  (if (= c 0)
      SKIP
      (alt
        (! empty SKIP)
        (? alloc (new-node)
           (P3A new-node c)))))

(define-process (P3A new-node c)
  (? rd-tail (tail)
     (? rd-next (p next) (equal? p tail)
        (? rd-tail (tail2)
           (if (not (equal? tail tail2))
               (P3A new-node c)
               (if (null? next)
                   (? cas-next (p q r b)
                      (and (equal? p tail)
                           (null? q)
                           (equal? r new-node))
                      (if b
                          (? cas-tail (q r b)
                             (and (equal? q tail)
                                  (equal? r new-node))
                             (P3L (- c 1)))
                          (P3A new-node c)))
                   (? cas-tail (q r b)
                      (and (equal? q tail)
                           (equal? r next))
                      (P3A new-node c))))))))

検査 P3 x C3

P3 と C3 の組み合わせで検査を行うと、以下のような結果となりました。 2x1 と 1x2 の組み合わせについては、問題が解消しました。

補足

残念ながら状態爆発のため、これ以上大きなパラメータでは検査を実行できません。 この程度の値では安心とはいえませんが、ABA 問題他についての知見は得られたのではないかと思います。

ゴミの値を空リスト () に変えるとデッドロックが消えてしまう場合があります。 なぜかというと、リトライに回されるからです。 このようにゴミの値によって振る舞いが変わるので、実際のプログラムではもっと見つけるのが困難ではないかと思います。

舌足らずな説明の上、やや駆け足になってしまってすみません。 早く間違いを確認してご報告しなければならないと思ったもので。 間違いを書いてしまったことについて、もう1度お詫びします。ごめんなさい。 検査で確認できるのは、検査したことだけだということを、改めて思い知りました。

2013/09/20
© 2013,2014,2015 PRINCIPIA Limited