Anda membangun sistem n-version. Tiga implementasi independen dari fungsi kritis yang sama, sebuah voter yang memilih hasil mayoritas, dan perasaan hangat bahwa Anda telah mengalahkan single point of failure.
Anda belum membuktikan fungsi-fungsi tersebut ekuivalen. Anda baru membuktikan mereka bisa dikompilasi.
Mengapa ekuivalensi adalah fondasi tersembunyi dari n-version programming
N-version programming adalah gagasan bahwa jika satu implementasi memiliki bug, yang lainnya mungkin tidak, sehingga voter bisa membuang outlier. Ini mengasumsikan outputnya bisa dibandingkan.
Jika fungsi A mengembalikan float dan fungsi B mengembalikan string, voter tidak punya dasar untuk berdiri. Tapi bahkan dengan tipe yang cocok, perbedaan semantik bisa mematikan. Satu mengurutkan naik, satu mengurutkan turun. Satu membulatkan setengah ke atas, satu membulatkan setengah ke genap. Voter melihat tiga jawaban berbeda dan tidak punya cara berprinsip untuk memilih.
Literatur tentang n-version programming penuh dengan studi yang menunjukkan bahwa program yang ditulis secara independen sering gagal dengan cara yang berkorelasi. Programmer membuat kesalahan yang sama. Mereka salah membaca spesifikasi yang sama yang ambigu. Jika spesifikasi Anda adalah “sort this list,” dan satu programmer mengimplementasikan quicksort sementara yang lain mengimplementasikan mergesort, Anda mungkin mengasumsikan mereka ekuivalen. Memang begitu, sampai Anda bertanya tentang stability. Atau sampai inputnya mengandung NaN.
Kebanyakan tim melewatkan equivalence checking karena rasanya seperti pekerjaan tambahan. Padahal bukan. Itulah pekerjaan yang membuat sisanya dari sistem menjadi bermakna.
Mengapa test suite Anda memberikan kepercayaan diri palsu
Anda menulis unit test. Kedua fungsi lolos. Anda menyatakan kemenangan.
Itu adalah category error. Tes bisa membuktikan keberadaan bug, tapi tidak pernah ketiadaannya. Dengan ruang input yang tak terbatas, atau bahkan yang terbatas besar saja, test coverage Anda adalah rounding error. Dua fungsi bisa sepakat di setiap kasus yang Anda pikirkan dan berbeda di kasus yang penting pada jam 3 pagi di production.
Saya mempelajari ini dengan cara yang sulit dalam sebuah proyek dengan dua JSON parser. Satu menggunakan json.loads bawaan Python, yang lain menggunakan parser hand-rolled untuk performa. Test suite kami punya lima puluh kasus. Keduanya lolos. Di production, seorang pelanggan mengirim objek JSON dengan duplicate key. Parser Python menyimpan nilai terakhir. Parser hand-rolled kami menyimpan nilai pertama. Voter melihat dua objek berbeda dan panik.
Property-based testing mendekatkan kita. Alih-alih memilih input secara manual, Anda mendeskripsikan properties yang harus dipenuhi kedua fungsi dan membiarkan generator mencari counterexample. Berikut contoh nyata menggunakan library Hypothesis Python:
from hypothesis import given, strategies as st
import math
def round_half_up(n):
return math.floor(n + 0.5)
@given(st.floats(allow_nan=False, allow_infinity=False))
def test_rounding_equivalence(n):
assert round_half_up(n) == round(n)
if __name__ == "__main__":
test_rounding_equivalence()Jalankan ini dan Hypothesis akan dengan cepat menemukan counterexample. round_half_up(2.5) mengembalikan 3. round(2.5) bawaan Python mengembalikan 2 karena menggunakan banker’s rounding, yang membulatkan ke angka genap terdekat. Kedua fungsi “benar” menurut suatu standar. Mereka tidak ekuivalen.
Property-based testing tidak akan membuktikan ekuivalensi. Ia akan menemukan edge case yang unit test Anda lewatkan. Itu berharga, tapi tetap saja falsifikasi, bukan verifikasi.
Bagaimana SMT solver bisa benar-benar membuktikan ekuivalensi
Jika Anda ingin bukti, Anda harus meninggalkan comfort zone testing dan memasuki dunia SMT solver. Idénya sederhana. Encode kedua fungsi sebagai formula logika dan tanyakan pada solver apakah ada input di mana mereka berbeda.
Untuk domain yang terbatas, ini bersifat mekanis. Berikut contoh menggunakan Z3 untuk membuktikan dua implementasi max integer ekuivalen:
from z3 import Int, Solver, If, Abs
x = Int('x')
y = Int('y')
# Standard max implementation
max_standard = If(x > y, x, y)
# Algebraic max: (x + y + abs(x - y)) / 2
max_algebraic = (x + y + Abs(x - y)) / 2
solver = Solver()
solver.add(max_standard != max_algebraic)
result = solver.check()
print(result) # unsatZ3 mengembalikan unsat, yang berarti tidak ada counterexample. Fungsi-fungsi tersebut ekuivalen untuk semua integer dalam model Z3. Itu adalah bukti nyata, terbatas pada teori yang Z3 gunakan untuk bernalar.
Anda bisa melakukan ini untuk fungsi yang lebih kompleks juga. Triknya adalah mengekspresikan fungsi Anda sebagai formula logika. Untuk loop, Anda unroll. Untuk array, Anda menggunakan array theory Z3. Untuk floating point, Anda menggunakan FP theory Z3 dan menerima bahwa solver mungkin time out pada ekspresi yang kompleks.
Kesenjangan antara “mekanis” dan “mudah” adalah di mana kebanyakan tim terjebak. Menerjemahkan fungsi Python ke bahasa Z3 membutuhkan pemahaman terhadap keduanya. Tapi setelah Anda punya terjemahannya, solver yang melakukan pekerjaan berat.
Tabel trade-off yang tidak ingin diterbitkan siapapun
Formal verification penuh, membuktikan ekuivalensi untuk semua input yang mungkin termasuk setiap edge case IEEE 754, adalah mungkin. Orang-orang melakukannya untuk cryptographic primitives dan sistem avionik. Biayanya berminggu-minggu atau berbulan-bulan waktu ahli dan membutuhkan alat seperti Coq atau Isabelle.
Property-based testing memakan waktu menit dan menangkap bug nyata, tapi tidak menawarkan jaminan.
Bounded verification dengan SMT solver berada di tengah. Ia memberi Anda jaminan untuk scope yang terdefinisi dengan baik. Scope tersebut mungkin mencakup 99,9% input production Anda. Apakah itu cukup baik tergantung pada apa biaya kegagalannya.
Tidak ada makan siang gratis. Pilih alat yang sesuai dengan toleransi risiko Anda dan keahlian tim Anda.
Sebuah voter yang tahu kapan harus menyerah
Kebanyakan sistem n-version mengimplementasikan naive majority voter: mengembalikan hasil yang paling umum, atau gagal jika tidak ada mayoritas. Voter yang lebih baik tahu ketidaktahuannya sendiri.
from collections import Counter
def naive_voter(results):
if not results:
raise ValueError("No results to vote on")
counts = Counter(results)
winner, count = counts.most_common(1)[0]
if count > len(results) / 2:
return winner
raise ValueError("No majority found")
def informed_voter(results, input_sample=None):
if not results:
raise ValueError("No results to vote on")
distinct = set(results)
if len(distinct) == 1:
return results[0]
# Log disagreement for later analysis
if input_sample is not None:
print(f"Disagreement on input {input_sample}: {distinct}")
counts = Counter(results)
winner, count = counts.most_common(1)[0]
if count > len(results) / 2:
return winner
raise ValueError("No majority found")Ketika voter melihat persistent disagreement pada kelas input tertentu, itu adalah sebuah sinyal. Entah asumsi ekuivalensi Anda salah, atau Anda telah menemukan bug dalam salah satu implementasi. Keduanya layak diketahui.
Voter tidak hanya ada di sana untuk memilih pemenang. Ia ada di sana untuk memberi tahu Anda kapan asumsi Anda tentang ekuivalensi salah.
Apa yang sebenarnya harus dilakukan selanjutnya
Mulailah dengan property-based testing. Ini murah, menemukan bug, dan memaksa Anda untuk mengartikulasikan apa artinya “ekuivalensi” untuk domain Anda. Apakah output yang bitwise identik? Output dalam epsilon tertentu? Output yang memenuhi postcondition yang sama?
Setelah Anda mendefinisikan ekuivalensi dengan tepat, beralihlah ke bounded verification jika domainnya terbatas dan stakes-nya tinggi. Gunakan Z3, CBMC, atau alat serupa untuk mendapatkan bukti mekanis untuk scope terbatas Anda.
Sisihkan formal verification penuh untuk bagian-bagian di mana bug benar-benar membunuh orang. Untuk segala hal lain, ketahuilah batas bukti Anda dan pantau disagreement di production. Sistem n-version terbaik adalah yang tahu apa yang tidak ia ketahui.