Correctness, Konsensus, dan FLP Impossibility

Back to IF3130 Sistem Paralel dan Terdistribusi

Correctness (Kebenaran) dan Masalah Konsensus

Questions/Cues

• Apa itu ‘Correctness’?

• Dua jenis properties?

• (1) Safety Properties?

• (2) Liveness Properties?

• Contoh Safety?

• Contoh Liveness?

• Apa itu Consensus Problem?

• 4 Properti Konsensus?

• (1) Agreement?

• (2) Integrity?

• (3) Termination?

• (4) Validity?

• Apa itu ‘FLP Impossibility’?

• Siapa penemu FLP?

• Apa asumsi model FLP?

• Apa implikasi FLP?

Reference Points

• Slides 15-19

Correctness in Distributed Systems

Correctness (kebenaran) sebuah sistem dinyatakan sebagai properties (pernyataan) yang mendeskripsikan perilaku sistem. Ada dua jenis utama:

1. Safety Properties

• Menyatakan bahwa “sesuatu yang buruk tidak akan pernah terjadi”.

• Jika sebuah safety property dilanggar satu kali saja (pada waktu t), ia akan dilanggar selamanya (tidak bisa diperbaiki).

• Contoh: “Hanya satu proses yang boleh berada di critical section pada satu waktu” (Mutual Exclusion).

• Cara termudah untuk menjamin safety adalah dengan “tidak melakukan apa-apa” (do nothing).

2. Liveness Properties

• Menyatakan bahwa “sesuatu yang baik pada akhirnya akan terjadi”.
• Meskipun sistem sedang dalam masalah (pada waktu t), selalu ada harapan bahwa properti ini akan terpenuhi di masa depan.
• Contoh: “Setiap permintaan pada akhirnya akan menerima respons”.

Tantangan utama dalam sistem terdistribusi adalah menjamin keduanya (Safety dan Liveness) secara bersamaan.

Problem: Consensus (Konsensus)

Konsensus adalah masalah fundamental di mana sekumpulan proses (node) harus setuju (sepakat) pada satu nilai (keputusan) yang sama.

• Properti Konsensus yang Benar:

  1. Agreement (Persetujuan): (Safety) Semua proses yang correct (tidak crash) harus setuju pada nilai yang sama.

  2. Integrity (Integritas): (Safety) Nilai yang disepakati harus merupakan nilai yang sebelumnya pernah diusulkan oleh salah satu proses. Sistem tidak boleh mengarang nilainya sendiri.

  3. Termination (Terminasi): (Liveness) Semua proses yang correct pada akhirnya harus mencapai keputusan. (Sistem tidak boleh hang selamanya).

  4. Validity (Validitas):- Jika semua proses correct mengusulkan nilai V yang sama, maka nilai V-lah yang harus disepakati.

Hasil Teoretis: FLP Impossibility

Ini adalah salah satu hasil teoretis paling penting dalam ilmu komputer.

• Penemu:- Fischer, Lynch, dan Paterson (1985).

• Teorema:- Menyatakan bahwa tidak ada algoritma deterministik- yang dapat menjamin konsensus dalam waktu terbatas (menjamin Termination) pada sistem asynchronous, bahkan jika hanya ada satu proses- yang gagal (model crash failure).

• Model Asumsi FLP:

  1. Sistem Asynchronous (tidak ada batas waktu).

  2. Network Reliable (pesan pasti sampai, tapi bisa tertunda).

  3. Minimal satu node bisa crash.

• Implikasi:- Ini adalah “pukulan” besar. Artinya, di dunia nyata (yang asynchronous), kita harus mengorbankan sesuatu. Algoritma konsensus praktis (seperti Paxos/Raft) harus “mengakali” teorema ini, biasanya dengan mengorbankan liveness (termination) dalam skenario terburuk, atau dengan menggunakan model yang lebih kuat (seperti partial synchrony).

Summary

Kebenaran (Correctness) sistem terdistribusi didefinisikan oleh- Safety (hal buruk tidak pernah terjadi) dan- Liveness (hal baik akhirnya terjadi). Masalah- Konsensus—di mana semua node harus setuju pada satu nilai—adalah inti dari banyak sistem. Namun, Teorema- FLP Impossibility membuktikan bahwa konsensus yang- dijamin berhenti (Termination/Liveness) adalah- mustahil dicapai dalam sistem- asynchronous jika ada risiko satu node- crash.

Additional Information

Pendalaman: Bagaimana Paxos dan Raft “Mengakali” FLP?

FLP berkata konsensus mustahil di model asynchronous murni. Algoritma praktis seperti Paxos- (Lamport) dan Raft- (Ongaro & Ousterhout) berhasil mencapai konsensus di dunia nyata. Bagaimana?

• Mereka tidak menggunakan model asynchronous murni.

• Raft dan Paxos menggunakan timeout- untuk mendeteksi kegagalan leader. Penggunaan timeout ini secara implisit mengasumsikan model Partial Synchrony- (lihat Ad Libitum Catatan 5).

• Mengorbankan Liveness (Termination):- Dalam skenario terburuk (misal, network partition yang membagi sistem 50/50, atau leader terus-menerus crash dan dipilih ulang), algoritma ini tidak bisa termination (gagal mencapai konsensus). Mereka mengorbankan liveness sementara demi menjamin safety (tidak pernah setuju pada nilai yang salah).

Pendalaman: Paxos vs. Raft

Keduanya adalah algoritma konsensus untuk model crash-recovery.

• Paxos (oleh Leslie Lamport):

  • Sangat penting secara teoretis, terbukti aman.

  • Terdiri dari dua fase: Phase 1 (Prepare/Promise) dan Phase 2 (Accept/Accepted).

  • Terkenal sangat sulit dipahami dan diimplementasikan dengan benar.

• Raft (dari Stanford):

  • Dibuat sebagai alternatif Paxos yang mudah dipahami (Understandable Consensus).

  • Memecah masalah konsensus menjadi 3 bagian:

    1. Leader Election:- Memilih satu node sebagai leader.

    2. Log Replication:- Leader menerima perintah, menuliskannya ke log miliknya, dan memaksa follower untuk menyalin log tersebut.

    3. Safety:- Menjamin jika sebuah entri log sudah di-commit, tidak ada leader lain yang bisa menimpanya.

  • Raft saat ini jauh lebih populer untuk implementasi baru (misal: di etcd Kubernetes, Consul).

Sumber & Referensi Lanjutan:

• Paper FLP:- “Impossibility of Distributed Consensus with One Faulty Process” oleh Fischer, Lynch, Paterson.

• Raft:- https://raft.github.io/ (Situs ini memiliki visualisasi yang sangat bagus untuk memahami cara kerja Raft).

• Paxos:- “Paxos Made Simple” oleh Leslie Lamport (Judulnya “Simple”, tapi isinya terkenal rumit).