Devel September 2019

devel@sel4.systems

11 participants
18 discussions

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 04 Sep '19

04 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

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel September 2019