Hi Ben, I think you are accessing all 2MB of the page, it's just that TEST_VADDR is being cast to a seL4_Word *, and doing pointer arithmetic like TEST_VADDR + 1 increments the address by the size of the type being pointed to (see https://www.gnu.org/software/c-intro-and-ref/manual/html_node/Pointer-Arithmetic.html), which for an seL4_Word on x86_64 is 8 bytes, not one. 8 * 0x00040000 is indeed 2MB so I suspect that if you cast the pointer to a uint8_t * or a char * instead, you'll find that your example works as expected.
- Alwin ________________________________ From: Ben McCart <b...@mccart.us> Sent: Wednesday, July 10, 2024 8:40 AM To: devel@sel4.systems <devel@sel4.systems> Subject: [seL4] seL4_X86_Page_Map on seL4_X86_LargePageObject != 2MiB [Some people who received this message don't often get email from b...@mccart.us. Learn why this is important at https://aka.ms/LearnAboutSenderIdentification ] I have created my own project on the PC99 architecture (x64) and have been working through the tutorial source (copy & pasted into my project) to learn and then prototype with seL4. I have done the mapping tutorial (pc99) and utilized that code within my project and everything seems to work just fine, but if I change out the seL4_X86_4K to seL4_X86_LargePageObject I don't end up with 2MiB of mappable virtual space. All the seL4 system calls through the client API return seL4_NoError. The seL4_LargePageBits value is 21 (2^21 == 2MB, and intel documentation for IA-32e shows that 2 MiB should be the large page size. However, if I address memory outside of the first 256 KiB it halts. The following works: seL4_Word *x = (seL4_Word *) TEST_VADDR; printf("Read x: %lu\n", *x); And this works: seL4_Word *x = (seL4_Word *) TEST_VADDR + 0x0003FFF0; printf("Read x: %lu\n", *x); But this halts when trying to dereference x to print it: seL4_Word *x = (seL4_Word *) TEST_VADDR + 0x00040000; printf("Read x: %lu\n", *x); I am running seL4 12.1 using QEMU with the following command line: qemu-system-x86_64 -cpu Nehalem,-vme,+pdpe1gb,-fsgsbase,-invpcid,+syscall,+lm,enforce -nographic -serial mon:stdio -m size=512M -s -S -kernel ../sel4-project/build/images/kernel-x86_64-pc99 -initrd build/cxxkit Does anybody have any idea why I might be having this issue and what I may do about it? -Ben McCart _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
