跳到主要内容

Virtual Time and Global States of Distributed Systems

Motivation

在分散式的環境中,缺乏common clock,如果能有一套好的logic clock作法,就可以基於這個common clock來設計distributed algorithmLamportTime, Clocks, and the Ordering of Events in a Distributed System Lamport 提出 Lamport ClockLamport Clocklinearly oredered的logic clock。

Lamport Clock有一個問題在於會喪失訊息,在這篇paper中,作者提出一套partically ordered logic clock的作法,改善了Lamport Clock遇到的問題,也證明了即時message 不是ordered,在這個clock vector的作法底下,我們還是可以做到global state snapshot

Lattice

在理解clock vector這種logical clock之前,要先理解lattice的概念。lattice是一種partically ordered set,集合中存在inf(最小值)和sup(最大值)。

Event structures

如果我們不考慮event發生的時間,只考慮event之間的關係,有先後關係的eventee < ee',如果沒有先後關係的event,則視為同時發生,則我們可以把events視為一種lattice

Cut events

我們想像某些event,會在local做某些action,然後在有限的時間內發給其他processprocess,則我們把這種event稱為 cut event,用 cic_i來表示。

把每個 processprocesscut event連起來,可以把events分成兩個partition,一邊是PAST,另外一邊是FUTURE。 而如果某個cut CC 裡面的ee',對所有 ee < e e'ee都在 CC 裡面,則稱CCconsistent cut

這裡我們可以的得到兩個定理:

  1. consistent cuts 是所有cutssublattice
  2. consistent cut裡面的任兩個 cut event cic_i, cjc_j 都不存在先後關係。

Vector time

LamportTime, Clocks, and the Ordering of Events in a Distributed System Lamport有提到logic clock的概念,如果 eeee' 早發生,則C(e)C(e) < C(e)C(e'),我們繼續沿用這個概念,但是定義為如果eeee'有先後關係,且e<e e < e',則 C(e)<C(e)C(e) < C(e'),但如果兩者無先後關係,則無法比大小。

沿著此概念,我們提出一種clock vector,此vector的長度為nn (nn為process的數目),每當processiprocess_i收到event或執行某些動作,就做tick (Ci[i]=Ci[i]+dC_i[i] = C_i[i]+d,d 屬於N N)。當 processiprocess_imessageprocessjprocess_jprocessjprocess_j會更新自己的clock vector,使 Cj=max(Cj,Ci)+dC_j = max(C_j, C_i) + d

由以上操作,我們可以得到一個定理:

對每一個i,ji, j Ci[i]>=Cj[i] C_i[i] >= C_j[i]

我們可以比較兩個vector v,uv, u,如果對任何一個iiv[i]<=u[i]v[i] <= u[i],則我們說 v<=uv <= u,如果v!=uv != u,則稱 v<uv < u,否則我們稱此二者平行。

然後我們也可以由反正法證明出,我們可以得到一個定理:

consistent cut XXiff iff tx=(C(c1)[1],...,C(cn)[n])t_x = (C(c_1)[1],...,C(c_n)[n])

而藉由得到consistent cut,我們可以得到所有在PAST partition 的event都早於在FUTURE的partition,因此我們滿足了partially ordered,所以clock vector是一種logic clock,因此我們可以得到一個common clock

Global state snapshot

clock vector應用在 Global state snapshot問題,可以藉由把每個snapshot event當成 cut event,我們可以得到這些event並不用像 Lamport-Chandy Algorithm所要求的,每個message必須要ordered,這些event在各個process的順序不用被要求,因為我們已經得到定理,$ Cut %%中的每個event都是同時的,不存在前後關係。