QOT

MySQL DBA’s intelligent assistant

Formal verification of PBXT locking code, my experience with verification tools

In the last few months we’ve got couple of bugs with the PBXT read/write locking code. One of the problems was directly in the lock/grant algorithm. It was strange to find such kind of error after quite long time of various testing and real-life usage. From the point of view of QA it was clear […]

Read the rest of Formal verification of PBXT locking code, my experience with verification tools