/* Page allocator. Hands out memory in page-size (or
page-multiple) chunks. See malloc.h for an allocator that
/* Page allocator. Hands out memory in page-size (or
page-multiple) chunks. See malloc.h for an allocator that
If PAL_USER is set, the page is obtained from the user pool,
otherwise from the kernel pool. If PAL_ZERO is set in FLAGS,
then the page is filled with zeros. If no pages are
If PAL_USER is set, the page is obtained from the user pool,
otherwise from the kernel pool. If PAL_ZERO is set in FLAGS,
then the page is filled with zeros. If no pages are