Jak TLA+ pomogło znaleźć 16-letni błąd w SQLite
Błąd w mechanizmie Write-Ahead Logging (WAL) w SQLite był obecny w kodzie przez szesnaście lat. Nikt go nie zauważył. Dopiero formalna weryfikacja przy pomocy narzędzia TLA+ ujawniła problem z przełączaniem ramek, który mógł prowadzić do utraty danych w specyficznych warunkach. To pokazuje, jak trudne jest projektowanie niezawodnych systemów transakcyjnych. TL;DR: Szesnastoletni błąd w implementacji algorytmu […]