- Devel - lists.sel4.systems

IOMUX on iMX6 conflict with libethdrivers
by Fabrizio Bertocci 26 Jun '18

26 Jun '18

Hi, I need your help in trying to understand what is the best way to implement a permanent fix I can push on the seL4 repository regarding the incompatibility issues between the libethdriver and MUX interface of the platsupport. This apply to the iMX6 ethernet driver. I'm not sure about other platforms. In short, the problem is that platsupport takes ownership of the entire MUX (maps the I/O) when the io_ops are initialized: Repo: seL4/seL4_libs File: libsel4platsupport/src/io.c Function: sel4platsupport_new_io_ops ... mux_sys_init(io_ops, get_mux_dependencies(), &io_ops->mux_sys); ... The above call end up calling the platform-specific mux_sys_init that maps only the first 4Kb of IO space from address 0x020e0000 (the base address of the IOMUX controller - note: the IOMUX controller uses 16Kb of address space for its registers, not 4Kb!!!): Repo: seL4/util_libs File: libplatsupport/src/plat/imx6/mux.c Function: mux_sys_init ... MAP_IF_NULL(io_ops, IMX6_IOMUXC, _mux.iomuxc); return imx6_mux_init_common(mux); The pointer "io_ops->mux_sys->priv" should point to the base address of the IOMUX of the SoC (in the virtual memory space of the calling process). The Ethernet driver unfortunately attempts to map the IOMUX again: Repo: seL4/util_libs File: libethdrivers/src/plat/imx6/uboot/mx6qsabrelite.c Function: setup_iomux_enet ... void *base = RESOURCE(&io_ops->io_mapper, IOMUXC); ... // Modify the IOMUX registers, then release the mapped IO: ... UNRESOURCE(&io_ops->io_mapper, IOMUXC, base); but using a larger size (the full 16Kb from the same base address of the IOMUX controller). So, the ethernet controller attempt to map the IO fails because it is already mapped, and nothing works. Right now in my project I've entirely commented out the initialization of the MUXC from the sel4platsupport_new_io_ops function. I understand that if the io_ops attempt to map the MUX (and leave it mapped) there must be a reason, unfortunately I fail to see it. The structure describing the MUXC register (struct imx6_iomuxc_regs, defined in libplatsupport/src/plat/imx6/mux.c) is private and not accessible outside that file, and the only two interface functions available (mux_feature_enable/mux_feature_disable) are not enough to be usable by the ethernet driver. The ethernet driver could also attempt to reuse the same mapped IOMUX (beside that the size of the mapped area is different and won't work anyway), but that will require using the 'priv' field of the io_ops->mux_sys (beside, even trying to map the whole 16Kb of the IOMUX and have the driver to reuse the same mapped address, for some unknown reasons it doesn't work). So, what is the right approach to fix this problem? Why the MUX subsystem maps some IO, never release it and keep it private for most of it? The IOMUX has been introduced somewhere between version 1.0 and 9.x... and it seems a half-baked job... Can we just comment it out if nobody is using it? Or if you have some ideas/suggestions on how to expand it in such a way the ethernet driver could use, please let me know. I'll be happy to implement it. Regards, Fabrizio

2 2

Problems with tk1 nonsecure
by Mike Clark 26 Jun '18

26 Jun '18

I just checked out a fresh copy of https://github.com/ SEL4PROJ/camkes-arm-vm-manifest and built an image for the TK1 using the docker build environment. I copied the resulting image to an SD card and it boots fine. If I switch to the unsecure mode, I get an error on boot. SMMU Address translation error: ID: 98 address: 0xae5be000 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x0 [ 10.204777] mmc1: ADMA error I have not made any changes, so my vm.smmu settings are all default. Any thoughts or help? Mike

3 9

Question about process and thread in tutorials
by 송대영 21 Jun '18

21 Jun '18

* I have question about process and thread in tutorials. 1. sel4 doesn't have process concept.But making new process is exist in tutorial hello-4.What is the exactly difference trhead in hello-2 and process in hello-4?2. In tutorials hello-4, where can I find access path that hello-4 process link hello-4-app?It means I think hello-4 process should designate hello-4-app's path.*

2 1

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 22 May '18

22 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