還在為資料庫事務一致性檢測而苦惱?讓Elle幫幫你,以TDSQL為例我們測測 | DB·洞見#7

来源:https://www.cnblogs.com/tencentdb/archive/2022/11/15/16892650.html
-Advertisement-
Play Games

資料庫用戶通常依賴隔離級別來確保數據一致性,但很多資料庫卻並未達到其所表明的級別。主要原因是:一方面,資料庫開發者對各個級別的理解有細微差異;另一方面,實現層面沒有達到理論上的要求。 用戶在使用或開發者在交付資料庫前,需要對隔離級別進行快速的正確性驗證,並且希望驗證是可靠的(沒有誤差)、快速的(多項 ...


資料庫用戶通常依賴隔離級別來確保數據一致性,但很多資料庫卻並未達到其所表明的級別。主要原因是:一方面,資料庫開發者對各個級別的理解有細微差異;另一方面,實現層面沒有達到理論上的要求。

用戶在使用或開發者在交付資料庫前,需要對隔離級別進行快速的正確性驗證,並且希望驗證是可靠的(沒有誤差)、快速的(多項式時間)、有效的(找出異常)、通用的(任意資料庫)、可解釋的(可以debug,可以復現)。

Elle 就是針對以上問題提出的一個基於 Adya 模型的黑盒一致性檢測工具。Elle 通過精心設計的讀寫操作和版本控制,可以檢驗出 Adya 提出的所有非謂詞異常,並且具有一定可解釋性和復現性。在實踐中,Elle 在所測的四個資料庫上都測出了數據不一致。

探索前沿研究,聚焦技術創新。本期由騰訊雲資料庫高級工程師陳育興為大家介紹資料庫事務一致性檢測的技術原理及相關實現,包括背景、動機、解決方案等內容。

一、背景介紹

1.1 數據異常

我們熟知的數據異常有臟讀、臟寫、丟失更新等很多種類,如果從數據異常的角度來解釋一致性,即一致性是保證不出現數據異常。

file

我們以一個經典案例數據異常(寫偏序(Write Skew))對此進行說明。某用戶有兩個投資賬戶,允許其中一個賬戶暫時虧損,但兩個賬戶總額不能為虧損。轉賬前兩個賬戶各有$100,兩個事務同時開啟,A事務查詢總餘額發現有$200,併在第一個賬戶取出$200,B事務查詢總餘額也是$200,並且在第二個賬戶取$200,兩個事務都提交成功。各取出$200、總共取出$400,但按正常理解,超額取錢是不允許的,這種情況就是數據異常。然而這種操作在絕大部分資料庫的預設配置中都會出現。

file

該例子的寫偏序的標準測試樣例如上圖所示:初始資料庫有兩行數據,兩個事務都各自讀一行數據,兩個事務分別更新對方讀的數據,最後兩個事務都提交成功,這就是標準的寫偏序。這在很多資料庫的預設級別和快照級別都會出現,用戶通常需要額外的約束或需要資料庫開啟可串列級別才能避免該異常。

1.2 隔離級別 VS 數據異常

一致性有強弱之分,資料庫中滿足強/弱一致性需要通過隔離級別來實現。在某些弱級別下,異常的出現被視為正常,因為有些異常在部分業務場景下是可以被接受的。那我們為何要允許數據異常的出現,而不是禁止所有異常出現從而保證正確性?因為正確性和性能之間需要權衡,正確性越高,性能越差,允許一些數據異常,性能也會有所提升。

file

標准定義下存在四種異常,從P0到P3,逐步禁止,比如P0是臟寫,在所有級別中都不允許出現;P1是臟讀,在讀未提交允許出現,幻讀則允許在RR級別下出現;可串列級別理論上不允許任何異常出現。隔離級別越強,允許的異常就越少,且通常隔離級別為逐級疊加,即弱隔離級別不允許出現的異常,在更強的隔離級別也不允許出現。

四種標準的異常只是數據異常中的一小部分,還有更多數據異常的形式。在四種標準的級別之上也有更多的隔離級別。

file

上表顯示的是新的異常和新的隔離級別之間的允許/不允許關係,但並非時時刻刻都如此嚴格。一方面,各廠商的資料庫產品會因理解和實現的不同致使部分異常沒有按預期出現或禁止。另一方面,上述異常僅僅是一小部分,理論上存在的級別也還有很多。因此很多資料庫新用戶不知道哪些異常會出現或不應該出現,以及如何去理解這些級別和異常

二、動機

2.1 非傳統隔離級別

下圖所示是部分非傳統的隔離級別。比較常見的是快照隔離級別,如圖所示的部份廠商,從名字上我們無法直接判斷這些級別的具體表現,相關文檔的描述也比較模糊,因此就會引申出一個問題,即它們應該等價於哪些級別、對比當前級別它們是強或弱。

file

2.2 用戶層面

從用戶角度來看,主要存在以下三方面問題:

  • 如何針對自身業務選擇隔離級別,如何理解這些(新)隔離級別。比如哪些異常允許出現,哪些異常不允許出現?
  • 資料庫申明的隔離級別沒有達到標準。比如Oracle申明支持可串列級別,但它只消除了四種標準的異常,沒有消除所有異常,存在寫偏序。在串列級別存在寫偏序異常,這種申明現象在很多資料庫中都會出現。
  • 對隔離級別的定義標準不同,不單是可串列級別,其他弱隔離級別也是如此。比如在可重覆讀級別,PostgreSQL不存在幻讀但存在寫偏序,SQL Server則不存在寫偏序異常但存在幻讀。

file

2.3 廠商層面

從廠商角度來看,主要存在以下兩方面問題:

一方面,資料庫需要迭代版本,但回歸測試樣例一般都不完整,只能在一定程度上進行驗證。比如PostgreSQL在2011年推出的9.1版本中已經實現可串列化的快照隔離(SSI),但因為某些步驟優化導致在第三方事務插入後馬上更新干擾的情況下,出現G2異常(寫偏序),正常情況下不應出現,直到2019年推出12.4版本才對此進行修複。

另一方面,廠商需要研發新型事務資料庫,需要驗證開發的正確性,確保沒有缺陷或者沒有程式上的bugs影響

file

三、解決方案

3.1 Jepsen/Elle事務一致性測試框架

對上述問題,我們可以利用一個事務一致性檢測方案——Jepsen/Elle方案進行解決。Jepsen是一個更強大的框架,可以檢測分散式一致性、線性一致性等多種一致性級別,Elle是其中的一個事務驗證模塊,Elle方案目前已經在VLDB 2020會議中發表。

file

整體來看,Jepsen/Elle事務一致性測試框架的作用如下:

  • 測試出各種級別下存在的異常,幫助理解當前級別的表現;
  • 通過理解當前級別,可以驗證當前隔離級別是否達到要求;
  • 測試結果可解釋、可溯源、可復現。

3.2 定義數據異常

在解決上述問題之前,我們需要知道如何定義數據異常,以及學術界又如何看待資料庫異常

file

前文提到最簡單的一致性是不存在任何數據異常,但如何判斷發生了數據異常呢?比如正常要讀提交的值但卻讀到未提交的寫,一個事務兩次讀但卻讀到不一樣的值,這些能否歸為數據異常?其實,這些異常在一定程度上都算是數據異常,只是表述不夠正式且無法總結規律,因此我們需要用更規範的方式來定義數據異常。

file

在判斷有無數據異常前,我們需要把資料庫執行後的數據抽象地表示出來。Elle方案里採用Adya表示模型,這是一個比較標準通用的表示模型,可以將資料庫操作對象以及操作方式抽象出來。比如對象通常有x、y、z, 可以對應不同key,再用R、W、C、A對應讀、寫、提交和回滾。在資料庫執行完操作後,我們把一組事務操作記錄下來成為歷史(history),調度(schedule)是歷史的首碼(prefix)。兩者的區別在於,調度里仍有未完成的事務,但歷史里全是已完成的事務。

現階段寫偏序的執行可以描述成一個調度,其中讀寫操作的下角標表示事務,對象的下角標表示版本數。以下圖為例,寫偏序的調度為:事務1進行了讀操作,讀取了對象為x的0版本數據,事務2讀了對象為y的0版本數據,事務1改了y對象的值,事務2修改了x對象的值。

file

有了調度和歷史的概念後,我們可以去構建衝突圖。衝突圖是以事務為點、衝突為邊的圖模型。比如上圖右邊的寫偏序例子,事務1的讀和事務2的寫作用在同一個對象x上,從版本來看事務1的版本更小、事務2的版本更大,因此存在從事務1到事務2的RW衝突邊。同理在y對象上,存在由事務2到事務1的RW邊。我們可以看到,該圖是一個環結果,我們可以通過環的存在來判斷數據異常的存在。因為我們認為串列執行的結果是一個沒有問題的數據狀態,比如事務1先做,再做事務2,就不會有數據異常,而衝突圖有環的情況,其實就是不可串列的執行結果,它的結果不等價於任何一個串列執行的結果。因此,我們認為執行的狀態或結果為不可串列的就存在異常

file

如果我們把資料庫執行轉成歷史,通過歷史去建模衝突圖,再去判斷衝突圖是否有環,就可以輕易判斷是否存在數據異常。因為歷史或調度模型里可以確定讀寫版本,從而確定衝突依賴關係,容易做判斷。

3.3 問題與挑戰

在現實中,資料庫執行結果有時很難獲取統計,即使可以獲取統計,也很難直接轉化為確定的歷史或者調度。這主要有兩方面的問題:一方面,依賴關係有時可能性很多,很難決定;另一方面,如果併發事務較多,不確定的依賴關係就會更多,需要分析和決定的成本很高,導致驗證速度慢或可能性太多,記憶體和計算資源不足以在短時間內驗證太多可能性。

file

數據讀寫之間的依賴判斷存在以下難點:

  • 兩個事務都對K=1更新值,從兩個事務的歷史數據無法得知誰先誰後;
  • 兩個事務都對K=1更新V=5,其他事務讀到K=1、V=5時,無法得知是哪個事務的寫的數據;
  • 事務讀寫後是否參與衝突依賴判斷,需要兩個事務在時間上有交叉。但很多分散式時間不可信、不對齊,時間不一定對等;

如果考慮將所有可串列的結果去匹配執行結果,本質上是NP-complete問題,是一個非多項式時間的驗證,計算成本非常高。

3.4 Jepsen/Elle解決方案

file

Jepsen/Elle解決方案首先要保證得到可靠的歷史,需要執行結果滿足兩個特性:

  • 可追溯性,需要知道版本之間的順序,決定ww依賴,誰先寫、誰後寫需要確認。
  • 可複原性,需要知道讀的是哪個版本、誰的寫,從而決定寫讀依賴;讀寫依賴可以根據寫寫依賴和寫讀依賴進行推導。

file

Jepsen/Elle的輸入設置分為三種操作:

  • 讀操作,select語句。
  • 插入操作,insert語句。
  • 更新操作,update語句。該update語句與普通update不同,需要在更新值時附帶原有值,把原有值和更新值都保留。

file

具體示例如下:首先往t1表裡插入新值K=1,V=1。R1讀表裡的內容,讀到k=1、 v=1。W1更新行的內容,讓值更新為2。因為更新時我們會將原有值加進來,所以當R2再次讀時,我們讀到的是k=1,v=“1 2”。以此類推,當再次更新值為3時,我們讀到的是“1 2 3”。同一個變數上的更新使其保持唯一則不會有歧義,我們也知道更新版本順序,再通過讀數據,可以輕易推導出這些操作的讀寫依賴關係。

file

上圖是論文中給出的例子。R1中間的事務,讀了K=255的值2,3,4,5;R2上面的事務,讀了K=255的值為2,3,4,5, 8;W3下麵的事務在K=255上寫了值為8,我們可以得到從W3到R2的WR依賴和R1到W3的RW依賴,從最上面的事務到中間的時間依賴(real-time 依賴),可以用作嚴格一致性的判斷。

file

Elle檢測模型基本遵循Adya文章定義的環分類,比如G0異常為全是WW邊的環,G1c為WW或WR組合的環,加上G-single和G2,這些異常環的組合類似於四種異常現象,所以也有逐步不允許的限制。我們驗證隔離級別是否達標,就從最簡單的四種異常驗證轉化為四大類環的檢測。

file

Elle檢測可以保證正確性,只要測出異常,則該異常一定存在。只要出現異常,理論上可以復現,也說明資料庫在該模型下不一致。另一方面,Elle不能保證完整性,Elle檢測後不代表系統完全滿足一致性,因為有些異常不能用環表示,比如臟讀、臟寫、中間讀以及有些需要狀態確認的異常,Elle也不能檢測謂詞異常。

file

Elle通過初期寫的特殊處理,所有的依賴關係都是確定性的,通過事務執行結果來判斷依賴關係的複雜度,基本上都是線性。我們可以看到,隨著併發增大,粉色線的時間基本是平穩線性增長,而傳統做法需要比對任意事務之間的順序,複雜度是階乘於事務個數,隨著併發增大,驗證時間為指數增長。

file

上圖是用Elle工具在PostgreSQL老版本上測出的異常,在可串列級別下存在寫偏序異常。右邊的可復現的例子中, 共有三個事務,兩個事務新插入數據,且相互沒有讀到新插入的數據,從而形成一個寫偏序的環。出現該異常的原因是,第三個事務對某個插入進行更新導致後面的讀依賴沒有作用在插入值上。

3.5 Test  on TDSQL

file

我們在TDSQL上進行測試。結果顯示,可串列級別不存在任何異常,RR級別的表現屬於快照隔離級別水平。

四、總結

綜上所述,Elle事務一致性檢測框架主要解決兩個問題:

  • 通過寫版本疊加,在更新時保留舊值,從而確定版本順序以及把執行結果變為歷史調度。
  • 通過衝突圖的環檢測,從歷史調度判斷有無數據異常。此外,Elle也可通過疊加時間要求來檢測嚴格一致性,比如T2是T1 commit之後才開始的,那麼串列執行時必須為T1->T2,不允許出現T2->T1。

file

上述情況只涉及部分級別,我們還可以根據實際情況細分出更多的級別和一致性模型,用Elle進行更多的驗證。

file

最後,我們還可以從以下四方面對Jepsen/Elle事務一致性測試框架進行優化:

  • 框架本身並不簡單,需要很多參數調節才能達到效果。比如有些情況壓測不充分,小概率異常難於發現,有時不易復現。
  • 不支持Delete,不支持謂詞範圍查詢。無法檢驗幻讀(Phantom),無法判別Repeatable Read和Serializable之間的區別。
  • 採用新數據格式,而非傳統回歸測試的SQL語句,分析和debug都比較困難。
  • Jepsen有額外錯誤註入功能,但作者在Elle文章中並沒有細說。比如很多異常是因為某些節點重啟斷聯導致的,正常情況下允許並無異常。

參考文獻

[1] Atul Adya, Barbara Liskov, Patrick E. O'Neil: Generalized Isolation Level Definitions. ICDE 2000: 67-78
[2] Peter Alvaro, Kyle Kingsbury: Elle: Inferring Isolation Anomalies from Experimental Observations. Proc. VLDB Endow. 14(3): 268-280 (2020)


您的分享是我們最大的動力!

-Advertisement-
Play Games
更多相關文章
  • (1)基於機器視覺及深度學習理論,研發AI瑕疵識別演算法,應用至刨花板生產線質檢工段,滿足高可靠性、高實時性的刨花板板面質檢需求。(2)基於工業互聯網平臺的異構設備及系統集成,實現數據接入、處理、分析、決策等流程化應用,支持多條刨花板產線集成,助力企業產線協同管理和產線綜合對標。 ...
  • 摘要 C/S端軟體,左側導航菜單+右側頁面切換的佈局很常見。 這篇文章介紹下使用ContentControl控制項和TabControl控制項如何實現基礎的頁面切換。 一、使用ContentControl實現頁面切換 頁面使用UserControl來實現。 基於MVVM框架的思想,利用數據綁定機制,將控 ...
  • windows10系統“無法安裝Windows沙盒:在固件中禁用了虛擬化支持”,另外操作無法安裝hyoer-v該固件中的虛擬化支持被禁用問題。 ####解決辦法: 我這裡以聯想拯救者r720筆記本電腦為例,開啟cpu虛擬化: 1、打開聯想筆記本電腦,重新啟動電腦,在啟動的時候快速按鍵盤上的F2按鍵, ...
  • //源文件 static uint32_t fac_us = 0; // us延時倍乘數 /** * @brief 初始化延遲函數 * 當使用ucos的時候,此函數會初始化ucos的時鐘節拍 * SYSTICK的時鐘固定為AHB時鐘的1/8 * @param SYSCLK 系統時鐘頻率 */ voi ...
  • //源文件 void LedPhyConfig() { RCC->AHB1ENR |= (1<<1); //使能GPIOB //LD1 GPIOB->MODER |= (1<<0*2); //輸出模式 GPIOB->OTYPER &= ~(1<<0); //推輓 GPIOB->OSPEEDR |= ...
  • 背景:內網環境伺服器不能直接安裝工具或服務,可以用一臺外網伺服器同步阿裡雲的yum倉庫,作為本地倉庫 搭建本地yum倉庫 編輯yum配置文件,開啟緩存使用功能,設置緩存路徑 cp /etc/yum.conf /etc/yum.conf.bak vim /etc/yum.conf cachedir=/ ...
  • SingleStore(前身 MemSQL)是一個為數據密集型應用設計的雲原生資料庫。它是一個分散式的關係型 SQL 資料庫管理系統(RDBMS),具有 ANSI SQL 支持,它以數據攝入、交易處理和查詢處理的速度而聞名。SingleStore 主要存儲關係型數據,但也可以存儲 JSON 數據、圖 ...
  • 一、Installing ClickHouse-22.10.2.11 on openEuler 1 地址 https://clickhouse.com https://packages.clickhouse.com https://github.com/ClickHouse/ClickHouse 2 ...
一周排行
    -Advertisement-
    Play Games
  • 移動開發(一):使用.NET MAUI開發第一個安卓APP 對於工作多年的C#程式員來說,近來想嘗試開發一款安卓APP,考慮了很久最終選擇使用.NET MAUI這個微軟官方的框架來嘗試體驗開發安卓APP,畢竟是使用Visual Studio開發工具,使用起來也比較的順手,結合微軟官方的教程進行了安卓 ...
  • 前言 QuestPDF 是一個開源 .NET 庫,用於生成 PDF 文檔。使用了C# Fluent API方式可簡化開發、減少錯誤並提高工作效率。利用它可以輕鬆生成 PDF 報告、發票、導出文件等。 項目介紹 QuestPDF 是一個革命性的開源 .NET 庫,它徹底改變了我們生成 PDF 文檔的方 ...
  • 項目地址 項目後端地址: https://github.com/ZyPLJ/ZYTteeHole 項目前端頁面地址: ZyPLJ/TreeHoleVue (github.com) https://github.com/ZyPLJ/TreeHoleVue 目前項目測試訪問地址: http://tree ...
  • 話不多說,直接開乾 一.下載 1.官方鏈接下載: https://www.microsoft.com/zh-cn/sql-server/sql-server-downloads 2.在下載目錄中找到下麵這個小的安裝包 SQL2022-SSEI-Dev.exe,運行開始下載SQL server; 二. ...
  • 前言 隨著物聯網(IoT)技術的迅猛發展,MQTT(消息隊列遙測傳輸)協議憑藉其輕量級和高效性,已成為眾多物聯網應用的首選通信標準。 MQTTnet 作為一個高性能的 .NET 開源庫,為 .NET 平臺上的 MQTT 客戶端與伺服器開發提供了強大的支持。 本文將全面介紹 MQTTnet 的核心功能 ...
  • Serilog支持多種接收器用於日誌存儲,增強器用於添加屬性,LogContext管理動態屬性,支持多種輸出格式包括純文本、JSON及ExpressionTemplate。還提供了自定義格式化選項,適用於不同需求。 ...
  • 目錄簡介獲取 HTML 文檔解析 HTML 文檔測試參考文章 簡介 動態內容網站使用 JavaScript 腳本動態檢索和渲染數據,爬取信息時需要模擬瀏覽器行為,否則獲取到的源碼基本是空的。 本文使用的爬取步驟如下: 使用 Selenium 獲取渲染後的 HTML 文檔 使用 HtmlAgility ...
  • 1.前言 什麼是熱更新 游戲或者軟體更新時,無需重新下載客戶端進行安裝,而是在應用程式啟動的情況下,在內部進行資源或者代碼更新 Unity目前常用熱更新解決方案 HybridCLR,Xlua,ILRuntime等 Unity目前常用資源管理解決方案 AssetBundles,Addressable, ...
  • 本文章主要是在C# ASP.NET Core Web API框架實現向手機發送驗證碼簡訊功能。這裡我選擇是一個互億無線簡訊驗證碼平臺,其實像阿裡雲,騰訊雲上面也可以。 首先我們先去 互億無線 https://www.ihuyi.com/api/sms.html 去註冊一個賬號 註冊完成賬號後,它會送 ...
  • 通過以下方式可以高效,並保證數據同步的可靠性 1.API設計 使用RESTful設計,確保API端點明確,並使用適當的HTTP方法(如POST用於創建,PUT用於更新)。 設計清晰的請求和響應模型,以確保客戶端能夠理解預期格式。 2.數據驗證 在伺服器端進行嚴格的數據驗證,確保接收到的數據符合預期格 ...