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, [email protected] 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 >>> [email protected] >>> https://sel4.systems/lists/listinfo/devel >> Cheers, >> Hesham _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
