Virtual Time and Global States of Distributed Systems
Motivation
在分散式的環境中,缺乏common clock,如果能有一套好的logic clock作法,就可以基於這個common clock來設計distributed algorithm。Lamport在Time, Clocks, and the Ordering of Events in a Distributed System Lamport 提出 Lamport Clock,Lamport Clock是linearly 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之間的關係,有先後關係的event < ,如果沒有先後關係的event,則視為同時發生,則我們可以把events視為一種lattice。
Cut events
我們想像某些event,會在local做某些action,然後在有限的時間內發給其他,則我們把這種event稱為 cut event,用 來表示。
把每個 的 cut event連起來,可以把events分成兩個partition,一邊是PAST,另外一邊是FUTURE。
而如果某個cut 裡面的,對所有 < ,都在 裡面,則稱為 consistent cut。
這裡我們可以的得到兩個定理:
consistent cuts是所有cuts的sublattice。consistent cut裡面的任兩個cut event, 都不存在先後關係。
Vector time
在 Lamport的Time, Clocks, and the Ordering of Events in a Distributed System Lamport有提到logic clock的概念,如果 比 早發生,則 < ,我們繼續沿用這個概念,但是定義為如果 跟有先後關係,且,則 ,但如果兩者無先後關係,則無法比大小。
沿著此概念,我們提出一種clock vector,此vector的長度為 (為process的數目),每當收到event或執行某些動作,就做tick (,d 屬於)。當 發message給 ,會更新自己的clock vector,使 。
由以上操作,我們可以得到一個定理:
對每一個,
我們可以比較兩個vector ,如果對任何一個, ,則我們說 ,如果,則稱 ,否則我們稱此二者平行。
然後我們也可以由反正法證明出,我們可以得到一個定理:
consistent cut , 。
而藉由得到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都是同時的,不存在前後關係。