Timothy Roscoe | Reasoning as a First-class Operating System Service (Jul 17, 2012)

Описание: Timothy Roscoe, Professor, Systems Group of hte Computer Science Department ETH Zurich, the Swiss Federal Institute of Technology argues in this talk for sophisticated automated reasoning capabilities as a first-class OS service. With such a service, one can delegate many OS policy decisions and calculations to a component which is highly flexible, expressive, and dynamic, provding considerable advantages of hard-coding such functionality in C or scripts. Modern operating systems face several engineering challenges: hardware is increasingly complex, increasingly diverse, and evolving rapidly. This, combined with parallel workloads having complex performance interactions with hardware make it hard to build a simple OS kernel which delivers good performance for a variety of platforms and workloads. We decided to tackle this head-on by building a reasoning engine as a first class service (the "System Knowledge Base") in the Barrelfish OS, borrowing ideas such fields as knowledge representation, constraint satisfaction, logic programming, and optimization. Doing so was not without problems, but we found it highly convenient in a number of widely different application areas - for example PCI programming, process coordination, spatial scheduling, and message routing. I'll discuss several of these, and how the structure of the OS as a whole changes when a facility like the SKB is availability.