13-15 November 2018
America/Vancouver timezone

Formal Methods for Kernel Hackers

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

Pavillion-Ballroom-AB

Sheraton Vancouver Wall Center

35
Refereed talk LPC Main Track

Speaker

Catalin Marinas

Description

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
Breakfast sponsor
Your browser is out of date!

Update your browser to view this website correctly. Update my browser now

×