Add comments explaining why we prefer non-device untypeds

libsel4utils/src/vspace/vspace.c

diff --git a/libsel4utils/src/vspace/vspace.c b/libsel4utils/src/vspace/vspace.c
index cd004b0..ac27a0b 100644
--- a/libsel4utils/src/vspace/vspace.c
+++ b/libsel4utils/src/vspace/vspace.c
@@ -504,6 +504,14 @@
         return NULL;
     }
 
+    /* Since sel4utils_new_pages() is an implementation of vspace_new_pages(),
+     * it should ideally be preferring to allocate device untypeds and leaving
+     * the non-device untypeds for VKA to use when it's allocating kernel objects.
+     *
+     * Unfortunately it currently has to prefer to allocate non-device untypeds
+     * to maintain compatibility with code that uses it incorrectly, such as
+     * code that calls vspace_new_pages() to allocate an IPC buffer.
+     */
     error = new_pages_at_vaddr(vspace, ret_vaddr, num_pages, size_bits, rights,
                                (int)true, false);
     if (error != 0) {