Address Space Types

There are four different address spaces the microkernel has to keep track of (and hence, four different kinds of addresses):

  • host physical (hpa_t)
  • host virtual (hva_t)
  • guest physical (gpa_t)
  • guest virtual (gva_t)

Using an unsigned long for all of these could easily get us into trouble. Instead, we define a separate type for each one (in lcd-domains/include/lcd_domains/types.h). There are also some static inlines for easily translating from one to the other.

In non-trivial code, when you're working with possibly all four address spaces, having separate types forces you to think properly about what you're doing.

Linux uses some limited forms of address space types, like phys_addr_t. But they aren't consistently used, I think.

I've noticed KVM doing something similar in their source code for different address space types. They don't seem to be as consistent though. Could be wrong.