Doniyor
Botirov.

Asinxron xatolar tasodifiy emas. Tasodifiy narsa — operatsion tizim tanlagan bajarilish tartibi, shuning uchun xato uch yuz yurishda bir marta chiqadi va takrorlanmaydi. unflake bu tanlovni OTdan tortib oladi: vaqt, taymerlar va tayyor kolbeklar tartibi sid asosidagi qiymatlarga aylanadi. Bir sid — bayt-baytigacha bir xil yurish. Topilgan xato minimal jadvalgacha siqiladi va istalgan mashinada takrorlanadi.

Yaxshi kunda ishlaydigan lider saylovini kim boʻlsa ham yozadi. Qiyin kun — tarmoq boʻlinib, ikki tugun oʻzini bosh deb hisoblagan, toʻrt soniya avvalgi xabar ikki marta yetib kelgan va oʻlikdan qaytgan tugun eskirgan log olib kelgan kun. bulwark — TypeScriptdagi Raft, uni determinlashgan simulyatsiya ushlab turadi: boʻlinishlar, qulashlar va xabarlar tartibining oʻzgarishi sid asosida beriladi, maqoladagi beshta xavfsizlik xossasi har bir holat oʻtishidan keyin tekshiriladi, mijoz operatsiyalarining har bir tarixi esa linearizatsiyaga tekshiriladi. Repozitoriydagi asosiy narsa — xatolar muzeyi: yettita eksponatning har biri Raftning aynan bitta qoidasini oʻchiradi va xarnessdan uni sid bilan hamda xossa nomi bilan tutishni talab qiladi. Bitta eksponat — xarness implementatsiyaning oʻzida topgan xato.

Har bir maʼlumotlar bazasi izolyatsiya darajalarini eʼlon qiladi. Ammo oʻz darajasi aslida nimaga yoʻl qoʻyishini deyarli hech kim koʻrsata olmaydi. «Bizda snapshot isolation» degani — bir vaqtning oʻzida ikkita daʼvo: undan zaifroq hech narsa yuz bermasligi va bu haqiqatan SI ekani, oʻsha nom ostidagi qatʼiyroq narsa emasligi. Ikkalasini ham kodni oʻqib tekshirib boʻlmaydi — bular matnning emas, bajarilishlarning xossalari. adya bajarilishlarni tutadi va soʻroq qiladi: bir tomondan — toʻrtta izolyatsiya darajasiga ega MVCC dvigateli, unda serializable Keyhill algoritmi bilan qilingan, aynan PostgreSQLdagi algoritm; ikkinchi tomondan — kuzatilgan tarixdan bogʻliqliklar grafini quradigan, undan sikllarni qidiradigan va topilganini Adya dissertatsiyasidagi nomlar bilan ataydigan tekshiruv: G0, G1a, G1b, G1c, G-single, G2-item. Har bir daraja ikki tomondan tekshiriladi: u oldini olishi shart boʻlgan narsani ishlab chiqarmaydi va keyingi daraja oldini oladigan narsani ishlab chiqaradi. Hech bir tomonga alohida ishonilmaydi — ular bir-birini fosh qiladi.

Bu repozitoriy unflake ning cheklovlar boʻlimidagi bitta jumla tufayli mavjud: yuzlab sid — juda yaxshi fazzing, ammo teorema emas. Jadvallar tanlanmasi xatolarni topadi va ularning yoʻqligini hech qachon isbotlamaydi; isbotlash — barcha erishiladigan holatlarni aylanib chiqish, bu esa eksponenta. Shuning uchun model checker dagi asosiy narsa qidiruv emas, qidirmaslikka imkon beradigan narsalar: simmetriya (oltita almashtiriladigan jarayon 15 625 taqsimot beradi, ammo atigi 210 multitoʻplam) va qisman tartiblangan qisqartirish. Asosiy muammo shundaki, buzilgan qisqartirish ishlaydiganidek javob beradi — «buzilish topilmadi». Shuning uchun toʻliq saralash yonida qoldirilgan — sekin va xato qila olmaydigan, — har bir spetsifikatsiya esa ikkalasida mos verdikt berishi shart. Jonlilik zaif adolat sharti ostida tekshiriladi: spinlok kontrmisol bilan tutiladi, Peterson algoritmi oʻtadi.