Linux Plumbers, Vancouver 2018
This is a talk I gave at Linux Plumbers 2018 on how to formally model the kernel queued spinlocks using PlusCal/TLA+. The effort led to finding and fixing liveness property violations in the actual C implementation.
This is a talk I gave at Linux Plumbers 2018 on how to formally model the kernel queued spinlocks using PlusCal/TLA+. The effort led to finding and fixing liveness property violations in the actual C implementation.