University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > Modular verification of preemptive OS kernels

  Browse A-Z

Log in

Cambridge users (raven)details Other usersdetails No account?details

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

Modular verification of preemptive OS kernels

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact William Denman.

Most major OS kernels today run on multiprocessor systems and are preemptive: it is possible for a process running in the kernel mode to get descheduled. Existing modular techniques for verifying concurrent code are not directly applicable in this setting: they rely on scheduling being implemented correctly, and in a preemptive kernel, the correctness of the scheduler is interdependent with the correctness of the code it schedules. This interdependency is even stronger in mainstream kernels, such as Linux, FreeBSD or XNU , where the scheduler and processes interact in complex ways.

In this talk I will present the first logic that is able to decompose the verification of preemptive multiprocessor kernel code into verifying the scheduler and the rest of the kernel separately, even in the presence of complex interdependencies between the two components present in mainstream kernels.

This is joint work with Hongseok Yang (University of Oxford, UK).

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Feminist Classics Revisited Horizon Forum: The Cell-Materials Interface New Thinking In Economics

Other talks

Sustainability of livestock production: water, welfare and woodland Grammar Variational Autoencoder Bioengineering conference: Innovation through convergence Disabled Academics in the 21st Century: 15th Annual Disability Lecture Anglo-Ottoman encounter in the Age of the Beloveds CANCELLED: The Loxbridge Triangle: Integrating the East-West Arch into the London Mega-region 'Politics in Uncertain Times: What will the world look like in 2050 and how do you know? An approach to the four colour theorem via Donaldson- Floer theory Knot Floer homology and algebraic methods Towards bulk extension of near-horizon geometries Existence of Lefschetz fibrations on Stein/Weinstein domains Measuring interacting electrons in low dimensional systems: spin-charge separation and 'replicas & tbd
 

© 2006-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity