跳到主要内容

Lamport-Chandy Algorithm

Motivation​

提出一個演算法，可以對distributed system的state做snapshot，並可以解決兩個問題:

  • Stable Property Detection
  • Checkpoint

而 Lamport-Chandy algorithm只要對每個node的state做snapshot，就可以合成一個 global state。

Stable Property Detection​

如果某個property的值變成true，在它的值就一直會保持在true，不會再改變了，例如系統是否deadlock，某個計算是否完成等。

藉由此演算法，我們可以藉由對系統做snapshot，來做stable property detection。

Prerequisite​

  • channels have infinite buffer
  • Delay 時間隨然隨意，但是不是infinite
  • channel裡的mesaage order是順序的
  • channel 是有directed
  • channel 整個graph是 strongly conntected

Global State of a distributed system​

Define event e=<p,s,s′,M,c> e = <p, s, s', M, c>，其中:

  • pp: process p pp in global state SS
  • cc: cc is a channel, 如果 cc 是 pp的 input channel，則MM 從 cc中消除，如果cc 是 pp的output channel，則把MM放到channel尾端
  • ss: pp的當下state
  • s′s': pp的下一個state

next function​

我們定義一個nextnext function使得：

  • s′s' = next(p,e)next(p, e)
  • next(c,e)next(c, e) =
    • 把 MM 從 channel移除，如果cc 是 input channel
    • 把 MM 加到channel尾部，如果cc 是 output channel

而global state S′S' = next(S,e)next(S, e)。

Lamport-Chandy Algorithm​

Marker​

每次要snapshot (record global state)，會由發起者process pp發送一個marker，這是一個特別的message，當其他 process 收到marker message，也會record state。

Marker-Sending Rule​

pp 在發送之前 marker之前會record自身的state，而且在record state前，不會再發送其他message。

Marker-Receiving Rule​

如果 收到marker的process qq還沒有record state，則:

q records its state;
q records channel c state as the empty sequence

如果已經 record state，則：

q records channel c state 在做p作完record之後，收到 marker之前的狀態

proof​

接著要證明，藉由上面的marker作法，我們可以得到系統的 global state。這邊定義兩種event:prerecording event和postrecording event。

  • prerecordingeventprerecording event: 如果 pp在 event ee 來了之後才record state，稱為 prerecording event
  • postrecrodingeventpostrecroding event: 反之，如果 pp在 event ee來之前record state，則 ee為 postrecording event。

要證明即使這些events 的順序兌換(event之間無相關性)，也不影響最終的SS結果。

假設 ej−1e_{j-1} 是一個發生在 process pp的 postrecording event，而 eje_{j}是一個發生在 process qq的 prerecording event。

ej−1e_{j-1} 與 eje_{j} 必定無相關性，因為：

  1. 因為 ej−1e_{j-1}是postrecording event，所以 marker早已送出去
  2. eje_{j} 發生的時候，qq 還能從 channel c收到message，那代表早收到marker，record過state了，那eje_j就是postrecording event而不是prerecording event，跟假設矛盾，所以ej−1e_{j-1} 與 eje_{j} 無相關性。

因此我們可以重排這些events的順序也不影響最後得到的global state SS的結果，故得證。

應用​

References​