Hi, I have two questions regarding dynamic-2 and dynamic-3 tutorials.
1. In dynamic-2 TASK 4, Why is the ipc_buffer_vaddr put in seL4_ARCH_PageTable_Map()? ipc_buffer_vaddr is the virtual address of the new physical frame allocated for the IPC buffer. I think seL4_ARCH_PageTable_Map's 3rd parameter is the virtual address of the page table frame.
2. In dynamic-3, it uses sel4utils_configure_process_custom() to create a new thread. I looked into the function and found that it created a vspace for the new thread. However, the tutorial's learning outcomes section says "this time the two threads will only share the same vspace", so I am confused. Does this tutorial create a new vspace for the new thread?
Mincheol
Hi,
As for the 1st question, all memory mapping functions accept virtual address of the memory region to be mapped, as the 3rd parameter. Tutorial "Mapping" allows to play with the API. (https://docs.sel4.systems/Tutorials/mapping.html)
Nataliya
Hi,
As for the 2nd question, looks like a new Vspace is created for a new thread, thank you for the finding!
Nataliya
-
mincheol＠vt.edu -
Nataliya Korovkina