- Devel - lists.sel4.systems

hello world difficulty
by Royce Mitchell III 09 Apr '21

09 Apr '21

I feel like an idiot for having to ask for help so early, but I'm trying to get started with the hello world tutorial and ran into a problem very quickly. First off I want to say thank you for all the work that's been put into the tutorils. The amount of information in them is quite daunting, but considering the subject matter it's actually very accessible all things considered. I have a Debian 10 linux VM that I'm using for testing. I'm okay building a VM dedicated solely to seL4 development if that's necessary, but I'm assuming it's not. FYI I had some difficulty with the prerequisites instructions regarding Debian. This may be the source of the problem I'm having but I'm not sure how to resolve it. Your setup instructions said to refer to the docker requirements but when I went there I couldn't find anything on that page that indicated what exactly I was supposed to install. All that being said, here is a capture from my terminal which I'm hoping illustrates the problem I'm having specifically: rmitchell@ou812:~/sel4-tutorials-manifest$ ./init --tut hello-world Traceback (most recent call last): File "./init", line 16, in <module> import common File "/home/rmitchell/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 16, in <module> import sh ModuleNotFoundError: No module named 'sh' rmitchell@ou812:~/sel4-tutorials-manifest$ python Python 3.9.1 (default, Mar 19 2021, 01:08:36) [GCC 8.3.0] on linux Type "help", "copyright", "credits" or "license" for more information. >>> import sh >>> sh.__version__ '1.14.1' >>> exit() As you can see from my example above, I have Python 3.9.1 installed and it is the default python interpreter on my system. The "sh" module is installed and accessible from Python's interactive interpreter, yet when the common.py file tries to import it, it complains that it can't find the 'sh' module. FYI sh is installed both at the system and user levels. I'll try digging into your source and see if I can figure out what the issue is. I'll share my findings if I figure it out before you guys point out my mistakes. Thanks! Royce Mitchell, IT Consultant ITAS Solutions royce3(a)itas-solutions.com There are three hard problems in computer science: naming things, and off-by-one errors.

3 6

seL4 service discovery question
by Royce Mitchell III 08 Apr '21

08 Apr '21

Hi all, I've been passively following seL4 for several years. I've been reading the documentation, tutorials, watching YouTube videos. The concepts behind capabilities and other types of kernel objects are starting to sink in but there's one piece of understanding that's eluding me. If I just haven't stumbled across it yet in the documentation, then pointing me in the right direction would be greatly appreciated. Given: * An ethernet driver named "e1000" and 2 devices "eth0" and "eth1" controlled by that driver. * A "tcp" service that would implement that network protocol. * A higher level service named "network" that implemented some kind of networking abstraction for us. How would: 1) the "network" service advertise its services as available via IPC? 2) an application locate this "network" service to be able to IPC with it? I assume the mechanisms here would also apply to interactions between services as well. I picked the "network" service in this example only because it would be the boundary between application and OS services. I'm guessing that maybe this is purely an OS design decision and not the purvue of the kernel itself. Perhaps init could launch a "service manager" process that would be responsible for starting up services and drivers for example and this "service manager" could provide an IPC endpoint back to init (or whomever) to use for IPC discovery. Then, whenever a new process is started, it is provided with the IPC discovery endpoint information that it is to inherit. If my assumptions are correct or close, or even dead wrong, would someone be willing to share some pseudo-code on what this could/should look like in seL4? If a central service manager is needed to glue the core OS together, does it represent a single point of failure and how would the OS recover if it crashes and loses it's database of available services without having to rebuild and restart all drivers and services? (I'm not saying that's a bad thing, just trying to wrap my head around how this particular part of seL4 works) Thanks, Royce Mitchell, IT Consultant ITAS Solutions royce3(a)itas-solutions.com There are three hard problems in computer science: naming things, and off-by-one errors.

6 14

Small question about copiing threads
by Сергей Волкович 07 Apr '21

07 Apr '21

Hello. My name is Serhgey Volkovich. Currently i trying to write my own posix compilant os subset. But i cannot understand some momments such what happen with main process memory if i create new thread with same pointer as it have main, and second process will try to change something in own memory. Will it change memory of main process?

1 0

About the BuildSystem of seL4
by Jerry Zhou 29 Mar '21

29 Mar '21

Hi guys, I am a newbie of seL4 and I am trying to get some understanding of it. So, my first question is about the build system of seL4: 1. Why cmake has been taken to build it? I think there are at least two shortcomings about current build system based on CMakeLists.txt: - Some build options were implied in the CMakeLists.txt. It's not easy to get a complete and comprehensive understanding of all the options. And some options depends on other options. Such as, ./init-build.sh -DPLATFORM=odroidc2 -DAARCH64=1 A new guys couldn't get a support list of PLATFORM option, and know AARCH64 is only for ARMv8 SoC easily. - There are too much branches of platform or SoC Architectures. Such as: if(KernelArchARM) include_directories("include/arch/arm/armv/${KernelArmArmV}/") include_directories("include/arch/arm/armv/${KernelArmArmV}/${KernelWordSize}") endif() if(KernelArmMach STREQUAL "exynos") include_directories("include/plat/exynos_common/") endif() if(KernelArchRiscV) include_directories("include/arch/${KernelArch}/arch/${KernelWordSize}") include_directories("include/plat/${KernelPlatform}/plat/${KernelWordSize}") endif() Linux Build System places the special build options and source files into the directory related with each architectures, and will generated a configure file (.config) during building. It's very good in my opinion. In Android Build System, a given project building inherits a common build options set, and update these parts only related the given project. It's very good for integration. And I want to know if there is a plan to update the build system or accept patches from volunteer? 2. I notice that, all kernel source files have been concatenated into a kernel_all.c, and compile the kernel_all.c. Is there some special reason for this step? It's a slight strange for me? Anyway, I am a new guy. I just want to understand it and if I could provide something to change it. Any comments are appreciated. Thanks, Jerry

2 2

seL4 as bootloader
by Isaac Beckett 29 Mar '21

29 Mar '21

The Linux kernel has support via the EFISTUB module to be loaded directly as an EFI bootloader, which if I recall correctly, also allows it to chainload another OS and be used as a fully-fledged multiboot bootloader. Is it practical to do something similar with seL4? Obviously on non-UEFI platforms it'd be entirely different code, but still.

2 1

About the BuildSystem of seL4
by zhouchunhua＠lixiang.com 26 Mar '21

26 Mar '21

Hi guys, I am a newbie of seL4 and I am trying to get some understanding of it. So, my first question is about the build system of seL4: 1. Why cmake has been taken to build it? I think there are at least two shortcomings about current build system based on CMakeLists.txt: - Some build options were implied in the CMakeLists.txt. It's not easy to get a complete and comprehensive understanding of all the options. And some options depends on other options. Such as, ./init-build.sh -DPLATFORM=odroidc2 -DAARCH64=1 A new guys couldn't get a support list of PLATFORM option, and know AARCH64 is only for ARMv8 SoC easily. - There are too much branches of platform or SoC Architectures. Such as: if(KernelArchARM) include_directories("include/arch/arm/armv/${KernelArmArmV}/") include_directories("include/arch/arm/armv/${KernelArmArmV}/${KernelWordSize}") endif() if(KernelArmMach STREQUAL "exynos") include_directories("include/plat/exynos_common/") endif() if(KernelArchRiscV) include_directories("include/arch/${KernelArch}/arch/${KernelWordSize}") include_directories("include/plat/${KernelPlatform}/plat/${KernelWordSize}") endif() Linux Build System places the special build options and source files into the directory related with each architectures, and will generated a configure file (.config) during building. It's very good in my opinion. In Android Build System, a given project building inherits a common build options set, and update these parts only related the given project. It's very good for integration. And I want to know if there is a plan to update the build system or accept patches from volunteer? 2. I notice that, all kernel source files have been concatenated into a kernel_all.c, and compile the kernel_all.c. Is there some special reason for this step? It's a slight strange for me? Anyway, I am a new guy. I just want to understand it and if I could provide something to change it. Any comments are appreciated. Thanks, Jerry

1 0

About the BuildSystem of seL4
by Jerry Zhou 26 Mar '21

26 Mar '21

Hi guys, I am a newbie of seL4 and I am trying to get some understanding of it. So, my first question is about the build system of seL4: 1. Why cmake has been taken to build it? I think there are at least two shortcomings about current build system based on CMakeLists.txt: - Some build options were implied in the CMakeLists.txt. It's not easy to get a complete and comprehensive understanding of all the options. And some options depends on other options. Such as, ./init-build.sh -DPLATFORM=odroidc2 -DAARCH64=1 A new guys couldn't get a support list of PLATFORM option, and know AARCH64 is only for ARMv8 SoC easily. - There are too much branches of platform or SoC Architectures. Such as: if(KernelArchARM) include_directories("include/arch/arm/armv/${KernelArmArmV}/") include_directories("include/arch/arm/armv/${KernelArmArmV}/${KernelWordSize}") endif() if(KernelArmMach STREQUAL "exynos") include_directories("include/plat/exynos_common/") endif() if(KernelArchRiscV) include_directories("include/arch/${KernelArch}/arch/${KernelWordSize}") include_directories("include/plat/${KernelPlatform}/plat/${KernelWordSize}") endif() Linux Build System places the special build options and source files into the directory related with each architectures, and will generated a configure file (.config) during building. It's very good in my opinion. In Android Build System, a given project building inherits a common build options set, and update these parts only related the given project. It's very good for integration. And I want to know if there is a plan to update the build system or accept patches from volunteer? 2. I notice that, all kernel source files have been concatenated into a kernel_all.c, and compile the kernel_all.c. Is there some special reason for this step? It's a slight strange for me? Anyway, I am a new guy. I just want to understand it and if I could provide something to change it. Any comments are appreciated. Thanks, Jerry

1 0

some confuse about Camkes and AOS sel4
by yadong.li 25 Mar '21

25 Mar '21

hi: I am try to understand the designing philosophy of seL4 kernel base on CAmkES, I didn't find a global memory server in this system But the AOS may be have memory server,even though I am not familiar with AOS now, I have three question: 1. what is the purpose of the existing of CAmkES and AOS meanwhile ? (static and dynamic ) 2. which one (AOS or CAmkES) will be vigorously developed by the seL4 community and fund later. 3. Is a good idea to provide global memory server in CAmkES system? I found usually CAmkES alloc untyped pool Statically for componet in .camkes file. Thank you very much

1 0

Pull requests now directly merged on GitHub
by Gerwin Klein 25 Mar '21

25 Mar '21

The next step in the making contributions easier is now complete: Pull requests for repositories in the seL4 GitHub org can now be merged on GitHub directly, without the loop thought Data61's CI infrastructure. Hopefully this will make merging pull requests faster and less painful. The exception for now are repositories with manifests (such as sel4test-manifest), because parts of these manifests are generated automatically. We're working on moving these as well. The testing and verification regime is the same as before, including extensive hardware tests and proofs, but the results and logs should now be visible directly on GitHub. Happy merging :-) Cheers, Gerwin

1 0

AMD-V Support
by ndaughety13＠gmail.com 24 Mar '21

24 Mar '21

I found "Your host machine has to have a CPU that supports Vt-x virtualization (for Intel CPUs), or AMD-V (for AMD CPUs, but that wasn’t tested)" at https://docs.sel4.systems/projects/camkes-vm/. In context, my understanding is that seL4 should work with AMD-V but it doesn't work on my AMD system. I also do not see any mention of it anywhere else -- not even in the source (could not find amd-v counter part to vtx in grep search of source). Noting that it has not been tested, could this be a build configuration problem or has support not actually been implemented? ...or am I missing something?

1 0