Donny Yang fbafb777b0 x64: Always set the high bits of certain pointers in the fastpath ...

seL4 is always in the top of memory, so the high bits of pointers are always 1.
The autogenerated unpacking code doesn't know that, however, so will try to
conditionally sign extend (in 64-bit mode), which wastes cycles in the fast
path. Instead, we can do the unpacking ourselves and explicitly set the high
bits.

2016-11-30 11:25:05 +11:00

..

fastpath.h

x64: Always set the high bits of certain pointers in the fastpath

2016-11-30 11:25:05 +11:00