~/talk

Modularizing CPU Semantics for Virtualization

on YouTube 25m
Talkat PriSC 2024 · on Saturday, 2024-01-20· [compilers-and-language-design]

speakers

name:Paolo G. Giarrusso
links:none on file
name:Abhishek Anand
links:none on file
name:Gregory Malecha
links:none on file
name:František Farka
links:none on file
name:Hoang-Hai Dang
links:none on file

resources

video:https://youtu.be/Vjd2cckWRkk
slides:none on file

summary

Proposes a concrete decomposition of ARM ASL into an unprivileged core and a small privileged handler so one common unprivileged semantics can be reused across bare-metal and virtualized runs. Builds a prototype interface around an address-translation handle (translate → read/write) and integrates with the microkernel Nova plus a C++ VMM; several instructions are refactored and many VMM C++ routines are mechanically verified, while the full ASL rewrite and end-to-end mechanized simulation remain work in progress.

AI-written summary · about

chapters (8)

  1. 0:00Introduction
  2. 1:51Virtualization stack goals
  3. 3:17Hardware-software decomposition
  4. 6:04Privileged vs unprivileged logic
  5. 7:27Instruction semantics examples
  6. 10:58Simulation proof intuition
  7. 14:27Summary
  8. 14:49Q&A

related talks

~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.