Menunggu race conditions muncul di produksi bukanlah pengujian. Itu adalah harapan yang menyamar sebagai ketekunan.
Anda bisa menjalankan aplikasi selama berminggu-minggu, memantau dashboard metric, dan tetap saja meluncurkan bug konkurensi yang baru terpicu ketika dua request mengenai jendela cache eviction yang persis sama. Masalahnya bukan karena Anda sial. Masalahnya adalah strategi pengujian Anda bergantung pada scheduler yang bersikap jahat demi kepentingan Anda, pada saat yang tepat, sementara Anda kebetulan sedang mengamati.
Ada cara yang lebih baik. Model checking memungkinkan Anda menjelajahi setiap interleaving yang mungkin dari logika konkuren Anda dalam hitungan detik, bukan hari. Ia akan menemukan race condition yang tidak Anda pikirkan untuk ditulis tesnya.
Apa yang sebenarnya dilakukan model checking
Model checking bukan fuzzer. Ia tidak melemparkan input acak ke kode Anda dan berdoa. Ia membangun model matematis dari kemungkinan state sistem Anda dan menelusurinya secara exhaustif.
Bayangkan program konkuren Anda sebagai graph. Setiap node adalah state: nilai variabel Anda, konten queue Anda, thread mana yang memegang lock mana. Setiap edge adalah langkah: thread membaca nilai, mengakuisisi mutex, atau mengirim pesan. Scheduler memilih thread mana yang berjalan berikutnya, dan pilihan itu membifurkasi graph.
Sebuah model checker berjalan melalui setiap path di graph ini. Jika ada path yang mengarah pada dua thread menulis ke memori yang sama tanpa sinkronisasi, ia melaporkan counterexample: urutan langkah eksak yang memicu bug.
Wawasan kuncinya adalah model checker mengontrol scheduler. Di produksi, Anda ada di bawah belas kasih sistem operasi. Di model checker, Anda adalah sistem operasi. Anda bisa menjeda thread sebelum mengeksekusi baris kritis, membiarkan thread lain menjalankan seluruh metodenya, lalu melanjutkan thread pertama. Anda bisa menjelajahi interleaving yang di dunia nyata akan memerlukan sinar kosmik dan gangguan jaringan untuk direproduksi.
Race condition yang model checker tangkap dalam milidetik
Berikut adalah bug klasik: dua goroutine menaikkan counter bersama.
package main
import (
"fmt"
"sync"
)
func main() {
var counter int
var wg sync.WaitGroup
for i := 0; i < 2; i++ {
wg.Add(1)
go func() {
defer wg.Done()
// Read, increment, write: three steps
val := counter
val++
counter = val
}()
}
wg.Wait()
fmt.Println(counter) // Expected 2, often prints 1
}Jalankan ini seribu kali dan mungkin mencetak 2 setiap saat. Scheduler bukan musuh Anda sesuka hati. Tapi model checker melihat urutan read-increment-write tiga langkah dan tahu: jika goroutine A membaca 0, lalu goroutine B membaca 0, lalu keduanya menaikkan dan menulis 1, counter berakhir di 1 alih-alih 2.
Ia tidak perlu berjalan selama berhari-hari. Ia hanya perlu menjelajahi dua branch.
Cara melakukan model checking pada kode Anda sendiri
Anda tidak perlu memverifikasi seluruh codebase secara formal untuk mendapatkan nilai dari model checking. Sebagian besar tim mendapatkan 80% manfaat dengan memodelkan 20% kode mereka tempat konkurensi benar-benar penting.
Workflow-nya terlihat seperti ini:
-
Isolasi komponen konkuren. Singkirkan HTTP handler, query database, dan logging. Fokus pada state machine: thread atau goroutine apa yang ada, state bersama apa yang mereka sentuh, dan primitif sinkronisasi apa yang digunakan?
-
Tulis model abstrak. Ganti struktur data nyata dengan versi sederhana yang menangkap perilaku yang Anda pedulikan. Jika Anda memeriksa job queue, Anda tidak memerlukan payload job yang sebenarnya. Anda memerlukan queue, worker, dan flag yang menunjukkan apakah job sedang berlangsung.
-
Definisikan properties yang ingin Anda pertahankan. Ini adalah invariant Anda. “Dua worker tidak pernah memproses job yang sama.” “Sebuah job tidak pernah hilang.” “Cache dan database tidak pernah bertentangan.”
-
Biarkan model checker berjalan. Ia akan mengatakan “semua invariant terpenuhi” atau memberi Anda counterexample trace.
Berikut adalah tampilan model minimal dalam Python menggunakan explicit-state checker sederhana:
from collections import namedtuple
# Abstract model of a counter with two threads
State = namedtuple('State', ['counter', 'pc1', 'pc2'])
def successors(state):
"""Return all states reachable in one step."""
results = []
c, pc1, pc2 = state
# Thread 1: three-step increment
if pc1 == 0:
results.append(State(c, 1, pc2)) # read
elif pc1 == 1:
results.append(State(c, 2, pc2)) # increment
elif pc1 == 2:
results.append(State(c + 1, 3, pc2)) # write
# Thread 2: three-step increment
if pc2 == 0:
results.append(State(c, pc1, 1))
elif pc2 == 1:
results.append(State(c, pc1, 2))
elif pc2 == 2:
results.append(State(c + 1, pc1, 3))
return results
def check():
initial = State(0, 0, 0)
visited = set()
stack = [initial]
while stack:
state = stack.pop()
if state in visited:
continue
visited.add(state)
# Invariant: if both threads finished, counter must be 2
if state.pc1 == 3 and state.pc2 == 3 and state.counter != 2:
print(f"BUG: counter={state.counter}")
return
stack.extend(successors(state))
print("No race condition found in model.")
check()Ini tidak siap produksi. Ini adalah dua puluh baris Python yang mendemonstrasikan ide tersebut. Model checker nyata seperti TLA+, Spin, atau mCRL2 menangani deduplikasi state, properties logika temporal, dan partial-order reduction sehingga Anda dapat memeriksa sistem dengan jutaan state. Tapi model mentalnya sama: enkode sistem Anda, nyatakan invariant, jelajahi.
Masalahnya: ledakan state space
Model checking tidak gratis. Jika Anda memiliki empat thread, masing-masing dengan sepuluh langkah berikutnya yang mungkin, graph state Anda tumbuh secara eksponensial. Tambahkan integer 64-bit dan state space menjadi benar-benar tidak dapat diperiksa.
Solusinya adalah abstraksi. Anda tidak memodelkan cache Anda yang sebenarnya. Anda memodelkan “cache memiliki key” atau “cache tidak memiliki key.” Anda tidak memodelkan database Anda yang sebenarnya. Anda memodelkan “committed” atau “uncommitted.”
Inilah bagian yang membuat orang tersandung. Mereka mencoba melakukan model checking pada kode nyata mereka dan checker berjalan selamanya. Lalu mereka meninggalkan model checking sepenuhnya, yang seperti meninggalkan unit test karena Anda mencoba menguji seluruh aplikasi dalam satu test case.
Disiplinnya adalah: modelkan konkurensinya, bukan business logic-nya. Jika race condition Anda bergantung pada nilai eksak dari user ID, Anda sudah kalah. Race conditions terjadi karena interleaving, bukan karena nilai data.
Alat yang benar-benar berfungsi
Jika Anda ingin mulai melakukan model checking pada kode nyata, Anda punya pilihan.
Untuk Go: gosim memungkinkan Anda menjalankan program Go dengan scheduler deterministik yang Anda kendalikan dari model checker. Ia akan menemukan interleaving yang merusak asumsi sync.Mutex Anda.
Untuk Rust: shuttle adalah framework pengujian konkurensi deterministik dari AWS Labs. Ia menjalankan kode async Anda ribuan kali dengan pilihan scheduler yang berbeda dan akan menemukan races yang loom (alat lain yang sangat baik) periksa di tingkat memory model.
Untuk sistem terdistribusi: TLA+ adalah pilihan kelas industri. Amazon menggunakannya untuk menemukan bug di DynamoDB dan S3 sebelum diluncurkan. Kurva pembelajarannya nyata, tapi return on investment untuk sistem kritis dapat diukur.
Untuk awal yang lembut: Tulis skrip Python seperti di atas. Butuh satu jam, menemukan bug, dan membangun intuisi yang membuat TLA+ kurang mistis ketika Anda membutuhkannya.
Apa yang ini tidak gantikan
Model checking menemukan logic error dalam kode konkuren. Ia tidak menemukan performance regression, memory leak, atau bug yang hanya muncul di bawah beban produksi. Ia tidak akan memberi tahu Anda bahwa kontensi mutex Anda melonjak pada 10.000 request per detik.
Gunakan bersama stress testing, bukan sebagai penggantinya. Stress testing memberi tahu Anda apakah sistem Anda bertahan dari beban. Model checking memberi tahu Anda apakah sistem Anda bertahan dari interleaving yang dibuat oleh beban tersebut.
Mulai dari mana
Pilih satu komponen konkuren yang pernah menggigit Anda sebelumnya. Sebuah job queue, connection pool, rate limiter. Tulis invariant dalam plain English. Lalu habiskan satu sore membangun model kecil.
Anda mungkin akan menemukan bug yang tidak Anda ketahui keberadaannya. Atau Anda akan memperoleh keyakinan bahwa bug yang Anda khawatirkan tidak bisa terjadi. Hasil mana pun lebih berharga daripada seminggu lagi menonton grafik produksi dan berharap.
Jika Anda menginginkan langkah konkret berikutnya, tutorial Learn TLA+ akan membawa Anda dari nol ke memeriksa protocol consensus terdistribusi dalam satu akhir pekan. Untuk Go dan Rust, tambahkan shuttle atau loom ke test suite Anda dan jalankan di CI. Pertama kali ia menangkap race sebelum code review, Anda akan bertanya-tanya mengapa Anda pernah mempercayai scheduler untuk melakukan pengujian untuk Anda.