分散アルゴリズム輪講３章通信プロトコル遠藤敏夫本章のプロトコル  (1) Balanced Sliding-window プロトコル直接つながれた2プロセス間でデータ列をやりとり  双方向  メッセージの消失がありうる通信路上で、信頼できる通信  OSIモデルのデータリンク層に相当  (2) Timer-based プロトコル (間にノードが挟まっているかもしれない)2プロセス間でデータ列をやりとり  単方向  通信チャネルの概念あり  メッセージの消失や複製がありうる通信路上で、信頼できる通信  OSIモデルのトランスポート層に相当メッセージを送りつけるだけではダメ  プロセスpからプロセスqへデータ列w0, w1, w2...を送信消失!! <6,w6> 送信ユーザ   通信プロセスp <5,w5> 通信プロセスq qに一部メッセージが届かない問題 pがそのことに気づかない問題受信ユーザ予備知識: Acknowledgement  通信プロセスp 通信プロセスq <data,1,w1>  <ack,1> <data,2,w2> <data,2,w2> <ack,2> ×  qにdataメッセージが届いたら、 pにackを返信 pにackがしばらく届かなければ、再送再送も失敗する可能性はあるが、「失敗した」とpが認識できることが重要プロトコルが満たすべき性質とは？   受信プロセスに届いたデータは正しい (safety property) データは受信プロセスにいつかは届く(かつ送信プロセスが認識)、またはエラーを送信プロセスが認識 (liveness property)   3.1 The Balanced Sliding-window Protocol 3.2 A Timer-based Protocol Balanced Sliding-windowプロトコルの概要(1)    2プロセスp, qが双方向に送信無限列のデータを、互いに歩調を合わせながら送信メッセージが消失、順番入れ替わりするかもしれない通信路を利用配列inp 配列inq 配列outp 配列outq 通信プロセスp 通信プロセスq Balanced Sliding-windowプロトコルの概要(2) 0以上の適当な定数lp, lqを用意(いわば歩調の「余裕」)  プロセスpはi番目データを<pack, inp[i], i>の形のパケットとして送信。ただし、outp[0..i-lp]がすでに受信済みであるときのみ  プロセスqが<pack, inp [i], i>を受け取ったとき、qは inq[0..i-lp]の送信がすでに成功したことを知る   つまり、 <pack, inp [i], i> は<pack, inq[i-lp], i-lp>に対するAck の役割を果たしている p, qを入れ替えても同様 Balanced Sliding-windowプロトコルが満たすべき性質  安全な配達: spが、pがこれからqから受け取るデータ番号の最小値であるとき、(sqも同様)  outp[0..sp-1]=inq[0..sp-1]かつ  outq[0..sq-1]=inp[0..sq-1]  いつかは配達:  任意のk≧0に対して、いつかはsp ≧kかつsq ≧k 変数の説明プロセスpが持つ変数  定数lp, lq (前述)  入力データinp[]  出力データoutp[]: 初期値は全要素とも‘udef’  sp: まだqから受け取っていないデータ番号の最小値。初期値0  ap: まだqからackを受け取っていないデータ番号の最小値。初期値0 プロセスqも同様 Balanced Sliding-windowプロトコル Algorithm 3.1  アクションSp(送信): sp+lp未満の番号のデータのみを送ることができる  アクションRp(受信): パケットを受け取ったら、必要に応じてsp, apを更新  アクションLp(消失): p宛てのパケットのどれかが消えるかもしれない  ただし、Qpはp宛てのパケットの集合 Balanced Sliding-windowプロトコルが満たす不変条件 P i  s p : outp [i ]  udef (0 p )  i  sq : outq [i ]  udef (0 q ) (1 p )   pack, w, i  Q p  w  inq [i ]  (i  sq  lq )   pack, w, i  Qq  w  in p [i ]  (i  s p  l p )  outp [i ]  udef  outp [i ]  inq [i ]  (a p  i  lq )  outq [i ]  udef  outq [i ]  in p [i ]  (aq  i  l p )  a p  sq  aq  s p  (1q ) (2 p ) (2q ) (3 p ) ( 3q ) Lemma: Pはどんなconfiguration(=pの状態+q の状態+Qpの状態+Qqの状態)に対しても成り立つ不変条件の証明の方針帰納法で証明  初期configurationに対してPは成り立つ  あるconfigurationに対してPが成り立つとき、そこから遷移したconfigurationに対してはどうか？ Lp Sq Lq Sp Sq Sp Sq Rp 不変条件の証明の一部 (2p)に注目。あるconfigurationでPが成り立っているとき、  SP: SPはoutp, apを変更しないので、SPによる遷移後も (2p)が成り立つ  Sq ,Rq, Lp, Lqも同様  Rp: Rpはoutp[i]の値をudefからwに変えうる(<pack,w,i> 受信時)。このパケットはRp適用前にはQpにあったので、(1p)よりw=inq[i]。  ap:=max(ap,i-lq+1)はap>i-lqを満たす。以上よりRpは(2p)を保存する。  Pを使ってうれしいこと(1) 「安全な配達」が成り立つ証明: (0p), (2p), (0q), (2q)より。 Pを使ってうれしいこと(2) 「いつかは配達」を証明するには仮定が必要  lp+lq>0  通信路が全く通じないと困る   あるパケットの送信actionが無限に長い時間適用可能なら、無限の頻度で(infinitely often)送信される同一パケットが無限の頻度で送信されるなら、無限の頻度で受信される Pを使ってうれしいこと(3) 「いつかは配達」の証明の概略  Pが成り立つとき、pによる<pack,inp[sq],sq>の送信、もしくはqによる<pack,inq[sp],sp>の送信のいずれかは適用可能である  前の仮定より上のパケットはいつか相手に届く  相手に届いたとき、sqかspのどちらかが増加する定数lp, lqの選び方について lp, lqは通信プロセスが使うメモリ量に影響   pはinp[]のap以前の部分にアクセスしない⇒ある時点でアクセスしうるinp[]の要素はlp+lq個以内 outp[]の要素がudef以外なのはsp+ lp+lq番目以下⇒通信プロセスが持っておくべきoutp[]の要素はlp+lq個以内必要メモリ量は2(lp+lq)で、lp, lqが小さいほどメモリ節約。一方、小さすぎると通信オーバラップができず、性能低下   3.1 The Balanced Sliding-window Protocol 3.2 A Timer-based Protocol Timer-basedプロトコルの概要   単方向接続(connection)オープン・クローズあり   接続をクローズしたら、その情報を捨ててよいタイムアウトあり   時間の概念利用一定時間以内に、送信ユーザに「送信成功」「送信失敗」のいずれかを知らせるタイマータイマーは実数変数  時間がxたつと全タイマーの値がx減る説明の上では大域時間の存在を考えるが、プロセス自体は大域時間にアクセスせず、局所的なタイマーのみを使う  t1=50 t2=40 時間30経過 t1=20 t2=10 本プロトコルで使われるタイマー (1) 時間切れパケットは消失 accept St deliver Rt 成否報告 Ut[] 通信プロセスq 受信ユーザ送信ユーザ通信プロセスp 本プロトコルで使われるタイマー (2)  送信プロセスp:   接続タイマーSt。一定時間(S)送信できなければ接続切断各送信データのタイマーUt[] 一定時間(U)送信できなければ、または  一定時間Ackが返ってこなければそのデータの送信は失敗したと見なす   受信プロセスq:   接続タイマーRt。一定時間(R)受信できなければ接続切断通信路:  各パケットのタイマーρ。受信前に一定時間(μ)が過ぎたパケットは消失する Timer-based プロトコルが満たす性質  No loss: 各データはaccept後、一定時間以内に  qが受信ユーザにdeliver  pが送信ユーザにエラー報告のいずれかが成される (両方成されてしまう可能性はある)  Ordering: qがdeliverするデータの番号は単調増加変数の説明変数: Figure 3.3に加え、  送信側変数    inp[]: 送信データ列 Ut[]: 各データのタイマー errorp[]: 各データの送信成否パケットの説明  pからqへのパケット <data,s,i,w,ρ>      s: start-of-sequenceビット。1のときオープン要求 i: データ番号 w: データ ρ: タイマー qからpへのパケット <ack,i,ρ>   i: データ番号 (i未満は受け取ったよ、の意) ρ: タイマー Timer-basedプロトコル    Algorithm 3.4: 送信側プロトコル Algorithm 3.5: 受信側プロトコル Algorithm 3.6: その他 Timer-basedプロトコルが満たす不変条件  配布資料参考  これらを満たすためには、 R≧μ+U  S≧R+2μ である必要    Ok(i)≡(error[i]=true)∨(qがi番目データをdeliver済み) pr=qが最後にdeliverしたデータ番号不変条件の説明(ごく一部)(1)  (6) 受信側qで接続中なら送信側pでも接続中であり、St≧Rt+μ(送信側の方が長生き)   Rqで受信側タイマーがRに更新される。近い過去(μ以内)において送信側タイマーがS(≧R+2μ)に更新されているはずなので。 (7) ackが通信路にあるとき、pで接続中であり、 ackよりpの接続の方が長生き  Sqでack(タイマー値μ)が送信された時点において Rt≧0である。このときSt≧μなので。不変条件の説明(ごく一部)(2)  (10) B+Low以下のiについてOk(i)  Lowが増え得るのはRp(Ack受け取り)かEp(タイムアウト)である。前者のときはdeliver済み((13)より)なのでok, 後者のときはerror(i)=trueとなるのでok Timer-basedプロトコルはNo lossを満たす   Epは、Ut[B+Low]=-2μ-R-λとなる前に適用されることを仮定 No loss: 各データはaccept後、U+2μ+R+λ時間以内に、deliverされるか、エラー報告される No lossの証明の概略 Accept済みのIについて一定時間以内にOk(I)となることを示したい  接続がクローズされているとき、I<Bなので(9)よりOk(I)が成り立つ  接続がオープンされているとき   I≧B+Lowのとき、inp[I]送信後２μ+R以内にdeliverまたはEp適用可能となる。deliver～送信の余裕U, Ep適用可～適用の余裕λを足して、 U+2μ+R+λ以内に Ok(I) I<B+Lowのとき、(10)よりOk(I)が成り立つ Orderingについて  Ordering: qがdeliverするデータ番号(inpにおける)は単調増加 Rqにおいて  接続が閉じていたとき、新たに受け取るデータはprより大きいはず  接続がすでに開いていたとき、新たに受け取るデータはB+Exp=pr+1 ??Timer-basedプロトコルに関して疑問「通信路上でμ時間たったパケットは消失」…現実には実現可能か？  パケットに送信時刻を記録し、受信ノードや中継ノードでチェック⇒みんなの時刻がそろっていなければ不可能  実用上のプロトコルでは、時刻のかわりに中継ノード数を利用することも(IPヘッダのTTL) この仮定が崩れ、古いパケットをqが受け付けてしまうと、 (6)が崩れる