Pendahuluan: Empat Baris Kode yang Melawan Intuisi ── Uji Litmus Store Buffering (SB)

Perhatikan program C konkuren bốn baris berikut. Dua variabel integer bersama x dan y diinisialisasi ke 0. Dua thread yang berjalan pada dua inti (core) CPU berbeda masing-masing mengeksekusi satu penulisan (Store) diikuti satu pembacaan (Load):

1
2
3
4
5
6
7
8
9

// Initial state in shared memory:
int x = 0, y = 0;
int r1 = 0, r2 = 0;

// Thread 1 (Core 0)          // Thread 2 (Core 1)
void thread1(void) {          void thread2(void) {
    x = 1;      // (S1)           y = 1;      // (S2)
    r1 = y;     // (L1)           r2 = x;     // (L2)
}                             }

Nilai akhir (r1, r2) apa saja yang mungkin terjadi setelah kedua thread selesai? Menurut akal sehat:

• Jika Thread 1 selesai sebelum Thread 2, hasilnya r1 = 0, r2 = 1.
• Jika Thread 2 selesai sebelum Thread 1, hasilnya r1 = 1, r2 = 0.
• Jika keduanya menjalankan baris pertama (x = 1 dan y = 1) sebelum baris kedua, hasilnya r1 = 1, r2 = 1.

Dalam urutan mana pun, setidaknya satu penulisan 1 pasti terjadi sebelum pembacaan oleh thread lawan; oleh karena itu, hasil r1 == 0 && r2 == 0 tampak mustahil secara matematis. Namun, jika Anda menjalankan kode ini pada prosesor modern Intel/AMD x86-64, chip Apple Silicon (ARMv8), atau dengan kompiler C/C++/Rust yang dioptimalkan (-O2), hasil “mustahil” r1 == 0 && r2 == 0 benar-benar terjadi ribuan kali per detik! Ini bukan kerusakan perangkat keras, melainkan akibat dari pengurutan ulang instruksi (Instruction Reordering) di bawah aturan “As-If” thread tunggal.

Bab 1: Ilusi Konsistensi Sekuensial (Sequential Consistency)

Pada tahun 1979, peraih Turing Award Leslie Lamport memformalkan model mental intuitif pemrogram sebagai Konsistensi Sekuensial (Sequential Consistency, SC): hasil dari setiap eksekusi adalah sama seolah-olah operasi dari semua prosesor dijalankan dalam satu urutan total global ($\prec_m$), dan operasi dari masing-masing prosesor muncul dalam urutan tersebut tepat sesuai urutan program (Program Order, $\prec_p$) yang tertulis di kode sumber.

Di bawah Konsistensi Sekuensial, ketidakmungkinan r1 == 0 && r2 == 0 dapat dibuktikan dalam tiga baris:

Agar $r_1 = 0$, pembacaan $L_1$ harus mendahului penulisan $S_2$ ($L_1 \prec_m S_2$). Demikian pula, $r_2 = 0$ mengharuskan $L_2 \prec_m S_1$. Menggabungkannya dengan urutan program $S_1 \prec_p L_1$ dan $S_2 \prec_p L_2$ menghasilkan siklus waktu yang kontradiktif $S_1 \prec L_1 \prec S_2 \prec L_2 \prec S_1$. Akan tetapi, karena x dan y adalah alamat berbeda tanpa ketergantungan data dalam satu thread, perangkat keras dan kompiler melanggar urutan global ini demi menyembunyikan latensi memori.

Bab 2: Model Memori Perangkat Keras ── Store Buffer, Protokol MESI, dan Invalidate Queue

2.1 Koherensi Cache MESI dan Reordering Store-Load melalui Store Buffer

Pada CPU 4 GHz modern, akses register hanya membutuhkan $0,25\text{ ns}$ (1 siklus) dan cache L1 sekitar $1\text{ ns}$, sedangkan sinkronisasi cache antar-inti atau akses DRAM membutuhkan $50\text{–}100\text{ ns}$ (hingga 300 siklus). Inti CPU menjaga koherensi baris cache melalui protokol MESI (Modified, Exclusive, Shared, Invalid). Saat Core 0 ingin mengubah variabel x yang berstatus Shared, ia harus menyiarkan pesan Invalidate (Read-For-Ownership, RFO) ke inti lainnya dan menunggu balasan konfirmasi (Ack).

Agar tidak menghentikan eksekusi selama puluhan siklus setiap kali menulis, semua CPU modern (termasuk x86-64!) menempatkan antrean FIFO privat bernama Store Buffer (buffer tulis) di antara unit eksekusi dan cache L1:

  flowchart TD
    subgraph Core0 ["Inti CPU 0 (Thread 1: x = 1; r1 = y;)"]
        Exec0["Unit Eksekusi (Core 0)"]
        SB0["Store Buffer Privat Core 0<br/>[Tertunda: x = 1] (Tidak terlihat oleh Core 1!)"]
        L1_0["Cache Data L1 (Core 0)<br/>y = 0 (Shared)"]
        Exec0 -- "1. Taruh x = 1 di Store Buffer & langsung lanjut" --> SB0
        Exec0 -- "2. Baca langsung r1 = y dari L1 (r1 = 0!)" --> L1_0
        SB0 -. "3. Kuras x = 1 ke L1 hanya setelah MESI Ack tiba" .-> L1_0
    end
    subgraph Core1 ["Inti CPU 1 (Thread 2: y = 1; r2 = x;)"]
        Exec1["Unit Eksekusi (Core 1)"]
        SB1["Store Buffer Privat Core 1<br/>[Tertunda: y = 1] (Tidak terlihat oleh Core 0!)"]
        L1_1["Cache Data L1 (Core 1)<br/>x = 0 (Shared)"]
        Exec1 -- "1. Taruh y = 1 di Store Buffer & langsung lanjut" --> SB1
        Exec1 -- "2. Baca langsung r2 = x dari L1 (r2 = 0!)" --> L1_1
        SB1 -. "3. Kuras y = 1 ke L1 hanya setelah MESI Ack tiba" .-> L1_1
    end
    L1_0 <== "Interkoneksi Koherensi Cache MESI (Invalidate / RFO)" ==> L1_1

Core 0 menyimpan x = 1 ke Store Buffer privatnya (belum terlihat oleh Core 1) dan langsung membaca r1 = y (0) dari cache L1 miliknya. Secara bersamaan, Core 1 menyimpan y = 1 ke Store Buffer-nya dan membaca r2 = x (0) dari cache L1 miliknya. Dengan demikian, pembacaan (Load) mendahului penulisan sebelumnya (Store) dalam visibilitas global: inilah Store-Load Reordering! (Jika Core 0 membaca kembali variabel x yang baru saja ditulisnya sendiri, mekanisme Store Buffer Forwarding langsung meneruskan x = 1 dari buffer lokal sehingga perilaku thread tunggal tetap terjaga.)

2.2 Model Kuat x86-TSO vs. Arsitektur Urutan Lemah (ARMv8, RISC-V, PowerPC)

Model x86-TSO (Total Store Order) dari Intel dan AMD menggunakan Store Buffer FIFO yang ketat: tidak pernah mengurutkan ulang Load-Load, Load-Store, maupun Store-Store, dan hanya mengizinkan pengurutan ulang Store -> Load. Sebaliknya, ARMv8-A (AArch64 / Apple Silicon), RISC-V (RVWMO), dan IBM PowerPC mengadopsi Model Memori Urutan Lemah (Weakly Ordered): akibat penggabungan tulis non-FIFO, pembacaan spekulatif out-of-order, dan Invalidate Queue, keempat kombinasi (Load-Load, Load-Store, Store-Store, Store-Load) dapat diurutkan ulang oleh perangkat keras!

Bab 3: Pengurutan Ulang Kompiler dan Teorema DRF-SC ── Mengapa Data Race Adalah Undefined Behavior (UB)

Bahkan pada CPU x86, pengiriman pesan tanpa sinkronisasi data = 42; ready = 1; tetap gagal karena kompiler pengoptimasi (gcc, clang, rustc) bebas mengurutkan ulang keempat jenis akses memori. Lebih buruk lagi: melalui Register Promotion dan Loop-Invariant Code Motion (LICM), kompiler mengubah loop tunggu while (!ready) menjadi pembacaan satu kali ke register diikuti loop tak terbatas (infinite loop)! Selain itu, kata kunci volatile di C/C++ hanya ditujukan untuk register MMIO dan tidak menghasilkan memory barrier CPU.

Pada tahun 1990, Sarita Adve dan Mark Hill membuktikan teorema DRF-SC (Data-Race-Free Sequential Consistency):

• Data Race: Dua thread mengakses lokasi memori yang sama secara bersamaan, setidaknya satu adalah penulisan, setidaknya satu non-atomik, dan tidak ada relasi Happens-Before ($\xrightarrow{hb}$) di antara keduanya.
• Kontrak DRF-SC: Jika program bebas dari Data Race (DRF), kompiler dan CPU menjamin setiap eksekusi berperilaku persis seperti Konsistensi Sekuensial (SC). Sebaliknya, satu saja Data Race di C/C++ atau Unsafe Rust menghasilkan Undefined Behavior (UB).

Bab 4: Relasi Happens-Before ($\xrightarrow{hb}$) dan Sinkronisasi Acquire-Release

Dalam model memori formal C++11 / C11 / Rust, ketika Thread 1 melakukan penulisan atomik Release $W_{\text{rel}}(x, v)$ dan Thread 2 melakukan pembacaan atomik Acquire $R_{\text{acq}}(x, v)$ yang membaca nilai tersebut ($W_{\text{rel}} \xrightarrow{rf} R_{\text{acq}}$), terbentuk jembatan lintas-thread bernama Synchronizes-With ($\xrightarrow{sw}$). Penutupan transitif dari urutan internal thread (Sequenced-Before, $\xrightarrow{sb}$) dan $\xrightarrow{sw}$ mendefinisikan relasi Happens-Before ($\xrightarrow{hb}$):

Dengan memory_order_release dan memory_order_acquire, pengiriman pesan dijamin aman secara matematis:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17

#include <atomic>
#include <cassert>

int data = 0;                        // Non-atomic payload
std::atomic<int> flag{0};            // Atomic synchronization variable

void producer_thread() {
    data = 42;                                           // (1) Sequenced-before (2)
    flag.store(1, std::memory_order_release);            // (2) Release store
}

void consumer_thread() {
    while (flag.load(std::memory_order_acquire) == 0) {  // (3) Acquire load
        // spin until flag == 1
    }
    assert(data == 42);                                  // (4) Guaranteed never to fail!
}

  flowchart TD
    subgraph Thread1 ["Thread Produsen (Core 0)"]
        W_data["(1) data = 42 (Penulisan non-atomik)"]
        W_flag["(2) flag.store(1, release) (Penulisan atomik Release)"]
        W_data -- "Sequenced-Before (sb)<br/>[Barrier Release melarang (1) turun melewati (2)!]" --> W_flag
    end
    subgraph Thread2 ["Thread Konsumen (Core 1)"]
        R_flag["(3) flag.load(acquire) == 1 (Pembacaan atomik Acquire)"]
        R_data["(4) assert(data == 42) (Pembacaan non-atomik)"]
        R_flag -- "Sequenced-Before (sb)<br/>[Barrier Acquire melarang (4) naik melewati (3)!]" --> R_data
    end
    W_flag == "Reads-From (rf) ⟹ Synchronizes-With (sw) terbentuk!" ==> R_flag
    W_data -. "Melalui transitivitas: Happens-Before (hb) terjamin!" .-> R_data

Bukti formal:

Bab 5: Spektrum Memory Ordering dan Pemetaan Instruksi CPU (MFENCE, DMB, LDAR/STLR)

C++ dan Rust menyediakan tiga tingkat pengurutan utama:

1. Relaxed: Hanya menjamin atomisitas dan urutan modifikasi ($\xrightarrow{mo}$) pada satu variabel tanpa sinkronisasi $\xrightarrow{sw}$ (cocok untuk penghitung sederhana).
2. Acquire / Release / AcqRel: Barrier satu arah (semantik Roach Motel) yang membentuk $\xrightarrow{sw}$, tetapi TIDAK mencegah pengurutan ulang Store -> Load ketika store(release) mendahului load(acquire).
3. SeqCst (bawaan): Menambahkan satu urutan total global $\xrightarrow{S}$ pada semua operasi SeqCst dan melarang pengurutan ulang Store -> Load (solusi untuk mencegah r1 == 0 && r2 == 0 pada uji SB).

Pada x86-64, Acquire dan Release dikompilasi menjadi instruksi mov biasa tanpa biaya perangkat keras, sedangkan store(seq_cst) menggunakan xchg (prefiks LOCK implisit) atau mfence untuk menguras Store Buffer. Pada ARMv8-A, instruksi khusus LDAR dan STLR menerapkan Acquire-Release dan SeqCst secara efisien tanpa memerlukan barrier penuh DMB ISH.