You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
From memory there's two kinds of allocations that can fail:
We have run out of memory (or the allocator has failed to find enough space)
We have tried to allocate a memory region at a physical address is already reserved or is in an untyped that does not have enough space or something like that.
Right now, each case gives a different kind of error. Both being kind of useless unless you are familiar with seL4 itself which you shouldn't have to be to use the Microkit.
For example, on QEMU (which has 2GB of RAM) if we try make a memory region of 4GB:
thread 'main' panicked at src/lib.rs:362:9:
Can't alloc of size 2097152, count: 2048 - no space
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
We should really be giving more specifics such as Cannot allocate memory region 'test' of size 4GB or something along those lines. Even better would be if we displayed how much total space there is, and how much is left by the time we get to the allocation that will fail.
The second case can be produced with the exact same SDF as the first but with a phys_addr as well, e.g:
ut [0x0..0x8000000], space left: 0x8000000
ut [0x8001000..0x8002000], space left: 0x1000
ut [0x8002000..0x8004000], space left: 0x2000
ut [0x8004000..0x8008000], space left: 0x4000
ut [0x8008000..0x8010000], space left: 0x8000
ut [0x8011000..0x8012000], space left: 0x1000
ut [0x8012000..0x8014000], space left: 0x2000
ut [0x8014000..0x8018000], space left: 0x4000
ut [0x8018000..0x8020000], space left: 0x8000
ut [0x8020000..0x8030000], space left: 0x10000
ut [0x8031000..0x8032000], space left: 0x1000
ut [0x8032000..0x8034000], space left: 0x2000
ut [0x8034000..0x8038000], space left: 0x4000
ut [0x8038000..0x8040000], space left: 0x8000
ut [0x8040000..0x8080000], space left: 0x40000
ut [0x8080000..0x8100000], space left: 0x80000
ut [0x8100000..0x8200000], space left: 0x100000
ut [0x8200000..0x8400000], space left: 0x200000
ut [0x8400000..0x8800000], space left: 0x400000
ut [0x8800000..0x9000000], space left: 0x800000
ut [0x9000000..0xa000000], space left: 0x1000000
ut [0xa000000..0xc000000], space left: 0x2000000
ut [0xc000000..0x10000000], space left: 0x4000000
ut [0x10000000..0x20000000], space left: 0x10000000
ut [0x20000000..0x40000000], space left: 0x20000000
ut [0x40000000..0x60000000], space left: 0x0
ut [0x60246000..0x60248000], space left: 0x1000
ut [0x60248000..0x60249000], space left: 0x1000
ut [0xc0000000..0x100000000], space left: 0x40000000
ut [0x100000000..0x200000000], space left: 0x100000000
ut [0x200000000..0x400000000], space left: 0x200000000
ut [0x400000000..0x800000000], space left: 0x400000000
ut [0x800000000..0x1000000000], space left: 0x800000000
ut [0x1000000000..0x2000000000], space left: 0x1000000000
ut [0x2000000000..0x4000000000], space left: 0x2000000000
ut [0x4000000000..0x8000000000], space left: 0x4000000000
ut [0x8000000000..0x10000000000], space left: 0x8000000000
thread 'main' panicked at src/main.rs:278:13:
Error: allocation for physical address 60000000 is too large (200000) for untyped
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
The main problem is that there are some 'hidden'/internal allocations for Microkit to build a system and then there are user-specific allocations and so making it clear whether this is some kind of internal error or an error caused by the user is important.
The text was updated successfully, but these errors were encountered:
In dstorer's case I think the issue was that the starting address was at the very end of an UT region. So the specific address didn't fall within any defined UT, which should have its own error message.
From memory there's two kinds of allocations that can fail:
Right now, each case gives a different kind of error. Both being kind of useless unless you are familiar with seL4 itself which you shouldn't have to be to use the Microkit.
For example, on QEMU (which has 2GB of RAM) if we try make a memory region of 4GB:
we get:
We should really be giving more specifics such as
Cannot allocate memory region 'test' of size 4GB
or something along those lines. Even better would be if we displayed how much total space there is, and how much is left by the time we get to the allocation that will fail.The second case can be produced with the exact same SDF as the first but with a
phys_addr
as well, e.g:this leads to this error message:
The main problem is that there are some 'hidden'/internal allocations for Microkit to build a system and then there are user-specific allocations and so making it clear whether this is some kind of internal error or an error caused by the user is important.
The text was updated successfully, but these errors were encountered: