J78 j IEICE 2000 1 最近の更新履歴 Hideo Fujiwara J78 j IEICE 2000 1

論 文

情報基礎理論ワークシ ョップ（LAシンポジ ウム ）論文小特集

共有 メモリマルチプ ロセッサシ ステムに おけ る同期時間最適な

無待機時計合せプ ロト コル

守屋 宣

井上美智子

増澤 利光

藤原 秀雄

Optimal Wait-Free Clock Synchronization Protocol on a Shared-Memory

Multi-Processor System

Sen MORIYA^†, Michiko INOUE^†, Toshimitsu MASUZAWA^†, and Hideo FUJIWARA^†

あらまし 共有 メモリマルチプ ロセッサシ ステム，特に ，シ ステム内のすべてのプ ロセッサが 大域パル スを共 有するフェーズ 内シ ステムに おけ る故障耐性をもつ時計合せプ ロト コルを 考察する．フェーズ 内シ ステムでは ， 正常なプ ロセッサは パル ス発生時に 同期し て動 作を 行 う．フェーズ 内シ ステムに おいて ，パル ス発生時にプ ロ セッサが 動作し ないような故障を居眠り故障と呼ぶ．居眠り故障の起こるフェーズ内シ ステムに おいて ，同期時 間と呼ばれ るある特定パル ス以上正常に 動作し 続けているすべてのプ ロセッサ同士の局所時計の時刻を一致させ るプ ロト コルを無待機時計合せプ ロト コルと呼ぶ．これ まで ，フェーズ 内シ ステムに おけ る無待機時計合せプ ロ ト コルとし て，同期時間_4n²₋3n − 1 のプロトコルが提案されていた（ n:プロセッサ数）．本論文では ，同期時 間12n の無待機時計合せプ ロトコルを提案する．また，無待機時計合せプロトコルの同期時間の下界が n − 1 であることを証明し ，本論文で提案するプ ロト コルが 同期時間に 関し てオーダ 的に 最適であることを示す．

キーワード 共有 メモリマルチプ ロセッサシ ステム，時計合せプ ロト コル ，故障耐性，無待機性，同期時間

1. ま え がき

マルチプ ロセッサシ ステムにおけ る重要な問題の一 つに ，プ ロセッサ間の同期を実現することがある．プ ロセッサ間の同期をとるための手段とし て ，大域時計 が よく用いられ る．し かし ，全プ ロセッサが 共通の一 つの 時計を参照する方法では ，その時計が 故障すれば ど のプ ロセッサも大域時計を利用できな くなるという 欠点が あ り，シ ステ ム全 体の 信 頼 性は 低い ．そこで ， 各プ ロセッサが 個別に 時計を実現し ，これらの時計を 同期させ ると い う方法が 提案され て いる_[1]∼_[4]．こ の方法では ，各プ ロセッサが 個別に 時計を実現するた め ，一部のプ ロセッサが 故障し ても正常なプ ロセッサ 間で 時計を同期するように実現するといった故障耐性 を もた せ ，信頼性を 上げ ると い うことが 考えられ る ． このような状況で ，各プ ロセッサが 管理する局所時計 を同期させるプ ロトコルを時計合せプ ロト コルと呼ぶ．

故障プ ロセッサが 存在するシ ステムにおけ る時計合

†奈良先端科学技術大学院大学情報科学研究科 ，生駒市

Graduate School of Information Science, Nara Institute of Science and Technology, Ikoma-shi, 630–0101 Japan

せ問題は多くのアプ リケーションにとって重要であり， また それ 自 体も 興 味 深い 問 題で あ る ．時 計 合せ 問 題 は ，これ まで 様々なモデルのもとで ，様々な結果が 示 され てい る（_{[1], [2]}など ）．本論文では ，各プ ロセッ サが 共通の大域パル スを共有するフェーズ 内シ ステム

（in-phase system^{）（ 図}1）に おけ る時 計 合せプ ロト コルを考察する．故障プ ロセッサが 存在するフェーズ 内シ ステムのもとでの 時計合せプ ロト コルは ，_Dolev らによって提案された_[3]．_Dolevらは ，プ ロセッサの 故障とし て任意時間動作を停止し た後に 動作停止に 気 づかずに 動作を 再開するという居眠り故障（_napping

fault）を対象とし ている．彼らのプ ロトコルは ，ある

定数_kに 対し ，以下の 二つの 条件を 保証する．_{(1) k} パル スの間，正常に 動作し 続けたプ ロセッサは ，それ 以降正常に 動作し 続け る限り，局所時計の値は 各パル スで₁ず つ増え る．_{(2) k}パル スの間 ，正常に 動作し 続け た 二つのプ ロセッサの 局所時計の 値は 一致する ． このプ ロト コルは ，各プ ロセッサは 少な くと も _k パ ル ス 動 作し 続け れば 他のプ ロセッサの 動 作に か か わ ら ず 局 所 時 計の 値を 一 致させ るこ とが で き ると い う 意味で ，無待機時計合せプ ロト コル（wait-free clock D– Vol. J83–D– No. 1 pp. 99–109 2000 1 99

図1 フェーズ内システム Fig. 1 In-phase system.

表1 フェーズ内システムにおける無待機時計合せプロト コル

Table 1 Wait-free clock synchronization protocols on an in-phase system.

同期時間

上界 下界

Dolev ら [3] 16n²+ n − 1 Papatriantafilou ら [4]⋆ 4n²−3n − 1

本論文 12n ⁿ−1

⋆ 自己安定無待機時計合せプ ロトコル

synchronization protocol）と 呼ば れ る ．ここで ，定 数_kを同期時間（synchronization time^{）と呼ぶ．無} 待機時計合せプ ロト コルでは ，居眠り故障を起こすプ ロセッサも _kパル ス正常に 動作し 続ければ 局所時計 を同期させ ることができ，また，任意個のプ ロセッサ が 居眠り故障を起こす場合でも故障プ ロセッサの動作 に 影響され ることなく局所時計を同期させ ることがで きる．

過去に 提案され たフェーズ内シ ステムにおけ る無待 機時計合せプ ロト コルを表₁に 示す．_Dolevらは ，同 期時間_16n²_{+ n − 1}（_n:プ ロセッサ数 ）の無待機時計 合せプ ロト コルを提案し た_[3]．また ，任意の初期シ ス テム状況から開始する実行においても大域時計を実現 する自己安定無待機時計合せプロトコルとして，_Dolev らは 同期 時間 _8n³_{+ n − 1}の 自己安定無待機 時計合 せプ ロト コルを提案し た_[3]．また ，Papatriantafilou らは ，同期時間_4n²_{− 3n − 1}の自己安定無待機時計 合せプ ロト コルを提案し た_[4]．本論文では ，同期時間 12nの無待機時計合せプ ロト コル _{W CS}の提案をし ， プ ロト コル_{W CS} の同 期時間が オーダ 的に 最適であ ることを示す．

2. 諸 定 義

本章でシ ステムのモデ ル ，無待機時計合せ問題を定 義する．本論文で 用いるシ ステムのモデ ル ，無待機時 計合せ問題の定義は ，文献_{[3], [4]}のものと同じ である．

n 個のプ ロセッサか ら な る 共 有 メモ リ マル チプ ロ セッサシ ステムを考え る．プ ロセッサは 共有変数を介

し てのみ通信を行うことができる．共有 メモリマルチ プ ロセッサシ ステム_Sを_{S = (P, V)}で定義する．こ こで ，_P はプ ロセッサの 集 合 ，_Vは 共有変 数の 集 合 で あ る ．プ ロセッサは₀から _{n − 1}まで の 相 異な る 識別子をもつとし ，識別子_iのプ ロセッサを_Piと表 す．また ，各共有変数は ，所有者と呼ばれ るある₁プ ロセッサのみが 書込みをでき，すべてのプ ロセッサが 読出し をできるとする．各プ ロセッサは 状態機械とし てモデ ル 化され る．状態_sのプ ロセッサ_Piは ，以下 の₍₁₎から₍₂₎の動作を₁ステップ の操作とし て行い， 次の状 態_s^′ に 遷移する ．₍₁₎状態_sに より決定する プ ロセ ッサ_Pjが 所有するすべての 共有変数を読み出 す

（ 注1）

．₍₂₎状態_s と_Pjが 所有する共有変数の 値を もとに ，_Piが 所有する共有変数を更新し ，状態_s

′

に 遷移する．

本論文では ，フェーズ 内シ ステムと呼ばれ る同期式 マルチプ ロセッサシ ステムを 扱う．フェーズ 内シ ステ ムとは ，全プ ロセッサが 共通の大域パル スを共有する シ ステムであり，全プ ロセッサは 大域パル スを受けた ときに₁ステップ の動作を同期し て行う．ただし ，本 論文では 後で述べる居眠り故障を考慮し ，各パル スで 全プ ロセッサが 動作するとは限らないとする．シ ステ ム_S の 大域状況を ，全プ ロセッサと 全共有変数の状 態の組で 表す．以降，このシ ステムの 大域状況のこと を ，単に 状況という．シ ステムの 実行は ，状況と各パ ル スで動作し たプ ロセッサの集合の無限または有限交 代列_{E = c0π1c1· · ·}で表すことができる．ここで ，各 ctは 状況を 表し ，特に_c0 は 各プ ロセッサ，共有変数 の特定の初期状態からなる初期状況を表す．また ，_πt は_t番目のパル ス発生時に₁ステップ の動作し たプ ロ セッサの集合を表す．実行_Eは ，有限であるときはあ る状況_cendで 終わ る．この 実行 _Eは ，各_tに 対し ， πtに 属する各プ ロセ ッサが_ct−1 をもとに 同期し て₁ ステップ の 動作を 行い ，状況が _ct に なったことを 意 味する．また ，_t番目のパル スが 発生し た（ 大域 ）時 刻を時刻_tと呼ぶ．また，状況_ctでの変数_Pi.xの値 を_Pi.x(t)で 表す．

プ ロセッサ_Pi に ついて ，_{Pi ∈ π/ t} の と き ，_Pi は

（ 注₁）：実際的には ，各プ ロセッサに 対し 一つの 共有 メモ リセルが 割り 当てられており，各プ ロセッサは 自分のセルを複 数のフ ィールド に 分割 し て使 用する．プ ロセ ッサは 各共有変数をフ ィールド に 割り当て ること に より，所有す るすべて の 共有変 数が 一つのセル に 格納で き るとす る ． プ ロセッサ_Piは ，状態sにより決定するプ ロセッサ_Pjのセル の読出 し を 行 うこと に より，_Pjが 所有するすべて の 共 有変数を 読み出すこと ができる．

時 刻 _t で 居 眠 り 故 障し た ，ま た は 単 に 居 眠 りし た と い う．_Pi が 時 刻 _t で 居 眠 りし た な らば ，_Pi は 時 刻 _tで は 全 く 動 作 をし な い ．すな わ ち ，_ct−1 と _ct に おけ る _Pi の 状 態と _Pi が 所 有 す る 共 有 変 数 の 値 は 変わ ら な い ．シ ステ ム _S の 実 行 _{E = c0π1c1· · ·} に 対し て ，プ ロセッサ_Pi が 時 刻 _t まで 連 続し て 動 作し た パ ル ス 数 を _{work(Pi, t)} と 表 す．す な わ ち ， work(Pi, t) = max{l|Pi ∈
t−(l−1)<_=t^′<_=t^{πt′}で あ}

り，_{work(Pi, t) = u}のと き_Piが 区間[t − u + 1, t] で 居眠りす ることな く動作し 続け たこ とを 意味す る ． ただし ，_{Pi∈ π/ t} のと きは ，_{work(Pi, t) = 0}と 定義 する．

次に ，フェーズ内シ ステムにおけ る無待機時計合せ 問題を定義する．各プ ロセッサ_Piは ，_Piの局所時計 を 表す 共 有変 数 _Clock を もつと す る ．任意の 時刻_t に 対し ，_tまで 連続し て 動作し たパル ス数がある定数 以上であ るよ うな 任意のプ ロセッサ_{Pi, Pj} の 局所時 計の 値が 一致し ，以降_Piが 動作し 続け る限り局所時 計の値が₁パル スご とに₁ずつ増え ることを保証する プ ロト コルを無待機時計合せプ ロト コルとい う．

［ 定義₁］ある正整数_kに対し ，任意の実行が 次の二 つの条件を満たすようなプ ロト コルを同期時間_kの無 待機時計合せプ ロト コルとい う．

(i) ^{調整完了性（}Adjustment^{）：任意の} t >_{= 1,}^任 意のプ ロセッサ_Piに対し ，_{work(Pi, t) >= k + 1}なら ば ，_Pi.Clock(t) = Pi.Clock(t − 1) + 1^{が 成り立つ．}

(ii) ^{一 致 性（}Agreement^{）：任 意の} t >_{= 1,} ^任意の プ ロ セ ッサ_{Pi, Pj} に 対し ，_{work(Pi, t) >= k, work} (Pj, t) >_{= k} ^{な らば ，}Pi.Clock(t) = Pj.Clock(t)^が

成り立つ． _✷

3. 無待機時計合せプ ロト コル

本章で ，フェーズ 内シ ステムにおけ る同期時間_12n の無待機時計合せプ ロト コル_WCSを提案する．プ ロ セッサ_Piのプ ログ ラムを図₂に 示す．図₂では ，共

有変数を_Clockのように大文字で 始まる変数名で表す．

また ，各プ ロセ ッサの 状 態を 局所変数の 集 合で 表し ， 局所変数を_curのように小文字で始まる変数名で表す． 特に 変数_curは ，共有変数を読み出すプ ロセッサの識 別子を表す変数である．

3. 1 プ ロト コルW CS 3. 1. 1 全体の流れ

本プ ロト コルでは ，各プ ロセッサ_Piは 以下の 二つ のモード をもつ．

• ^{調整中モード （adjusting} mode^）

• ^{調整済モード （}adjusted mode^）

また，調整中モード は 三つのピ リオド ，準備ピ リオド

（_4nステップ ），調査ピ リオド（_nステップ ），調整ピ リオド（_nステップ ）から構成され る．初期状況では ， 全プ ロセッサが 調整中モード の 準備ピ リオド に いる ． 調整中モード にあるプ ロセッサ_Piは ，手続き_adjust に従って時計調整を行っていき ，やがて調査ピ リオド ， 調整ピ リオド へ移行する．調整ピ リオド において 手続 きcheck adjustedにより時計調整が 終了し たと 判定し たならば ，調整済モード へ移行する．調整済モード に あ るプ ロセッサは ，ステップご とに 局所時計の値を₁ ずつ増やす．また，プ ロセッサ_Piはすべてのステップ において_Pi自身及び 他のプ ロセッサの居眠りのチェッ クを 行 う（ 手続き_{check nap}）．時計調整を 始めてか ら 居眠りをし たプ ロセッサは ，調整中モード におけ る 時計調整を正し くできない，または ，調整済モード に おいて 正し い時計の値を維持できないことになる．そ こで ，自分の 居 眠りを 検知し た 場 合 ，プ ロセッサ _Pi は 手続きpartial resetを行い，準備ピ リオド の始めか ら 時計調整をやり直す．また ，他のプ ロセッサ _Pjの 居眠りを 検知し たならば ，共有変数を通し て_Pjに 知 らせる．

本プ ロト コルにおけ る時計調整のア イデアを図₃に 示す．プ ロセッサ_Piが 調整中モード で 時計調整を 開 始し てから次に故障を検知し てpartial reset^を行うま での区間を世代と呼ぶ ．各プ ロセッサは ，現在の世代 での ステップ 数を 表す共有変数_{Work count} を 使 う． 時計調整を開始し たプ ロセッサは ，現在の世代を自分 より早く始めたプ ロセッサを_{Work count}により調べ る．図₂に示すように，現在の世代を後から 始めたプ ロセッサは ，自分より早く始めたプ ロセッサの局所時 計だけをもとにし て時計調整を行う．

以下，調整中モード における手続き_adjustによる時 計調整の詳細について説明し ，次に手続き_{check nap} による居眠りのチェックについて説明する．

3. 1. 2 時計調整（ 手続き_adjust）

調 整 中モード に い るプ ロセッサは ，準 備ピ リオド ， 調 査ピ リオド で は 共 有 変 数の 読 出し が そ の 所 有プ ロ セッサの 識別子が 巡回する順序の繰返し になるように ステップ を 続け，調整ピ リオド ではプ ロト コルに 従っ て読出し の順序を変更する．調査ピ リオド で ，他のプ ロセッサが そのときの 世代を始めた時刻を調べる．調 整ピ リオド では ，自分より早く世代を始めた他のプ ロ

図2 プロトコル WCS Fig. 2 Protocol WCS .

図3 プロトコル WCS のアイデア Fig. 3 Idea of protocol WCS .

セッサの 局所時計と自分の局所時計を一致させる．ま た ，_4nステップ の 準備ピ リオド は ，調査ピ リオド で 他のプ ロセッサが 時計調整を始めた時刻を正し く調べ られ ることを保証するために 必要とする（ 補題₁）．

調査ピ リオド では，プロセッサ_Piは_Pj.W ork count により，_Piが 世代を始めた時刻に 対する，_Pjが その ときの世代を始めた相対時刻を調べる．ただし ，_Piが Pjの居眠りを検知したならば ，_Pjは遅くとも次に_Pi の共有変数を読み出すステップ でpartial reset^を行う ので ，_Pi は_Pj を 時 計調 整を 遅 く開 始し たプ ロセッ サとし て扱う．調整ピ リオド では ，その所有者が 時計 調整を始めた時刻の順に 共有変数を読み出す．その 順 序を知るため，調査ピ リオド の最後の ステップで 手続 き_{sort list}に より_Piより早く時計調整を始めたプ ロ セッサを 時計調整を開始し た時刻の順にソートし ，そ の結果を配列_listに 格納する．ただし ，同時刻に 時計 調整を開始し たプ ロセッサが 複数存在するならば ，識 別子に より 順 序を 付け る．_Pi より 早 く時計調整を 始 めたプ ロセッサがなければ ，手続きcheck adjust^によ り，この ステップ で _Piは 調整ピ リオド に 入ることな く調整済モード へ移行する．

調整ピ リオド では，_Piはまず最も早く時計調整を始 めたプ ロセッサ，すな わ ち_listの 先頭に あ るプ ロセッ サの 局所時計に 自分の時計を合わせる．その後，原則 とし て_listの順に ，_Piより早く時計調整を始めた他の プ ロセッサの局所時計と自分の局所時計が 一致し てい ることを確認し ていく．調整ピ リオド のステップ は 以 下のよ うに 行う．以下では ，その ステップ で 読み出す 共有変数の所有者を_Pjとする．

• Pi^がPjの 居眠りを 検知し たとき，または_Pj が 自身の居 眠りを 検知し たと きは ，_Pj の 局所時計に 合わせることも，一致確認もし ない．次の ステップ で は_listの次のプ ロセッサの 共有変数を 読み出す．この とき，_Piは_Pjの時計を無視すると呼ぶ（₆₈行 ）．

• Pjが まだ調整中モード のときは ，今回のステッ プ では_Pjの局所時計に 合わせない，または一致確認 をし ない．次のステップでも再び _Pjの読出し をする．

• Piがこれ まで局所時計を合わせた，または一致 確認し たプ ロセッサが 信頼できないと 判断し たら ，現 在の局所時計を棄却し（₈₁行 ），_Pjの局所時計に合わ せる．このために ，局所時計を合わせた ，または 一致 確認し たプ ロセッサ集 合を 表す _Sync,無視または 棄 却をし たプ ロセッサの 集合_Asyncを使う．

• Pi^とPjが ，現在の世代で ，共通のプ ロセッサ

Pmの局所時計に 合わせた，または 一致確認し ている にもかかわらず，両者の局所時計が 一致し ないならば ， Pi^はpartial resetを行い時計調整をやり直す．

プ ロセッサ_Piは ，_Piより早く時計調整を始めたす べてのプ ロセッサ，すな わ ち配 列_listに おいて _Pi よ り前にあるすべてのプ ロセッサの局所時計に 対し ，合 わせる，一致確認をする，または 無視し たとき，手続 きcheck adjust^によりPiは 調整中モード から 調整済 モード に移行する．プ ロトコル_WCSは，現在の世代の 時計調整を始めてから_Piが居眠りすることなく動作し 続けている場合は ，_Pi.Work count = 6n^{に 達する前} に 調整中モード から 調整済モード へ移行することを保 証する（ 補題₄で証明 ）．そこで，調整済モード へ移行 することな く_Pi.Work count = 6n^{に 達するならば ，} Piが居眠りし ていたことになり，partial reset^を行い 時計調整をやり直す．以降，この場合のpartial reset を時間超過リセット，他の場合，すなわち先に 述べた 場合と 後で 述べ る手続き _{check nap}に よる場合を 居 眠りリセットと呼んで 区別する．

3. 1. 3 居眠りのチェック（ 手続き_{check nap}） 各プ ロセッサは ，初期状態からのステップ 数を表す 共有変数Count（ 初期値₀）を使う．また ，新し い世 代の時計調整を開始するたびに更新する共有変数_Gen

（ 初期値₁）をもつ ．_{Gen = g}の間の時計調整を ，世 代_gの時計調整と呼ぶ．

プ ロセッサ_Piが_Pjの共有変数を読み出すステップ に おいて ，前回の _Pj の共有変数を読み出し た ステッ プ からの_{Pi.Count, Pj.Count}の増分の差（ 図₂，第 38^行，dif f^{で 表す ）により，}Pi^{は 自身または}Pj^が

居眠りし ていたことを判定する．_Piが_Pjの居眠りを 検知し たならば（ 第₄₀行の 条件式が 成立 ），_Pj.Gen の値を_Piの変数_Invalidjに代入することにより，_Pi は_Pjの居眠りを_Pjに 知らせる．_Piは 自身の居眠り を検知し たときに_Pi.Work count >_{= n}^{ならば（ 第}42 行または 第₄₃行の条件式が 成立 ），partial reset^を行 う

（ 注2）

．プ ロセッサ _Pi が 居眠りをし たならば ，複数 のプ ロセ ッサと の_Countの増 分差の比較に おいて _Pi が_Pi 自身の 居眠りを 検知し 得る．このような居眠り 検知の 重複を 避け るため ，_Pi.Work count >_{= n}^{を 条}

（ 注2）：手 続きcheck napは 完全に 居眠りを 検知で きるわけではな い． 例えば ，すべてのプ ロセッサが 同時に同期間居眠りを するような 場合は ， ど のプ ロセッサも居 眠りをし なか ったかのよ うに動作を 継続する．し か し ，プ ロト コル_WCSが 正当であるために 十分な 居眠り検出は 行ってい る．

件とし ている．

3. 2 W CS の正当性

プ ロト コル_WCSが 同期時間_12nの無待機時計合せ プ ロト コルであることを 示す．本論文では ，一部の補 題に 関し ては 証明を 省略する ．詳細は 文献_[5]を 参照 され たい．

同 期 時 間 を ，プ ロ セッサ が 居 眠 り を し て か ら partial resetを行うまでのステップ 数と，時計調整を 始めてから（ 初期状態またはpartial reset^{を行ってか} ら ）調整済モード へ移行するまでのステップ 数に 分け て 考え る．プ ロト コル_WCSでは ，調整ピ リオド での n回の ステップ 後も調整中モード から 調整済モード へ 移行し ないならば ，_Pi.Work count(t^′− 1) = 6n − 1 なる時刻_t

′

で 時間超過リセットを行う．補題₄では ， 調整中モード のプ ロセッサが 時計調整を始めてから 居 眠りをし ていない，かつ居眠りリセット を行わないな らば ，_Pi.Work count (t^′− 1) = 6n − 1^{な る時刻}t^′ までに 調整済モード へ移行することを示す．補題₇で は ，調整済モード の二つのプ ロセッサが 十分長く居眠 りすることなく動作し 続けているならば ，両者の局所 時 計の 値が 一 致するこ と を 示す．補 題₈では ，プ ロ セッサが 居眠りをし てからpartial reset^{を行うまでの} ステップ 数がたかだか_6nであることを示す．補題₉， 10で ，任意の実行に対し 調整完了性と一致性が 成り立 つことを示す．

時計調整を始めた時刻の前後関係を表すため，_{ti< tj} または_{ti= tj∧ i > j}ならば ，_{(ti, i) ≺ (tj, j)}と定義 する．また ，_{(ti, i) ≺ (tj, j)}または_{(ti, i) = (tj, j)}な らば ，_{(ti, i) (tj, j)}とする．プ ロセッサ_Piの時刻_ti の 手 続き_{sort list}に おいて ，list[p] = j,list[p^′] = j^′ なるプ ロセッサ_Pj,Pj′ に対し _{p < p}^′が 成り立つなら ば ，_Pj−→

i

t_iPj′ ^と記す．

手続き_{sort list}のソート の結果に関し て以下の補題 が 成り立つ．

［ 補題₁］任意の時刻を_tとする．区間[t+2n+1, t+ 5n]において，三つのプ ロセッサ_Pj

1, Pj2, Pj3^は正常

に 動 作し 続け，か つpartial resetを 行わな いと す る ． また ，_{(t1, j1) (t2, j2) ≺ (t3, j3), t1} >= t + 4n + 1 か つ _t3 <_{= t + 5n}で あ る時刻_{t1, t2, t3}で ，それぞ れ Pj1, Pj2, Pj3 ^{が 手続きsort listを行ったとする．この}

とき，_Pj

2−→^j_t³₃Pj3 ^{ならば ，}Pj^′−→^j_t1¹Pj1 ^{な るすべ}

ての_j

′

に対し ，_Pj′−→

j3

t3^{Pj2またはPj3−→} j3 t3^Pj′が

成り立つ． _✷

steps(Pi, t^′, t)を 以下のよ うに 定義する ．_t

′_{< t}

の

と き ，区 間 _[t

′_{, t − 1]}

で の ステップ 数と す る ．また ， t^′ = t ^{の と き は} steps(Pi, t^′, t) = 0 ^{とし ，}t^′ > t の と き は _{−steps(Pi, t, t}

′₎

と 定 義 す る ．こ の 定 義 よ り，任 意 の _{t1, t2, t3} に 対し て _{steps(Pi, t1, t2) +} steps(Pi, t2, t3) = steps(Pi, t1, t3)^{が 成り立つ．プ ロ} ト コル より，_{steps(Pi, t}

′_{, t)}

に 対し ，以下の事実が 成 り立つ．

［ 事実₂］任意のプ ロセッサ_{Pi, Pj}と 時刻_tに 対し ， steps(Pi, t^′, t)が 以下を満たすような時刻_t^′が存在す るならば ，_Piは 区間_[t^′_{, t − 1]}のある時刻で_Pjが 所 有する共有変数を読み出すステップ を行っている．

(a) n <_{= P}i.W ork count(t − 1) <_{= 5n}^または7n <₌ Pi.W ork count(t − 1)^{ならば ，}steps(Pi, t^′, t) = n

(b) 5n < Pi.W ork count(t − 1) < 7n ^{な ら ば ，} steps(Pi, t^′, t) = 2n

(c) Pi.W ork count(t − 1) < n ^{な ら ば ，}steps

(Pi, t^′, t) = 3n − 1 _✷

Pi^{が 世代} gの 調整ピ リオド での ステップ 数，すな わち，時刻_tで_{sort list}を行った後，partial reset^を 実行するか 調整済モード へ移 行する時刻_t^′ まで の ス テップ 数_{steps(Pi, t + 1, t}^′_{+ 1)}を_{α(Pi, g)}と記す．

補 題₃，₄ で は ，以 下に 示す 条 件_Aを 満た すプ ロ セッサ _Piを考え る．

 条件_A： _Pi が 時 刻 _t で partial reset^{を 実 行し ，} work(Pi, t + 6n) >_{= 6n}^かつ[t, t + 6n]^{で居眠りリセッ} ト を行わない．

条 件_Aを 満た す _Pi に 対し ，_{α = α(P¯ i, Pi.Gen(t))} とする．このと き，世代 _Pi.Gen(t)の時計調整で _Pi が 時 間 超 過 リセット を 行 うな らば ，時 刻 _{t + 6n} で partial reset^{を 行うので} α = n¯ が 成り立つ．よって ，

¯

α < nが 成り立つならば ，_Piが 時刻_tまでに 調整済 モード へ移行する．

条 件_Aを 満た すプ ロセッサ _Piが 調 整ピ リオド に い る 区 間 [t + 5n + 1, t + 5n + ¯α]に 属 す る 各 時 刻 s ^{に 対し ，}2種 類のプ ロ セッサ _{readers, dests} を 以 下の よ うに 時 刻 _{t + 5n + ¯α}か ら 再 帰 的に 定 義 す る

（ 図₄）．まず，_{readert+5n+ ¯α= Pi}とする．時刻_sで readersが 読み出す共有変数の所有者を_destsと定義 する ．_{readers, dests}(t + 5n + 2 <_{= s <}= t + 5n + ¯^α) に 対し ，_readers が 時 刻_sと _{s − 1}で 同じ プ ロセッ サ の 共 有 変 数 の 読 出し を す る な ら ば _{readers−1 =} readers と 定 義し ，異 な る 共 有 変 数 の 読 出し を す るな らば _{readers−1 = dests} と 定 義 す る ．こ こ で ， dests (t + 5n + 1 <= s < t + 5n + ¯^{α) の リ スト}

図4 プロセッサ，時刻の定義 Fig. 4 Definitions of processors and times.

dlist = destt+5n+1, destt+5n+2, · · · , destt+5n+ ¯α ^{を ，}

readersが 同一でありかつ連続するように 分割し た極

大部分 リスト_dlist¹_{, dlist}², · · · , dlist^{hを 考え る．各} x(1 <_{= x <= h)}^{に 対し ，}dlist^{x で 共 通の} readers ^を

Pi_x, dlist^x= dests_x, dests_x+1, · · · , dests^′_x^{とし ，}Pi_x

が 世代_Pix.Gen(s

′

x− 1)^においてsort list^{を行うなら} ば ，その時刻を_{sort time}^xとする．ここで ，以下の 補題が 成り立つ．

［ 補題₃］すべての _{x(1 <= x <= h)}に 対し ，以下が 成 り立つ．

(a) dlist^xの要素はすべて 異なる．

(b) Pix ^{は 区間}[t + 2n + 1, s^′x− 1]^{で 居眠りをし} ない．

(c) x < h ^{な ら ば，}(t + 4n + 1, 0) (sort time^x, ix) ≺ (sort time^x+1, ix+1)

(^証明) ^すべての x(1 <_{= x <= h)}に 対し て 条件が 成り 立つことを_{x = h}の場合から 帰納的に 示す．

ま ず，_{x = h} の 場 合に 条 件_(a)，_(b)が 成 り 立 つ こ と を 示 す．定 義 よ り，_{Pix = Pi} で あ る ．ま た ， work(Pi, t + 6n) >_{= 6n}^より区間[t + 2n + 1, s^′_h− 1] で 居眠りし て いな い ．_Piは _{[sh, s}

′

h^{]で 調整ピ リオド}

に あ る の で ，こ の 区 間 で は _list の 順に 共 有 変 数 を 読 み 出し て い る ．し た が って ，_dlist^h は _dests

h ^と

dests_h−→ⁱ_{sort time}^h _h Pm−→ⁱ_{sort time}^h hPi ^{な る す べ}

ての_Pmからなり，_dlist

h

の要素はすべて 異なる． 次に ，x + 1, · · · , h^{に 対し て 条件}(a)^，(b)^，(c)^が 成 り 立 つ な らば ，_x に 対し て 条 件_(a)，_(b)，_(c)が

成 り 立 つ こ と を 示 す．まず，_(b)が 成 り 立 つ こ と を 示す．定 義より，_{Pix = destsx+1} で あ る ．_Pix+1 は 時 刻_s

′

x^{, s}x+1 ^{で 連 続し て} Pix の 共 有 変 数 を 読 み 出 す．こ こ で ，_Pi

x+1 ^{は 時 刻 s}

′

x で 調 整ピ リ オド に い る の で_Pi

x+1.W ork count(s^′x− 1) >_{= 5n} ^{で あ り，} (sort time^x+1, ix+1) (sort time^h, ih)^{が 成り立つ} ので ，2n + 1 <_{= P}i_x+1.W ork count(t + 3n) <_{= 3n}^が 成り立つ．よって，事実₂より区間[t + 2n + 1, t + 3n] に _Pi

x+1^がPix の 共 有変数を 読み 出す ステップ が 存 在する．_{[t + 3n, s}^′_{x− 1]}で_Pixが 居眠りをし ている ならば ，遅くとも時 刻 _s^′_x までに _Pi

x+1 ^{が Pi}x ^{の 居}

眠りを 検 知す るか ，時 刻_s

′

x− 1 ^{まで に} Pi_x ^{が 自 身}

の 居 眠りに 気づ いて 次世代の 時計調整を 始めている ． また ，_Pi.W ork count(t + 2n) = 2n ^{が 成 り 立 つの} で ，事実₂より区間[t + n + 1, t + 2n]^にPi^がPix

の 共 有 変数を 読み 出す ステップ が 存在する ．よって ， [t + 2n + 1, t + 3n − 1]^でPi_xが居眠りをしているなら ば ，_Piに必ず検知され る．時刻_s

′

x− 1^でPix^は調整

ピ リオド に あるので ，_Pix.W ork count(t + 5n) >_{= n} が 成り 立 ち ，事実 ₂より [t + 3n + 1, t + 5n]^で Pi

の共有変数を 通し て_Pi

x が 自身の居眠りを 検知する． よって ，時刻_sx+1では _Pix 以外のプ ロセッサの 共有 変数を読み出すので ，矛盾する．よって ，_Pixは 区間 [t + 2n + 1, s^′_x− 1]で居眠りをし ていない．すなわち， (b)^{が 成り立つ．}

また ，時刻 _s^′_{x− 1} で _Pi

x は 調 整 中モード に い る こ と よ り_Pix.W ork count(s^′x− 1) < 6n^{が 成り 立} つので_{sort time}

x _>

= t + 4n + 1 が 成 り 立 つ ．区 間 [t + 4n + 1, sort time^x+1]^でPix^{, P}i_x+1^{はともに 居}

眠りし て いな いので ，_{Pix −→}

i_x+1

sort time^{x+1 Pix+1 よ}

り，_{(sort time}^x_{, ix}) ≺ (sort time^x+1, ix+1)^{が 成り} 立つ．すなわち，_(c)が 成り立つ．

(sort time^x, ix) (sort time^h, ih) ^{が 成 り 立 つ} の で ，区 間 _{[sx, s}

′

x^{] で P}ix は 調 整 ピ リ オド に あ る．よって，_dlist^xは_destsx と_destsx−→

i_x sort time^x

Pm−→ⁱ_{sort time}^x xdests^′_x ^{な るプ ロセッサ} Pm^{か ら な}

り，_dlist

x

の 要素は すべて 異な る．すなわ ち，_(a)が

成り立つ． _✷

［ 補題₄］条件_Aを満たすプ ロセッサ_Piは時刻_t+6n までに 調整済モード へ移行する．

(^証明) ^すべてのs (t + 5n + 1 <_{= s <}= t + 5n + ¯^α)の間 で_destsが 異なり，かつ_destsとし て_Piが 現れない ことを示すことにより，_{α < n¯} が成り立つことを示す．

h = 1^{の場合，すなわち}dlist = dlist^{1 の場合，補}

題_{3 (a)}より_dlistの要素はすべて異なり，また_dlist に_Piが 現れない．し たが って ，_{α < n¯} が 成り立つ． 次に_{h > 1}の場合を考え る．補題_{3 (a)}より，任意 の_{x(1 <= x <= h)}に対し_dlist^xの要素がすべて異なる． 以下では ，任意の異な るx, y(1 <_{= x <}= h, 1 <= y <= h) に対し ，_Piが_dlist

x

に現れず，_dlist

x

と_dlist

y

に共 通 要 素が 現れ な い こ と を 示 す．補 題_{3 (b)}よ り，任 意 の x, y(1 <= x < y <= h) ^{に 対し ，Pix は 区 間} [t + 2n + 1, t + 5n]^{を 含 む区間}[t + 2n + 1, s^′_x− 1] で 正 常に 動 作し 続け て い る ．また ，補 題_{3 (c)}より， (t + 4n + 1, 0) (sort time^x, ix) ≺ (sort time^y, iy) が 成り立 つ ．し たが って ，_{Pj1 = Pix, Pj2 = Pi}

y−1^,

Pj3 ^{= P}iy^{, t}1 = sort time^x, t2 = sort time^y−1, t3 = sort time^y と 定 め た と き に 補 題 ₁ が 成 り 立 つ ．す な わ ち ，_Pj′−→

j1

sort time^xPj1 ^{な るプ ロ セ}

ッサ _Pj′ に 対 し て ，_Pj′−→

j3

sort time^yPj2 ^{ま た は}

Pj3−→^j_{sort time}³ yPj′^{が成り立つ．したがって，}dlist^x と _dlist

y

に 共 通 要 素 が 現 れ る こ と は な い ．ま た ， Pi = Pi_h ^{な の で ，補 題} 1 ^{よ り} Pi ^はdlist^{x に 現}

れない． _✷

プ ロト コル_WCSでは ，プ ロセッサは すべての 居眠 りを 検知するわけではない．よって，二つのプ ロセッ サ_Pi,Pjが 居眠りするタ イミングに より，_Piは「_Pj は_Piより後で時計調整を始めた 」と判定するときに ， Pj^が「Pi^はPjより後で 時計調整を始めた 」と 矛盾 し た判定をする場合がある．この場合，_{Pi, Pj}は互い に 局所時計を参照することなく調整済モード へ移行す ると考えられ る．し かし ，手続き_{sort list}のソート の 結果に 関し て以下の補題が 成り立ち，_{Pi, Pj}が 十分長 く動作し ているならば 両者が 矛盾し た判定をすること はない．

［ 補題₅］任 意の 時 刻を _t, 任 意の 異な るプ ロセッサ を _{Pi, Pj} と す る ．_{Pi, Pj} は それ ぞ れ 時 刻 _{ti, tj} で sort listを 行 い ，か つ ，そ れ ぞ れ 区 間 _{[ti, t], [tj, t]} で partial resetを 行 わ な か った と す る ．こ の と き ， work(Pi, t) > 4n ^{か つ} work(Pj, t) > 4n ^{な ら ば ，} Pj−→ⁱt_iPi^またはPi−→^jt_j^{Pjが 成り立つ．} ✷

手続き_adjustの説明で述べたように，プ ロセッサ_Pi が 自分の局所時計をある時刻_ti,jでプ ロセッサ_Pjの 局所時計に 合わせた ，または_Pjの局所時計と一致す ることを 確認し たあと ，_Piが _Pj の局 所時計を 棄却 することがある．し かし ，_ti,j 以降に_{Pi, Pj}がともに partial resetをすることなく動作し 続け るよ うな 場合 には 以下の補題が 成り立つ．

［ 補題₆］任意の異なるプ ロセッサ_{Pi, Pj}に対し ，あ る時刻_tで_{Pi, Pj}がともに 調整済モード であったと し ，_work(Pi, t) > 4n, work(Pj, t) > 4n^{が 成り立つ} とする．また ，時刻_ti,jで_Piは自分の局所時計を_Pj の局所時計に 合わせた ，または _Pjの局所時計と一致 することを確認し たとし ，区間_{[ti,j, t]}で_{Pi, Pj}はと もにpartial resetを行わないとする．このとき，区間 [ti,j, t]^でPi^はPjの局所時計を棄却し ない． _✷

［ 補題₇］任 意の 時 刻を _t, 任 意の 異な るプ ロセッサ を _{Pi, Pj} と す る ．時 刻 _t で _{Pi, Pj} が と も に 調 整 済モ ード で あった と す る ．こ のと き ，_{work(Pi, t) >} 4n, work(Pj, t) > 4n ^{な ら ば，}Pi.Clock(t) = Pj.Clock(t)^{が 成り立つ．}

(^証明) Pi, Pj^{は，それぞれ世代}Pi.Gen(t), Pj.Gen(t) の時計調整において，_{sort list}を行っている．_{Pi, Pj}が sort listを 行った 時刻をそれぞれ _{ti, tj} と すると 補題 5^よりPj−→ⁱt_iPi^またはPi−→^jt_j^{Pjが 成り立つ．一}

般性を失うことなく，_Pj−→

i

t_iPi^{と仮定する．このと}

き，_Piは 世代_Pi.Gen(t)のあ る時刻_t

′

で 自分の局所 時計を_Pjの局所時計の値と合わせるか，一致している ことを確認し ，区間_[t^′_{, t]}で_Pjはpartial reset^{を 行} わない．よって，_Pi.Clock(t

′_{) = P}

j.Clock(t^′− 1) + 1 が 成り立つ ．ここで ，補題₆より，区間_[t

′_{, t]}

で _Pi が_Pjの局所時計を 棄却することはない．また ，区間 [t^′, t]^でPi, Pj^はともにpartial reset^{をすることはな} いので ，それぞれ ステップご とに 局所時計の値を₁ず つ増やす．し たが って，

steps(Pi, t^′, t) = steps(Pj, t^′, t) (1)

で あ るこ と を 示せば よい ．こ こで ，_t^′ >= t − 4n + 1 ならば ，区間 _[t^′_{, t]}では _{Pi, Pj}は と もに 正常に 動 作 し 続け るので 明らかに 式₍₁₎は 成り立つ ．以下では ， t^′< t − 4n + 1^{の場合を考え る．}

事 実 ₂ よ り，区 間 [t − 4n + 1, t − n] ^{の あ る 時} 刻 _t^′′ で _Pi は _Pj の 局 所 変 数 を 読 出し す る ス テッ プ を 行って お り，また _t^′′_{(<= t − n)} よ り 後で_Pj は Pi の 局 所 変 数 を 読 出し す る ス テップ を 行って い る ． 区 間_[t

′_{, t]}

で _{Pi, Pj} は と もにpartial reset^{を 行わな} いので ，区 間 _[t

′_{, t}′′_]

の 各 ステップ で _Piが _Pi また は _Pj の 居 眠りを 検知す ることは な い ．し たが って ， steps(Pi, t^′, t^′′) = steps(Pj, t^′, t^′′)^{であ る．更に ，区} 間_[t,

′′_t]

では_{Pi, Pj}はともに 正常に 動作し 続け るの で_{steps(Pi, t,}

′′t) = steps(Pj, t,^′′t)^{が 成り立つ ．し} たが って ，式₍₁₎は 成り立つ． _✷

次の補題で ，居眠りをし てからpartial resetを行う までの ステップ 数を考察する．

［ 補題₈］プ ロセッサ_Piが 時刻_tでpartial reset^を 実行し たならば ，_work(Pi, t) < 6n^{が 成り立つ．} (^証明) Pi^は時刻t^でPjが所有する共有変数を読み出 すとし ，_tより前で最後に_Piが_Vjを読み出すステップ を行った時刻を_t

′

とする．時刻_tのpartial reset^{が 時} 間超過リセットならば ，補題₄より_work(Pi, t) < 6n が 成り立つ．時刻_tのpartial reset^{が 居眠りリセット} ならば ，以下の_(a)∼_(c)の条件式の うちいずれかが 成 り立つ．

(a) ^第42^行：Pi.W ork count(t − 1) >_{= n} ^{か つ} Pi.diff (t) < 0

(b) ^第43^行：Pi.W ork count(t − 1) >_{= n} ^{か つ} Pj.Invalidi^>_{= Gen}

(c) ^第74–75^行：Pi.Sync(t−1) ⊂ Pj.Async (t−1), Pj.Sync |= ∅^かつPi.Clock(t − 1) |= Pj.Clock(t − 1) (a)^，(b)^{が 成り立つ場合に} work(Pi, t) < 6n^{が 成り} 立つことは ，事実₂を用いて示され る．以下では ，_(c) が 成り立つ場合を考察する．

時刻_tで第₇₆行を行うことより_Pi.W ork count(t− 1) < 6n^{で あ り，}Pi.Sync(t − 1) |= ∅ ^{よ り} Pi ^は

5n <_{= P}i.W ork count(tm− 1) < Pi.W ork count(t − 1) ^{で あ る 時 刻} tm で ，調 整 済 モ ード の プ ロ セッ サ _Pm の 局 所 時 計 と 自 分 の 局 所 時 計 を 合 わ せ る か ，一 致し て い る こ と を 確 認し て い る ．こ の と き ， Pi.Clock(tm) = Pm.Clock(tm− 1) + 1^{が 成り立つ．} 以下では ，_{work(Pi, t) >= 6n}を仮定し て矛盾を導く．

Pi, Pj ^が t 以 前 で 最 後 に _{sort list}を 行った 時 刻 を そ れ ぞ れ _{ti, tj} と す る ．ま た ，_Pi が _t 以 前 で 最 後に partial reset を 行った 時 刻 を _t⁰_, す な わ ち W ork count(t⁰) = 0 と す る ．た だ し ，_t 以 前 に partial resetを行っていないならば ，_t⁰_{= 0}とする． work(Pi, t) >_{= 6n}^{か つ}Pi.W ork count(t − 1) < 6n よ り，_Pi は _[t⁰_{, t]} で は 居 眠 り す る こ と な く 正 常 に 動 作し 続 け る ．事 実 ₂ よ り，_[t⁰ _{+ 1, t}⁰_{+ n]} に Pi ^が Pj, Pm それ ぞ れ の 局 所 変 数 を 読 み 出 す ス テ ップ が 存 在 す る ．ま た ，_Pi は ，_tm よ り 前 で _Pm の ，_t よ り 前 で _Pj の 居 眠 り を 検 知し な い ．し た が って ，_{work(Pm, tm− 1) >= tm− t}⁰ − n > 4n, work(Pj, t − 1) > work(Pj, tm− 1) > 4n^{が 成り立} つ．以下，時刻_{tm− 1}での_Pjのモード に より場合 分けし て考える．

(c1) ^時刻tm− 1^でPjが 調整済モード の場合

補題₇より_{Pm.Clock(tm− 1) = Pj.Clock(tm− 1)} が 成り立つ．区間_{[tm, t − 1]}で_{Pi, Pj}が 居眠りする ことはないので ，_Pi.Clock(t − 1) = Pj.Clock(t − 1) が 成り立ち，_(c)に 矛盾する．

(c2) ^時刻tm− 1^でPjが 調整中モード の場合 Pi, Pj ^{は と も に} tm− 3n(> t − 4n) ^{以 降 の 各プ ロ} セッサの_{Work count} の値を もとに_{sort list}を 行 う． Pi, Pj, Pm^は[tm−3n, tm−1]で正常に動作し 続けるの で，_Pm−→ⁱ_t

i^{PjよりPm−→} j

t_j^{Pjが成り立つ．したが}

って，_Pjは世代_{Pj.Gen(t−1)}中のある時刻_t^′_mで_Pm の局所時計に自分の局所時計を合わせるか，_Pmと自分 の局所時計が 一致することを確認し ている．すなわち， Pj.Clock(t^′_m) = Pm.Clock(t^′_m− 1) + 1^{が 成り立つ．} Pm^は区間[t^′_m, tm− 1]^または[tm, t^′_m− 1]^{で正常に動} 作し 続け，_Pjは区間_[t^′_{m, t−1]}で正常に動作し 続ける． し たが って ，_{steps(Pj, t}^′_m, t) = steps(Pm, t^′m, tm) + steps(Pi, tm, t)^よりPi.Clock(t − 1) = Pj.Clock(t − 1)^{が 成り立ち，}(c)^{に 矛盾する．} _✷

［ 補題₉］（ 調整完了性 ） 任 意 の _{t >= 1,} 任 意 の プ ロ セッサ _Pi に 対 し ，_work(Pi, t − 1) >_{= 12n} ^な ら ば _Pi.M ode(t − 1) = “adjusted” ^{が 成 り 立} ち ，_work(Pi, t) > 12n ^{な ら ば} Pi.Clock(t) = Pi.Clock(t − 1) + 1^{が 成り立つ．}

(^{証 明}) ^{プ ロ セッサ} Pi ^が t − 12n 以 前 で 最 後 に 居 眠 り し た 時 刻 を _tn と す る と ，_tn 以 降 の 時 刻 t^{′ で} partial reset を 実 行し た 場 合 ，補 題 ₈ よ り， work(Pi, t^′) < 6n^{が成り立つ．よって，}work(Pi, t) >₌ 12n^{ならば ，}Pi^は時刻t−6n^以降にpartial reset^を行 うことはない．よって，_Pi.W ork count(t−1) >_{= 6n}^が 成り立ち，補題₄より_Pi.M ode(t − 1) = “adjusted” が 成 り 立 つ ．また ，_work(Pi, t) > 12n ^{な らば ，}Pi

は 時 刻 _t で 調 整 済 モ ード の ス テップ を 行 う の で Pi.Clock(t) = Pi.Clock(t − 1) + 1^{が成り立つ．}_✷

［ 補題₁₀］（ 一致性 ） 任意の_{t >= 1,}任意のプ ロセッサ Pi, Pj^{に対し ，}work(Pi, t) >= 12n, work(P^{j, t) >}= 12n ならば_Pi.Clock(t) = Pj.Clock(t)^{が 成り立つ．} (^証明) ^補題9^より，Pi.M ode(t − 1) = “adjusted” かつ_Pj.M ode(t − 1) = “adjusted”^{であ る．よって ，} 補題₇より_Pi.Clock(t) = Pj.Clock(t)^{が 成り立つ．}

✷

［ 定理₁₁］プ ロトコル_{W CS}は ，同期時間_12nの無 待機時計合せプ ロト コルである． _✷

また ，同期時間に 関し て以下の定理が 成り立ち，プ ロト コル_WCSの同期時間はオーダ 的に最適である．