Testlar xatoning yoʻqligini isbotlamaydi. Nima isbotlaydi

Bu farq qayerda pulga tushadi

Toʻrttasi ham kod hajmi haqida emas, birikmalar soni haqida. Aynan shu — toʻliq saralash amalda qoʻllanadigan soha: protokollar, holat mashinalari, blokirovkalar, xizmatlar oʻrtasidagi kelishuv. Oddiy CRUD bu sohaga kirmaydi va u yerga model tekshiruvini sudrash keraksiz.

Model tekshiruvi nima

Siz tizimni holat mashinasi sifatida tasvirlaysiz: boshlangʻich holatlar, amallar (har birida ishga tushish sharti va natijasi) va doim rost boʻlishi kerak boʻlgan daʼvolar. Keyin vosita barcha erishiladigan holatlarni aylanib chiqadi va yo daʼvo yolgʻon boʻlgan holatga yoʻl topadi, yo bunday yoʻl yoʻqligini isbotlaydi.

const spec = {
  name: 'counter',
  processes: 2,
  init: [{ n: 0 }],
  actions: [
    {
      name: 'p0: oshirish',
      process: 0,
      reads: ['n'],
      writes: ['n'],
      step: (s) => (s.n < 3 ? [{ n: s.n + 1 }] : []),
    },
  ],
  invariants: [{ name: 'n haddan oshmaydi', reads: ['n'], holds: (s) => s.n <= 3 }],
  terminal: (s) => s.n === 3,
};

Shaklning bitta tafsiloti muhim: shart va natija bitta funksiyada yashaydi. Amalning oʻzi keyingi holatlarni qaytaradi, boʻsh roʻyxat esa «hozir imkonsiz» degani. Shunda ular bir-biridan ajralib keta olmaydi — qoʻlda yozilgan modellardagi klassik xato manbai.

Ikkinchisi: reads, writes va simmetrik jarayonlar toʻplami taxmin qilinmaydi, eʼlon qilinadi. TLA+ ham xuddi shuni soʻraydi. Toʻlovi halol: notoʻgʻri eʼlon spetsifikatsiyadagi xatoga aylanadi, kerakli holatlarni jimgina uloqtirgan vositaning yashirin nosozligiga emas.

Kontrmisol verdiktdan muhimroq

«Buzilish mumkin» degan javob unga olib boradigan yoʻlsiz foydasiz. Kenglik boʻyicha qidiruv yoʻlni tuzilishiga koʻra eng qisqa qiladi, shuning uchun kontrmisol dampga emas, hodisa bayonnomasiga oʻxshab oʻqiladi.

✗ peterson (check then set) — invariant "at most one process in the critical section"

  trace
    (initial)                    pc=00 flag=00
    p0: check the other flag     pc=10 flag=00
    p1: check the other flag     pc=11 flag=00
    p0: raise flag and enter     pc=31 flag=10
    p1: raise flag and enter     pc=33 flag=11

Ikkalasi ham qaradi, ikkalasi ham tushirilgan bayroqni koʻrdi, ikkalasi ham kirdi. Toʻrt qadam — va bayroq nega tekshiruvdan oldin koʻtarilishi kerakligi ravshan. Trassa boʻlsa bunday narsa bir daqiqada, «baʼzan ikkalasi ichkarida qoladi» boʻlsa haftalab tahlil qilinadi.

Nega saralashni toʻgʻridan-toʻgʻri qilib boʻlmaydi

Holatlar soni koʻpaytma kabi oʻsadi: besh fazadagi oltita jarayon — 15 625 birikma, bu esa oʻyinchoq misol. Shuning uchun vositaning asosiy qismi qidiruv emas, qidirmaslikka imkon beradigan narsalar.

Oxirgi qator birinchi ikkitasidan muhimroq. Jarayonlar doimo bir-birining oʻzgaruvchilarini oʻqib-yozadigan joyda qisqartiradigan narsa yoʻq — vosita esa halol hech narsa bermasligi shart. Bu qator testda daʼvo sifatida turibdi: u yerda yutuq eʼlon qilgan vosita yolgʻon aytgan boʻlardi.

Qidirmaslikning ikki usuli

Simmetriya. Jarayonlar almashtiriladigan boʻlsa, faqat ularning oʻrin almashuvi bilan farq qiladigan holatlar — bitta holat. Besh fazadagi oltita ishchi 15 625 taqsimot beradi, ammo atigi 210 multitoʻplam: qaysi biri qayerda emas, nechtasi qayerda ekani muhim.

Oʻrin almashadigan amallar. Ikki amal umumiy hech narsaga tegmasa, ular orasidagi tartib kuzatilmaydi: bir tartibni oʻrganib, ikkinchisidan hech narsa bilmaysiz. Rasman bu ample toʻplamlar va ularning toʻrtta sharti bor, har biri oʻz oʻrnini haqqoniy egallaydi — bittasini olib tashlang, tekshiruv buzilishlarni ishonch bilan oʻtkazib yubora boshlaydi.

Qisqartiruvchining oʻzini qanday tekshirish kerak

Mana bu butun ishning eng yoqimsiz joyi. Kerakli holatlarni uloqtirgan qisqartirish ishlaydigani bilan aynan bir xil natija beradi: «buzilish topilmadi». Qisqartirilgan qidiruv ichidan qaysi birini ushlab turganingizni ajratib boʻlmaydi.

Yagona ishlaydigan javob — qisqartirishga soʻzida ishonmaslik. Toʻliq saralash yonida qoladi: sekin, toʻliq va xato qila olmaydigan. Har bir spetsifikatsiya ikkala qidiruvdan oʻtadi va qisqartirilgan verdikt toʻligʻiga mos kelishi shart. Qisqartirishga muallifi ishonchli boʻlgani uchun emas, xato qila olmaydigan narsa bilan rozi boʻlgani uchun ishoniladi.

Bu kafolatning chegarasi bor va uni ochiq aytish kerak: solishtirish toʻliq saralash hali ishga tushadigan joyda — kichik modellarda mumkin. Aynan qisqartirish kerak boʻlmagan joyda. Bu yondashuvning tugʻma xossasi va u tekshiruvni bekor qilmaydi, ammo uning shiftini belgilaydi.

Jonlilik: tizim qulamaydi, shunchaki yetib bormaydi

Xavfsizlik «yomon holatga erishsa boʻladimi» degan savol va kenglik boʻyicha qidiruv unga javob beradi. Jonlilik «yaxshi narsa qachondir yuz beradimi» degan savol va uni yaxshi narsa hech qachon yuz bermaydigan cheksiz yurish buzadi. Chekli fazoda bunday yurish — arqon: siklgacha yoʻl va keyin abadiy sikl.

Muammo shundaki, bunday sikllarning koʻpi bemaʼni: ular ishga tushishi mumkin boʻlgan jarayon hech qachon ishga tushirilmasligini talab qiladi. Ularni zaif adolat kesib tashlaydi: uzluksiz tayyor jarayon qachondir qadam tashlashi shart. Bu shartsiz har qanday konkurent dastur jonlilikni «yiqitadi» va tekshiruv foydasiz boʻladi.

✗ spinlock — can loop forever without process 0 reaching its critical section
  The cycle is fair: process 1 keeps moving; process 0 is blocked

  then forever
    p1: acquire   pc=03 lock=1
    p1: release   pc=00 lock=-1

Spinlok xavfsiz — ikkalasi bir vaqtda ichkarida boʻlmaydi — va ayni paytda ochlikka olib keladi. Peterson algoritmi xuddi shu tekshiruvdan oʻtadi va turn oʻzgaruvchisi aynan shuning uchun mavjud. «Xavfsiz» bilan «xavfsiz va yetib boradi» orasidagi farqni atay bilish kerak: navbatlarda, qulflarda va taqsimlangan blokirovkalarda aynan u monitoringda xato sifatida koʻrinmaydigan osilib qolishlar manbai.

Bu usul nimani uddalay olmaydi

• Kod emas, model tekshiriladi. Bu ham asosiy chegara, ham asosiy xavf: isbotlangan model va undan uzoqlashgan implementatsiya — oddiy holat. Model gʻoya xatolarini, testlar bajarilish xatolarini tutadi; biri ikkinchisini almashtirmaydi.
• Qisqartirishlar siz eʼlon qilgan narsaga nisbatan toʻgʻri. Eʼlon qilinmagan oʻzgaruvchini yozadigan amal uloqtirilgan holatlarga olib kelishi mumkin. Bu tahlil emas, shartnoma.
• Faqat invariantlar va jonlilikning bitta shakli. «Doim rost» va zaif adolat ostida «qachondir yuz beradi». Ichma-ich vaqt operatorlari ham, kuchli adolat ham, toʻliq LTL ham yoʻq.
• Hammasi xotirada. Milliardlar emas, minglab holatlar: diskdagi saqlash ham, ramziy tasvir ham yoʻq.
• Jiddiy ish uchun TLC va SPIN bor. Ular ortida oʻn yilliklar, diskdagi holat ombori, taqsimlangan tekshiruv va shu ish uchun oʻylab topilgan tillar.

Tijorat loyihasida bu qachon oʻzini oqlaydi

Pul jihatidan bu maʼlumotdagi xato ishlamay qolishdan qimmatga tushadigan joyda oʻzini oqlaydi: moliyaviy tizimlar, qoldiqlar hisobi, tashqi provayderlar bilan integratsiyalar. Yondosh tahlillar — toʻlovlar idempotentligi va master qulaganda maʼlumotlar bilan nima boʻlishi.