September 2019 - Devel - lists.sel4.systems

Adding an Extra Component in Camkes
by Amit Goyal 03 Oct '19

03 Oct '19

Hi, I was trying to add an extra component in hello-camkes-1 example. Here are the small tweaks that I did. a) hello-camkes-1-camkes.template import <std_connector.camkes>; import "components/Client1/Client1.camkes"; import "components/Client2/Client2.camkes"; import "components/Echo/Echo.camkes"; assembly { composition { component Client1 client1; component Client2 client2; component Echo echo; connection seL4RPC hello_con(from client1.hello1, to echo.hello2); } } -------------------------------------------------------------------------------------------------------------------------- b) CMakeLists.text cmake_minimum_required(VERSION 3.7.2) project(hello-camkes-1 C) DeclareTutorialsCAmkESComponent(Client TEMPLATE_SOURCES components/Client1/src/client1.c) DeclareTutorialsCAmkESComponent(Client TEMPLATE_SOURCES components/Client2/src/client2.c) DeclareTutorialsCAmkESComponent(Echo TEMPLATE_SOURCES components/Echo/src/echo.c) DeclareCAmkESComponent(EmptyComponent) DeclareTutorialsCAmkESRootserver(hello-camkes-1.camkes ADL_IS_TEMPLATE TEMPLATE_SOURCES interfaces/HelloSimple.camkes TUTORIAL_SOURCES components/Client1/Client1.camkes components/Client2/Client2.camkes components/Echo/Echo.camkes ) ------------------------------------------------------------------------------------------------------------------------ I am getting the following error: STDERR: CMake Warning at tools/seL4/cmake-tool/flags.cmake:123 (message): Kernel supports hardware floating point but toolchain does not Call Stack (most recent call first): tools/seL4/cmake-tool/base.cmake:58 (include) tools/seL4/cmake-tool/all.cmake:16 (include) CMakeLists.txt:21 (include) CMake Error at build/projects/sel4-tutorials/camkes-gen.cmake:192 (target_link_libraries): Error evaluating generator expression: $<TARGET_PROPERTY:CAmkESComponent_Client1,COMPONENT_LIBS> Target "CAmkESComponent_Client1" not found. Call Stack (most recent call first): tools/camkes/camkes.cmake:591 (include) projects/sel4-tutorials/CMakeLists.txt:257 (GenerateCAmkESRootserver) CMake Error at build/projects/sel4-tutorials/cam... (2531 more, please see e.stderr) ----------------------------------------------------------------------------------------------------------------- Can you please suggest a possible solution. -- Thanks and Regards, Amit Goyal

2 1

Questions about building Raspberry Pi image on SEL4
by Zhonghao Liao 03 Oct '19

03 Oct '19

Hi, I am Zhonghao Liao, a graduate student from Iowa State University. We are doing a security related project and would like to deploy the code to the SEL 4. The hardware we use is Raspberry Pi 3 B+. We follow the tutorial here <https://docs.sel4.systems/Hardware/Rpi3.html> and have successfully loaded the SEL4 test image. We think the next step should be building the image for the application and run it on the Raspberry Pi. We followed the CAmKES tutorial <https://docs.sel4.systems/CAmkES/> and tried to use the command: ../init-build.sh -DPLATFORM=sabre -DAARCH32=1 -DCAMKES_APP=adder -DSIMULATION=1 to build the image for the Raspberry Pi but we failed. In fact, we change the settings.cmake file in the camkes-project folder and add "rpi3" at line 36: set(valid_arm_platform "am335x;sabre;kzm;exynos5410;exynos5422;tx1;tx2;zynq7000;rpi3") and the command we used is: ../init-build.sh -DPLATFORM=rpi3-DAARCH32=1 -DCAMKES_APP=adder -DSIMULATION=1 We did get an image but we cannot simulate using QEMU: ninja: Image Name: Created: Tue Sep 17 09:30:30 2019 Image Type: ARM Linux Kernel Image (uncompressed) Data Size: 2110464 Bytes = 2061.00 KiB = 2.01 MiB Load Address: 0157c000 Entry Point: 0157c000 ./simulate: Unsupported platform or architecture for simulation Also we tried to load the image into the RPi3 but we are also defeated: bootelf {loadaddr} ## No elf image at address {loadaddr} I think our problem is that we don't provide enough dependencies to support building the RPi image. But we have no idea where to start. Could you please give us any advice? Otherwise, If the CAmkES can not be used, how do I build an application on SEL4 and run it on the Raspberry Pi? Thanks for your patient and looking forward to your reply. Thank you! Best, Zhonghao

2 1

Enable benchmarking tools on SEL4
by Zhonghao Liao 20 Sep '19

20 Sep '19

Hi, I am going to measure the resource consumption of process on SEL4 and I found the tutorial here: https://docs.sel4.systems/BenchmarkingGuide.html One thing I am confused about is how to enable the benchmark feature shown below: "This feature can be enabled from the menuconfig list (seL4 Kernel > Enable benchmarks > Track threads and kernel CPU utilisation time)." It seems like there should be a file "menuconfig" or some other similar object I can modify. But I cannot find such an object. I would appreciate if you could give me any suggestions. Thank you! Best, Zhonghao

2 1

Using RPC in two different container
by Shahnewaz Sakib 19 Sep '19

19 Sep '19

Hi, I just used hello-camkes-1 tutorial to send and receive a message between a client and an echo. My understanding is that both client and echo are in the same machine but different address. What changes do I need to make so that client and echo are in different machine? I have used docker for using seL4 environment. I was thinking about using container1 for client and container2 for echo and communicate between them. Is there any way I can do it by modifying the hello-camkes-1tutorial? If not, can anyone suggest a way to do it? Thanks! -- Regards' Shahnewaz Karim Sakib

2 1

Issues with broadcasting a message in seL4
by Shahnewaz Sakib 13 Sep '19

13 Sep '19

Hi, I was trying to generate a simple broadcasting message in sel4. I have used a c code I found in the internet. #include <stdio.h> #include <sys/socket.h> #include <arpa/inet.h> #include <stdlib.h> #include <string.h> #include <unistd.h> void DieWithError(char *errorMessage) { perror(errorMessage); exit(1); } int main(int argc, char *argv[]) { int sock; struct sockaddr_in broadcastAddr; char *broadcastIP; unsigned short broadcastPort; char *sendString; int broadcastPermission; unsigned int sendStringLen; broadcastIP = "0.0.0.0"; broadcastPort = 6741; sendString = "Hello World!"; printf("start\n"); printf("Socket is about to be created!\n"); if ( (sock = socket(AF_INET, SOCK_DGRAM, 0)) < 0 ) { perror("socket creation failed"); exit(EXIT_FAILURE); } printf("Socket is created! \n"); broadcastPermission = 1; if (setsockopt(sock, SOL_SOCKET, SO_BROADCAST, (void *) &broadcastPermission, sizeof(broadcastPermission)) < 0) DieWithError("setsockopt() failed"); memset(&broadcastAddr, 0, sizeof(broadcastAddr)); broadcastAddr.sin_family = AF_INET; broadcastAddr.sin_addr.s_addr = inet_addr(broadcastIP); broadcastAddr.sin_port = htons(broadcastPort); sendStringLen = strlen(sendString); for (;;) { if (sendto(sock, sendString, sendStringLen, 0, (struct sockaddr *) &broadcastAddr, sizeof(broadcastAddr)) != sendStringLen) DieWithError("sendto() sent a different number of bytes than expected"); sleep(3); } return 0; } However, I get the error in syscall 41. What I understood is that for some reason the socket is not created successfully and can't find an endpoint. What can be the reason for that? libsel4muslcsys: Error attempting syscall 41 Caught cap fault in send phase at address (nil) while trying to handle: vm fault on data at address 0x28 with status 0x4 in thread 0xffffff801fe09400 "rootserver" at address 0x40e3af With stack: 0x41ce28: 0x40c0fe 0x41ce30: 0x418720 0x41ce38: 0x0 0x41ce40: 0x41ceb0 0x41ce48: 0x0 0x41ce50: 0x0 0x41ce58: 0x4011bd 0x41ce60: 0x41cf10 0x41ce68: 0x200402323 0x41ce70: 0x3 0x41ce78: 0x3 0x41ce80: 0x41ceb0 0x41ce88: 0x401ce2 0x41ce90: 0xffffffff00000000 0x41ce98: 0x412008 0x41cea0: 0x1a5500000041cf20 Thanks! -- Regards' Shahnewaz Karim Sakib

2 1

CAmkES 3.7.0 bug?
by Zippy Maniac 11 Sep '19

11 Sep '19

Hi, I am porting an old application from CAmkES 2.x to CAmkES 3.7.0. But I am having an issue with a very large dataport. The data structure mapped between components needs to be about 25 MiB. I have defined the size of the connection to be 64 MiB. But compilation fails. Looking at the generated code for the shared data I see this struct { char content[ROUND_UP_UNSAFE(sizeof(ui_config_t), PAGE_SIZE_4K)]; } to_0_ui_configbuf_data ALIGN(16777216) SECTION("align_24bit") USED; extern typeof(to_0_ui_configbuf_data) to_0_ui_configbuf_data ALIGN(67108864) VISIBLE; static_assert(sizeof(to_0_ui_configbuf_data) <= 67108864, "typeof(to_0_ui_configbuf_data) size greater than dataport size."); static_assert(sizeof(to_0_ui_configbuf_data) % 16777216 == 0, "to_0_ui_configbuf_data not page-sized. Template bug in its declaration? Suggested formulation: `char to_0_ui_configbuf_data[ROUND_UP_UNSAFE(sizeof(...), PAGE_SIZE_4K)];`"); But compilation fails with projects/musllibc/build-temp/stage/include/assert.h:12:23: error: static assertion failed: "to_0_ui_configbuf_data not page-sized. Template bug in its declaration? Suggested formulation: `char to_0_ui_configbuf_data[ROUND_UP_UNSAFE(sizeof(...), PAGE_SIZE_4K)];`" The assert is looking for the buffer to be a multiple of 16MiB but the ROUND_UP_UNSAFE is only doing working to a multiple of 4KiB. PAGE_SIZE_4K is hard coded in the template but the alignment has changed from 12bit to 24bit so CAmkES is aware of the large data structure. I guess I could pad and align my data structure to a multiple of 16MiB. Also, having hard coded numbers in my top level CAmkES configuration for the dataport size is a bit of a maintenance nightmare. Being able to use a #define from the code base would be ideal but this doesn't work. It does work for paddr and irq_number specifications! Cheers, Zippy

2 2

Error with the file handling in camkes tutorial
by Akshat Garg 11 Sep '19

11 Sep '19

Hi all, I am trying to understand how the camkes system works. I get stuck up on a problem where I tried to change the code of camkes 1 tutorial ( https://docs.sel4.systems/Tutorials/hello-camkes-1.html) a bit. In a simple sender receiver code, I tried to write the contents, received by the receiver, in a file. But, while doing it I got the following error message. The error message was not letting me to create a file in any mode. When using read mode with FILE *fptr = fopen("xxxyyyzzz", "r"); I encountered the following message: sys_open_impl@sys_io.c:205 Failed to open file xxxyyyzzz FAULT HANDLER: data fault from client1.control (ID 0x1) on address 0, pc = 0x411754, fsr = 0x4 FAULT HANDLER: rip = 0x411754 FAULT HANDLER: rsp = 0x528ae8 When using write mode with FILE *fptr = fopen("xxxyyyzzz", "w"); I encountered the following message: sys_open_impl@sys_io.c:191 Open only supports O_RDONLY, not 0x241 on xxxyyyzzz Assertion failed: flags == O_RDONLY (../projects/seL4_libs/libsel4muslcsys/src/sys_io.c: sys_open_impl: 192) Kindly, suggest me a way out or let me know the reason if not possible. -Akshat

2 1

Compiling Error for Hello World
by Shahnewaz Sakib 11 Sep '19

11 Sep '19

Hi, I was trying to compile hello world using the tutorial here <https://docs.sel4.systems/Tutorials/#get-the-code>. I was able to compile sel4test before and I built the dependencies using docker. For running hello world, I used the command "../init --plat pc99 --tut hello-world". Then I got the following error message: Traceback (most recent call last): File "../init", line 16, in <module> import common File "/home/bikas/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 16, in <module> import sh ModuleNotFoundError: No module named 'sh' I have looked into my machine and I do have sh in "/usr/bin/sh". I am not sure what is the source of the error. Please let me know. Thanks! -- Shahnewaz Karim Sakib

2 1

Muen
by Gergely Buday 07 Sep '19

07 Sep '19

Hi, how does Muen relate to seL4? https://muen.codelabs.ch/ e.g. it claims to be the first verified microkernel. - Gergely

2 1

Issues about compile C program
by Zhonghao Liao 03 Sep '19

03 Sep '19

Hi, I am a graduate student and I am doing ainformation security related research project using SEL4. I installed the SEL4 kernel on a raspberry pie 3. The problem is that I can't compile C programs on this Raspberry Pi. Any suggestions for solving this problem? Thank you! Best, Zhonghao Liao

2 1