Nov 13 – 15, 2018
America/Vancouver timezone

Formal Methods for Kernel Hackers

Nov 14, 2018, 2:45 PM
Pavillion/Ballroom-AB (Sheraton Vancouver Wall Center)


Sheraton Vancouver Wall Center

Refereed talk LPC Main Track


Catalin Marinas


Formal methods have a reputation of being difficult, accessible mostly to academics and of little use to the typical kernel hacker. This talk aims to show how, without "formal" training, one can use such tools for the benefit of the Linux kernel. It will introduce a few formal models that helped find actual bugs in the Linux kernel and start a discussion around future uses from modelling existing kernel implementation (e.g. cpu hotplug, page cache states, mm_user/mm_count) to formally specifying new design choices. The introductory examples are written in PlusCal (an algorithm language based on TLA+) but no prior knowledge is required.

I agree to abide by the anti-harassment policy Yes

Primary author

Catalin Marinas

Presentation materials

Platinum sponsors

Gold sponsors

Silver sponsors

Catchbox sponsor
T-Shirt sponsor