Concurrency Modelleri ve Concurrent Kodu Doğrulamak: Shared Memory, Actor, CSP ve Model Checking
Concurrency modeli durumun sahibini ve haberleşme şeklini belirler: shared memory'de herkes kilitle sırayla dokunur, actor ve CSP'de durumun tek sahibi vardır ve haberleşme mesajladır. Bookstore stok rezervasyonunu lock, actor ve channel pipeline ile kuruyor, actor'ün içi hatasızken oku-sonra-yaz protokolünün 1.000 stoktan 4.000 kitap sattırdığını gösteriyor ve aynı check-then-act hatasını TLA+ ile model check edip TLC'nin karşı örneğini okuyoruz.
14 Kas 2026
·
13 dk
·
14
