- Devel - lists.sel4.systems

GPIO on Sabre imx6
by Parvaneh Ahgajani 10 Feb '20

10 Feb '20

Hello all, I am working with sabre lite board and using camkes framework. In my implementation I have a driver component that has 7 dataport buf and I connected these buffers to hardware component. In source of component driver I am initialize gpio_sys, mux_sys and pins using these functions: - imx6_mux_init() - imx6_gpio_sys_init() - gpio_new() Here I have copied some part of my code: ****************************************** gpio_sys_t gpio_sys; gpio_t pins[32*7]; mux_sys_t mux_sys; void gpio__init() { imx6_mux_init(NULL, &mux_sys); imx6_gpio_sys_init((void*)gpio0, (void*)gpio1, (void*)gpio2, (void*)gpio3, (void*)gpio4, (void*)gpio5, (void*)gpio6, &mux_sys, &gpio_sys); } void gpio_init_pin(int pin, int direction) { if(pin>0 && pin< sizeof(pins)/sizeof(pins[0])) { gpio_new(&gpio_sys, pin, (enum gpio_dir)direction, &pins[pin]); } } void gpio_set_pin(int pin, int value) { if(pin >= 0 && pin < (sizeof(pins)/sizeof(pins[0]))) { if(value) { gpio_set(&pins[pin]); } else { gpio_clr(&pins[pin]); } } } int gpio_read_pin(int pin) { if(pin>0 && pin< sizeof(pins)/sizeof(pins[0])) { return gpio_get(&pins[pin]); } return -1; } ****************************************** By calling "gpio_init_pin(ALARM_PIN= 28, 0);" I am getting this error: Assertion failed: bank->data == v (PATH/projects/util_libs/libplatsupport/src/plat/imx6/gpio.c: imx6_gpio_write: 144) How can I fix this error? How should I specify the GPIO pins? Thank you for your time and consideration, Parvaneh.

2 3

(no subject)
by abdi mahmud haji 06 Feb '20

06 Feb '20

hi everybody i have quick questions regarding how can you take an input form terminal in seL4,i am trying to run a simple code of my own on sel4 and to display a message we use printf(), why scanf() is not working for me the way printf work.is there another way to do that

2 1

Question about MCS branch
by Isaac Beckett 05 Feb '20

05 Feb '20

I have a bit of a noobish question, why are timing/scheduling abilities being added to the kernel? I understand that userland still controls scheduling, regardless of which branch is being used, but I'm confused as to wby scheduling features needed to be added to the kernel itself.

2 1

Configuring CAmkES projects
by Grant Jurgensen 01 Feb '20

01 Feb '20

Hi everyone, I have a couple questions regarding the current CMake build structure for CAmkES projects. It seems that the current structure intends you to put your project in the camkes/apps folder, and then build your project with `../init-build -DCAMKES_APP=<project_name>`, or the equivalent using the griddle script. What I don't understand is how you are supposed to configure your project. It seems easy_settings.cmake is always loaded. Is it advisable to edit this file? In the past, I could also tweak configuration variables manually by invoking the ccmake gui on the top-level directory. Now that there is no CMakeLists.txt in the top-level directory, this does not work. If I try it in my project's directory, it tells me the cache is empty. Is it still possible to edit CMake cache variables with ccmake? Thanks! Grant Jurgensen

2 2

Recycle resources used by a thread after it terminates
by Alexandre Mutel 01 Feb '20

01 Feb '20

Hi, I have a design question regarding how to recycle capabilities/memory frames that were used by a thread once it terminates. Let's assume that there is a MemoryManager server responsible to serve virtual memory to user processes (e.g similar to implementing VirtualAlloc). The MemoryManager has to maintain the list of untyped object, retype them, maintain likely a list of resources allocated for a user thread, likely copy/mint the page frames to forward them to the user process...etc. But when a thread terminates, as I can't see any related events in seL4, I would assume that the user process would have to explicitly notify the MemoryManager on exit. Then the MemoryManager would know which user thread has exited and would update/recover the used capabilities and destroy them, in order to recover untyped objects. Would it be a proper design that plays well with seL4? Do you think that it could be done more efficiently with seL4? Thank you!

2 2

AMD CPUs and SMP scalability
by Demi M. Obenour 30 Jan '20

30 Jan '20

My understanding is that seL4 plans on scaling to large multi-core server processors by using Intel TSX. However, AMD has not implemented TSX, and TSX has been involved in many recent side-channel attacks. AMD systems are attractive both from a performance and a security perspective, but my understanding is that the performance of seL4 on them will be terrible. Are there plans to implement and verify a version of seL4 that scales to multicore AMD server-class CPUs? The problem with a multikernel is that not having thread migration is likely to cause starvation on many practical workloads Sincerely, Demi

2 2

Status of side-channel attack mitigation
by Demi M. Obenour 30 Jan '20

30 Jan '20

What is the current status of seL4 with respect to Meltdown, Spectre, L1TF, MDS and other CPU vulnerabilities? Thank you, Demi

2 2

(no subject)
by abdi mahmud haji 30 Jan '20

30 Jan '20

hi i have been wondering how can i install or put another OS( like , window ,linux )on the top of seL4 microkernel can some one help

2 1

Are there any plans to re-add seL4_Untyped_RetypeAtOffset?
by Andrew Warkentin 29 Jan '20

29 Jan '20

Speaking of things that would be useful for large dynamic systems, are there any plans to add seL4_Untyped_RetypeAtOffset from the old experimental branch to the current mainline kernel? I am writing a buddy untyped allocator for UX/RT, and being able to retype at arbitrary offsets would reduce overhead quite a bit because I could just retype from the highest-order untyped objects most of the time rather than having to create two child untyped objects per split. If not, I will probably end up re-adding it myself later on (sometime after UX/RT is running actual user programs).

5 20

Camkes and Memory-Mapped Peripherals
by Michael Neises 29 Jan '20

29 Jan '20

Hello, I'm trying to access a memory-mapped peripheral on the exynos5422 (ODROID XU4). I have the physical address of the peripheral's registers from the exynos5422 data sheet. As per the Camkes manual, I've used the seL4HardwareMMIO connection type to facilitate this. However, while I can use the excess bytes of the "dataport Buf" as expected, there is a data fault when I try to read from the peripheral's memory-mapped (and readable) registers: """ FAULT HANDLER: data fault from test_component.test_component_0_control (ID 0x1) on address 0, pc = 0x3250c, fsr = 0x211 """ Besides defining the hardware component and this connection in Camkes, is there anything else I must do? I will appreciate any guidance on this matter. Best, Michael Neises

2 1