回答有關分佈式系統的幾個核心問題
本文是作者在 FLOPS 2022 會議上的演講，重點分享了使用 Liquid Haskell 語言集成驗證系統來構建可靠的分佈式系統的有趣的探索經歷。
早上好，FLOPS！我是 Lindsey Kuper。我是加州大學聖克魯茲分校的助理教授。
非常感謝 Atsushi 和 Michael 以及整個 FLOPS 組織團隊邀請我在 FLOPS 上發言，以及他們組織這次活動的工作。就個人而言，FLOPS 是我第一次有論文被拒絕的會議，那是在 2010 年我剛開始讀研究生的時候。所以今天被邀請做這個演講，我感到特別榮幸。
這個演講是關於我最近在做的非常興奮的事情，即使用現代語言集成驗證工具來幫助我們構建保證按預期工作的分佈式系統的潛力，這些保證不僅適用於模型，還適用於真實運行的代碼。
在本次演講的開始部分，我將解釋我所說的 “分佈式系統” 的含義以及它們所面臨的具體挑戰。然後簡單介紹一下 Liquid Haskell 語言集成的驗證系統。最後，探險記：我將分享我和我的學生和合作者一直在這個領域開展的兩個項目的一些亮點。
那麼，讓我們從討論分佈式系統開始吧！
1 什麼是分佈式系統？
想象一些獨立的機器通過網絡相互傳遞消息進行通信。它們可能相距很近或相距很遠，但我們對所謂的地理分佈式系統特別感興趣，其中該網絡可能跨越整個星球。例如，該圖中的節點大致對應於亞馬遜一些數據中心的位置。正是在這個更大的 “行星尺度” 上，出現了一些最有趣和最具挑戰性的問題。
其中許多問題與故障有關，並且需要在系統出現部分故障的情況下繼續運行。亞馬遜在其關於 Dynamo 數據存儲系統的 SOSP 2007 論文中對此進行了非常生動的描述：“客戶必須能夠將商品添加到他們的購物車中，即使磁盤出現故障、網絡路由抖動或數據中心被龍捲風摧毀。” （我恰好來自美國中西部的愛荷華州，所以龍捲風對我來說是非常真實的成長過程，但可以隨意替換你選擇的任何自然災害。）
因此，由於龍捲風或任何其他原因，不僅網絡連接會失敗，而且該網絡中的節點也會失敗。即使在出現故障的情況下，系統也必須繼續運行並響應請求，這一點很重要，因爲用 Werner Vogels 的話來說，“一切都在失敗”。
因此，部分故障的問題，以及需要在部分故障存在的情況下繼續運行，在許多方面是分佈式系統的定義特徵。
2 光速很慢
但是在地理分佈式系統中，我們還有另一個基本問題，那就是光速很慢！
這是一束電線，每根大約 30 釐米長。格蕾絲 · 霍珀（Grace Hopper）在她的有名的講座中分發了這些，以展示電信號在一納秒內可以傳播的距離。這些是她分發的一些實際的電線；他們現在在史密森尼博物館。
所以，光速很慢！它在一納秒內僅移動約 30 釐米。或者，正如我的朋友 Mae Milano 所說，每個時鐘週期只有大約 4 英寸。
因此，如果我們談論的機器可能彼此位於世界的另一端，那麼即使在理想條件下，在消息發送和消息到達之間也可能會經歷很多時鐘週期。
3 複製
所以，無論我們是在談論故障——磁盤故障、宇宙射線、網絡連接被反剷挖掘機截斷、數據中心被龍捲風摧毀——或者只是更普通但不可避免的問題，即相距很遠的機器之間的長時間延遲，緩解這些挑戰的一種方法是在多個物理位置複製數據。這有助於確保數據的可用性——換句話說，有助於確保每個請求都得到有意義的響應。
如果我有我不想丟失並且我想確保仍然可用的數據，無論是我女兒的嬰兒照片還是我可能關心的任何其他數據，我將存儲該數據的多個副本在數據中心內，以及在不同數據中心之間。
這樣做是出於容錯的原因——你擁有的副本越多，你丟失它的可能性就越小——以及數據局部性，以最大限度地減少延遲——我們希望數據的副本接近任何人的嘗試訪問它 - 以及吞吐量的原因：如果你有多個數據副本，那麼原則上你可以爲更多嘗試同時訪問它的客戶提供服務。但是，儘管出於所有這些原因擁有多個副本是必不可少的，但它引入了必須保持副本彼此一致的新問題，特別是在我們擁有的網絡中，由於網絡分區，副本之間的延遲可能任意長。
4 一致性
因此，正如我告訴參加我的分佈式系統課程的本科生，複製既是大多數分佈式系統問題的原因，也是解決方案。我們必須複製數據，但我們必須保持這些副本彼此一致。
現在，我們知道試圖始終保持地理分佈的副本完全一致是徒勞的。一個經典的不可能結果告訴我們，在存在網絡分區的情況下實現完美一致性的唯一方法是犧牲數據的可用性。由於在處理地理分佈式數據時網絡分區是不可避免的，我們通常選擇以允許客戶觀察副本之間某些類型的分歧的方式設計系統，以優先考慮可用性。
如果我們要允許副本之間存在某些類型的分歧，那麼我們需要一種指定策略的方法，該策略告訴我們允許副本以何種方式不同意，在什麼情況下允許他們不同意，以及在什麼情況下他們必須同意。讓我們看一下這些一致性策略的幾個示例，以及可能違反它們的一些方式。
5 強收斂
感興趣的屬性之一稱爲強收斂。這表示如果副本已收到相同的更新集（以任何順序），則這些副本具有相同的狀態。
例如，假設我和我的伴侶都在更新我們共享的女兒照片相冊，名爲 photos。我添加了一張照片，首先將其添加到副本 R1，稍後再添加到副本 R2。與此同時，我的搭檔添加了一張不同的照片，它首先出現在 R2 中，然後出現在 R1 中。儘管副本以相反的順序接收更新，但它們的狀態最終是一致的。因此，本次執行具有較強的收斂性。
在這個例子中，情況很明顯，因爲我們複製的數據結構是一個集合，並且這兩個添加到集合中的元素相互交換。
6 確保強收斂
然而，總的來說，我們必須仔細設計數據結構的接口，以確保在每次執行中都保持強大的收斂性。
例如，這裏有一個不同的執行，它不是強收斂的。假設我們從具有包含一張照片的相同相冊的兩個副本開始。和以前一樣，我添加了一張照片。假設我的照片首先進入 R1。同時，假設我們的照片應用程序提供了一個 share_with_mom 以照片爲參數的操作。我的夥伴想與他的媽媽分享照片，因此他嘗試將 share_with_mom 操作映射到相冊中的所有內容。
該 map 操作首先進入 R2，然後應用於相冊中的所有內容，此時相冊只是一張照片。但後來當我添加的照片到達時，它在 map 操作運行時不是集合的一部分，所以根據副本 R2，它沒有與我的婆婆共享。同時，副本 R1 接收第二個 map 操作並映射兩張照片，因此兩張照片都被共享。不幸的是，這些操作不會相互通信，因此，如果此地圖操作是我們相冊提供的接口的一部分，那麼每次執行都不會保持強收斂。
解決此問題的一種方法是仔細設計數據結構的接口，以確保其上的所有操作都可以通信。具有這種行爲的數據結構被稱爲無衝突複製數據類型或 CRDT，它們通常通過巧妙的技巧使操作可以在原本不會進行的情況下進行交換，或者利用關於應用操作順序的假設來工作。新的 CRDT 設計是一個活躍的研究領域。隨着這些數據結構的設計變得越來越複雜，它們激發了對機械驗證實現的需求，這些實現可以保證在所有可能的執行中收斂。
我們稍後會回到這個問題，但在此之前，讓我們先看看另一種一致性問題。
7 因果傳遞
再說一次，我向相冊添加了一張照片。我碰巧與副本 R1 通信，R1 將更新異步發送到 R2。後來，我的搭檔過來看照片。他看到了我的更新，因爲他碰巧與進行更新的副本相同。但是假設他在那之後試圖發表評論，不幸的是，那篇文章發給了 R2，它還沒有拿到照片。因爲照片還沒有，所以複製品不能附加評論。
這可能會表現爲某種難以理解的錯誤消息，例如 “抱歉，出了點問題。再試一次。” 你可能以前見過這種東西。
要了解這裏出了什麼問題，我們必須考慮事件的因果關係。我的搭檔試圖對這張照片發表評論，因爲他在服務器的回覆中看到了這張照片。這是由於之前的添加操作而發生的。所以，這個添加操作是嘗試評論的因果歷史的一部分，我們可以通過隨着時間的推移跟蹤這些消息並看到評論操作可以從添加操作中看到。但在嘗試評論發生時，此副本尚未發現其因果歷史中的此添加事件。所以這違反了所謂的因果一致性。
解決此問題的一種方法是使用確保消息按因果順序傳遞到副本的機制，其中 “已傳遞” 一詞意味着在收到後實際應用於副本的狀態。一種廣泛使用的方法是將元數據附加到每條消息中，以總結該消息的因果歷史——例如，矢量時鐘。我們可以使用此元數據來確定兩條消息之間的因果關係（如果有的話），並延遲將消息傳遞到給定副本，直到每條因果先前的消息都已傳遞。在這種情況下，comment 發送到副本 R2 的消息將排隊，直到 add 消息到達，然後可以應用評論。
在這裏，我再次認爲需要機械驗證的實現，因爲因果消息排序抽象是分佈式系統非常有用的構建塊，但是很多系統並沒有做到這一點。我們稍後再討論這個問題。
8 我們應該執行什麼一致性策略？
事實證明，知道我們應該執行哪個策略也很重要，因爲這些一致性策略以及它們指定的有關執行的屬性不一定很好地映射到我們關心的給定應用程序的不變量上。
例如，假設我和我的夥伴正在使用照片共享服務的免費層級，它說我們最多可以擁有 1000 張照片，否則我們必須開始付費，不然我們將面臨刪除舊照片的風險。如果相冊中有 999 張照片，添加一張照片應該沒問題；沒有違反不變量。
另一方面，如果我的伴侶也同時添加了照片怎麼辦？那麼，當兩個副本同步時，就會違反不變量。
我們應該怎麼做呢？如果需要維護不變量，則需要拒絕我的更新或我的夥伴的更新，這將要求我們每次添加照片時同步副本。在實踐中，我們可能希望避免這種同步，直到我們接近 1000 張照片的限制。此外，其他操作，如刪除照片，不需要同步來保持這個特定的不變量。一般來說，同步副本的需求取決於操作和我們需要維護的特定於應用程序的不變量。
我們之前談到的與應用程序無關的屬性，如強收斂和因果消息傳遞，並不能讓我們一路走好，但它們可能會讓我們走上一段路。事實上，驗證這些特定於應用程序的屬性的工作通常依賴於已經存在強收斂或因果消息傳遞等屬性的假設。如果我們可以依賴底層數據結構的某些屬性是真實的，或者在其之下，消息傳遞層，我們可以簡化應用程序級別的驗證任務（或者，就此而言，只是關於應用程序代碼行爲的非正式推理）。
9 分佈式一致性策略動物園
我們剛剛看到了一些我們可能希望針對複製數據的一致性實施的策略示例。要知道這樣的策略適用於所有執行，需要對通常非常大的執行狀態空間進行推理，其中有很多消息丟失和消息排序的可能性。
這些策略的規範稱爲一致性模型，其中有很多。不久前我向我的研究生展示了這個數字，現在它困擾着他們的夢想。它來自 Viotti 和 Vukolić 於 2016 年發表的一篇調查論文，其中對分佈式系統文獻中的 50 多個一致性概念進行了分類，並按照所謂的 “語義強度” 對它們進行了排序。
換句話說，一致性模型的順序越高，允許的執行次數越少，副本之間的分歧就越少。你走的越低，允許的執行越多，副本之間的分歧越大。而且，正如你所看到的，這是一個偏序——有許多對一致性模型，其中一個都不比另一個強。
剛纔，我們看了這個空間的兩點。我們剛纔談到的因果一致性在左邊結束了。我們之前談到的強收斂性並沒有出現在 Viotti 和 Vukolić 的身上，儘管他們確實在他們的論文中談到了這一點。如果確實出現了，它必須是右側 “強最終一致性” 和左側 “因果 + 一致性” 的下限。
雖然圖中沒有出現強收斂，但我認爲獨立考慮它是一個很好的屬性，因爲它是強最終一致性的安全部分。這個數字有點令人困惑，不僅因爲這個偏序集合有這麼多元素，還因爲這個集合的一些元素將安全性和活性屬性混爲一談。但如果它令人困惑，那隻能說明即使弄清楚如何從分佈式系統中指定我們想要的行爲也很困難（更不用說實際驗證這些規範是否得到滿足）。
所以我們有兩個問題。一個問題是爲給定的應用程序確定我們想要什麼策略、策略組合或策略的一部分。另一個問題是確保沒有執行違反該策略。這些都是難題，程序員不應該在沒有幫助的情況下獨自馴服這個動物園。程序員應該擁有強大的、語言集成的工具來指定他們想要從分佈式系統實現中獲得的行爲，然後確保他們的實現符合這些規範。
10 藍天的願景
所以，這就是藍天願景：我們希望程序員能夠機械地指定和驗證正確性屬性——不僅僅是模型，而是分佈式系統的真實、可執行實現。此外，他們應該能夠使用集成到他們用於實現的相同通用、工業強度編程語言中的驗證功能來做到這一點。
我們中的許多人已經被通過表達類型系統的語言集成驗證所吸引，這就是我今天要討論的驗證方法。
這將我帶到了談話的下一部分。我們剛剛討論了分佈式系統和一些我們可能想要指定和驗證的屬性示例；現在我們將介紹 Liquid Haskell 並轉向我們如何以及是否可以使用 Liquid Haskell 來完成我們想要的。
11 細化類型
Liquid Haskell 採用的語言集成驗證方法以細化類型爲中心。出於本次演講的目的，我將細化類型定義爲允許程序員指定邏輯謂詞的數據類型，這些謂詞限制或細化可以包含該類型的值集。根據謂詞語言的表達能力，程序員可以使用細化類型指定豐富的屬性，有時會以類型檢查的可判定性爲代價。Liquid Haskell 所基於的 Liquid 類型通過將細化謂詞限制爲 SMT 可判定邏輯來避免該問題。
這裏有幾個簡單的例子，我使用 Liquid Haskell 語法編寫的。
例如，我們可以定義一個稱爲精化 EvenInt 的 Haskell 內置 Int 類型的類型，它帶有一個細化謂詞，我在這裏強調過，它表示我們的 Int 必須能被 2 整除。
type EvenInt = { n:Int | n mod 2 == 0 }同樣，我們可以 OddInt 使用細化謂詞定義一個類型，該謂詞表示除以 2 時得到餘數 1。
type OddInt = { n:Int | n mod 2 == 1 }讓我們看看如何使用這些類型。在 Liquid Haskell 中，我可以編寫一個名爲的函數 oddAdd，它需要兩個 OddInts 並返回它們的總和。參數的類型表示 x 和 y 將爲奇數的前置條件，返回類型 EvenInt 表示 x + y 將評估爲偶數的後置條件。
oddAdd :: OddInt -> OddInt -> EvenInt oddAdd x y = x + yLiquid Haskell 通過生成在編譯時由底層 SMT 求解器檢查的驗證條件來自動證明此類後置條件成立。如果求解器發現驗證條件無效，則類型檢查失敗。例如，如果返回類型爲 oddAdd，OddInt 則 oddAdd 函數將無法進行類型檢查，Liquid Haskell 將產生類型錯誤消息。
雖然這對於熟悉細化類型的人來說都不是什麼新鮮事，但值得指出的是，就我們目前所見，我們已經可以做一些相當有用的事情了。例如，這裏有一個 tail 從 Haskell Prelude（Haskell 的標準庫）調用的函數，給定一個列表，它給出了該列表頭部之後的所有內容，該列表必須是非空的。如果你要調用 tail 一個空列表，你會在運行時得到一個異常。
tail :: [a] -> [a]
tail (_:xs) = xs
tail [] = error "oh no!"使用細化類型，我們可以給出 tail 一個表示其輸入不能是空列表的類型。
tail :: { l:[a] | l /= [] } -> [a]
tail (_:xs) = xs如果我們這樣做，那麼我們實際上可以擺脫空列表的情況，使我們的代碼更簡單一些。
此外，我們還可以在返回類型中添加一個細化謂詞，tail 這將說明它返回的列表的長度；特別是，它比參數列表的長度短一個。所以現在 tail 有一個後置條件，可能對 tail。
tail :: { l:[a] | xs /= [] } -> { l':[a] | len l - 1 == len l' }到目前爲止，這幾乎是你對細化類型系統的期望。然而，我認爲 Liquid Haskell 真正閃耀的地方在於，它允許你超越指定單個函數的前置條件和後置條件，並允許你使用一種稱爲細化反射的機制來驗證不特定於任何特定函數定義的外部屬性。讓我們回到偶數和奇數的例子，看看它會是什麼樣子。
12 細化反射
這是一個名爲 sumEven 的類型 sumEven 表示 oddAdd 返回偶數的外在屬性。實際上，sumEven 是一個 Haskell 函數，它返回一個返回偶數的證明 oddAdd。
我們看到返回類型 sumEven 是 Proof。在 Liquid Haskell 中，這種 Proof 類型只是 Haskell 的 ()（單位）類型的類型別名。精煉謂詞 Proof 指定我們要證明的屬性 oddAdd——即，當我們調用 時，結果將是偶數。得益於 Liquid Haskell 的細化反射機制，我們能夠在 oddAdd 細化類型中指向 sumEven。
我們現在可以編寫 sumEven 函數的主體：它忽略它的參數並返回 ()（單位）。sumEven 的函數體看起來並不多 - 但它是一個誠實的證明術語！它看起來不太像的原因是這個特殊的證明——如果 x 和 y 是奇數，那麼調用 oddAdd x y 將評估爲偶數的證明——是底層 SMT 求解器很容易自動執行的證明。如果不是這樣，那麼我們需要在這裏編寫一個更高級的證明術語，使用 Liquid Haskell 提供的證明組合器。
現在，sumEven 不是太令人興奮的財產；畢竟，它並沒有告訴我們任何我們從 oddAdd。但是現在我們有了 oddAdd 在細化謂詞中引用的能力，我們也可以做更多有趣的事情。例如，我可以使用 Liquid Haskell 來證明它 oddAdd 是可交換的。
這次我們返回類型的細化謂詞有兩次調用 oddAdd，所以我們需要一個與多次調用的結果相關的證明。再一次，Liquid Haskell 可以自動提出這個證明。它部分是通過利用底層 SMT 求解器的知識來實現的，即整數上的加法是可交換的。
雖然這兩種證明都是自動的，但總的來說，情況可能並非如此。Liquid Haskell 程序員可以在細化類型中指定任意外部屬性，然後程序員可以通過使用提供的證明組合器編寫包含這些細化類型的程序來證明這些外部屬性。
因此，Liquid Haskell 可以做的比傳統的細化類型更多。它不只是讓你爲你正在編寫的程序提供更精確的類型。它還允許你使用細化類型註釋作爲指定你可能想要證明的代碼的任何可判定屬性的地方。然後，你可以通過編寫 Haskell 程序來容納這些類型來幫助 SMT 求解器證明該屬性。
我認爲 Liquid Haskell 位於基於 SMT 的程序驗證器（如 Dafny）和利用 Curry-Howard 對應關係的證明助手（如 Coq 和 Agda）的交叉點。Liquid Haskell 程序可以包含應用程序代碼，如 oddAdd（像往常一樣在執行時運行）和驗證代碼，如 sumEvenand 和 oddAddComm，它們只經過類型檢查，但令人高興的是，它們都只是 Haskell 程序，只是具有細化類型。
基於 Haskell 可以讓程序員逐漸將代碼從普通的 Haskell 移植到 Liquid Haskell，在代碼中添加更豐富的規範。例如，程序員可能從 的實現開始 oddAdd，Int -> Int -> Int 然後將其細化爲 OddInt -> OddInt -> EvenInt，然後證明外部屬性 sumEven 和 oddAddComm，然後再使用 sumEven 和 oddAddComm 作爲前提來證明另一個更有趣的外在屬性。
最後要注意的是，與傳統的證明助手不同，傳統的證明助手需要你從用證明助手的白話語言編寫的代碼中提取可執行實現，在 Liquid Haskell 中，你直接證明了有關你將要執行的代碼的事情運行，所以最後，你可以立即執行經過驗證的代碼，無需提取步驟，因此無需信任提取過程。
13 探險記
現在我們已經體驗了 Liquid Haskell，讓我們開始有趣的部分：探險記！在我的小組中，我們一直在研究如何使用 Liquid Haskell，特別是我們如何使用這種精巧的反射能力來表達和證明分佈式系統實現的有趣屬性。
特別是，我們有興趣解決我在演講開始部分討論的兩個問題：首先，確保複製的數據結構是強收斂的，其次，保證消息以因果順序在副本中傳遞。我在演講開始部分討論的第三個問題是保證特定於應用程序的不變量成立的問題，雖然我不會專門討論這個問題，但我會指出我們的目標之一是前兩個驗證任務的結果可用作驗證這些應用程序級屬性的模塊化構建塊。所以如果我們成功了，第三個任務會更容易。
14 已驗證 CRDT 的強收斂性
首先，驗證複製數據結構的強收斂性。這是與合作者 Yiyun Liu、James Parker、Michael Hicks 和 Niki Vazou 以及我的博士生 Patrick Redmond 共同完成的。回想一下，強收斂意味着如果副本以任何順序應用了相同的更新操作集，那麼它們具有相同的狀態。提供此屬性的數據結構稱爲無衝突複製數據類型或 CRDT。
就像我們之前看到的，複製數據結構的強收斂取決於對該數據結構的操作的交換性。這取決於數據結構提供了哪些操作。然而，一旦你有了交換性證明，獲得強收斂的其餘推理就與特定複製數據結構的細節無關。
我們能夠通過在 Liquid Haskell 中的通用 CRDT 接口級別聲明和證明強收斂性來利用這種獨立性，然後爲我們想要驗證的每個單獨的 CRDT 插入一個特定於數據結構的交換性證明。
在 Haskell 中，這些通用接口被稱爲類型類，並且能夠以這種模塊化方式進行這種證明需要擴展 Liquid Haskell 以添加在類型類級別聲明和證明屬性的能力。這實際上是一個巨大的挑戰，因爲在類型類被編譯掉之後，Liquid Haskell 在 Haskell 代碼的中間級別上運行。我的合作者擴展了 Liquid Haskell 以支持類型類，這需要對 Liquid Haskell 進行大修並帶來了自己有趣的挑戰，你可以在我們的 OOPSLA '20 論文中閱讀所有相關內容。
一旦可以在 Liquid Haskell 中聲明和證明類型類的屬性，這意味着 CRDT 類型類級別的與操作無關的證明可以與單個 CRDT 級別的特定於操作的交換性證明相結合，以獲得完整的強證明該 CRDT 的收斂性。
讓我們仔細看看我們需要在類型類級別證明的屬性，以及我們如何在 Liquid Haskell 中表達它。
15 一個經過驗證的 CRDT 類型類
所以，這裏有一個用於 CRDT 的 Liquid Haskell 類型類。類型類的每個實例都有一個關聯 Op 類型，該類型指定可以更新 CRDT 狀態的操作。該 apply 方法接受一個狀態，對其運行給定的操作，並返回更新後的狀態。類型 lawCommut 指定了操作必須可交換的屬性，單個 CRDT 實例的實現者需要提供這樣的可交換性證明。
我在這裏展示的是 CRDT 類型類的簡化版本，它在我們的實際實現中省略了一些微妙之處。特別是，實際上並非所有操作都必須通信；相反，有一個特定於 CRDT 的 “兼容” 操作的概念，實際上只有兼容的操作必須是可交換的，因爲 CRDT 的設計排除了不兼容的操作不能同時應用。
此外，某些操作只能在 CRDT 處於給定狀態時應用。對於最簡單的 CRDT，例如只增長計數器，所有操作都將相互兼容並且始終適用，而對於更復雜的 CRDT，情況並非如此。你可以在我們的論文中找到有關此兼容性概念的更多詳細信息。
一旦我們能夠以這種方式定義 CRDT 類型類，我們就能夠在類型類級別表達強大的收斂性。這是 strongConvergence Liquid Haskell 中的財產聲明。這再次從真實事物中簡化，但抓住了關鍵思想，即如果兩個操作列表是彼此的排列，那麼將任一操作應用於相同的輸入 CRDT 狀態將產生相同的輸出狀態。這個屬性的證明是大約 300 行 Liquid Haskell 代碼。它是通過對操作列表進行歸納，並利用 CRDT 實例提供的操作交換性證明。然而，strongConvergence 證明獨立於任何特定的 CRDT 實例，因此適用於所有這些實例。
我之前對應用程序代碼和驗證碼進行了區分，我們也可以在這裏看到。該 apply 函數實際上在運行時用於 CRDT 的實現。lawCommut 函數和函數永遠不會在 strongConvergence 運行時運行，所以它們是驗證碼。
但是我們可以從 的細化類型中看出，它是對的行爲 lawCommut 的一個證明，也正是由於 Liquid Haskell 的細化反射，纔有可能引用 in 的類型。最後，作爲函數調用，或者換句話說，用作引理，在 strongConvergence 的主體中，因爲它太長，所以這裏沒有顯示。
16 已驗證的 CRDT 實例
現在，CRDT 實例提供這種操作交換性證明有多容易 lawCommut？這取決於 CRDT 的複雜性。這裏有幾個例子。
最簡單的 CRDT 之一是隻能增長的計數器。此計數器上的操作只是數字，CRDT 的狀態是它們的總和。對於這個 CRDT，Liquid Haskell 可以自動執行交換性證明，就像我之前展示的加法交換性證明一樣。
另一方面，這裏有一個更高級的 CRDT：一個支持鍵值對上的插入、更新和刪除操作的字典，其中值本身是 CRDT 類型的。對於這個 CRDT，交換性證明佔用了超過一千行代碼。
交換性證明的複雜性是 CRDT 實現複雜性的結果。例如，對於這個字典 CRDT，我省略了 apply 函數的實現，但它有點毛茸茸。例如，如果它接收到尚未插入的鍵的更新操作，它將這些更新操作存儲在待處理操作的緩衝區中，然後在相關插入發生時立即應用它們。
值得指出的是，這種實現複雜性是必要的，因爲這些 CRDT 的設計方式幾乎不需要來自底層消息傳遞層的排序保證。這就是爲什麼一個副本可以接收尚未到達該副本的密鑰的更新操作的原因。雖然這確實意味着我們可以在更多設置中使用我們的 CRDT，但它爲非平凡的 CRDT 提供了更加艱苦的驗證工作。
儘管我們在將與 CRDT 無關的強收斂性證明與特定於 CRDT 的交換性證明分開的方式上已經有了一些模塊化，但這種艱苦的驗證工作表明，一種更加模塊化的方法可以將較低級別的消息傳遞問題與較高級別的數據分開需要結構語義。這個想法將引導我們進入我將在本次演講中討論的第二個也是最後一個項目。
17 回到因果交付
讓我們回顧一下我們之前看到的示例，以激發對因果消息傳遞的需求。在此示例中，我用新照片更新了共享相冊，我的夥伴看到了它，但是當他試圖對新照片發表評論時，他與尚未獲得更新的副本通信。正如我們所討論的，這違反了消息的因果順序：他的評論因果取決於我之前的照片添加操作。
解決此類問題的一種方法是讓副本跟蹤表示它們彼此傳遞了多少消息的元數據，並讓消息攜帶表示它們的因果依賴關係的元數據，並且直到它的依賴關係纔在副本上傳遞消息已經很滿意了。例如，從副本 1 到我的夥伴的響應可以攜帶一個向量時鐘，指示副本 1 知道一個消息傳遞，並且該向量時鐘元數據可以在來自客戶端的下一個請求中線程化。當請求到達副本 2 時，副本 2 可以檢查向量時鐘，將其與自己的時鐘進行比較，確定消息是否可傳遞，如果需要，將消息排隊，直到收到並傳遞了因果前面的消息。
18 指定因果傳遞
在廣播消息的情況下確保因果消息傳遞的經典協議稱爲 CBCAST 協議，是 “因果廣播” 的縮寫。該協議由 Ken Birman 等人介紹。在 90 年代初期，他們在 Isis 系統的背景下進行了容錯分佈式計算。
該協議確保當一個進程接收到一條消息時，該消息在必要時被延遲然後傳遞，這意味着僅在任何因果先前的消息已經傳遞之後才應用於該進程的狀態。特別是，如果消息 m 的發送發生在消息 m'的發送之前，在 Lamport 的發生之前關係的意義上，那麼我們知道在所有進程中，m 的傳遞必須先於 m' 的傳遞。
在 CBCAST 中，這是通過使用矢量時鐘來表示因果依賴關係，並在接收方的隊列中延遲消息直到可以傳遞它們來完成的。通過將接收進程的向量時鐘與消息的向量時鐘進行比較來完成可傳遞性檢查。
在我們最近的工作中，我和我的學生在 Liquid Haskell 中實現了 Birman 等人的 CBCAST 協議，並且我們使用 Liquid Haskell 來驗證我們的實現是否具有因果傳遞屬性。
下面是我們如何使用 Liquid Haskell 中的改進來表達觀察因果傳遞的過程類型的簡化視圖。因此，一個進程會跟蹤迄今爲止在其上發生的事件，包括它所傳遞的任何消息——而該事件序列構成了它的進程歷史。這種類型 ，CausalDelivery 表示如果任何兩條消息 m 和 m'都出現在進程歷史中作爲已傳遞，並且 m 因果上在 m' 之前，那麼這些傳遞必須以與其因果一致的順序出現在進程歷史中命令。因此，這實質上是從論文中獲取因果傳遞的定義，並將其轉化爲我們可以對流程強制執行的屬性。
現在我們已經定義了這種類型，驗證任務是確保對於任何可以通過運行 CBCAST 協議實際產生的過程歷史，這種因果傳遞屬性都成立。
19 驗證因果傳遞協議
我們實現這一點的方法是用狀態轉換系統來表達 CBCAST 協議，其中狀態表示進程的狀態，狀態轉換是廣播、接收或傳遞消息的操作。在這裏，Op 類型表示這三種狀態轉換，step 函數將我們從進程狀態帶到進程狀態。
然後我們可以證明我在 causalDeliveryPreservation 這裏調用的一個屬性，它表示如果一個進程一開始就觀察到因果傳遞，那麼任何可能由協議產生的狀態轉換序列產生的進程也將觀察到因果傳遞。
這需要幾百行 Liquid Haskell 代碼來證明，其中最有趣的部分當然是處理 deliver 操作的部分。
我認爲關於這個結果有一些有趣的事情需要指出。首先，我們發現真正的關鍵是在狀態轉換系統方面實現協議。這不是原始論文中描述的方式，儘管當然所有的想法都在那裏。但我們發現這是我們需要做的才能表達和證明這樣的屬性，我們花了一段時間才得出這個設計，儘管回想起來似乎很明顯。
其次，我想指出，這個協議對消息的內容是完全不可知的。它只查看附加到消息的因果元數據，而不是消息本身。現在，這種選擇也有不利之處。如果你正在實現一個端到端系統，那麼如果你對正在處理的消息的語義有所瞭解，那麼你可能能夠對消息傳遞做出更明智的選擇。
例如，一條可能被因果廣播協議認爲無法傳遞的消息在你的自定義語義下可能會更快地傳遞。另一方面，選擇與消息內容無關意味着我們現在擁有一個通用的、經過驗證的因果消息廣播庫，它可以作爲許多應用程序的基礎。
20 需求層次結構
我們現在即將結束我的演講，但如果我要談論因果廣播作爲基礎，那麼我不禁要展示這個令人愉快的形象，我不能把它歸功於 - 這個形象由目前在 CMU 攻讀博士學位的 Matt Weidner 創建。這裏的想法是，一旦滿足基本需求——食物、水、住所、互聯網——然後因果廣播就位於其之上，作爲 CRDT 的基礎，因此也是協作軟件的基礎。
我之前提到過，我們的一些 CRDT 進行了艱苦的證明工作來驗證，部分原因是因爲這些 CRDT 沒有假設來自底層網絡的因果消息傳遞。然而，既然我們確實有這項關於驗證因果廣播的新工作，我的主張是執行這些 CRDT 交換性證明會更容易，我想回去重新審視這項工作並在因果廣播的基礎上進行構建。
相反，一些 CRDT 實際上並不需要因果廣播來強收斂，例如，我之前展示的計數器 CRDT，事實上，我的主張是那些不需要因果廣播的正是那些 Liquid Haskell 可以自動驗證 的交換性。對於那些做需要因果廣播，驗證任務，更不用說 CRDT 本身的實現，現在應該會變得更簡單，因爲我們已經建立了因果廣播。
我還想補充一點，CRDT 並不是唯一可以位於這個層次結構級別的東西。一旦你有了因果廣播，實現一個因果一致的數據庫也變得相對簡單。PL 社區已經在驗證因果一致性方面做了很多出色的工作，但據我所知，這項工作並沒有將因果廣播協議分解到它自己單獨驗證的層中，這就是我們已經完成了。所以我們認爲應該可以在因果廣播之上以模塊化方式驗證因果一致性，這是我們接下來要研究的事情之一。
21 我們到了嗎
在我結束演講時，我想回到我之前提到的這個藍天願景：程序員應該能夠機械地表達和證明分佈式系統的可執行實現的豐富正確性，使用相同的工業強度語言他們用於實現本身。我們到了嗎？到目前爲止，我們的結果表明使用 Liquid Haskell 是可能的。不幸的是，我認爲這仍然太難了。
由於細化反射，Liquid Haskell 可以習慣了把 Haskell 變成了一個證明助手，沒錯，我覺得這一切都是可能的，這很好。但是在 Liquid Haskell 中開發長證明是相當痛苦的。
部分問題在於，Agda 和 Coq 等更成熟的證明助手爲交互式證明開發和對證明狀態的洞察提供了更好的支持（例如，仍然需要證明哪些子目標才能完成部分完整的證明）。相比之下，Liquid Haskell 只提供非常粗粒度的反饋——它要麼報告類型錯誤，這意味着你的證明沒有完成，要麼沒有，這意味着它已經完成。
我和我的學生和合作者一直在思考如何改善這種情況，我們的建議之一是擴展 Liquid Haskell，支持 Agda 風格的類型孔，以及利用它們的交互式編輯命令。類型化的漏洞將允許程序員指出證明的未完成部分，並在與編譯器的對話中逐步完成證明。雖然 GHC Haskell 已經擁有自己的受 Agda 啓發的類型孔支持，但我們認爲如果結合 Liquid Haskell 的細化類型和 SMT 自動化，類型孔將特別強大和有用。
我們去年在 HATRA 研討會上發表了一篇關於這個想法的簡短論文，但是還有很多工作要做，所以我會邀請任何有興趣在這裏提供幫助的人合作。
22 結論
總而言之，我們看到我們可以使用 Liquid Haskell 的細化類型來表達有關複製數據結構的收斂性的屬性，並使用 Liquid Haskell 的細化反射和證明組合從外部證明這些屬性。同樣，我們可以表達和證明廣播消息在流程中傳遞的順序的屬性，這應該能夠更容易地在消息傳遞層之上實現和驗證應用程序，無論是 CRDT 還是其他任何東西。雖然 Liquid Haskell 可以勝任這項任務，但我們仍然認爲它可以更容易使用，我們期待繼續改進它。
本文由 Readfog 進行 AMP 轉碼，版權歸原作者所有。
來源：https://mp.weixin.qq.com/s/w8x54EjqOrmL6YedbCLujA