Model based system configuration and tasteful hardware

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

• Reto Achermann (ETH Zurich)
• Thursday 06 July 2017, 10:00-11:00
• FW26, Computer Laboratory, William Gates Building.

If you have a question about this talk, please contact Liang Wang.

The hardware/software boundary in modern heterogeneous multicore computers is increasingly complex, and diverse across different platforms. A single memory access by a core or DMA engine traverses multiple hardware translation and caching steps, and the destination memory cell or register often appears at different physical addresses for different cores. Interrupts pass through a complex topology of interrupt controllers and remappers before delivery to one or more cores, each with specific constraints on their configurations. System software must not only correctly understand the specific hardware at hand, but also configure it appropriately at runtime. We propose a formal model of address spaces and resources in a system that allows us to express and verify invariants of the system’s runtime configuration, and illustrate (and motivate) it with several real platforms we have encountered in the process of OS implementation. We proof that at the example of a software loaded TLB that preserving invariants stated in the specification is not always possible. Lastly, we use the model specification to generate system configuration such as kernel page-tables.

This talk is part of the Computer Laboratory Systems Research Group Seminar series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• CL's SRG seminar
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Computer Laboratory Systems Research Group Seminar
• Department of Computer Science and Technology talks and seminars
• FW26, Computer Laboratory, William Gates Building
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• rp587

Note that ex-directory lists are not shown.