Something seems to be missing in regards to flushing specific ranges of
the TLB. For the moment, flushing the entire thing seems to make it
work alright.
Should give 39-bit DMA addressing on the relevant chipsets.
v2: allocate contig 16KiB for dummy pages, reported by mwk on irc