Giới thiệu thuật toán đồng thuận Paxos: nguồn gốc tên gọi, cách tiếp cận, chi tiết thuật toán và chứng minh định lí.

Paper The Part-Time Parliament - Leslie Lamport

Giới thiệu về đồng thuận

Định nghĩa

The consensus problem requires agreement among a number of processes (or agents) for a single data value. Some of the processes (agents) may fail or be unreliable in other ways, so consensus protocols must be fault tolerant or resilient. Wikipedia

Problem

Input: Có N process. Mỗi process P_i:

  • nhận vào input là 0 hoặc 1
  • Trả ra một output là V_i - khởi tạo có thể là B_i.

Output: Thiết kế một thuật toán rơi vào một trong 2 trường hợp sau:

  • Toàn bộ các process đưa ra output là 0
  • Toàn bộ các process đưa ra output là 1

Các kết quả

Một thuật toán consensus tổng quát sẽ thỏa mãn 3 thuộc tính

  • Agreement: các correct process sẽ phải đồng thuận trên cùng một giá trị
  • Integrity: Nếu tất cả correct process quyết định cùng một giá trị v, phải tồn tại một process đã propose giá trị v.
  • Termination: Eventually toàn bộ các process đều phải đồng thuận trên cùng một giá trị

Bài toán đồng thuận:

  • Có thể giải quyết được trên môi trường mạng đồng bộ.
  • không thể giải quyết được trên môi trường mạng bất đồng bộ (FLP Impossibility)

Đồng thuận là bài toán fundemental nhất trong hệ thống phân tán. Tham khảo chi tiết thêm tại: Đồng thuận trong hệ thống phân tán

Single-decree Paxos

Paper

Giới thiệu

Là một thuật toán đồng thuận, được trình bày vào năm 1989 bởi Lesie Lamport - nổi tiếng trước đấy với Lamport timestamp. (giải thưởng Dijkstra năm 2000).

Paxos đảm bảo tính đúng đắn (safety) và eventually liveness, do vậy vẫn đảm bảo theo định lí FLP Impossibility: Paxos không đảm bảo hệ thống sẽ đạt được đồng thuận. Sẽ được trình bày rõ hơn ở phần sau.

Câu hỏi: Khác biệt giữa single-decree Paxos và các thuật toán đồng thuận khác như Raft / ZAB / ViewStamped Replication là gì?

Trả lời: Các thuật toán đồng thuận nêu trên được thiết kế để đồng thuận trên nhiều giá trị, thích hợp để vận hành ngay lập tức. Single Paxos được giới thiệu vào năm 1989 - giải quyết trực tiếp về sự đồng thuận như phần định nghĩa. Do vậy, Single-decree Paxos chỉ xử lí đồng thuận trên một giá trị.

Nguồn gốc

Nguồn gốc tên gọi từ Paper đầu tiên - The Part-Time Parliament, nói về nghị viện (partliament) trên một hòn đảo tên là Paxos (Hi Lạp), người dân ở đây được gọi là Paxon, cần thông qua (consensus) các điều luật (decree). Các thông tin trên hòn đảo này:

  • Part-time legislators: những người thông qua các đạo luật. Việc thông qua các đạo luật ở hòn đảo rất đơn giản: khi có ai raise ra một đạo luật mới, họ sẽ approve. Tuy nhiên, không ai muốn làm công việc này full-time cả mà chỉ part-time. Có thể họ làm trong cùng một ngày, làm giữa chừng rồi về nhà chơi với vợ. legislators là đại diện cho các node trong hệ thống phân tán, và việc có thể ra khỏi tòa thị chính → node có thể crash bất cứ lúc nào.
  • Messenger: người giao thư - là cách giao tiếp duy nhất giữa các legislators. Người giao thư là người trung thực: họ không sửa đổi nội dung thông tin, tuy nhiên lại rất lười: lâu lâu có thể bỏ việc giữa chừng và hay quên. Do vậy, thi thoảng họ quên mất là đã deliver thông tin, do vậy có thể deliver lại nhiều lần cho cùng một thông tin. Messenger đại diện cho mô hình asynchronous network trong hệ thống phân tán.
  • Decree: là các điều khoản cần được thông qua. Nghị viện cần đồng thuận trên các điều khoản này. Là nguồn gốc tên gọi của Single-decree / Multi-Decree Paxos.
  • President: là người đứng đầu, để quản lí việc đồng thuận trên nhiều điều khoản khác nhau (là leader trong mô hình Multi-Paxos). Tương tự như các cư dân khác, president cũng rất lười và có thể bỏ việc giữa chừng - đại diện cho việc leader có thể bị crash bất kì lúc nào trong quá trình thực thi.

Components

Role

  • Proposer: là một node có khả năng propose một giá trị cho acceptor
  • Acceptor: nhận giá trị từ proposer và đưa ra quyết định accept / deny
  • Learner: học được kết quả từ acceptor

Một node có thể đóng nhiều role. Ví dụ, nếu một node là proposer và acceptor, khi node đấy propose một giá trị V thì đồng thời cũng sẽ accept luôn giá trị V đấy.

Gói tin Có 4 gói tin, và chia thành 2 phase:

Phase 1:

  • Prepare
  • Promise

Phase 2:

  • Propose / Accept-Request
  • Accept

Thuật toán đồng thuận Raft: có 3 role là Leader; Follower; Candidate và chỉ có 2 gói tin: RequestVote và AppendEntries. So sánh giữa Paxos và Raft:

  • Điểm mạnh: Chia nhỏ các role / gói tin → dễ dàng tối ưu hóa thuật toán hơn. Hơn nữa, tuy rằng Raft chỉ dùng có 2 gói tin nhưng lại piggyback rất nhiều thông tin vào các gói tin.
  • Điểm yếu: phức tạp hơn trong việc hiểu thuật toán.

Thinking Process

Design 1

Proposer Acceptor
Send propose(v) đến acceptor Khi nhận được propose(v):
- nếu đã decide giá trị Vx: trả về Vx cho proposer (agreement property)
- nếu chưa decide: nhận V và send decide(v) đến các learner

Nhược điểm: Availability. do chỉ có 1 acceptor: nếu acceptor bị fail, hệ thống không thể đạt được đồng thuận được.

Design 2:

Sử dụng quorum: Ta sẽ tăng số acceptor lên để có được high availability. Một giá trị v được chọn khi strictly majority các acceptor cùng decide một giá trị V.

Proposer Acceptor
Send propose(v) đến acceptor Khi nhận được propose(v):
- nếu đã decide giá trị Vx: trả về Vx cho proposer (agreement property)
- nếu chưa decide: When majority of correct acceptors have decided v: send decide(v) to learners

Nhược điểm:

Split Vote: Nếu acceptor chỉ accept giá trị đầu tiên nhận được → nếu nhiều proposal, có thể không có proposal nào được chọn.

SplitVote

Conflicting choice: Ngược lại, nếu acceptor accept mọi giá trị nhận được → consensus trên nhiều giá trị

Conflicting Choice

Design 3:

Khi một giá trị được chọn, các proposal tương lai phải propose cùng một giá trị. → 2-phase protocol

Tiếp cận: Sử dụng một “logical timestamp”. Ta sẽ tạo ra ballot number: là một số tự nhiên duy nhất gắn liền với các proposal được tạo bởi các proposer.

Cách tạo: Giả dụ với một hệ thống có 3 node: node 1 sử dụng các ballot number dạng 3k+1 (e.g.: 1/4/7) Node 2 sử dụng các ballot id dạng 3k+2 (e.g.: 2/5/8). Node 3 sử dụng các ballot number dạng 3k (e.g.: 3/6/9)

Proposer Acceptor
Send propose(ballot, value) đến acceptor, với ballot là ballot tạo ra và duy nhất, value là giá trị mà proposer muốn propose Khi nhận được propose(ballot, value):
- Nếu ballot < bất ki một ballot nào nhận được: gói tin này thuộc về quá khứ –> reject
- Nếu đã decide giá trị Vx: set v=Vx (nhằm đảm bảo agreement property)
- Nếu chưa quyết định bất kì giá trị nào: set v=value
Trả về cho proposer promise(ballot, v)
Sau khi nhận được response: nếu được majority votes:
- nếu tồn tại một giá trị V_i trả về: set V_sent = V_i
- Ngược lại, set V_sent = V (giá trị muốn propose ban đầu)
Gửi Accept(ballot, V_sent) 		Khi nhận được accept(ballot, value):
- Nếu ballot < bất ki một ballot nào nhận được: ballot này thuộc về quá khứ –> reject
- Set V_local = value, sau đấy gửi kết quả cho learner.

Thuật toán

Message Table

Paxos Algorithm

Một số khả năng có thể xảy ra lúc thực thi

Trường hợp 1: Là trường hợp hiển nhiên nhất. Giá trị trước đấy đã được chọn (quá bán) Paxos Algorithm

Trường hợp 2: Giá trị trước đấy chưa được chọn trên quá bán, nhưng proposer đã thấy Paxos Algorithm

Trường hợp 3: Giá trị trước đó chưa được chọn, và proposer chưa thấy Paxos Algorithm

Tính đúng đắn

Agreement: khi acceptor nhận được prepare(e) từ proposer, và đã nhận được một giá trị v trước đó → thông báo cho proposer → ta đang cố gắng đồng thuận trên cùng một giá trị. Ta sẽ chứng minh rõ hơn ở phần sau.

Integrity

Termination Paxos Algorithm

Ta thấy rằng thuật toán không đảm bảo sẽ kết thúc trong mọi trường hợp (tương tự hầu như các thuật toán consensus khác), và do thấy không vi phạm định lí FLP Impossibility.

Chứng minh

Tại sao ta nên nắm được chứng minh thuật toán

  • Hiểu rõ được thuật toán
  • Cần implement lại thuật toán
  • Optimize thuật toán

Ta sẽ chứng minh thuộc tính agreement: thuật toán chỉ đồng thuận trên tối đa một giá trị.

Định nghĩa

Proposal (m, u) là một proposal với ballot id = m, và giá trị là u.

Proposal (m, u) gọi là accepted khi và chỉ khi được accept bởi ít nhất 1 process.

Proposal (m, u) gọi là selected khi và chỉ khi được accept bởi quá bán các process.

-> Một nhận xét đơn giản: Nếu proposal M=(m, u) được selected, proposal M phải được *accepted trên ít nhất một node.

Như vậy, ta cần chứng minh: với bất kì 2 proposal (m, u) và (m’, w) được chọn bất kì, thì u = w. Hay nói cách khác, toàn bộ các node đồng thuận trên tối đa một giá trị. Lưu ý: có thể có nhiều ballot id, hay nói cách khác, đồng thuận không áp dụng cho ballot id.

Chứng minh

Ta dùng phản chứng: Giả sử tồn tại 2 proposal (m, u) và (m’, w) được chọn mà u != w. Dễ dàng thấy được là m != m’:

–> Nếu m = m’: 2 bộ proposal (m, u) và (m’, w) đều xuất phát từ cùng một proposer do ballot id là unique giữa các proposer. Song song đó, một proposer chỉ propose tối đa một giá trị, do vậy u phải bằng với w. Mâu thuẫn với giả thiết.

Do vậy, m != m’. Không mất tính tổng quát, giả sử m < m’.

gọi n là proposal number nhỏ nhất mà n > m, đồng thời proposal (n, v) được accepted với v != u. Cặp giá trị (n, v) luôn tồn tại. Ví dụ ta lấy proposal (m’, w) được nêu ở phần trên:

  • m’ > m (giả thiết thêm vào)
  • w != u (giả thiết ban đầu)
  • Proposal (m’, w) được selected**, do vậy proposal (m’, w) phải được **accept* trên ít nhất một node.

Từ đó, ta có chuỗi proposal, sắp xếp theo ballot id tăng dần như sau:

(m, u) (m1, u) (m2, u) ... (m_x, u) (n, v) ... (m', w) (lưu ý: giá trị luôn là u cho đến khi ballot id = n, value bị switch sang v)

Vì n nhỏ nhất mà proposal (n, v) mà v != u, do vậy, với mọi k mà m <= k < n, toàn bộ accepted proposal (k, value) sẽ có value = u - như minh họa ở trên (1)

Ta sẽ chứng minh phản chứng là không tìm được n như vậy.

Ta có 2 nhận xét sau:

Nhận xét 1: Proposal (m, u) được accepted → (m, u) được selected bởi một majority các acceptor M1.

Nhận xét 2: Proposal (n, v) được accepted → hiển nhiên tồn tại một proposer P đã send message Accept-Request(n, v). Và trước khi proposer P gửi request Accept-Request(n, v), theo thuật toán, P sẽ tổng hợp giá trị v từ các request Promise(n, [k, value)] từ một majority M2, với value là một giá trị bất kì và k < n (lí do: nếu tồn tại k > n, proposer sẽ reject). Lưu ý: value có thể rỗng - nếu acceptor chưa nhận bất kì một proposal nào. (2)

Paxos Algorithm

Do 2 majority set luôn giao nhau tại tối thiểu một node, Gọi S3 là giao giữa M1 và M2. Do vậy:

  • Do S3 thuộc M1, S3 đã accepted proposal (m, u)
  • Do S3 thuộc M2, S3 đã accepted proposal (n, v), và đồng thời cũng đã send request Promise(n, [k, value]) về cho P (như trình bày phần trên)

Ta sẽ chứng minh value trong trường hợp này bằng u. (*):

Vì n > m (giả thiết), S3 phải accept proposal (m, u) trước khi gửi Promise(n, (k, value)), nếu ngược lại, thì proposal (m, u) sẽ bị reject vì m < n. Đồng thời, m <= k vì bất kì acceptor nào cũng chỉ giữ ballot ID lớn nhất từng xuất hiện (giữa m và k, S3 có thể nhận nhiều proposal khác). (3)

Từ (2) và (3) => m <= k < n, và cùng với (1), value phải bằng u.

Do vậy, process S3 cũng chính là acceptor đã gửi ngược về cho process P giá trị u. (như hình vẽ)

(*) được chứng minh.

Ta sẽ tiếp tục chứng minh u là giá trị lớn nhất được trả về cho P. (**)

Xét một request Promise(n, [j, value]) bất kì mà các node trong M2 sẽ gửi về cho proposer P:

  • Nếu j < k: sẽ nhận v (lí do: chọn giá trị từ acceptor có ballot ID lớn nhất)
  • Nếu k <= j < n: do m <= k , thành ra m <= j < n: và từ (1), value phải bằng u.

Do vậy (**) được chứng minh.

Ta thấy, u là giá trị lớn nhất mà các acceptor trả về cho proposer P, do vậy theo thuật toán, P sẽ gửi message Accept-Request(n, u) về cho các acceptor. Do vậy, u == v, trái với giả thiết ban đầu.

Do vậy, với bất kì 2 proposal (m, v) và (m’, v’) nào được chọn, thì v phải bằng v’. Do vậy, toàn bộ các node trong hệ thống đều đồng thuận tối đa một giá trị.

Raft và Single-decree Paxos có cách tiếp cận tương đối giống nhau để chứng minh. Ta có thể tham khảo thêm phần chứng minh về Raft tại bài viết này

Nhận xét về paper

Điểm tốt

  • Không quá khó đọc để hiểu ý chính như chúng ta thường nghe
  • Gắn nội dung một bài toán thuần về theory qua một ngữ cảnh thông thường rất là hay, và dí dỏm.
  • Cách trình bày đi theo cách quá trình tạo ra protocol chứ không phải kết quả cuối cùng. Cách viết này của bác Lesie Lamport được ứng dụng trên rất nhiều paper được viết ra.

Điểm yếu

  • Phối trộn liên tục nội dung giữa bài toán thực tế (part-time parliament), bài toán lí thuyết và chứng minh lí thuyết.
  • Dễ hiểu để nắm nội dung. Nhưng nếu ta đọc paper về Raft rồi thì sẽ thấy nội dung này còn thật sự xa để implement trên hệ thống thực tế. Đặc biệt là Multi-decree Paxos. Tuy nhiên điểm yếu này được improve một phần ở version sau: “Paxos made Simple”