I could use a clue as to the cause of this problem.

The program has its free slots start index set correctly.

It is trying to allocate a dma buffer. (4k with a known physical address).

The vspace has been properly set up and knows the phys addresses of its free memory.

This used to work fine in a different process, but I can’t find anything I’ve done

different/wrong in this one…


I’ve added some extra printfs, and some debug code (in kernel/src/object/untyped.c).

    /* Ensure that the destination slots are all empty. */

    slots.cnode = CTE_PTR(cap_cnode_cap_get_capCNodePtr(nodeCap));

    slots.offset = nodeOffset;

    slots.length = nodeWindow;

    for (i = nodeOffset; i < nodeOffset + nodeWindow; i++) {

        status = ensureEmptySlot(slots.cnode + i);

        if (status != EXCEPTION_NONE) {

            userError("Untyped Retype: Slot #%d from %p in destination window non-empty.", (int)i, (void *)slots.cnode);

            userError("Untyped Retype: At offset #%d length %d.", (int)nodeOffset, (int)nodeWindow);

            int j = 0;


                status = ensureEmptySlot(slots.cnode + (i + j));

                if (status == EXCEPTION_NONE) {

                    userError("Next Free Slot at #%d from %p.", (int)(i+j), (void *)slots.cnode);

                    status = EXCEPTION_SYSCALL_ERROR;




            return status;





And finally, here is the output from the console:


<<seL4(CPU 0) [decodeCNodeInvocation/94 T0xffffff8001a25400 "Lockmaproc" @4196e8]: CNode Copy/Mint/Move/Mutate: Destination not empty.>>

<<seL4(CPU 0) [decodeUntypedInvocation/166 T0xffffff8001a25400 "Lockmaproc" @420f2c]: Untyped Retype: Slot #196 from 0xffffff807f000000 in destination window non-empty.>>

<<seL4(CPU 0) [decodeUntypedInvocation/167 T0xffffff8001a25400 "Lockmaproc" @420f2c]: Untyped Retype: At offset #196 length 1.>>

<<seL4(CPU 0) [decodeUntypedInvocation/172 T0xffffff8001a25400 "Lockmaproc" @420f2c]: Next Free Slot at #197 from 0xffffff807f000000.>>

_refill_pool@split.c:187 Failed to retype untyped, error 8

vka_alloc_object_at_maybe_dev@object.h:59 Failed to allocate object of size 4096, error 1

dma_alloc@page_dma.c:92 Failed to allocate untyped of size 12


I need a hint… help?








This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.