- Devel - lists.sel4.systems

camkes and compcert
by Michael Neises 21 Jun '18

21 Jun '18

Hello, I understand that the proof for seL4 implies that the compiler and linker do not need to be trusted, because their output can be verified by a tool. Does this output-verification also apply to CAmkES C code for components and interfaces? Specifically, I'm working on a project where we want to have certain functionality implemented in C to be run on the seL4 microkernel. Would we gain any proof by using compcert, or is the output-verification sufficient? And is there any way to execute previously-compiled C binaries in a CAmkES component? I tried system calls, but I learned that won't work with the microkernel :-) I looked into the build architecture of the project, but I couldn't find where CAmkES components were being compiled. I looked into replacing gcc with compcert for the system, but there are used many flags available to gcc that are not available to compcert, so I scratched that idea. Thank you for your help. -Michael

2 1

Regarding porting SEL4 on RISCV hardware
by Sathya Narayanan N 15 Jun '18

15 Jun '18

Hi Members, I am trying to port SEL4 on RISCV hardware. I am stuck in finding the DTB/DTS files path in sel4test folder. Could someone guide me where these files exist and how to change the memory map for UART console. Actually, We changed the code for putchar in systems.c for Linux. So, I am trying to figure out, how to do something similar for SEL4. Please let me know, if someone has ported SEL$ to RISCV hardware. -- regards, Sathya

2 1

feL4: seL4 + Rust
by Jon Lamb 11 Jun '18

11 Jun '18

Hi all! We've been working on a way to write Rust programs for seL4, and would like to share it with you: https://github.com/PolySync/cargo-fel4.git With cargo-fel4, you can write a seL4 task in Rust, expose it through a prescribed entry point, and then build it along with the kernel. For now, it exposes only the system calls by way of Bindgen (a C-to-Rust bindings generator); however, we have plans to build up more idiomatic and Rusty abstractions in the near future. Cheers! Jon, Dan, Zack, and Nathan at PolySync

1 0

seL4_Wait crash if kernel is compiled with -O0 (qemu, pc99, gcc 4.8.2)
by Fabrizio Bertocci 25 May '18

25 May '18

Hi, After hours of debugging I have discovered a quite nasty issue where seL4_Wait() crash if I build the kernel without optimization (gcc option -O0) on a pc99 tested with qemu. How to reproduce: Just create an endpoint (from a vka) and call seL4_Wait(). The simplest reproducer can be obtained from the hello-2 tutorial: - Copy the main.c from the solution directory in the apps/hello-2/src/main.c - Add the following codes right after the creation of vka (TASK 5, approx line 150): { printf("WAITING----------------------------------------------\n"); seL4_Word myBadge; vka_object_t ep_object = {0}; error = vka_alloc_endpoint(&vka, &ep_object); ZF_LOGF_IFERR(error, "Failed to allocate new endpoint object.\n"); seL4_Wait(ep_object.cptr, &myBadge); printf("---------------------------------------------- DONE!!\n"); } Essentially the added code, creates an endpoint using vka and calls seL4_Wait() on it... I expect the code to block forever since there are no other threads that can unblock it... - Build it and run it with: make pc99_hello-2_defconfig make make simulate Expected output: Booting all finished, dropped to user space 4 untypeds of size 12 4 untypeds of size 13 [...] 6 untypeds of size 29 WAITING---------------------------------------------- - Now change the configuration using 'make menuconfig' and select: seL4 Kernel -> Build Options -> Compiler optimisation flag (-O2) and change it to -O0, save the new configuration. - Rebuild and run: make simulate Now you get a kernel exception: [...] 6 untypeds of size 29 WAITING---------------------------------------------- ========== KERNEL EXCEPTION ========== Vector: 0xd ErrCode: 0xa658 IP: 0xe0118ce5 SP: 0xffaf7e28 FLAGS: 0x86 CR0: 0x8001003b CR2: 0x0 (page-fault address) CR3: 0x142000 (page-directory physical address) CR4: 0x100290 Stack Dump: *0xffaf7e28 == 0xe011a658 *0xffaf7e2c == 0x0 *0xffaf7e30 == 0x0 *0xffaf7e34 == 0xe011a658 *0xffaf7e38 == 0x8 *0xffaf7e3c == 0x202 *0xffaf7e40 == 0x0 *0xffaf7e44 == 0x0 *0xffaf7e48 == 0x10 *0xffaf7e4c == 0x7 *0xffaf7e50 == 0x0 *0xffaf7e54 == 0x0 *0xffaf7e58 == 0x0 *0xffaf7e5c == 0x0 *0xffaf7e60 == 0x0 *0xffaf7e64 == 0x0 *0xffaf7e68 == 0x0 *0xffaf7e6c == 0x0 *0xffaf7e70 == 0x0 *0xffaf7e74 == 0x0 Halting... halting... Kernel entry via Interrupt, irq 157 Version info: - gcc: gcc (GCC) 4.8.5 20150623 (Red Hat 4.8.5-11) - qemu: QEMU emulator version 2.0.0, Copyright (c) 2003-2008 Fabrice Bellard - Build environment: CentOS Linux release 7.3.1611 (Core) Other info: - gcc 4.8.5 doesn't seem to support the 'Nehalem' x86 microarchitecture, so I am selecting the 'Generic' microarchitecture (Toolchain Options -> X86 microarchitecture) - Even the tutorial 'hello-timer' fails exactly with the same exception without any modifications if you build the kernel with -O0. - Tested on a Beaglebone black: no problems compiling kernel with -O0 Regards, Fabrizio Bertocci Real-Time Innovations, Inc.

2 1

Tutorials broken?
by Fabrizio Bertocci 21 May '18

21 May '18

Hi all, I was going through the tutorials, unfortunately I've been finding very challenging to follow the instructions as I keep encountering issues after issue. First, the repo command seems to be incorrect. In document: https://docs.sel4.systems/Tutorials/ it says: repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest -m sel4-tutorials.xml but the manifest file 'sel4-tutorials.xml' does not exist on the git repository (of the sel4-tutorial-manifest). What is the correct manifest file to use? There are two manifests (in any branch and tag): master.xml and default.xml. default.xml seems to use the 'new' format of identifying the individual versions of the libraries (through the hash). Let's assume the correct manifest to use is the 'default.xml' from the 'sel4-tutorials' branch and initialize the workspace with: repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest -b sel4-tutorials repo sync So, now: first tutorial, ok (but this tutorial does very little). Second tutorial (hello-2), not so good... to avoid mistake, I am copying directly the solution into the app area: cp projects/sel4-tutorials/solutions/hello-2/src/main.c apps/hello-2/src/main.c make pc99_hello-2_defconfig make ... and the build fails with: [...]/workspaces/sel4-tutorials-2/stage/x86/pc99/lib/libsel4allocman.a(virtual_pool.o): In function `_add_page': [...]/workspaces/sel4-tutorials-2/libs/libsel4allocman/src/mspace/virtual_pool.c:52: undefined reference to `vspace_get_map_obj' The missing function appears to be part of libsel4vspace, that is missing from the library dependency list. Let's add it to add it to the apps/hello-2/Makefile: diff --git a/exercises/hello-2/Makefile b/exercises/hello-2/Makefile index 25c0b35..97a4fc6 100644 --- a/exercises/hello-2/Makefile +++ b/exercises/hello-2/Makefile @@ -28,6 +28,7 @@ ASMFILES += $(patsubst $(SOURCE_DIR)/%,%,$(wildcard $(SOURCE_DIR)/src/plat/${PLA # Libraries required to build the target LIBS = c sel4 sel4muslcsys \ sel4simple sel4vka sel4allocman \ + sel4vspace \ sel4platsupport platsupport \ utils sel4simple-default sel4utils sel4debug Now it builds successfully, unfortunately when running, the child thread doesn't appear to run at all. This is the output of qemu running 'make simulate': Booting all finished, dropped to user space 4 untypeds of size 12 5 untypeds of size 13 5 untypeds of size 14 4 untypeds of size 15 4 untypeds of size 16 4 untypeds of size 17 4 untypeds of size 18 5 untypeds of size 19 5 untypeds of size 20 2 untypeds of size 21 4 untypeds of size 22 4 untypeds of size 23 2 untypeds of size 24 3 untypeds of size 25 3 untypeds of size 26 3 untypeds of size 27 1 untypeds of size 28 6 untypeds of size 29 main: hello world I would have expected seeing on the output the string 'thread_2: hallo wereld' somewhere... Why the thread 2 does not run? This code was working last time I checked (version 5.2). I tried then to continue testing the tutorials, and I went to the hello-3. Hello-3 is based on the Hello-2 but adds an endpoint for IPC between the main thread and the child thread. Surprisingly, this app not only builds out of the box without errors (apparently libsel4vspace was already added to its Makefile), but even running it, works as expected: Booting all finished, dropped to user space 3 untypeds of size 12 5 untypeds of size 13 5 untypeds of size 14 4 untypeds of size 15 4 untypeds of size 16 4 untypeds of size 17 4 untypeds of size 18 5 untypeds of size 19 5 untypeds of size 20 2 untypeds of size 21 4 untypeds of size 22 4 untypeds of size 23 2 untypeds of size 24 3 untypeds of size 25 3 untypeds of size 26 3 untypeds of size 27 1 untypeds of size 28 6 untypeds of size 29 main: hello world thread_2: hallo wereld thread_2: got a message 0x6161 from 0x61 main: got a reply: 0xffff9e9e Right now I suspect that seL4_TCB_Configure() does not work correctly if we don't provide an endpoint (because that's essentially the main difference between the two tests). Can somebody try to run the tutorials and perhaps confirm the problem? Regards, Fabrizio Bertocci Real-Time Innovations, Inc. Sunnyvale, CA

1 0

docker build error
by Paolo Crisafulli 18 May '18

18 May '18

Hi all, I'm using the docker build environment provided by https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles Currently, "make sel4" fails with this message: E: Package 'ncurses-dev' has no installation candidate Anyone experimenting the same behaviour? Cheers, Paolo

2 2

Help with Isabelle/AutoCorres
by Burkhart Wolff 18 May '18

18 May '18

Dear all, I stumbled into some problems with AutoCorres and would be grateful if someone could help me. I used the recent version autocorres1.4 under Isabelle2017. A) Running under MacOS, cpp is apparently not running inside install_C_file (yes, I installed the cpp wrapper: >>>>>>>>>>>>>>>>>>>>>> !/bin/bash # Wrapper for clang C preprocessor on MacOS export L4CPP="-DTARGET=ARM -DTARGET_ARM -DPLATFORM=Sabre -DPLATFORM_Sabre" llvm-gcc -Wno-invalid-pp-token -E -x c $@ <<<<<<<<<<<<<<<<<<<<<< and made sure that it is in the path of the shell in which I started Isabelle.) Does anyone know a cause for this behaviour or a feasible workaround ? (besides doing the expansions by hand) Is there an explicit Isabelle shell variable where the path to cpp must be set ? B) I get a weird crash of AutoCorres without a clue what might cause it: I have a T4.h file with >>>>>>>>>>>>>>>>>>>>>>> #define N_TEETH ( 100 * MODULO ) // shaft encoder's number of teeth per turn #define SIZE_OF_SPEED_FIFO 10 // number of samples to compute average speed extern const char *InputField[]; enum State { S1=1, S2, S3, S4, S5, S6, SFail=0 }; enum Status { FAIL, SUCCESS }; enum InputPatterns { Ph1 = 1, Ph2 = 5, Ph3 = 4, Ph4 = 6, Ph5 = 2, Ph6 = 3 }; struct OBits { int C1 ; int C2 ; int C3 ; } Obits; /********* Output data *****************/ extern enum Status O_Position_Valid; extern unsigned int O_Position_Count; extern unsigned int Relative_Position; extern int Instantaneous_Speed; extern int Mean_Speed; <<<<<<<<<<<<<<<<<<<<<<<<<<<<< and a T4.c file with: >>>>>>>>>>>>>>>>>>>>>>>>>>>>> #include "T4_AlgoODO.h" enum Status O_P_V = SUCCESS; unsigned int O_P_C = 0; unsigned int Relative_Position = 0; int I_Speed = 0; int Mean_Speed = 0; int Acceleration = 0; int scale = 1000; int PI_approx = 3141; struct OBits Input; enum State OState; const unsigned int Radius = 500; const unsigned int Sampling_Rate = 400; unsigned int F_O_P_C = 0; int Speed_FIFO[10 /*SIZE_OF_SPEED_FIFO*/]; int FIFO_pointer = 0; <<<<<<<<<<<<<<<<<<<<<<<<<<<<<<< Loading this in Isabelle/AutoCorres with: >>>>>>>>>>>>>>>>>>>>>>>>> install_C_file "code/c/T4.c” <<<<<<<<<<<<<<<<<<<<<<<<< results in the following AutoCorres crash: … exception Fail raised (line 175 of "~/codebox/odo_new/odo/autocorres-1.4/c-parser/calculate_state.ML"): translate_inttype: incomplete array! Can anybody tell me what this means and propose a workaround ? Best regards B. Wolff

2 1

Untyped Retype destination not empty?
by Richard Clark 18 May '18

18 May '18

Hi! I could use a clue as to the cause of this problem. The program has its free slots start index set correctly. It is trying to allocate a dma buffer. (4k with a known physical address). The vspace has been properly set up and knows the phys addresses of its free memory. This used to work fine in a different process, but I can't find anything I've done different/wrong in this one... I've added some extra printfs, and some debug code (in kernel/src/object/untyped.c). /* Ensure that the destination slots are all empty. */ slots.cnode = CTE_PTR(cap_cnode_cap_get_capCNodePtr(nodeCap)); slots.offset = nodeOffset; slots.length = nodeWindow; for (i = nodeOffset; i < nodeOffset + nodeWindow; i++) { status = ensureEmptySlot(slots.cnode + i); if (status != EXCEPTION_NONE) { userError("Untyped Retype: Slot #%d from %p in destination window non-empty.", (int)i, (void *)slots.cnode); userError("Untyped Retype: At offset #%d length %d.", (int)nodeOffset, (int)nodeWindow); int j = 0; for(j=0;j<2048;j++){ status = ensureEmptySlot(slots.cnode + (i + j)); if (status == EXCEPTION_NONE) { userError("Next Free Slot at #%d from %p.", (int)(i+j), (void *)slots.cnode); status = EXCEPTION_SYSCALL_ERROR; break; } } return status; } } And finally, here is the output from the console: <<seL4(CPU 0) [decodeCNodeInvocation/94 T0xffffff8001a25400 "Lockmaproc" @4196e8]: CNode Copy/Mint/Move/Mutate: Destination not empty.>> <<seL4(CPU 0) [decodeUntypedInvocation/166 T0xffffff8001a25400 "Lockmaproc" @420f2c]: Untyped Retype: Slot #196 from 0xffffff807f000000 in destination window non-empty.>> <<seL4(CPU 0) [decodeUntypedInvocation/167 T0xffffff8001a25400 "Lockmaproc" @420f2c]: Untyped Retype: At offset #196 length 1.>> <<seL4(CPU 0) [decodeUntypedInvocation/172 T0xffffff8001a25400 "Lockmaproc" @420f2c]: Next Free Slot at #197 from 0xffffff807f000000.>> _refill_pool@split.c:187 Failed to retype untyped, error 8 vka_alloc_object_at_maybe_dev@object.h:59 Failed to allocate object of size 4096, error 1 dma_alloc@page_dma.c:92 Failed to allocate untyped of size 12 I need a hint... help? Thanks! Richard ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

2 1

Automatic testing using qemu
by Paolo Crisafulli 17 May '18

17 May '18

Hi there, I have written a seL4 app using CAmkES, that I am continuously building using Jenkins. I'd like to add a test step to this continuous integration process, launching the app with qemu and parsing the output to validate my expectations. The thing is, although all the active ("control") components reach their last instruction after a while, seL4 does not "exit" (which is expected I guess) and qemu does not stop, keeping my continuous integration job running for ever. Any idea on how to achieve this? Thank you very much in advance. Cheers, Paolo Crisafulli

3 5

Booting seL4, MMU configuration on armv7a-ve
by Jonas Persson 30 Apr '18

30 Apr '18

Hello, I'm new to seL4 and I'm trying to get seL4 running on an Cortex-A7 with VE extensions (NXP IMX6UL). One of the experiments I wish to do is measure how fast I can get from POR to seL4 doing something meningful. To achive optimal boot speed I have a custom bootloader that does the bare minimum. The boot flow looks like this; 1. POR 2. Init HW 3. Load & verify blobs for trust zone and seL4 4. Jump to TEE init (OP-TEE) 5. Tee init code returns to bootloader with the CPU in HYP mode At this point we're back in the bootloader, there is no MMU, D cache or I cache active 6. Configure MMU 7. Jump to seL4 kernel entry I'm currently struggling with getting the MMU properly setup and I was hoping that someone here might shed some light on what I would need to do. I've looked at the elf-loader and from what I can understand it will setup a basic memory-mapping for the kernel only. Some of the questions that stand out in my head are : 1) How should the hand over work between the BL and seL4 with respect to setting up more mappings, for example IO memory. Should the PGD & PMD tables created by the bootloader be shared with the kernel? 2) What needs to be configured before calling the seL4 entry? Thanks, Jonas

1 0