Hi Adrian, Thank you very much for your explain. I might have some misunderstanding about the source code. First may I ask what the kernel window means? Does it means the virtual memory space kernel can access (through pptr_t)? I can see the dev_p_regs[] (kernel/src/plat/tk1/machine/hardware.c) has multiple parts: the first is the RAM part, VM_HOST_PA_START - VM_HOST_PA_START + VM_HOST_PA_SIZE (0xb0000000 — 0xf0000000), the rest are real device region from 0x01000000 - 0x7c000000 approximately. I guess my question is why put the second half as a “device” instead of putting it together in avail_p_regs[]? Is it somehow due to the support of virtualization? Here is the booting procedure according to my understanding, could you take a look and see if I got it right? 1. the code start at the ELF-loader main() (tools/elfloader/src/arch-arm/boot.c) which is loaded in physical memory 0x82000000 for TK1 (tools/elfloader/gen_boot_image.sh) 2. the boot code unpack the ELF and find the kernel image and the user-land image, the kernel is loaded at 0x80000000 the user land image is loaded at 0x80037000 approximately 3. MMU is enabled and a “boot" page directory is created that maps physical 0x80000000 to (0xe0000000 - 0xf0000000) 4. enter the kernel code _start, which setup up vector table and kernel stack; then init_kernel(); then try_init_kernel() calls map_kernel_window() I’m not sure why map_kernel_windows() remap the virtual address kernelBase (start from 0xe0000000) to physical address physBase (0x80000000) again or did I miss anything? Also I’m not sure what those armHSGlobalPGD[], armHSGlobalPD[] for, I assume it is for context switch? (deleted diagram due to size limit) Thanks -Dan
Hi Daniel, On 21/06/17 08:26, Daniel Wang wrote:
Hi Adrian,
Thank you very much for your explain. I might have some misunderstanding about the source code. First may I ask what the kernel window means? Does it means the virtual memory space kernel can access (through pptr_t)?
Yes
I can see the *dev_p_regs*[] (kernel/src/plat/tk1/machine/hardware.c) has multiple parts: the first is the RAM part, *VM_HOST_PA_START - VM_HOST_PA_START + VM_HOST_PA_SIZE* (0xb0000000 — 0xf0000000), the rest are real device region from 0x01000000 - 0x7c000000 approximately. I guess my question is why put the second half as a “device” instead of putting it together in avail_p_regs[]? Is it somehow due to the support of virtualization?
Here is the booting procedure according to my understanding, could you take a look and see if I got it right?
1. the code start at the ELF-loader *main()* (tools/elfloader/src/arch-arm/boot.c) which is loaded in physical memory 0x82000000 for TK1 (tools/elfloader/gen_boot_image.sh) 2. the boot code unpack the ELF and find the kernel image and the user-land image, the kernel is loaded at 0x80000000 the user land image is loaded at 0x80037000 approximately 3. MMU is enabled and a “boot" page directory is created that maps physical 0x80000000 to (0xe0000000 - 0xf0000000) 4. enter the kernel code *_start*,* *which* *setup up vector table and kernel stack; then *init_kernel()*;* *then* try_init_kernel() *calls* map_kernel_window()*
I’m not sure why map_kernel_windows() remap the virtual address kernelBase (start from 0xe0000000) to physical address physBase (0x80000000) again or did I miss anything?
The kernel needs to remap its own device drivers (e.g. serial and timer), trap vectors, and assert its 512 MiB constraint. It also has to maintain this "global page directory" (read: kernel window), and copy it to newly created address spaces (besides user-level mapping). There are also some verification assumptions regarding this (verification only deals with the kernel, not the elfloader). A kernel's global page directory (e.g. armKSGlobalPD[] or armHSGlobalPGD[]) always has only "kernel's global mappings (pptr_t)", while normal thread's page directories have both kernel mappings and user mappings. The kernel works in a "global page directory" during bootstrap, idle thread, and if there's an error with user's thread page directory (e.g. has been deleted).
Also I’m not sure what those armHSGlobalPGD[], armHSGlobalPD[] for, I assume it is for context switch?
Those are the global page directories for the kernel when it's running in ARM hypervisor mode, similar to theircorresponding armKSGlobalPD[] (when the kernel is not in hypervisor mode). Hope this answer helps.
(deleted diagram due to size limit)
Thanks -Dan
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Cheers, Hesham
Thank you very much Hesham! A follow up question: I know that ARM Linux uses TTBR0 only to for different process’s virtual memory. The TTBR0 is stored in process TCB and when context switch is needed the TTBR0 register is replaced with the scheduled process’s TTBR0. I’m wondering if that the same for seL4. The reason I ask is that if seL4 maintains an armKSGlobalPD[], is that means it uses armKSGlobalPD[] for user land process context switch? Thanks -Dan
On Jun 21, 2017, at 3:32 PM, Hesham.Almatary@data61.csiro.au wrote:
Hi Daniel,
On 21/06/17 08:26, Daniel Wang wrote:
Hi Adrian,
Thank you very much for your explain. I might have some misunderstanding about the source code. First may I ask what the kernel window means? Does it means the virtual memory space kernel can access (through pptr_t)?
Yes
I can see the *dev_p_regs*[] (kernel/src/plat/tk1/machine/hardware.c) has multiple parts: the first is the RAM part, *VM_HOST_PA_START - VM_HOST_PA_START + VM_HOST_PA_SIZE* (0xb0000000 — 0xf0000000), the rest are real device region from 0x01000000 - 0x7c000000 approximately. I guess my question is why put the second half as a “device” instead of putting it together in avail_p_regs[]? Is it somehow due to the support of virtualization?
Here is the booting procedure according to my understanding, could you take a look and see if I got it right?
1. the code start at the ELF-loader *main()* (tools/elfloader/src/arch-arm/boot.c) which is loaded in physical memory 0x82000000 for TK1 (tools/elfloader/gen_boot_image.sh) 2. the boot code unpack the ELF and find the kernel image and the user-land image, the kernel is loaded at 0x80000000 the user land image is loaded at 0x80037000 approximately 3. MMU is enabled and a “boot" page directory is created that maps physical 0x80000000 to (0xe0000000 - 0xf0000000) 4. enter the kernel code *_start*,* *which* *setup up vector table and kernel stack; then *init_kernel()*;* *then* try_init_kernel() *calls* map_kernel_window()*
I’m not sure why map_kernel_windows() remap the virtual address kernelBase (start from 0xe0000000) to physical address physBase (0x80000000) again or did I miss anything?
The kernel needs to remap its own device drivers (e.g. serial and timer), trap vectors, and assert its 512 MiB constraint. It also has to maintain this "global page directory" (read: kernel window), and copy it to newly created address spaces (besides user-level mapping). There are also some verification assumptions regarding this (verification only deals with the kernel, not the elfloader).
A kernel's global page directory (e.g. armKSGlobalPD[] or armHSGlobalPGD[]) always has only "kernel's global mappings (pptr_t)", while normal thread's page directories have both kernel mappings and user mappings.
The kernel works in a "global page directory" during bootstrap, idle thread, and if there's an error with user's thread page directory (e.g. has been deleted).
Also I’m not sure what those armHSGlobalPGD[], armHSGlobalPD[] for, I assume it is for context switch?
Those are the global page directories for the kernel when it's running in ARM hypervisor mode, similar to theircorresponding armKSGlobalPD[] (when the kernel is not in hypervisor mode).
Hope this answer helps.
(deleted diagram due to size limit)
Thanks -Dan
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Cheers, Hesham
Hi Daniel, On 22/06/17 06:44, Daniel Wang wrote:
Thank you very much Hesham! A follow up question:
I know that ARM Linux uses TTBR0 only to for different process’s virtual memory. The TTBR0 is stored in process TCB and when context switch is needed the TTBR0 register is replaced with the scheduled process’s TTBR0. I’m wondering if that the same for seL4. The reason I ask is that if seL4 maintains an armKSGlobalPD[], is that means it uses armKSGlobalPD[] for user land process context switch? No, armKSGlobalPD[] (global page directory) is never used for user-level processes. In the case of ARM, it doesn't have an ASID. As I described in the previous reply, it's only being used in specific situations. And yes, like linux, each process (or a thread with a unique address space) has its own TTBR0/ASID, and those are being context switched (see armv_contextSwitch()).
Regards, Hesham
Thanks -Dan
On Jun 21, 2017, at 3:32 PM, Hesham.Almatary@data61.csiro.au wrote:
Hi Daniel,
On 21/06/17 08:26, Daniel Wang wrote:
Hi Adrian,
Thank you very much for your explain. I might have some misunderstanding about the source code. First may I ask what the kernel window means? Does it means the virtual memory space kernel can access (through pptr_t)?
Yes
I can see the *dev_p_regs*[] (kernel/src/plat/tk1/machine/hardware.c) has multiple parts: the first is the RAM part, *VM_HOST_PA_START - VM_HOST_PA_START + VM_HOST_PA_SIZE* (0xb0000000 — 0xf0000000), the rest are real device region from 0x01000000 - 0x7c000000 approximately. I guess my question is why put the second half as a “device” instead of putting it together in avail_p_regs[]? Is it somehow due to the support of virtualization?
Here is the booting procedure according to my understanding, could you take a look and see if I got it right?
1. the code start at the ELF-loader *main()* (tools/elfloader/src/arch-arm/boot.c) which is loaded in physical memory 0x82000000 for TK1 (tools/elfloader/gen_boot_image.sh) 2. the boot code unpack the ELF and find the kernel image and the user-land image, the kernel is loaded at 0x80000000 the user land image is loaded at 0x80037000 approximately 3. MMU is enabled and a “boot" page directory is created that maps physical 0x80000000 to (0xe0000000 - 0xf0000000) 4. enter the kernel code *_start*,* *which* *setup up vector table and kernel stack; then *init_kernel()*;* *then* try_init_kernel() *calls* map_kernel_window()*
I’m not sure why map_kernel_windows() remap the virtual address kernelBase (start from 0xe0000000) to physical address physBase (0x80000000) again or did I miss anything?
The kernel needs to remap its own device drivers (e.g. serial and timer), trap vectors, and assert its 512 MiB constraint. It also has to maintain this "global page directory" (read: kernel window), and copy it to newly created address spaces (besides user-level mapping). There are also some verification assumptions regarding this (verification only deals with the kernel, not the elfloader).
A kernel's global page directory (e.g. armKSGlobalPD[] or armHSGlobalPGD[]) always has only "kernel's global mappings (pptr_t)", while normal thread's page directories have both kernel mappings and user mappings.
The kernel works in a "global page directory" during bootstrap, idle thread, and if there's an error with user's thread page directory (e.g. has been deleted).
Also I’m not sure what those armHSGlobalPGD[], armHSGlobalPD[] for, I assume it is for context switch?
Those are the global page directories for the kernel when it's running in ARM hypervisor mode, similar to theircorresponding armKSGlobalPD[] (when the kernel is not in hypervisor mode).
Hope this answer helps.
(deleted diagram due to size limit)
Thanks -Dan
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel Cheers, Hesham
participants (2)
-
Daniel Wang -
Hesham.Almatary＠data61.csiro.au