Think Stitch
PRINCIPIA  最近の更新


セマフォによるバリア(ランデブ)

先日、Allen B. Downey という方の書いた The Little Book of Semaphores という本を知りました。 セマフォを使って様々なマルチスレッドの同期問題を料理するという楽しい本です。 こちらのサイトから PDF をダウンロードすることができます。

今日はこの中から材料を借りてお料理したいと思います。 題材はバリアです。 バリアというのは、おおまかにいうと、ある処理がかならず別の処理の前とか後に行われることを保証するものです。

例えば上図のように4つのスレッドがあって、それぞれ a.k, b.k という仕事をこの順序で行うとします。 もし何も制限がなければ a, b 入り混じって任意の順序で仕事が行われることになります。 しかし、図のようにバリアを差しはさむと、すべての a.k が完了したあとで最初の b.k が実行されることが保証されます。 別のいい方をすると、a.k の実行が終わったスレッドが全員そろうまで一度待つということです。 その意味で、このバリアのことをランデブと呼ぶこともあるようです。

ここでの問題は、オペレーティングシステムが提供するセマフォとミューテックスを使って、このバリアを実装することです。

最初のプログラム

元本では問題を説明した後にヒントを出して読者に考えてもらうというスタイルをとっています。 さらに、正しくないコードを示して、どこが間違っているのかを考えてもらうという構成になっています。 ちょっとわざとらしいものもあるのですけど(人のこといえない)、ここはのせられていくことにします。

最初のコードは次のようになっています。

1 int n # the number of threads
2 int count = 0
3 Semaphore mutex = 1
4 Semaphore barrier = 0
1 rendezvous
2
3 mutex.wait()
4     count = count + 1
5 mutex.signal()
6
7 if count == n: barrier.signal()
8
9 barrier.wait()
10
11 critical point

これを SyncStitch のモデルにします。

セマフォ SEM

セマフォはいつもと同じです。N はプロセスの数です。(本のプログラムでは小文字の n です。)

(define-process (SEM c)
  (alt
    (if (= c 0)
        STOP
        (! wait (SEM (- c 1))))
    (if (= c N)
        STOP
        (! signal (SEM (+ c 1))))))

ミューテックス MUTEX

元本ではミューテックスもセマフォを使っていますが、ここではいつものミューテックスを使います。同じことです。

カウンタ CNT

変数 count を表すプロセス CNT を用意します。 プロセス間で共有される変数です。 単に読み書きするだけのインターフェイス rd, wr を用意します。 定義域は 0 <= c <= N です。N が含まれることに注意が必要です。

(define-process (CNT c)
  (alt
    (! rd (c) (CNT c))
    (? wr (x) (CNT x))))

ワーカープロセス P

上記のプログラムを実行するプロセスを定義します。 上のプログラムをそのまま状態遷移図にして、前後に仕事のイベント a.id, b.id を加えただけです。 プロセス ID は抽象状態で定義したものを継承しています。

横に長くなるのがいやだったので、折り曲げました。ちょっと見にくいですけど。

システムプロセス SYSTEM

最後に、いつものようにプロセスを並行合成してシステムプロセスを作ります。 ワーカーはインターリーブで並行合成します。 サービスを共有するためです。 次に、同じくサービスプロセス群をインターリーブで合成します。直接の相互作用はないからです。 最後にインターフェイスとなるイベント・チャネルを同期リストに指定して並行合成します。 これらはシステム内部のイベントなのですべて隠蔽します。 したがって hpar を使うことができます。

(define-process SYSTEM
  (hpar (list lock unlock
              wait signal
              rd wr)
    (xpar id (interval 0 N) '() (P id))
    (par '()
      (SEM 0)
      MUTEX
      (CNT 0))))

バリアの仕様

さて、チェックすべきバリアの性質、つまり仕様を記述しましょう。 ちょっと脱線しますと、アルゴリズムの本を読んでいると、プログラムはもちろんきちんと書いてあるわけですけど、それで何ができるのか、何はできないのかというゴールである仕様がいまひとつ明確ではないものがあります。 毎度同じ話で申し訳ないですけど、日本語(あるいはその他自然言語)での説明にはどうしても曖昧なところが残ってしまうようです。 日本語では厳密なことが書けないといっているわけではありません。 ただ、日本語ですべての場合を厳密に尽くした説明を書こうとすると、かなり量が増えるし、法律の文章のように読みにくくなるでしょう。 (仕様書は法律の文章のようにあるべきだという方もいるかもしれませんが。) その点、形式化された表現というのは便利なわけです。 両方をバランスよく使ってくれるといいんですけどね。

話を戻して、仕様をモデル化しましょう。ここでチェックすべきは、a.k と b.k が混ざらないということです。 そこで次のように書くことができます。

(define-process SPEC
  (seq
    (xpar k (interval 0 N) '()
        (! (list-ref as k) SKIP))
    (xpar k (interval 0 N) '()
        (! (list-ref bs k) SKIP))
    STOP))

まず各 a.k を任意の順序で実行することができます。 これを表現するにはインターリーブを使うことができます。 すべての a.k が完了したら、同じように b.k を任意の順序で実行できます。 すべての a.k が完了してから b.k を開始するという順序性は、逐次合成 seq で表すことができます。

尚、プログラムは1度だけ実行したら停止することにします。 STOP ではなく、正常終了するようにすることもできますが、セマフォやミューテックスに終了のためのしくみを入れなければならず、問題の本質が見えにくくなるので簡単のため停止としました。

検査

では検査を行いましょう。 プログラムを見たときから、これは動かないと思った人も多いでしょう。 結果は次のようになります。

まずデッドロックを調べてみると、次のようになっています。

a.k がすべて完了してから b.0 が実行されていますが、その後でデッドロックしています。 プロセス 0 は P7 にいるので停止しています。 プロセス 1, 2 はそれぞれ状態 P4, P5 にいて、wait 待ちです。 signal を1度しか発行していないのですから、これは当然でしょうね。

もう1つ、拒否違反も見てみましょう。 仕様は次のとおりです。 すべての a.k が完了しているので、次にどの b.k も実行可能です。

これに対してシステムは次のようになっています。

実行可能なのは b.2 だけで、あとのプロセス P0, P1 はどちらも状態 P4 にいて wait 待ちです。 これもデッドロックと同じ状況で、b.2 発生後デッドロックになります。

修正されたプログラム

修正版として次のプログラムが出ています。

1 rendezvous
2
3 mutex.wait()
4     count = count + 1
5 mutex.signal()
6
7 if count == n: barrier.signal()
8
9 barrier.wait()
10 barrier.signal()
11
12 critical point

10行目に signal が追加されました。 これのおかげで、全員が集合したあと、一人ずつパタパタと wait, signal を通過して出て行くことができます。 この連続した wait, signal のことをターンスタイル(turnstile)というのだそうです。 たぶん、遊園地の入場ゲートとか、海外だと駅の改札出口にある、金属のバーが回転するやつのことだと思います。

ではモデルも修正することにします。 修正箇所は1箇所、signal を追加するだけです。

検査 2

再度検査をすると次のようになります。

正当性検査はパスしました。 デッドロックの状況は次のとおりです。

これはすべてのプロセスが最後まで到達して停止した状態 P8 にいるので問題ありません。

バリア部分の抽出

上のモデルではバリアの動作をワーカープロセスに直接埋め込みましたが、これを分離して再利用できるようにすることもできます。 まずバリアの部分だけを取り出します。

するとワーカープロセスは次のように書くことができます。 これは逐次合成 seq を使ったプロセスの再利用パターンです。

(define-process (P id)
  (seq
    (! (list-ref as id) SKIP)
    BARRIER
    (! (list-ref bs id) STOP)))

こうしてみると手続き型の言語で書いているかのようです。 構造的には、セマフォ、ミューテックス、カウンタが裏で動いているサービスで、プロセス BARRIER はインターフェイス手続きみたいな感じです。

残念ながらこのバリアは1度しか使えないので、再利用可能にしてもあまりうれしくありません。 使い終わったあとは、カウンタもセマフォも初期状態ではないからです。 元本では、この問題につづいてバリアを再利用可能にする話が書いてありますので、それを使えば再利用できるようになります。 (つまりご自分でどうぞという意味です^^;)

補足

バリアの種類

バリアにはもっと細かい分類があるようです。メモリバリアのあたりを調べるといろいろ見つかります。 バリアの他に、フェンス、ランデブなども出てきます。

ターンスタイルの実行効率

上のナイーブなターンスタイルは、システムコールが頻繁に発生するのであまり効率的とはいえません。 セマフォの実装の中には、カウント値を一気に変えることができるものがあります。 これを使うと効率を改善できます。 元本でもその改良の話が出てきます。 (つまりご自分でどうぞという意味です^^;)

バリアの仕様は安全性?

バリアの仕様は、一見安全性の検査のように思えます。 確かに a, b が混ざらないという点では安全性です。 しかし、ここでの要求はもっと厳しくて、必ずすべての b.k が発生しなければならない、しかも任意の順序で発生できなければならないことを要求しています。 したがって拒否まで含めた検査が必要です。

実際、デッドロックを起こしてしまう最初のプログラムでも、安全性の検査はパスしてしまいます。 実は、プロセス STOP はどんな安全性検査もパスしてしまうのです。 何もしないのですから、何も悪いことが起こるはずがありません。 これはテストをしなければバグが見つからないのと同じことです。

安全性の検査、つまりトレースによる比較は次のように定義されていました。

一方、プロセス STOP のトレースは空列 () だけです。

どんなプロセスも、空列 () をトレースとして持っていますから、STOP はどんなプロセスに対しても条件を満たすことになります。

いま、トレースによる比較を、拒否も含めた正当性検査と同じように、次の記号で表すとします。

区別のために T をつけてあります。 すると、任意のプロセス P に対して次が成り立つことになります。

これを非決定的選択を使った定義に書き直すと次のようになります。ここでも区別のために T をつけてあります。

これは STOP が ⊓T の単位元であることを意味しています。 限量子のはなしを読んでくださった方にはちょっと驚きの結果かもしれません。 トレースがプロセスを識別する能力が弱いからこんなことになるんですね。

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