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-Arithm...), 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
Sent: Wednesday, July 10, 2024 8:40 AM
To: 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 ben@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
