BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Model based system configuration and tasteful hardware - Reto Ache
 rmann (ETH Zurich)
DTSTART:20170706T090000Z
DTEND:20170706T100000Z
UID:TALK73211@talks.cam.ac.uk
CONTACT:Liang Wang
DESCRIPTION:The hardware/software boundary in modern heterogeneous multico
 re\ncomputers is increasingly complex\, and diverse across different\nplat
 forms. A single memory access by a core or DMA engine traverses\nmultiple 
 hardware translation and caching steps\, and the destination\nmemory cell 
 or register often appears at different physical addresses\nfor different c
 ores. Interrupts pass through a complex topology of\ninterrupt controllers
  and remappers before delivery to one or more\ncores\, each with specific 
 constraints on their configurations. System\nsoftware must not only correc
 tly understand the specific hardware at\nhand\, but also configure it appr
 opriately at runtime. We propose a\nformal model of address spaces and res
 ources in a system that allows\nus to express and verify invariants of the
  system’s runtime\nconfiguration\, and illustrate (and motivate) it with
  several real\nplatforms we have encountered in the process of OS implemen
 tation.\nWe proof that at the example of a software loaded TLB that preser
 ving\ninvariants stated in the specification is not always possible. Lastl
 y\,\nwe use the model specification to generate system configuration such\
 nas kernel page-tables.
LOCATION:FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR