As stated in the question, I'm not certain about how the integer part of the elements in the untyped_mmios array in devices.camkes are derived?
E.g. in the TX2 devices.camkes file:
vm0.untyped_mmios = [ "0x3886000:12", // GICV Iface. /* The purpose of these untyped regions is to force the untyped * allocator to treat this memory region as reserved so that when we * try to ensure that the VMM is placed into this region in RAM, it * will definitely be available for placement. * * This address pertains to guest-vm@f1000000 in the overlay DTS */ "0xF1000000:24", "0xF2000000:25", "0xF4000000:26", "0xF8000000:24", ];
I recognise that the range of addresses here covers the VM_RAM_SIZE specified, and so the pattern that emerges is:
24 --> 0x01000000 25 --> 0x02000000 26 --> 0x04000000
And so the above would cover the range 0xf1000000 --> 0xf9000000, which is the range of memory specified for the VM.
Is this simply a case of the integer representing double the value with each increment. E.g:
Ben Turner Senior Engineer Roke Manor Research Ltd Tel: +44 (0)1794 833721 firstname.lastname@example.org:email@example.com
________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________
As stated in the question, I'm not certain about how the integer part of the elements in the untyped_mmios array in devices.camkes are derived? "0xF1000000:24", "0xF2000000:25", "0xF4000000:26", "0xF8000000:24",
You are right that the numbers represent the size of the untyped mmios being created, 0xF1000000:24 -> [0xF1000000, 0xF1000000 + 0x1000000). In the example you gave, the four elements are defining a single ram region, but because the objects being created are seL4 untypeds that the vmm uses to construct the RAM device, there is an seL4 constraint that untyped objects can't be larger than their alignment. So camkes wouldn't be able to create an untyped object defined as: "0xF1000000:27" as this object would only have an alignment of 2^24 and seL4 would reject the retype invocation.
Hope this answers your question.
"Turner," == Turner, Ben firstname.lastname@example.org writes:
Turner,> Hi all, As stated in the question, I'm not certain about how Turner,> the integer part of the elements in the untyped_mmios array Turner,> in devices.camkes are derived?
It's a power-of-two, representing the size of the object. 2^12 is 4096 or 0x1000, 2^24 is 0x01000000