- 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 06 Feb '20

06 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 02 Feb '20

02 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 02 Feb '20

02 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 31 Jan '20

31 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 31 Jan '20

31 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

Re: [seL4] Request for enhancement: Notification queues
by Millar, Curtis (Data61, Kensington NSW) 25 Jan '20

25 Jan '20

> I strongly suspect the more fundamental and general extension would be > to remove the scalability limitation of Notifications, probably by > generalising them to a hierarchy, i.e. you signal a sub-notification > which then signals the higher-level notification. I?m not claiming > having thought this through, though. Having thought about this a little, I think that it is useful to observe that the case where such cases where large numbers of notifications need to be received the receiver uses a roughly similar interface to endpoints (seL4_Send to wait for an event and seL4_NBSend to poll for events). If we allow send queues of endpoints to include notification objects in addition to threads we could multiplex notifications via an endpoint by binding the notifications to the endpoint. This could also allow for the removal of notification binding for threads; if they want to receive both notifications and synchronous IPC they can bind the notification to the endpoint. This design should also work with MCS whereby donation of scheduling contexts from notification objects would become roughly the same as donation from a thread with a scheduling context. I think the cleanest implementation would be to allow a notification to contain its own endpoint capability, similar to the manner in which TCBs conatain capabilities. Any time an idle notification is invoked with a send it then queues on the endpoint to which is capability refers if one exists. Send invocations of 'active' (potentially queued) notifications would perform the same XOR operation as currently occurs. When receiving on an endpoint where the first blocked object is a notification the badge received is the badge of the endpoint capability owned by the notification and the notification word is simply placed in the first message register. Whilst I think that this (or something similar) is the most simple case for implementing multiplexing it would have some impact on the semantics and implementation of some objects. Even at this small a scale the verification burden will still be considerable as this change would impact all verified builds. I think further discussion and evaluation of a solution is needed before we can determine that it is sufficiently beneficial to have this feature in the kernel and to commit to maintaining the feature and including it in the verified configurations. Cheers, Curtis Millar

2 1

Request for enhancement: Notification queues
by Demi M. Obenour 24 Jan '20

24 Jan '20

While studying seL4, I noticed that there is no mechanism to wait for one of many notifications. This proposal solves this with a new type of capability, which I call a notification queue. I don’t have the knowledge to determine how they should be implemented, so instead I will describe the general idea. A notification queue is a capability to which notification objects can be attached. When an attached endpoint is notified, a user-provided pointer is pushed onto the queue. Notification queues are edge-triggered, so subsequent notifications do not cause further entries to be added to the queue unless the notification has been read. The queue is implemented as a buffer which is read-only to userspace, but read-write to seL4. When creating a notification queue, userspace must provide sufficient untyped memory to ensure that the queue will not fill up. This ensures that sending a notification cannot fail due to resource exhaustion. Queues can be resized by the application if needed. Attempts to add too many endpoints to a queue results in an error being returned. A notification object can only be attached to one notification queue at a time. It can be detached from a queue and later attached to another. Notification queues can be used whenever a notification object is expected, except that they cannot be badged. Badging a notification queue would make no sense. When polled, a notification queue returns the number of events that have been added to it since it was last polled. Adding one notification queue to another may or may not be allowed. Allowing it would increase flexibility, but also increase implementation complexity. It is also possible to attach a TCB to a queue; the queue is notified when the TCB exits. Only seL4 can send to a notification queue. No userspace process can ever possess a send capability to such a queue. While a notification queue can be accessed from any number of tasks, performance on multi-core systems may be improved if each queue is used from the same core that its attached notifications are used on. Constructive feedback on this proposal is welcome. Sincerely, Demi

3 8

seL4 on unverified ARM platforms
by Demi M. Obenour 23 Jan '20

23 Jan '20

My understanding is that seL4 is currently only verified for one particular ARM platform. Is it considered production-ready on other ARM boards? Sincerely, Demi

2 3

Re: [seL4] Request for enhancement: Notification queues
by Heiser, Gernot (Data61, Kensington NSW) 23 Jan '20

23 Jan '20

On 22 Jan 2020, at 14:44, Demi Obenour <demiobenour(a)gmail.com<mailto:demiobenour@gmail.com>> wrote: But everything needs a really convincing argument, that’s based on a functional limitation that prevents implementation of certain important classes of systems. If it’s only a performance argument, we’ll need to be convinced that it really is a performance bottleneck in realistic systems. Do you believe it is likely to be? I haven’t seen a convincing use case where it is. Gernot

1 0

Plans for verification of IOMMU support on x86? Binary verification?
by Demi M. Obenour 21 Jan '20

21 Jan '20

Are there plans to verify the IOMMU support on x86? x86 without DMA is not very useful, so IOMMU support is needed for the proofs to apply in practice. Sincerely, Demi

2 1

Initializing of the sel4 tutorials fails because of missing the CMakeLists.txt
by Florian Berenbrinker 16 Jan '20

16 Jan '20

2 3

Re: [seL4] Suggestion for Abdurahman
by Harry Butterworth 12 Jan '20

12 Jan '20

Take a look at Andy’s Binary Editor nyangau.org/be/be.html and implement an open source equivalent as an integrated debugger for seL4. You will need to be able to get keyboard input, write characters to the screen and get access to files containing the structure definitions. You can provide the structure definitions at boot time. You won’t need an OS or POSIX or even much of a standard library; the implementation just requires the language runtime, a parser, a few data structures, and a bit of printf-like code. You could write it all and make it completely self-contained which would allow you to keep the footprint really small. Steps to proceed are as follows: 1) Pick a language. I’d probably pick C++ for this but you might also consider D or Rust or maybe COGENT. 2) Work out how to write a small test program in your chosen language and get seL4 to run it. This will require an implementation of the runtime for the language. If this hasn’t been done already for the language you pick, you can implement bits of the runtime as you go along when they are needed. If you fail at this step, go back to step 1, pick a different language. 3) Work out how to get your test program to write characters to the screen (or serial console perhaps). 4) Work out how to get keyboard input. 5) Define the grammar for the structure definitions. If you happen to pick COGENT you might look at DARGENT. 6) Understand the Model View Controller design pattern. 7) Write a parser to parse the structure definitions to create a model. You’ll want the model to use lazy evaluation so the whole system defined by the structure definitions can be represented but there is only overhead for the bits that are being actively browsed. 8) Implement a view for the model which displays a selected part on the console. 9) Implement a controller for the view and model which is an event loop that handles keyboard input and manipulates the model and view accordingly. After getting your new debugger to work for browsing the entire system including the kernel data structures, find a way to integrate it which allows it to be configured to run with only the capability it needs for the debugging you want to do. After that you could make sure it can be used for debugging real time applications with a guarantee not to interfere with their real time operation. For bonus points, if you have picked COGENT, you might finish off with a formal proof that your debugger displays the correct characters on the console according to the structure definitions, contents of memory and history of keyboard input. This (in fact the whole task) would be complicated by the fact that the memory contents change all the time underneath you as you browse a live system so you’d have to work out how to incorporate that and still prove something useful. Enjoy On Fri, Jan 10, 2020 at 8:21 PM abdi mahmud haji < abdimahmudhaji227(a)gmail.com> wrote: > hey guys > I'm abdurahman and i have same question for you > i have been studying microkernel for a little well now specially seL4 and > i have done almost every tutorials in sel4 -tutorials and i have a crazy > idea ,that is i when try to build a 'shell or prompt' on the seL4 > mircokernel but i don't have any idea how to do or where to start . does > any one have a suggestion for me > > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel >

1 1

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

11 Jan '20

hey guys I'm abdurahman and i have same question for you i have been studying microkernel for a little well now specially seL4 and i have done almost every tutorials in sel4 -tutorials and i have a crazy idea ,that is i when try to build a 'shell or prompt' on the seL4 mircokernel but i don't have any idea how to do or where to start . does any one have a suggestion for me

4 3

Using seL4_DebugSnapshot()
by rasd＠riseup.net 09 Jan '20

09 Jan '20

Can someone provide more information about using seL4_DebugSnapshot? >From its description in documentation, I would expect it to print out a CapDL struct over a debugging port/console. Instead, it waits for user commands for various data types sends back binary data[0]. Since the commands are all 0xa0-0xff[1], it doesn't seem like DebugSnapshot expects a human and a keyboard to be present on the other end. Is there some internal debugging tool that is supposed to be used with this system call? Is DebugSnapshot still used? Any advice or information is appreciated. ras [0] https://github.com/seL4/seL4/blob/master/src/arch/arm/32/machine/capdl.c [1] https://github.com/seL4/seL4/blob/master/include/machine/capdl.h

2 1

答复: some question about the compile of global-components in camkes_arm_vm project
by yadong.li 09 Jan '20

09 Jan '20

I found some example in odroid_vm, I want to make sure my understanding is correct? In CMakeLists.txt DeclareCAmkESComponent(HelloWorld) is just tell me there is a component called “HelloWorld” If you want this component to be compiled to project You must add call in your assembly in .cmakes file like below: assembly { composition { component HelloWorld hello; } Thank you very much 发件人: yadong.li 发送时间: 2019年12月28日 15:32 收件人: 'devel(a)sel4.systems' 主题: some question about the compile of global-components in camkes_arm_vm project hi， I have some question about the compile of global-components in camkes_arm_vm project. 1、In projects/global-components/components, there are some directory include FileServer, SerialServer, TimeServer and the others. I found FileServer had been compiled to project， but the other directory have not been compiled Is there some on-off switch control the compile ？ But I did not find it. 2、The CAmkES of FileServer component did not have a "int run(void) {}, If I want to add an new component with run entry， but it is not rootserver（I think one project only have one rootserver），it run with vm rootserver parallelly？ what should I do ？ Is there some example. Thank you very much

2 1

Error while building in docker
by Edward Sandberg 09 Jan '20

09 Jan '20

This morning I saw this error when building sel4: /bin/sh: 1: PROTOBUF_PROTOC_EXECUTABLE-NOTFOUND: not found I noticed a warning when starting the docker container about trustworthysystems/camkes:latest being over 30 days old. I thought that using an up to date pull of: https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles.git would keep the build env up to date but that apparently is either not the case or there is a problem with the repo. I ran: docker pull trustworthysystems/camkes and the warning was resolved and I could build seL4. Is pulling that docker image supposed to be necessary? Thanks! -- Edward Sandberg Adventium Labs 111 3rd Avenue S. Suite #100 Minneapolis, MN 55401 ed.sandberg(a)adventiumlabs.com

2 1

fastpath performance test
by Dd Nirvana 05 Jan '20

05 Jan '20

Hi guys, I have downloaded the lastest seL4 repo and built the seL4 kernel. And I reuse the code in sel4test/projects/sel4test/apps/sel4test-tests/src/tests/ipc.c. To test the fast, I made minor modifications: first, set caller and callee to the same priority; second, caller uses seL4_Call while callee uses seL4_ReplyRecv. However, the fastpath takes more than 2000 cycles (a round trip). Build: use the lastest provided docker and ../init-build.sh - DPLATFORM=x86_64 -DCMAKE_BUILD_TYPE=Release Both hardware and Qemu show similar results. (4.0GHz skylake CPU) BTW. The manifest is the same as https://sel4.systems/About/Performance/home.pml (i.e., bf13e9f673484825a60f9950cf688ff33ac841ad). Any advices about the issue? Best, Jinyu Gu, Institute of Parallel and Distributed Systems (IPADS), School of Software, Shanghai Jiao Tong University

2 1

Understand seL4 x86_64 Kernel ABI calling convention
by Alexandre Mutel 03 Jan '20

03 Jan '20

Hello! While looking at the code base and checking generated code, I'm not sure about the pertinence of having a different ABI from user System V ABI for kernel calls, as it is implying a bit more unnecessary register shuffling, and I was wondering why this choice was made to have r10, r8, r9, r15? instead of keeping System V ABI and just replace rcx by r10 as it is discarded by syscall: SystemVABI_x86_64_user: rdi, rsi, rdx, rcx, r8, r9 SystemVABI_x86_64_Linux_kernel: rdi, rsi, rdx, r10, r8, r9 SystemVABI_x86_64_seL4: rdi, rsi, r10, r8, r9, r15 So on a Linux Kernel, only the register rcx will be transferred to r10 (when transitioning from user to syscall), but in seL4, it has to reshuffle arguments rdx to r9. (Note for context: I'm working on a project where I don't use a standard C compiler to interface with the seL4 Kernel API, and where the register allocator of the compiler might not be as efficient as GCC/CLang after everything is inlined, that's why I'm looking into these details)

1 1

Hardware-aided Trusted Computing devroom at FOSDEM
by Vasily A. Sartakov 01 Jan '20

01 Jan '20

Hello I would like to invite your to participate in a new devroom: Hardware-aided Trusted Computing. The devroom is devoted to open source projects on top of modern TEEs like Intel SGX, AMD SEV/SVE, Arm TrustZone. You can find the schedule here: https://fosdem.org/2020/schedule/track/hardware_aided_trusted_computing/ I hope this will be interesting for the community. See you at FOSDEM. -- Dr.-Eng. V. A. Sartakov

2 1

some question about the compile of global-components in camkes_arm_vm project
by yadong.li 28 Dec '19

28 Dec '19

hi， I have some question about the compile of global-components in camkes_arm_vm project. 1、In projects/global-components/components, there are some directory include FileServer, SerialServer, TimeServer and the others. I found FileServer had been compiled to project， but the other directory have not been compiled Is there some on-off switch control the compile ？ But I did not find it. 2、The CAmkES of FileServer component did not have a "int run(void) {}, If I want to add an new component with run entry， but it is not rootserver（I think one project only have one rootserver），it run with vm rootserver parallelly？ what should I do ？ Is there some example. Thank you very much

1 0

Camkes Project on Sabre Lite i.mx6 board
by Parvaneh Ahgajani 19 Dec '19

19 Dec '19

Hello all, I am trying to have my own seL4 demo on Sabre Lite board. I am using this command to create the image file: ../init-build.sh -DPLATFORM=sabre -DCROSS_COMPILER_PREFIX=arm-linux-gnueabi- -DCAMKES_APP=adder After that I run this commands to boot the image: fatload mmc 1 0x41000000 adder(image file) The bootm command gives this error: Wrong Image Format for bootm command ERROR: can't get kernel image! I tried bootelf but it stuck and does not show the correct answer: bootelf 0x41000000 CACHE: Misaligned operation at range [10598000, 105980a4] CACHE: Misaligned operation at range [10599000, 105a3434] CACHE: Misaligned operation at range [105a3434, 105a3c23] CACHE: Misaligned operation at range [107fc000, 1080a038] ## Starting application at 0x10598000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10 paddr=[10598000..1080a037] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 1069c064. Loaded DTB from 1069c064. paddr=[10038000..10042fff] ELF-loading image 'kernel' paddr=[10000000..10037fff] vaddr=[e0000000..e0037fff] virt_entry=e0000000 ELF-loading image 'capdl-loader' paddr=[10043000..1019bfff] vaddr=[10000..168fff] virt_entry=188dc ELF loader relocated, continuing boot... Enabling MMU and paging It seems It does not go to kernel-image entry point and bootstrap the kernel! Is there any thing that I need to perform on board? Thank you, Parvaneh Aghajani.

2 1

Blog on seL4 licensing
by Heiser, Gernot (Data61, Kensington NSW) 10 Dec '19

10 Dec '19

The question of what the seL4 license actually means, in particular, to which degree it may force deployer’s IP to be open-sourced (*), has come up repeatedly, and from informal discussions I realised that misconceptions abound. I tried to clear up such confusion in a blog that I just posted: https://microkerneldude.wordpress.com/2019/12/09/what-does-sel4s-license-im… Enjoy, Gernot (*) short answer: normally not at all!

1 0

try to add vm in zynqmp, but when run rootserve crash.
by yadong.li 03 Dec '19

03 Dec '19

hi： I try add vm in zynqmp, but when run rootserve crash. print See appendix for the log Function call stack create_objects for (int ut_index = 0; ut_index < spec->num_untyped; ut_index++) { .... CDL_Object *obj = &spec->objects[obj_id]; CDL_ObjectType capdl_obj_type = CDL_Obj_Type(obj); ----case crash } I fount when it access 0x440010 (the 42th of capdl_spec.objs, 0~41 objs access is OK) which is (CDL_Object)obj->type will case the crash, but I access the 42th obj->name ("frame_vm0_group_bin_0132" can be printed) is OK. [42] = { #ifdef CONFIG_DEBUG_BUILD .name = "frame_vm0_group_bin_0132", #endif .type = CDL_Frame, .size_bits = 21, .frame_extra = { .paddr = 0, }, }, what may be the problem ? mmu? Thank you very much. log: ## Starting application at 0x02793000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[2793000..481106f] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 2878d08. Loaded DTB from 2878d08. paddr=[239000..23afff] ELF-loading image 'kernel' paddr=[0..238fff] vaddr=[ff8000000000..ff8000238fff] virt_entry=ff8000000000 ELF-loading image 'capdl-loader' paddr=[23b000..2393fff] vaddr=[400000..2558fff] virt_entry=408af8 ELF loader relocated, continuing boot... Enabling hypervisor MMU and paging Jumping to kernel-image entry point... Warning: gpt_cntfrq 33333000, expected 100000000 Bootstrapping kernel Booting all finished, dropped to user space Caught cap fault in send phase at address (nil) while trying to handle: vm fault on data at address 0x440010 with status 0x93800007 in thread 0xff887f81b400 "rootserver" at address 0x4026e4 With stack: 0x2553d50: 0x424a9a 0x2553d58: 0x43ffb8 0x2553d60: 0x2553de0 0x2553d68: 0x408a4c 0x2553d70: 0x255a000 0x2553d78: 0x453588 0x2553d80: 0x0 0x2553d88: 0x25 0x2553d90: 0x900000000 0x2553d98: 0x100000000000009 0x2553da0: 0x800000000 0x2553da8: 0x43ffb8 0x2553db0: 0x2186 0x2553db8: 0x21dd 0x2553dc0: 0x2a 0x2553dc8: 0x408a40

1 0

Userspace debugging with QEMU/gdb
by Jiusheng Liu 02 Dec '19

02 Dec '19

Hi, >From the page https://docs.sel4.systems/DebuggingGuide.html (section Userspace debugging), I know we can debug userspace process by command below: ---------------------------- cmd example start ---------------------------------------- gdb ./dynamic-2 Reading symbols from ./dynamic-2...done. (gdb) target remote :1234 Remote debugging using :1234 0x000000000000fff0 in ?? () (gdb) break main Breakpoint 1 at 0x402011: file sel4-tutorials-manifest/dynamic-2/main.c, line 161. (gdb) c Continuing. Breakpoint 1, main () at sel4-tutorials-manifest/dynamic-2/main.c:161 161 (gdb) ---------------------------- cmd example end ---------------------------------------- It works for normal userspace process (such as the example code in tutorials: https://docs.sel4.systems/Tutorials/dynamic-2.html ). But when I want to debug the userspace process for the code in the tutorials page https://docs.sel4.systems/Tutorials/camkes-vm-linux.html (one virtual machine in seL4), I cannot catch the breakpoints. So can you help me to explain why I cannot catch the breakpoint? and can we debug the vmm create process with qemu/gdb? Thanks.

2 2

Re: [seL4] Devel Digest, Vol 66, Issue 26
by Millar, Curtis (Data61, Kensington NSW) 26 Nov '19

26 Nov '19

> As I'm playing with a prototype language and OS while building it on > top of seL4, > I'm not using any intermediate C layers to connect to the seL4 API (so > custom build and > integration and no C runtime), while most of the samples out there are > heavily relying on > some foundations, which is completely understandable, considering how > it can be involving > to build anything relevant on top of the seL4 API. > So as I'm just really getting started to integrate with seL4 (and > I love?? it!) I have to go through > all these details, but I hope that I won't be spamming unnecessarily > here! ? If you are looking to avoid any C interop or runtime that should be completely possible. The only requirement the kernel makes is that user- level code needs to keep track of the IPC buffer address on its own (unlike previous versions which ensure that a particular register contains the IPC buffer address). If you want a minimal runtime without TLS you could store the IPC buffer address in a global variable and ensure that your system call wrappers use that global variable to load and store data into the IPC buffer.

1 0

Re: [seL4] Understand how TLS is setup in the root server for x64
by Millar, Curtis (Data61, Kensington NSW) 26 Nov '19

26 Nov '19

Hi Alexandre, > I'm trying to understand how the TLS is setup for the root server on > x64 (to access for example the IPC buffer) > but I'm failing to connect the pieces and how the server is correctly > setting the FS register. There is detailed documentation for the TLS change on the page for RFC- 3. https://sel4.atlassian.net/browse/RFC-3 In essence, the new TLS model stores the address of the IPC buffer in a thread-local variable which must be initialised by your process or threading runtime along with general TLS intialisation. https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/functions.h#L… To assist with this there is a simple sel4runtime library which provides a minimal C-runtime and tools for initialising TLS. https://github.com/SEL4PROJ/sel4runtime On x86_64 the TLS register can be set without calling into the kernel by using the `wrfsbase` instruction or by using the `sel4runtime_set_tls_base` function from the sel4runtime library. > Now, I'm failing to find in the codebase where the ELF loader is > actually detecting the TLS segment and the according setup with the > TLS register. The ELF loader is not responsible for TLS initialisation, the C-runtime is responsible for configuring TLS of the initial thread. https://bitbucket.ts.data61.csiro.au/projects/SEL4PROJ/repos/sel4runtime/br… > Never mind, I discovered that I in order to access a TLS variable you > need to call `seL4_TCB_SetTLSBase` on seL4_CapInitThreadTCB first in > the root server, as I'm trying to work on a bare bone usage of seL4 to > better understand it, this part was not obvious from the existing more > complex samples! In general I would recommend having the initial thread in a process initialise its own TLS via the runtime and any new thread configure its own TLS in the initialisation code before the main function call of that thread with the `sel4runtime_set_tls_base`. Each new thread will also need to use `seL4_SetIPCBuffer` to initialise the IPC buffer address in its TLS before performing any invocations or any other system calls. Cheers, Curtis Millar Systems Engineer, Trustworthy Systems, CSIRO's Data61 curtis.millar(a)data61.csiro.au Data61, CSIRO Level 3, K17 Building UNSW Gate 14, Barker St Kensington NSW 2033 Australia

2 1

Is there a "modern" seL4 manifest/configuration that is known to run on CMA34CR?
by Nogin, Aleksey 24 Nov '19

24 Nov '19

Unless I am looking in the wrong place, all the CMA34CR support was removed in https://github.com/seL4/camkes-vm/commit/aab3478acc4705a3161f5bf59625f7c96a…. Is there something that remains? If not, what would be the best starting point to try to port a demo running on CMA34CR board from an old (early 2017) version of the sel4/camkes/etc to a recent stable release (e.g, 10.1.1)? Thanks. Aleksey CONFIDENTIALITY NOTICE: The information transmitted in this email, including attachments, is intended only for the person(s) or entity to which it is addressed and may contain confidential, proprietary and/or privileged material exempt from disclosure under applicable law. Any review, retransmission, dissemination or other use of, or taking of any action in reliance upon this information by persons or entities other than the intended recipient is prohibited. If you received this message in error, please contact the sender immediately and destroy any copies of this information in their entirety.

2 4

Understand how TLS is setup in the root server for x64
by Alexandre Mutel 24 Nov '19

24 Nov '19

Hello! I'm trying to understand how the TLS is setup for the root server on x64 (to access for example the IPC buffer) but I'm failing to connect the pieces and how the server is correctly setting the FS register. For example the sel4_Send function is codegen like this (using -ftls-model=local-exec) Function: seL4_Send push r15 mov rdx,0FFFFFFFFFFFFFFFDh push rbx mov rax,[fs:0] mov r10,[rax+8] mov r8,[rax+10h] mov r9,[rax+18h] mov r15,[rax+20h] mov rbx,rsp syscall mov rsp,rbx pop rbx pop r15 ret The instruction `mov rax,[fs:0]` is accessing the seL4_IPCBuffer* and the the executable has a TLS segments of 8 bytes for the pointer. all good. Now, I'm failing to find in the codebase where the ELF loader is actually detecting the TLS segment and the according setup with the TLS register. And I'm wondering if the setup for the codegen is not wrong on my side (e.g the local-exec is not working), so that instead of having a FS register it would be a direct memory access. Does anyone have a clue about this? Thank you!

1 2

Fwd: port sel4 to RK3308(quad cortex-a35)
by Yun Zhou 22 Nov '19

22 Nov '19

---------- Forwarded message --------- 发件人： Yun Zhou <shiny725829(a)gmail.com> Date: 2019年10月25日周五下午9:52 Subject: port sel4 to RK3308(quad cortex-a35) To: <devel-owner(a)sel4.systems> Dear sel4 Experts How are you I found some information about sel4, and sel4 is great microkernel OS, i want port sel4 to RK3308(quad cortex-a35, GICv2) for real time audio signal processing. Form the Tutorials I found sel4 just support cortex-a53, I would like to ask does sel4 support cortex-a35 SMP mode. and because our application is real time audio processing so system delay must lower than 3ms and hard real-time determinism. Will sel4 support real-time signal processing? Looking forward to your reply Thanks &Kind regards Yun

2 1

Nasty bug in global-components/templates/rpc-signalling.template.c
by Nogin, Aleksey 22 Nov '19

22 Nov '19

After spending a few hours debugging time server not working for me, I realized that global-components/templates/rpc-signalling.template.c that was added earlier this year contains the following /*- set badge = str(configuration[c.instance.name].get("%s_attributes" % c.interface.name)).strip('"') -*/ [...] /*- do badges.sort() -*/ [...] int /*? me.interface.name ?*/_largest_badge(void) { return /*? badges[len(badges) - 1] ?*/; } Unfortunately for me, my Trusted Build generated camkes had the attributes numbered 1,2,3,10,11,12,13 and therefore the above core was claiming that the time_server_largest_badge is 3 :(. Obviously, the issue is the combination of the str and sort, resulting in the last badge being the one largest lexicographically, not numerically :(. Replacing the str with int (and correspondingly removing the strip) solved the problem for me. P.S. Well, solved that particular problem for me, not the problem of time server not working - looks like now I will have to debug FAULT HANDLER: data fault from time_server.time_server_0_control (ID 0x2) on address 0x84b8ba, pc = 0x42439d, fsr = 0x4 FAULT HANDLER: Register dump: FAULT HANDLER: rip :0x42439d FAULT HANDLER: rsp :0x454cf0 FAULT HANDLER: rflags :0x10202 FAULT HANDLER: rax :0x413a33 FAULT HANDLER: rbx :0x437e88 FAULT HANDLER: rcx :0x0 FAULT HANDLER: rdx :0x437e98 FAULT HANDLER: rsi :0x28 FAULT HANDLER: rdi :0x437e98 FAULT HANDLER: rbp :0x454d70 FAULT HANDLER: r8 :0xffffffff FAULT HANDLER: r9 :0x0 FAULT HANDLER: r10 :0xe8 FAULT HANDLER: r11 :0x293 FAULT HANDLER: r12 :0x413a32 FAULT HANDLER: r13 :0x84b8ba FAULT HANDLER: r14 :0x0 FAULT HANDLER: r15 :0x0 FAULT HANDLER: fs_base :0x44a460 FAULT HANDLER: gs_base :0x0 FAULT HANDLER: memory map: FAULT HANDLER: +-- 0x0000000000458fff -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x0000000000458000 -- FAULT HANDLER: | IPC buffer FAULT HANDLER: +-- 0x0000000000457000 -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x0000000000456000 -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x0000000000455000 -- FAULT HANDLER: | stack FAULT HANDLER: +-- 0x0000000000451000 -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x0000000000450000 -- FAULT HANDLER: | code and data FAULT HANDLER: +-- 0x0000000000400000 - :( Aleksey CONFIDENTIALITY NOTICE: The information transmitted in this email, including attachments, is intended only for the person(s) or entity to which it is addressed and may contain confidential, proprietary and/or privileged material exempt from disclosure under applicable law. Any review, retransmission, dissemination or other use of, or taking of any action in reliance upon this information by persons or entities other than the intended recipient is prohibited. If you received this message in error, please contact the sender immediately and destroy any copies of this information in their entirety.

2 1

(no subject)
by abdi mahmud haji 22 Nov '19

22 Nov '19

I was trying to build camkes-vm-crossvm tutorials by using "./init --tut camkes-vm-crossvm" and it initiate some folder with some file and some folder is empty and some are missing.So can someone help me how to fix it,and this the following is it output. ============================================== ./init --tut camkes-vm-crossvm loading initial cache file ../settings.cmake -- The C compiler identification is GNU 5.4.0 -- Check for working C compiler: /usr/bin/gcc -- Check for working C compiler: /usr/bin/gcc -- works -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- The CXX compiler identification is GNU 5.4.0 -- Check for working CXX compiler: /usr/bin/g++ -- Check for working CXX compiler: /usr/bin/g++ -- works -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Detecting CXX compile features -- Detecting CXX compile features - done -- The ASM compiler identification is GNU -- Found assembler: /usr/bin/gcc -- Found musllibc: /home/sel4/sel4-tutorials-manifest/projects/musllibc -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- CPIO test cpio_reproducible_flag FAILED -- /home/sel4/sel4-tutorials-manifest/camkes-vm-crossvm_build/camkes-vm-crossvm/ast.pickle is out of date. Regenerating... ERROR:CAmkES:/home/sel4/sel4-tutorials-manifest/camkes-vm-crossvm/crossvm_tutorial.camkes:27:1: } ERROR:CAmkES: ^ ERROR:CAmkES:Syntax error in input at '}' (type _ANON_1) line 34 col 1 CMake Error at tools/camkes/camkes.cmake:494 (message): Failed to generate /home/sel4/sel4-tutorials-manifest/camkes-vm-crossvm_build/camkes-vm-crossvm/ast.pickle Call Stack (most recent call first): camkes-vm-crossvm/CMakeLists.txt:37 (GenerateCAmkESRootserver) -- Configuring incomplete, errors occurred! See also "/home/sel4/sel4-tutorials-manifest/camkes-vm-crossvm_build/CMakeFiles/CMakeOutput.log". Traceback (most recent call last): File "./init", line 96, in <module> File "./init", line 85, in main File "/home/sel4/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 107, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/home/sel4/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 75, in _init_build_directory return sh.cmake(args + ['..'], _cwd=directory, _out=output, _err=output) File "/home/sel4/.local/lib/python3.5/site-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/home/sel4/.local/lib/python3.5/site-packages/sh.py", line 774, in __init__ self.wait() File "/home/sel4/.local/lib/python3.5/site-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/home/sel4/.local/lib/python3.5/site-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /usr/local/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DFORCE_IOMMU=ON -DTUTORIAL_DIR=camkes-vm-crossvm -C ../settings.cmake .. STDOUT: STDERR: =============================================

2 1

compile camkes_arm_vm project(tx1 vm_minimal), The file format is not correct
by yadong.li 22 Nov '19

22 Nov '19

Hi I compile camkes_arm_vm with tx1 vm_minimal Command: ../init-build.sh -DAARCH64=TRUE -DCAMKES_VM_APP=vm_minimal -DPLATFORM=tx1 Buf output file is not elf # aarch64-linux-gnu-objcopy -O binary images/capdl-loader-image-arm-tx1 sel4-vmm-minimal aarch64-linux-gnu-objcopy:images/capdl-loader-image-arm-tx1: File format not recognized see appendix for the log Thank you very much Log: 1、配置环境 #<mailto:root@HP-Z240:/home/yadong.li/seL4/camkes_arm_vm/build_temp> ../init-build.sh -DAARCH64=TRUE -DCAMKES_VM_APP=vm_minimal -DPLATFORM=tx1 loading initial cache file /home/yadong.li/seL4/camkes_arm_vm/projects/vm/settings.cmake correct_platform_strings: Based on toolchain, setting KernelSel4Arch: aarch64 -- Found seL4: /home/yadong.li/seL4/camkes_arm_vm/kernel …………. -- Found camkes-arm-vm: /home/yadong.li/seL4/camkes_arm_vm/projects/vm -- Found camkes-tool: /home/yadong.li/seL4/camkes_arm_vm/projects/camkes-tool -- Found global-components: /home/yadong.li/seL4/camkes_arm_vm/projects/global-components -- Found camkes-vm: /home/yadong.li/seL4/camkes_arm_vm/projects/camkes-vm -- Found camkes-vm-images: /home/yadong.li/seL4/camkes_arm_vm/projects/camkes-vm-images -- Found sel4_projects_libs: /home/yadong.li/seL4/camkes_arm_vm/projects/seL4_projects_libs -- Found elfloader-tool: /home/yadong.li/seL4/camkes_arm_vm/tools/seL4/elfloader-tool -- Found musllibc: /home/yadong.li/seL4/camkes_arm_vm/projects/musllibc -- Found util_libs: /home/yadong.li/seL4/camkes_arm_vm/projects/util_libs -- Found seL4_libs: /home/yadong.li/seL4/camkes_arm_vm/projects/seL4_libs -- Found projects_libs: /home/yadong.li/seL4/camkes_arm_vm/projects/projects_libs -- Found capdl: /home/yadong.li/seL4/camkes_arm_vm/projects/capdl -- /home/yadong.li/seL4/camkes_arm_vm/build_temp/kernel/gen_headers/plat/machine/devices_gen.h is out of date. Regenerating... -- CPIO test cpio_reproducible_flag PASSED -- Found sel4runtime: /home/yadong.li/seL4/camkes_arm_vm/projects/sel4runtime -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- /home/yadong.li/seL4/camkes_arm_vm/build_temp/ast.pickle is out of date. Regenerating... -- /home/yadong.li/seL4/camkes_arm_vm/build_temp/camkes-gen.cmake is out of date. Regenerating... -- Configuring done -- Generating done -- Build files have been written to: /home/yadong.li/seL4/camkes_arm_vm/build_temp 2、编译 #<mailto:root@HP-Z240:/home/yadong.li/seL4/camkes_arm_vm/build_temp> ninja [41/320] Performing CAmkES generation for 15 files [58/320] Generating capDL-tool/parse-capDL stack build --fast Building all executables for `capDL-tool' once. After a successful build of all of them, only specified executables will be rebuilt. capDL-tool-1.0.0.1: configure (exe) Configuring capDL-tool-1.0.0.1... capDL-tool-1.0.0.1: build (exe) Preprocessing executable 'parse-capDL' for capDL-tool-1.0.0.1... [ 1 of 16] Compiling CapDL.Model ( CapDL/Model.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/Model.o ) [ 2 of 16] Compiling CapDL.State ( CapDL/State.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/State.o ) [ 3 of 16] Compiling CapDL.PrintUtils ( CapDL/PrintUtils.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintUtils.o ) [ 4 of 16] Compiling CapDL.PrintC ( CapDL/PrintC.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintC.o ) [ 5 of 16] Compiling CapDL.PrintDot ( CapDL/PrintDot.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintDot.o ) [ 6 of 16] Compiling CapDL.PrintIsabelle ( CapDL/PrintIsabelle.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintIsabelle.o ) [ 7 of 16] Compiling CapDL.PrintModel ( CapDL/PrintModel.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintModel.o ) [ 8 of 16] Compiling CapDL.PrintXml ( CapDL/PrintXml.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintXml.o ) [ 9 of 16] Compiling CapDL.Matrix ( CapDL/Matrix.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/Matrix.o ) [10 of 16] Compiling CapDL.STCC ( CapDL/STCC.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/STCC.o ) [11 of 16] Compiling CapDL.AST ( CapDL/AST.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/AST.o ) [12 of 16] Compiling CapDL.MakeModel ( CapDL/MakeModel.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/MakeModel.o ) [13 of 16] Compiling CapDL.ParserUtils ( CapDL/ParserUtils.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/ParserUtils.o ) [14 of 16] Compiling CapDL.DumpParser ( CapDL/DumpParser.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/DumpParser.o ) [15 of 16] Compiling CapDL.Parser ( CapDL/Parser.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/Parser.o ) [16 of 16] Compiling Main ( Main.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/Main.o ) Linking .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL ... capDL-tool-1.0.0.1: copy/register Installing executable(s) in /home/yadong.li/seL4/camkes_arm_vm/build_temp/capDL-tool/.stack-work/install/x86_64-linux/lts-9.21/8.0.2/bin stack install Copying from /home/yadong.li/seL4/camkes_arm_vm/build_temp/capDL-tool/.stack-work/install/x86_64-linux/lts-9.21/8.0.2/bin/parse-capDL to /home/yadong.li/seL4/camkes_arm_vm/build_temp/capDL-tool/parse-capDL Copied executables to /home/yadong.li/seL4/camkes_arm_vm/build_temp/capDL-tool: - parse-capDL Warning: Installation path /home/yadong.li/seL4/camkes_arm_vm/build_temp/capDL-tool not found on the PATH environment variable. [68/320] Building C object CMakeFiles/vm0.instance.bin.dir/components/VM/src/main.c.obj ………………….. musllibc/build-temp/stage/include/inttypes.h:133:27: note: format string is defined here #define PRIuPTR __PRIPTR "u" [320/320] Generating images/capdl-loader-image-arm-tx1 #file images/capdl-loader-image-arm-tx1 images/capdl-loader-image-arm-tx1: data #arch64-linux-gnu-objcopy -O binary images/capdl-loader-image-arm-tx1 sel4-vmm-minimal aarch64-linux-gnu-objcopy:images/capdl-loader-image-arm-tx1: File format not recognized

2 1

Camkes and GPIO
by Parvaneh Ahgajani 21 Nov '19

21 Nov '19

Hello all, I am trying to implement a simple demo on sel4 using camkes. I need to add some external hardware like sensors to my demo. For this purpose I need GPIO programming. Could you please point me to some example GPIO components? Should I add hardware component? or just use <platsupport.GPIO.h> to write signal on pins on source files? Thank you for your time and consideration, Parveneh.

2 5

releasing confidentiality
by Michael Neises 15 Nov '19

15 Nov '19

Hi, I know that seL4 provides confidentiality, which is described as a property that "means that data cannot be read without permission." Given this wording, I wonder if it is not possible to revoke those permissions in certain cases. In particular, I would like for one camkes component to be able to perform runtime measurements, such as heap analysis, on another component. Or even better, I would like for a component to be able to perform runtime measurements on a program running within the camkes linux vm. Is such a feat possible? Best, Michael Neises

3 2

Fwd: camkes vm question
by Michael Neises 15 Nov '19

15 Nov '19

Hello, In my system, sel4 is loaded by u-boot from an sd card that contains only an ELF image. I would like to store some sensitive data in plaintext for use in a non-vm component, but I worry that it can be read from the ELF image. Can this sd card data be accessed from within a linux vm instance? Or otherwise, is it certain that the vm cannot access this data? Best, Michael Neises

2 2

TLB issue
by Stefan Kalkowski 15 Nov '19

15 Nov '19

Dear sel4 community, yesterday I've started to develop a low-level platform test to stress several multi-processor aspects on top of the Genode API. Thereby, I've recognized that on sel4/x86_64 the TLB is practically not always cleaned properly in SMP systems. The test spawns threads of one protection domain on each available cpu. Each thread accesses one of the first words of a shared dataspace. Afterwards the main thread on CPU 0 detaches and destroys the dataspace. Unfortunately, the threads on other CPUs still successfully access the corresponding memory instead of triggering a fault. To be able to reproduce the problem, you might investigate the simple test case here: https://github.com/skalk/genode/commit/2d2d7f982555f551227ad5dcbf9df46705d7… My colleague Alexander Boettcher already investigated the problem in part, and might share his insights with you. Best regards Stefan -- Stefan Kalkowski Genode labs https://github.com.skalk | https://genode.org

3 3

Re: [seL4] RISC-V port
by Zhuang, Siwei (Data61, Kensington NSW) 14 Nov '19

14 Nov '19

It looks like either you're using the libarchive in python2 or the package is outdated. Try something like, pip3 install libarchive --upgrade You may need to remove the libarchive from python2, although seL4test requires both python2 and 3. Regards, Siwei On Wed, 2019-11-13 at 20:26 -0800, Jacob Yu wrote: > Thanks, Siwei. > > After I have done a clean build (by removing previous installation in > "/opt/riscv"), I am able to enable "multilib" when building > "riscv-gnu-toolchain" successfully. I also found out that I needed to > build Newlib. > > I can now run " ../init-build.sh -DPLATFORM=spike -DRISCV64=TRUE > -DSIMULATION=1" in the build directory under seL4Test but still failed in > ninja: > > [1/20] Generating gen_headers/image_start_addr.h > FAILED: elfloader/gen_headers/image_start_addr.h > cd /home/webuser/Dev/l4/l4dev/seL4test/cbuild/elfloader && sh -c > "/home/webuser/Dev/l4/l4dev/seL4test/tools/seL4/elfloader-tool/../cmake- > tool/helpers/shoehorn.py > /home/webuser/Dev/l4/l4dev/seL4test/cbuild/kernel/gen_headers/plat/machine/p > latform_gen.yaml > /home/webuser/Dev/l4/l4dev/seL4test/cbuild/elfloader/archive.o > > /home/webuser/Dev/l4/l4dev/seL4test/cbuild/elfloader/gen_headers//image_star > t_addr.h" > Traceback (most recent call last): > File > "/home/webuser/Dev/l4/l4dev/seL4test/tools/seL4/elfloader-tool/../cmake- > tool/helpers/shoehorn.py", > line 81, in <module> > def get_bytes(entry: libarchive.entry.ArchiveEntry) -> io.BytesIO: > AttributeError: module 'libarchive' has no attribute 'entry' > ninja: build stopped: subcommand failed. > > Thank again for all the help. > > Regards, > > > Jacob > > On Tue, Nov 12, 2019 at 4:37 PM Zhuang, Siwei (Data61, Kensington NSW) < > Siwei.Zhuang(a)data61.csiro.au> wrote: > > > Hi Jacob, > > > > Never had this problem before, so just a blind guess. > > > > As you can build "riscv-pk", you must be using the cross compiler from > > your > > previous build(with multilib disabled). Try removing the previous > > installation in "/opt/riscv", and also do "make clean" to remove all the > > previous build directories. > > > > I noticed that the log you attached says "Checking whether the C compiler > > works ... no", have a look at "config.log" to see if there's any useful > > info. > > > > Also make sure you have enough disk space, my build takes 21GB. > > > > Regards, > > Siwei > > > > On Tue, 2019-11-12 at 11:31 -0800, Jacob Yu wrote: > > > Hi > > > > > > I am able to install & build "riscv-pk" and "riscv-isa-sim", and then > > > try > > > out Spike. Many thank! > > > > > > > ./configure --prefix=/opt/riscv --enable-multilib > > > > sudo make linux > > > Otherwise, I also tried to enable "multilib" when building > > > "riscv-gnu-toolchain" but with no luck. It complained: > > > > > > > ... > > > > configure: error: in > > > `/home/webuser/Dev/risc-v/riscv-gnu-toolchain/build-gcc-linux- > > > stage2/riscv64-unknown-linux-gnu/lib32/ilp32/libgomp': > > > > configure: error: C compiler cannot create executables > > > > > > And make failed with: > > > > > > > Makefile:13703: recipe for target 'configure-target-libgomp' failed > > > > make[2]: *** [configure-target-libgomp] Error 1 > > > > > > Again, any suggestions? > > > > > > Regards, > > > > > > > > > Jacob > > > ============================================================ > > > ... > > > checking for riscv64-unknown-linux-gnu-gcc... > > > /home/webuser/Dev/risc-v/riscv-gnu-toolchain/build-gcc-linux- > > > stage2/./gcc/xgcc > > > > > -B/home/webuser/Dev/risc-v/riscv-gnu-toolchain/build-gcc-linux- > > stage2/./gcc/ > > > -B/opt/riscv/riscv64-unknown-linux-gnu/bin/ > > > -B/opt/riscv/riscv64-unknown-linux-gnu/lib/ -isystem > > > /opt/riscv/riscv64-unknown-linux-gnu/include -isystem > > > /opt/riscv/riscv64-unknown-linux-gnu/sys-include -march=rv32imac > > > -mabi=ilp32 > > > > > > > > > > > > *checking whether the C compiler works... noconfigure: error: in > > > `/home/webuser/Dev/risc-v/riscv-gnu-toolchain/build-gcc-linux- > > > stage2/riscv64-unknown-linux-gnu/lib32/ilp32/libgomp':configure: > > > error: C compiler cannot create executablesSee `config.log' for more > > > details* > > > > > > *Makefile:13703: recipe for target 'configure-target-libgomp' > > > failedmake[2]: *** [configure-target-libgomp] Error 1* > > > make[2]: Leaving directory > > > '/home/webuser/Dev/risc-v/riscv-gnu-toolchain/build-gcc-linux-stage2' > > > Makefile:951: recipe for target 'all' failed > > > make[1]: *** [all] Error 2 > > > make[1]: Leaving directory > > > '/home/webuser/Dev/risc-v/riscv-gnu-toolchain/build-gcc-linux-stage2' > > > Makefile:304: recipe for target 'stamps/build-gcc-linux-stage2' failed > > > make: *** [stamps/build-gcc-linux-stage2] Error 2 > > > > > > On Mon, Nov 11, 2019 at 5:52 PM Zhuang, Siwei (Data61, Kensington NSW) < > > > Siwei.Zhuang(a)data61.csiro.au> wrote: > > > > > > > No, building riscv-isa-sim alone is sufficient if you only need Spike. > > > > > > > > seL4 also generates a script called "simulate" in the your build > > > > directory. > > > > The script invokes qemu for simulation. > > > > > > > > Regards, > > > > Siwei > > > > > > > > On Mon, 2019-11-11 at 17:20 -0800, Jacob Yu wrote: > > > > > Thanks, Siwei for the info. I'll give it a try. > > > > > > > > > > > Running seL4 no longer requires RISC-V tools. In case you want to > > use > > > > > Spike, > > > > > > I'd suggest building the riscv-isa-sim separately to get the > > > > > > latest > > > > code. > > > > > Does this require RISC-V tools to build? > > > > > > > > > > Best, > > > > > > > > > > > > > > > Jacob > > > > > > > > > > On Sun, Nov 10, 2019 at 10:58 PM Zhuang, Siwei (Data61, Kensington > > NSW) > > > > > < > > > > > Siwei.Zhuang(a)data61.csiro.au> wrote: > > > > > > > > > > > Hi Jacob, > > > > > > > > > > > > You need to enable multilib when building "riscv-gnu-toolchain". > > > > > > > > > > > > ./configure --prefix=/path-to-install-toolchain > > --enable-multilib > > > > > > then > > > > > > make or make linux > > > > > > > > > > > > Running seL4 no longer requires RISC-V tools. In case you want to > > use > > > > > > Spike, > > > > > > I'd suggest building the riscv-isa-sim separately to get the > > > > > > latest > > > > code. > > > > > > Regards, > > > > > > Siwei > > > > > > > > > > > > On Sun, 2019-11-10 at 15:50 -0800, Jacob Yu wrote: > > > > > > > Hi > > > > > > > > > > > > > > I am trying to build "seL4 tests" for "Spike" platform (the > > RISC-V > > > > > > > simulator from UC Berkeley) on Ubuntu 18.04.3 LTS, a 64-bit > > system. > > > > > > > First of all, I was able to build RISC-V tools with "build.sh" > > after > > > > > > > manually installing "riscv-gnu-toolchain" from GitHub as well as > > > > > > additional > > > > > > > python modules (future, ply, protobuf). I then kicked of > > > > > > "../init-build.sh > > > > > > > -DPLATFORM=spike -DRISCV64=TRUE -DSIMULATION=1" from local build > > > > > > directory. > > > > > > > After that, however, "ninja" command complained about "undefined > > > > > > reference > > > > > > > to `__nedf2'". I understand there is no FPU support in "Spike" > > > > platform > > > > > > so > > > > > > > a need for "soft-float" module. Where should I specify > > "-lsoft-fp"? > > > > > > > Any suggestions? > > > > > > > > > > > > > > Thanks, > > > > > > > > > > > > > > > > > > > > > Jacob > > > > > > > _______________________________________________ > > > > > > > Devel mailing list > > > > > > > Devel(a)sel4.systems > > > > > > > https://sel4.systems/lists/listinfo/devel

2 1

RISC-V port
by Jacob Yu 13 Nov '19

13 Nov '19

Hi I am trying to build "seL4 tests" for "Spike" platform (the RISC-V simulator from UC Berkeley) on Ubuntu 18.04.3 LTS, a 64-bit system. First of all, I was able to build RISC-V tools with "build.sh" after manually installing "riscv-gnu-toolchain" from GitHub as well as additional python modules (future, ply, protobuf). I then kicked of "../init-build.sh -DPLATFORM=spike -DRISCV64=TRUE -DSIMULATION=1" from local build directory. After that, however, "ninja" command complained about "undefined reference to `__nedf2'". I understand there is no FPU support in "Spike" platform so a need for "soft-float" module. Where should I specify "-lsoft-fp"? Any suggestions? Thanks, Jacob

2 5

Re: [seL4] RISC-V port
by Jesse Millwood 12 Nov '19

12 Nov '19

I do believe you can use SiFive's toolchain: https://static.dev.sifive.com/dev-tools/riscv64-unknown-elf-gcc-8.3.0-2019.… Then you don't have to compile it. There is also Data61's Docker https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles If you look at the make file there are some targets for including the RISC-V toolchain. Jesse On 2019-11-11 1:58 a.m., Zhuang, Siwei (Data61, Kensington NSW) wrote: > Hi Jacob, > > You need to enable multilib when building "riscv-gnu-toolchain". > > ./configure --prefix=/path-to-install-toolchain --enable-multilib > then > make or make linux > > Running seL4 no longer requires RISC-V tools. In case you want to use Spike, > I'd suggest building the riscv-isa-sim separately to get the latest code. > > Regards, > Siwei > > On Sun, 2019-11-10 at 15:50 -0800, Jacob Yu wrote: >> Hi >> >> I am trying to build "seL4 tests" for "Spike" platform (the RISC-V >> simulator from UC Berkeley) on Ubuntu 18.04.3 LTS, a 64-bit system. >> >> First of all, I was able to build RISC-V tools with "build.sh" after >> manually installing "riscv-gnu-toolchain" from GitHub as well as additional >> python modules (future, ply, protobuf). I then kicked of "../init-build.sh >> -DPLATFORM=spike -DRISCV64=TRUE -DSIMULATION=1" from local build directory. >> >> After that, however, "ninja" command complained about "undefined reference >> to `__nedf2'". I understand there is no FPU support in "Spike" platform so >> a need for "soft-float" module. Where should I specify "-lsoft-fp"? >> >> Any suggestions? >> >> Thanks, >> >> >> Jacob >> _______________________________________________ >> Devel mailing list >> Devel(a)sel4.systems >> https://sel4.systems/lists/listinfo/devel > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel

1 0

Rust ports on Genode/seL4
by guo minskey 11 Nov '19

11 Nov '19

Hi, guys, I am trying to build genode/sel4 on x86_64 platform and expect to get a GUI working. And so I enable this option in my build.conf : REPOSITORIES += $(GENODE_DIR)/repos/libports. Seems that rust support is broken (because rustc version ??). Which version of rustc should I use to build rust ports on genode ? Or how can I disable rust ports in build.conf configuration or somewhere else ? thanks, -Minskey

3 3

a letter for seeking help about sel4
by 李庚 08 Nov '19

08 Nov '19

Dear Sir or Madam, Very Sorry to brother you. We have get into trouble after compiling sel4 following the https://docs.sel4.systems/Docker.html,may I seek some advice from you? First,I attmpt to follow the https://docs.sel4.systems/Hardware/VMware/,however,error "Failed to allocate object of size xxxx" ara discovered in serial_output.txt . Second,we wanna to make a sel4 startup disk for x86_64,is there any useful Document ? Sorry again for this sudden interruption and I would be very grateful if receive your reply. Yours Sinerely, Andrew

2 1

Building seL4test x86_64 on Debian with the Docker image
by Jacob Yu 05 Nov '19

05 Nov '19

Hi I am building "seL4test" using the Docker image on Ubuntu 18.04.3 LTS, a 64-bit system. After entering "../init-build.sh -DPLATFORM=x86_64 -DSIMULATION=TRUE" in a build directory within Docker it complained "Could NOT find NANOPB (missing: PROTOBUF_PROTOC_EXECUTABLE)". I wonder should I manually download and install protocol buffer compiler, protoc? Please advise. Thank for your help. Jacob =============================================== loading initial cache file /host/projects/sel4test/settings.cmake correct_platform_strings: Attempting to correct PLATFORM: x86_64 to new valid KernelPlatform: pc99 KernelSel4Arch: x86_64 -- Found seL4: /host/kernel -- The C compiler identification is GNU 6.5.0 -- The CXX compiler identification is GNU 6.5.0 -- The ASM compiler identification is GNU -- Found assembler: /usr/bin/gcc -- Check for working C compiler: /usr/bin/gcc -- Check for working C compiler: /usr/bin/gcc -- works -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- Check for working CXX compiler: /usr/bin/g++ -- Check for working CXX compiler: /usr/bin/g++ -- works -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Detecting CXX compile features -- Detecting CXX compile features - done -- Found elfloader-tool: /host/tools/seL4/elfloader-tool -- Found musllibc: /host/projects/musllibc -- Found util_libs: /host/projects/util_libs -- Found seL4_libs: /host/projects/seL4_libs -- Found sel4_projects_libs: /host/projects/sel4_projects_libs -- Found sel4runtime: /host/projects/sel4runtime -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- Found PythonInterp: /usr/bin/python (found version "2.7.15") -- Could NOT find NANOPB (missing: PROTOBUF_PROTOC_EXECUTABLE) -- CPIO test cpio_reproducible_flag PASSED -- Configuring done -- Generating done -- Build files have been written to: /host/build-x86

2 2

Re: [seL4] Devel Digest, Vol 65, Issue 24
by Mcleod, Kent (Data61, Kensington NSW) 05 Nov '19

05 Nov '19

> abdi@abdi-HP-P-PC:~/sel4-tutorials-manifest$ ./init --tut hello-world > loading initial cache file ../settings.cmake > CMake Error: Error: generator : Ninja > Does not match the generator used previously: Unix Makefiles > Either remove the CMakeCache.txt file and CMakeFiles directory or choose a different binary directory. These errors indicate that CMake already believes a project has been created in the target directory and that this project was a Makefile based project. Is there any CMakeCache.txt files located anywhere in the project structure that may be causing CMake to get confused? Otherwise you could reinitialise the tutorial project and try initialising hello-world again and that would also fix your problem.

1 0

Re: [seL4] Devel Digest, Vol 65, Issue 24
by abdi mahmud haji 31 Oct '19

31 Oct '19

i am working on sel4-tutorials for the first time .i setup my machine accordingly and then when i trying to generate the tutorials like this "./init --tut hello-world" i keep getting an error message and dont know what to do or how to fix it . the error was like bellowing =================================================== abdi@abdi-HP-P-PC:~/sel4-tutorials-manifest$ ./init --tut hello-world loading initial cache file ../settings.cmake CMake Error: Error: generator : Ninja Does not match the generator used previously: Unix Makefiles Either remove the CMakeCache.txt file and CMakeFiles directory or choose a different binary directory. Traceback (most recent call last): File "./init", line 96, in <module> File "./init", line 85, in main File "/home/abdi/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 107, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/home/abdi/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 75, in _init_build_directory return sh.cmake(args + ['..'], _cwd=directory, _out=output, _err=output) File "/home/abdi/.local/lib/python3.6/site-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/home/abdi/.local/lib/python3.6/site-packages/sh.py", line 774, in __init__ self.wait() File "/home/abdi/.local/lib/python3.6/site-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/home/abdi/.local/lib/python3.6/site-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /home/abdi/.local/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-world82varrcf -C ../settings.cmake .. STDOUT: STDERR: ====================================================================== is there someone who suggests what i should do please. thanks On Sun, Oct 27, 2019 at 4:00 AM <devel-request(a)sel4.systems> wrote: > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe via the World Wide Web, visit > https://sel4.systems/lists/listinfo/devel > or, via email, send a message with subject or body 'help' to > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > > Today's Topics: > > 1. Re: releasing confidentiality > (Heiser, Gernot (Data61, Kensington NSW)) > 2. Fwd: port sel4 to RK3308(quad cortex-a35) (Yun Zhou) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Sat, 26 Oct 2019 03:07:23 +0000 > From: "Heiser, Gernot (Data61, Kensington NSW)" > <Gernot.Heiser(a)data61.csiro.au> > To: "devel(a)sel4.systems" <devel(a)sel4.systems> > Subject: Re: [seL4] releasing confidentiality > Message-ID: <5FEA58C5-9011-49B7-9790-28B4B54849EF(a)data61.csiro.au> > Content-Type: text/plain; charset="utf-8" > > On 26 Oct 2019, at 08:00, Michael Neises <neisesmichael(a)gmail.com> wrote: > > > > Hi, > > > > I know that seL4 provides confidentiality, which is described as a > property that "means that data cannot be read without permission." Given > this wording, I wonder if it is not possible to revoke those permissions in > certain cases. In particular, I would like for one camkes component to be > able to perform runtime measurements, such as heap analysis, on another > component. Or even better, I would like for a component to be able to > perform runtime measurements on a program running within the camkes linux > vm. Is such a feat possible? > > Hi Michael > > seL4’s confidentiality (and other security) enforcement means that the > kernel guarantees that you can only access objects to which you have been > given explicit permission (in the form of a capability). How those > permissions are allocated is a matter of policy, the kernel doesn’t care, > it only enforces. > > In particular, it is totally possible in seL4 to give one component access > to another component’s address space, that’s for the user-level policy > framework to decide. > > Whether the present CAmkES framework supports this is a different > question, which I’ll leave to someone who’s more up to date with CAmkES > details. > > Gernot > > > ------------------------------ > > Message: 2 > Date: Sat, 26 Oct 2019 10:35:50 +0800 > From: Yun Zhou <shiny725829(a)gmail.com> > To: devel(a)sel4.systems > Subject: [seL4] Fwd: port sel4 to RK3308(quad cortex-a35) > Message-ID: > <CAHNKqcxb7ws3MD=- > nwJka6HKEcA4hXZipJv0vdsStetJjxP-yg(a)mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > ---------- Forwarded message --------- > 发件人： Yun Zhou <shiny725829(a)gmail.com> > Date: 2019年10月25日周五下午9:52 > Subject: port sel4 to RK3308(quad cortex-a35) > To: <devel-owner(a)sel4.systems> > > > Dear sel4 Experts > How are you > I found some information about sel4, and sel4 is great microkernel OS, i > want port sel4 to RK3308(quad cortex-a35, GICv2) for real time audio signal > processing. Form the Tutorials I found sel4 just support cortex-a53, I > would like to ask does sel4 support cortex-a35 SMP mode. and because our > application is real time audio processing so system delay must lower than > 3ms and hard real-time determinism. > Will sel4 support real-time signal processing? > Looking forward to your reply > > Thanks &Kind regards > Yun >

1 0

The seL4 Foundation is coming!
by Heiser, Gernot (Data61, Kensington NSW) 25 Oct '19

25 Oct '19

Re-post from announce(a)sel4.systems<mailto:announce@sel4.systems> regarding the seL4 Foundation. We’ll start recruiting members soon. Gernot Begin forwarded message: From: Announcements about seL4 -- low volume list <announce(a)sel4.systems<mailto:announce@sel4.systems>> Subject: [seL4 Announce] The seL4 Foundation is coming! Date: 25 October 2019 at 17:09:30 AEDT To: "announce(a)sel4.systems<mailto:announce@sel4.systems>" <announce(a)sel4.systems<mailto:announce@sel4.systems>> Reply-To: <announce(a)sel4.systems<mailto:announce@sel4.systems>> Dear seL4 community, With great excitement we announce that we are in the process of setting up an seL4 Foundation, similar to foundations for other open-source projects, such as Linux and RISC-V. This will form an open, transparent and neutral organisation tasked with growing the seL4 ecosystem. It will bring together developers of the seL4 kernel, developers of seL4-based components and frameworks, and those deploying seL4-based systems. Its focus will be on coordinating, directing and standardising development of the seL4 ecosystem in order to reduce barriers to adoption, raising funds for accelerating development, and ensuring clarity of verification claims. This was originally announced at the seL4 Summit in the US last month. I apologise for the delay in this posting (side-tracked with various issues). Gernot on behalf of the Trustworthy Systems team _______________________________________________ Announce mailing list Announce(a)sel4.systems<mailto:Announce@sel4.systems> https://sel4.systems/lists/listinfo/announce

1 0

Upcoming release planned
by Mcleod, Kent (Data61, Kensington NSW) 23 Oct '19

23 Oct '19

Hi all, I'm announcing that we are planning a new versioned release of seL4, capDL and CAmkES in about 3 weeks - around 11 November. We want to provide an opportunity for people to report issues or provide patches that can be fixed/incorporated for the versioned release. The last versioned release occurred almost 12 months ago and we plan on returning to a shorter release cycle of several weeks per cycle. Feel free to raise new issues across our GitHub repositories and we will also try to address any currently outstanding issues that have been neglected. Here is a highlight list of what changes are going to be in the upcoming versioned release: ## seL4 - Add GrantReply access right for endpoint capabilities. `seL4_Call` is permitted on endpoints with either the Grant or the GrantReply access rights. Capabilities can only be transferred in a reply message if receiver's endpoint capability has the Grant right. The GrantReply access right allows endpoints to be configured for two-way communication without also providing the right to transfer authority via capability transfer. - Merging of the mixed-criticality scheduling (MCS) branch into master. Previously the MCS branch only received versioned releases. Merging it into master under a build configuration (KernelIsMCS) makes it easier to keep up to date with changes to master and other tooling/libraries in-between versioned releases. Verification work is still on-going. - Continued development of the newly added RISC-V platform to support in-progress verification. - Auto-generation of Arm and RISC-V kernel platform definitions from a provided devicetree as well as support for passing a devicetree to the root task via the seL4_BootInfo structure. Interrupt controllers, timers and other devices required by the kernel can also be selected in the devicetree provided that the kernel already has a compatible driver. - Support for AArch64 hypervisors is in active development with initial support for Cortex-A53 and Cortex-A57 cores - De-duplicating kernel platform configurations and code in order to reduce the effort required to support additional platforms. - New platforms added: BeagleBone Blue, Hardkernel ODROID-C2, Freescale i.MX8M, i.MX8M Mini, Arm FVP (based on foundation-v8-gicv3.dts), QEMU ARM virt platform (with 3 CPUs: cortex-A15, cortex-A53 and cortex-A57) and possibly PINE64 ROCKPro64. - Implement RFC-3: Cross-platform thread-local storage (TLS) support. https://sel4.atlassian.net/browse/RFC-3. This provides a way for a thread to access or modify a thread-specific pointer without requiring a capability to itself. On architectures that don't provide unprivileged write access to this pointer a new syscall `seL4_SetTLSBase` is added that performs this operation. The kernel no longer reserves a register for holding a thread's IPC buffer and it is the thread's responsibility for managing this. `libsel4` declares a pointer to a thread's IPC buffer using a `__thread` keyword and a new user-level library `sel4runtime` can be used to provide a minimal supporting runtime. Additionally, the IPC buffer's userData field is no longer used for holding a pointer to the IPC buffer. - Better SMP Arm IRQ handling: Support is added for creating IRQ handler capabilities for core-local interrupts (PPIs) for each core and for also specifying a target core for global interrupts (SPIs) via the new invocation `IRQControl_GetTriggerCore`. - Merge ARCH_Page_Remap functionality into ARCH_Page_Map. Remap was used for updating the mapping attributes of a page without changing its virtual address. Now ARCH_Page_Map can be performed on an existing mapping to achieve the same result. The ARCH_Page_Remap invocation has been removed from all configurations. - Support for compiling the kernel with Clang. For a more complete list see the CHANGES file in the seL4 repository. ## CAmkES - Support for the new seL4 Endpoint GrantReply access right for CAmkES connector types. This allows multi-sender/single-receiver connectors such as `seL4RPCCall` that don't also provide the ability for arbitrary capability transfer from sender to receiver. Previously the `seL4RPC` connector was used instead of `seL4RPCCall` to create an Endpoint without a Grant right. This used a combination of `seL4_Send` and `seL4_Wait` to communicate without the ability for capability transfer, however this only supports a single sender and single receiver. - Better support for configuring components with a provided devicetree. This support includes adding a seL4DTBHardware connector that can be used instead of seL4HardwareMMIO and seL4HardwareInterrupt and can be used to extract IRQs and MMIO register information out of the devicetree node rather than specifying the info directly. This connector can also be used to access a devicetree within a component at for querying further device information. There is also a connector seL4VMDTBPassthrough that can be used for specifying devices to pass through to a `camkes-arm-vm` VM component. - CapDL Refinement framework. These are generated Isabelle proof scripts to prove that the generated capDL respects the isolation properties expected from its CAmkES system specification. Only the AARCH32 platform is supported. The generated capDL is a specification of seL4 objects and capabilities that will implement the CAmkES system specification. This specification is then given to a system initialiser to create the objects and capabilities and load the system. - Support for RISC-V systems. ## capDL capDL refers to the capability distribution language and tools contained in https://github.com/seL4/capdl. CAmkES uses these tools for generating a capDL specification and then uses the `capdl-loader-app` as it's seL4 root task for initialising the system. As we are in the process of developing additional loaders we are going to start providing versioned releases of the capDL set of tools. Changes since the last seL4 release: - Support for the new seL4 Endpoint GrantReply access rights in the CapDL spec. Endpoint capabilities in the capDL spec can now have Read, Write, Grant and GrantReply rights. - Static Untyped allocation of spec objects. This is support for performing offline pre-allocation of spec objects to the Untyped objects that are expected to be provided in the seL4_BootInfo by the kernel. Having a static allocation of spec objects to Untypeds allows for more simple loaders that do not have to perform resource allocation during initialisation. This feature is optional and a spec is still valid if objects aren't allocated from Untyped objects. - Support for loading RISC-V systems.

1 0

CAmkES languages
by Michael Neises 21 Oct '19

21 Oct '19

Hi, I have an application written in CakeML that I would like to include in a CAmkES component, but all the documentation I can find only uses C code. Is it possible to use a non-C language as source for a CAmkES component? If so, how can I accomplish this? Best, Michael Neises

2 1

Zynq UltraScale+ locks up after hours running
by Leonid Meyerovich 05 Oct '19

05 Oct '19

Hello, We are running seL4 microkernel on 4 cores Zynq UltraScale+ (zcu102 board). The implementation includes multiple processes, hypervisor and virtual machine running on dedicated core. After several hours running (it could be 2 or even 8 hours) the whole microkernel locks up. After some investigation I have found that no interrupts generated anymore - at least there is no interrupts coming to ISR. Inside ISR I have monitored PL2 Physical Timer Control register, which feeds a scheduler and didn't find any problems - it stays enabled and not masked. I will appreciate any idea/direction for approaching this problem. Thank you, Leonid ________________________________ 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.

5 24

Re: [seL4] [Non-DoD Source] Devel Digest, Vol 65, Issue 5
by Seeberger, John T CIV USN NAS PAX MD (USA) 05 Oct '19

05 Oct '19

I have noticed this also. Thad ________________________________________ From: Devel [devel-bounces(a)sel4.systems] on behalf of devel-request(a)sel4.systems [devel-request(a)sel4.systems] Sent: Thursday, October 03, 2019 8:24 AM To: devel(a)sel4.systems Subject: [Non-DoD Source] Devel Digest, Vol 65, Issue 5 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel or, via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Re: Zynq UltraScale+ locks up after hours running (Shen, Yanyan (Data61, Kensington NSW)) 2. Re: How to use sel4runtime (Millar, Curtis (Data61, Kensington NSW)) 3. Re: Zynq UltraScale+ locks up after hours running (Leonid Meyerovich) ---------------------------------------------------------------------- Message: 1 Date: Thu, 3 Oct 2019 06:43:52 +0000 From: "Shen, Yanyan (Data61, Kensington NSW)" <Yanyan.Shen(a)data61.csiro.au> To: "lmeyerovich(a)i-a-i.com" <lmeyerovich(a)i-a-i.com>, "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] Zynq UltraScale+ locks up after hours running Message-ID: <78ebf24ad9274ca75e18b5fca8575a09bc423b82.camel(a)data61.csiro.au> Content-Type: text/plain; charset="utf-8" Hi Leonid, Could you provide a bit more about your software configuration? For instance, do you have multiple VMs running on dedicated hardware cores? How are the VM and processes configured? Also, you mean there were no interrupts at all on all the four cores? Regards, Yanyan On Wed, 2019-10-02 at 16:01 +0000, Leonid Meyerovich wrote: > Hello, > > We are running seL4 microkernel on 4 cores Zynq UltraScale+ (zcu102 > board). The implementation includes multiple processes, hypervisor > and virtual machine running on dedicated core. After several hours > running (it could be 2 or even 8 hours) the whole microkernel locks > up. After some investigation I have found that no interrupts > generated anymore - at least there is no interrupts coming to ISR. > Inside ISR I have monitored PL2 Physical Timer Control register, > which feeds a scheduler and didn't find any problems - it stays > enabled and not masked. > > I will appreciate any idea/direction for approaching this problem. > > Thank you, > > Leonid > > > > > 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. > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel ------------------------------ Message: 2 Date: Thu, 3 Oct 2019 07:04:41 +0000 From: "Millar, Curtis (Data61, Kensington NSW)" <Curtis.Millar(a)data61.csiro.au> To: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] How to use sel4runtime Message-ID: <ad55f3a5de7838e0f9d16a94905647a0ead42249.camel(a)data61.csiro.au> Content-Type: text/plain; charset="utf-8" Hi Baltazar, > Another (less exclusively RISC-V related, though I am targeting RISC-V > still) question - I've been trying to figure out the sel4runtime repo, > but I'm a bit confused on how to set it up. Specifically: > > * How much of a "minimal seL4 environment" do I need to initialize > first? The sel4runtime is a minimal C runtime specifically for seL4. It handles the initialization of all applications (root servers and System-V ELF processes) on an seL4 system. A minimal project will require a repo project containing seL4, seL4_tools, musl, and sel4runtime (along with a root task application). sel4runtime is then used as the C runtime for all applications built in the project and is responsible for providing the entrypoints and calling into the main function. > * Do does my program with main() also need to specify a root task, or > is that part of the minimal environment? You will still need to provide a root task application. sel4runtime is only responsible for handling process startup for C applications. > * Is there a specific recommended location for the sel4runtime repo? The sel4runtime repo is usually placed in the projects directory. You can see sel4-tutorials-manifest[^1] repository on github for an example of how the dependecies are laid out. [^1]: https://github.com/SEL4PROJ/sel4-tutorials-manifest Cheers, Curtis Millar Systems Engineer, Trustworthy Systems, CSIRO's Data61 curtis.millar(a)data61.csiro.au Data61, CSIRO Level 3, K17 Building UNSW Gate 14, Barker St Kensington NSW 2033 Australia

2 1

[FOSDEM] [Fwd: CfP: FOSDEM 2020 - Microkernels and Component-based OS devroom] (fwd)
by Stefan Kalkowski 04 Oct '19

04 Oct '19

Hello sel4 community, I think below announcement might be interesting for you too. Best regards Stefan Kalkowski -------- Forwarded Message -------- From: Julian Stecklina <js(a)alien8.de> Reply-To: microkernel-devroom(a)lists.fosdem.org To: l4-hackers(a)os.inf.tu-dresden.de, users(a)lists.genode.org, microkernel-devroom(a)lists.fosdem.org, ukvly-announce(a)freelists.org, helenos-devel(a)lists.modry.cz Subject: CfP: FOSDEM 2020 - Microkernels and Component-based OS devroom Date: Fri, 04 Oct 2019 00:38:35 +0200 [Resent due to wrong Reply-To: header] FOSDEM 2020 - Microkernels and Component-based OS devroom CALL FOR PARTICIPATION The developers of several free and open-source microkernel-based operating systems will meet at FOSDEM 2020 [1] in Brussels, Belgium and will share a developer room. The devroom is currently looking for content in the form of talks and activities related to the area of microkernel-, unikernel-, and component-based operating systems. Possible topics include, but are not limited to: * introduction of a specific OS or framework * design of subsystems and the general architecture of an OS * used languages and tools * enabling support for hardware (architectures, device drivers) * enabling support for programming languages * maintenance and testing * security and robustness * trends and challenges * use cases, experiences, lessons learned and demos The deadline for your proposal is on December 1, 2019. Please use the Pentabarf [2] system to submit your proposals. You do not need to create a new account if you already have one. Make sure to include the following in your proposal: * title of your talk (will be printed in the FOSDEM booklet) * your full name (will be printed in the FOSDEM booklet) * a short abstract (one or two paragraphs) * duration of your talk (at least 25 and no longer than 55 min) The official devroom schedule (along with the accepted talks) will be announced on December 15 on the devroom's mailing list [3] and the speakers will be notified via e-mail. The schedule will also be published on the FOSDEM website. You are invited to send any other suggestions for what you want to see or do at the devroom to the list. We will also use this list to organize the traditional devroom dinner that will happen on the first day of FOSDEM. About the devroom Since the first Microkernel devroom at FOSDEM 2012, this devroom has been part of each following FOSDEM. The focus gradually widened to include component-based operating systems. By now it has become a somewhat institutionalized tradition for the community to meet there; to this date over a dozen projects have participated in one way or another. Each of the projects face similar challenges but come up with partially different solutions. Therefore, the goal of the devroom is to bring the various projects together, let them exchange ideas, cross-pollinate and socialize. Social events It also has become a habit that the microkernel projects dine together somewhere in Brussels. The year 2020 will not be any different, so there is going to be a dinner on Saturday night. We try place a reservation, so we will inform you about the exact location and time later. Consult the FOSDEM web and other projects for additional social events such as the famous FOSDEM-organized Friday Beer Event and the FOSDEM-arranged free sightseeing tours for spouses. About FOSDEM FOSDEM is a two-day event organised by volunteers to promote the widespread use of free and open source software. Taking place in the beautiful city of Brussels (Belgium), FOSDEM is widely recognised as the best such conference in Europe. FOSDEM covers a wide spectrum of free and open source software projects, and offers a platform for people to collaborate. To this end, FOSDEM has set up developer rooms (devrooms) with network/internet connectivity and projectors where teams can meet and showcase their projects. Devrooms are a place for teams to discuss, hack and publicly present latest directions, lightning talks, news and discussions. Besides developer rooms, FOSDEM also offers main tracks, lightning talks, certification exams and project stands. Every year, FOSDEM hosts more than 5000 developers at the ULB Solbosch campus. Participation and attendance is totally free, though the organisers gratefully accept donations and sponsorship. No registration necessary. Important dates recap * 2019-12-01: Deadline for submissions * 2019-12-15: Schedule published and speakers notified of acceptance * 2020-02-01: Devroom Dinner (details to be announced) * 2020-02-01/2020-02-02: The devroom takes places (check the schedule) Links [1] https://fosdem.org/ [2] https://penta.fosdem.org/submission/FOSDEM20 [3] https://lists.fosdem.org/listinfo/microkernel-devroom _______________________________________________ FOSDEM mailing list FOSDEM(a)lists.fosdem.org https://lists.fosdem.org/listinfo/fosdem ----- End forwarded message ----- -- Stefan Kalkowski Genode labs https://github.com.skalk | https://genode.org

1 0

Re: [seL4] CapDL output to isabelle file
by Lim, Japheth (Data61, Kensington NSW) 04 Oct '19

04 Oct '19

Hi Norrathep, Norrathep Rattanavipanon wrote: > I have been trying to generate Isabelle file from CapDL specification. But > I run into an error when I'm running the command: > > ./parse-capDL --isabelle=out.thy --object-sizes=object_sizes.yaml > example-arm.cdl > We recently put in a major change to the Isabelle translator. The input capDL file is now required to be pre-allocated, i.e. every object must be placed in an untyped with a known physical address. The existing example files date from before this change, and so they don't meet the requirements to be translated into Isabelle. Sorry that you got confusing error messages as a result. We plan to make this more consistent in the near future. > Is there any step I'm missing? Or does the tool not support the conversion > to Isabelle? The standard way is to build a CAmkES application with the option `CAmkESCapDLStaticAlloc` enabled. This will generate a suitable capDL file for proofs. Based on your other question thread, you may be interested in our README for CAmkES proofs: https://github.com/seL4/camkes-tool/tree/master/cdl-refine-tests This generates proofs between the CAmkES high-level model and the capDL system representation. However, we are not working on C glue code proofs at the moment. This is all work in progress, and quite rough around the edges. Nevertheless, we're happy to try to answer any questions you might have. It would help if we knew more about your work, so that we can give more specific replies. Cheers, Japheth Lim Proof Engineer, Trustworthy Systems

3 5

Initialising Camkes App before another dependent Camkes app
by yogidk . 03 Oct '19

03 Oct '19

Hi, I have a Camkes app (app1) which depends on another Camkes app (app2), which means my app1 must start only after app2 is completely initialized. For this currently I use a signal RPC wait in app1 and the corresponding RPC emit from app2 after app2 is completely initialized. Is there any other way in CamkES which will ensure that app1 starts only after app2 is completely initialized without using RPC signalling (emit and wait) ? How can this dependency be built ? Regards yk

3 2

Re: [seL4] How to use sel4runtime
by Millar, Curtis (Data61, Kensington NSW) 03 Oct '19

03 Oct '19

Hi Baltazar, > Another (less exclusively RISC-V related, though I am targeting RISC-V > still) question - I've been trying to figure out the sel4runtime repo, > but I'm a bit confused on how to set it up. Specifically: > > * How much of a "minimal seL4 environment" do I need to initialize > first? The sel4runtime is a minimal C runtime specifically for seL4. It handles the initialization of all applications (root servers and System-V ELF processes) on an seL4 system. A minimal project will require a repo project containing seL4, seL4_tools, musl, and sel4runtime (along with a root task application). sel4runtime is then used as the C runtime for all applications built in the project and is responsible for providing the entrypoints and calling into the main function. > * Do does my program with main() also need to specify a root task, or > is that part of the minimal environment? You will still need to provide a root task application. sel4runtime is only responsible for handling process startup for C applications. > * Is there a specific recommended location for the sel4runtime repo? The sel4runtime repo is usually placed in the projects directory. You can see sel4-tutorials-manifest[^1] repository on github for an example of how the dependecies are laid out. [^1]: https://github.com/SEL4PROJ/sel4-tutorials-manifest Cheers, Curtis Millar Systems Engineer, Trustworthy Systems, CSIRO's Data61 curtis.millar(a)data61.csiro.au Data61, CSIRO Level 3, K17 Building UNSW Gate 14, Barker St Kensington NSW 2033 Australia

1 0

Run VM guest on seL4 using CAmkEs
by Khalid Amen 03 Oct '19

03 Oct '19

Hello, I am trying to run VM guest on seL4 using CAmkEs. I have setup my linux machine and installed dependencies. I have run seL4 hello world example. What do I need to do run VM guest in seL4? I have serached online to see. The documentation says that to create VM guests and applications on seL4, I need to use CAmkES. I followed this link: https://docs.sel4.systems/Tutorials/camkes-vm-linux.html. What do I need to create VM on top of seL4 using CAmkES? Also, I want seL4 to run as hypervisor. I have found a tutorial on how to run it from these links. https://github.com/seL4/camkes-vm-examples/blob/master/README.md https://docs.sel4.systems/Tutorials/camkes-vm-linux But, I did not understand the following: You can boot the tutorial on an x86 hardware platform with a multiboot boot loader, or use the QEMU <https://www.qemu.org/> simulator. *Note if you are using QEMU it is important to ensure that your host machine has VT-x support and KVM <https://www.linux-kvm.org/page/Main_Page> installed. You also need to ensure you have enabled nested virtulisation with KVM guests as described here <https://www.linux-kvm.org/page/Nested_Guests>.* After building is completed with ninja, how do I excute the following: Then boot images/kernel-x86_64-pc99 and images/capdl-loader-experimental-image-x86_64-pc99 (or *.ia32-pc99 if built for 32-bit) with the multiboot boot loader of your choice. -- Regards, Khalid Ameen

2 1

Sel4 for quadcore riscv64imafd
by Sreenadh S 03 Oct '19

03 Oct '19

I want to build sel4 for quadcore riscv64imafd and run the test programs, how to do that? Regards, Sreenadh S, CDAC, Trivandrum, India

2 1

seL4_FailedLookup in vmware
by KAP Benjamin 03 Oct '19

03 Oct '19

Hello I set up VMware according to this guide https://docs.sel4.systems/Hardware/VMware/ (using serial output to file) and compiled the picoserver CAmkES application (for x86_64) to run inside the VMware machine. However, I do encounter a seL4_FailedLookup error. I understand the error message but cannot figure out why it occurs nor how to fix it (probably my pci configuration is wrong). Attached you find the serial_output file. For the ethernet configuration I used linux in the same VM to figure out the details: 1) ip addr: 2: ens32: <BROADCAST,MULTICAST,UP,LOWER_UP> mtu 1500 qdisc fq_codel state UNKNOWN group default qlen 1000 link/ether 00:0c:29:90:a7:4a brd ff:ff:ff:ff:ff:ff 2) lspci -vvv: 02:00.0 Ethernet controller: Advanced Micro Devices, Inc. [AMD] 79c970 [PCnet32 LANCE] (rev 10) Subsystem: Advanced Micro Devices, Inc. [AMD] PCnet - Fast 79C971 Physical Slot: 32 Control: I/O+ Mem+ BusMaster+ SpecCycle- MemWINV- VGASnoop- ParErr- Stepping- SERR- FastB2B- DisINTx- Status: Cap- 66MHz- UDF- FastB2B+ ParErr- DEVSEL=medium >TAbort- <TAbort- <MAbort- >SERR- <PERR- INTx- Latency: 64 (1500ns min, 63750ns max) Interrupt: pin A routed to IRQ 18 Region 0: I/O ports at 2000 [size=128] [virtual] Expansion ROM at fd500000 [disabled] [size=64K] Kernel driver in use: pcnet32 Kernel modules: pcnet32 3) dmesg | grep "02:00.0": ... [ 0.378516] pci 0000:02:00.0: BAR 6: assigned [mem 0xfd500000-0xfd50ffff pref] ... 4) lspci -nn: 02:00.0 Ethernet controller [0200]: Advanced Micro Devices, Inc. [AMD] 79c970 [PCnet32 LANCE] [1022:2000] (rev 10) And here the configuration part inside picoserver.camkes (anything else NOT pasted here is unmodified): picoserver.ethdriver_mac = [0x00, 0x0c, 0x29, 0x90, 0xa7, 0x4a]; .... hwethdriver.mmio_paddr = 0xfd500000 hwethdriver.mmio_size = 0x10000 hwethdriver.irq_irq_type = "pci"; hwethdriver.irq_irq_ioapic = 0; hwethdriver.irq_irq_ioapic_pin = 18; hwethdriver.irq_irq_vector = 18; ethdriver.iospaces = "0x0:0x02:0x00:0"; ethdriver.iospace_id = 0x0200; ethdriver.pci_bdf = "0x02:0x00.0"; I am sorry to bother you with this; I am fairly new to low level stuff. Any help would be very much appreciated. Best regards, Benjamin

2 1

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 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

seL4 UART input (on RISC-V)?
by Ortiz, Baltazar 22 Aug '19

22 Aug '19

Hi all, I've been looking through the seL4 libraries and examples, and it seems to me that serial input should in some way be possible - the refos example appears to have a terminal, and I would imagine that debugging via GDB requires input in addition to output. However, the code to do this is unclear to me. Calling getchar() or similar leads to the unimplemented readv syscall, and calling __arch_getchar or similar causes a cap error even after running platsupport_serial_setup_simple(). Is there a step I'm missing? I'm specifically trying to get this working on RISC-V. Thanks, Baltazar ________________________________ Notice: This email and any attachments may contain proprietary (Draper non-public) and/or export-controlled information of Draper. If you are not the intended recipient of this email, please immediately notify the sender by replying to this email and immediately destroy all copies of this email. ________________________________

2 4

CapDL output to isabelle file
by Norrathep Rattanavipanon 21 Aug '19

21 Aug '19

Hello, I have been trying to generate Isabelle file from CapDL specification. But I run into an error when I'm running the command: ./parse-capDL --isabelle=out.thy --object-sizes=object_sizes.yaml example-arm.cdl warning: specifying untyped child multiple times is deprecated: ut = a, child = name warning: specifying untyped child multiple times is deprecated: ut = b, child = name warning: specifying untyped child multiple times is deprecated: ut = something, child = rm_ut parse-capDL: CapDL/PrintIsabelle.hs:180:15-71: Irrefutable pattern failed for pattern ut@(Untyped {maybePaddr = Just utPaddr}) where example-arm.cdl is the example I got from CapDL repo ( https://github.com/seL4/capdl/blob/master/capDL-tool/example-arm.cdl) And object_sizes.yaml contains: seL4_TCBObject: 10 seL4_EndpointObject: 4 seL4_NotificationObject: 4 seL4_SmallPageObject: 12 seL4_LargePageObject: 16 seL4_ASID_Pool: 12 seL4_ASID_Table: 10 seL4_Slot: 4 seL4_Value_MinUntypedBits: 4 seL4_Value_MaxUntypedBits: 29 seL4_PageTableObject: 10 seL4_PageDirectoryObject: 14 seL4_ARM_SectionObject: 20 seL4_ARM_SuperSectionObject: 24 seL4_IOPageTableObject: 12 seL4_IOPorts: 0 seL4_IODevice: 0 seL4_ARMIODevice: 0 seL4_IRQ: 0 seL4_IOAPICIRQ: 0 seL4_MSIIRQ: 0 The same error also occurs when I used parse-capdL executable generated by Camkes repo. Is there any step I'm missing? Or does the tool not support the conversion to Isabelle? Best, Norrathep -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

1 0

Shared memory in CapDL
by Norrathep Rattanavipanon 12 Aug '19

12 Aug '19

Hi, I have been reading Andrew Boyton's thesis about CapDL and realized that CapDL does not support a shared memory page. Is it still a limitation in CapDL/Camkes? Or has it somehow been addressed? Does this limitation include the case where a page is mapped/shared with different access rights? e.g., a page is mapped writable to one process and the same page is mapped only readable to another process? Best, Norrathep -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 5

How to use sel4runtime
by Ortiz, Baltazar 10 Aug '19

10 Aug '19

Hi all, Another (less exclusively RISC-V related, though I am targeting RISC-V still) question - I've been trying to figure out the sel4runtime repo, but I'm a bit confused on how to set it up. Specifically: * How much of a "minimal seL4 environment" do I need to initialize first? * Do does my program with main() also need to specify a root task, or is that part of the minimal environment? * Is there a specific recommended location for the sel4runtime repo? Thanks! Baltazar ________________________________ Notice: This email and any attachments may contain proprietary (Draper non-public) and/or export-controlled information of Draper. If you are not the intended recipient of this email, please immediately notify the sender by replying to this email and immediately destroy all copies of this email. ________________________________

1 0

SeL4 on 32 bit RISC-V
by Ortiz, Baltazar 09 Aug '19

09 Aug '19

Hi all, I'm looking into getting seL4 booting on 32 bit RISC-V. Currently working with seL4test 10.1.1, QEMU 4.0.0, and an upstream copy of riscv-gnu-toolchain (is there a specific release I should try?). I'm able to get seL4 to build after deleting a few CONST labels that the compiler was complaining about, but when I try to run the simulation script, I get the following output: > ./simulate -b /home/baltazar/qemu/build/riscv32-softmmu/qemu-system-riscv32 > /home/baltazar/qemu/build/riscv32-softmmu/qemu-system-riscv32 -machine spike_v1.10 -nographic -s -serial mon:stdio -m size=2000M -kernel images/sel4test-driver-image-riscv-spike > bbl loader > /host/sel4test-upstream-riscv/tools/riscv-pk/machine/minit.c:74: assertion failed: !(read_csr(misa) & fd_mask) > Power off Are there any tricks for getting this working right now? Thanks, Baltazar ________________________________ Notice: This email and any attachments may contain proprietary (Draper non-public) and/or export-controlled information of Draper. If you are not the intended recipient of this email, please immediately notify the sender by replying to this email and immediately destroy all copies of this email. ________________________________

3 5

CAmkES Tutorial Generation Issues
by Austin Owens 23 Jul '19

23 Jul '19

Hello, I am able to generate, build, and execute the majority of tutorials using init, ninja, qemu, etc. within sel4-tutorials-manifest. However, I am having issues generating the tutorials specifically for the CamkES tutorials. I have installed all of the system requirements and I am running on Ubuntu 18. The output I get is the following: # ./init --tut hello-camkes-0 loading initial cache file ../settings.cmake -- The C compiler identification is GNU 7.4.0 -- Check for working C compiler: /usr/bin/gcc -- Check for working C compiler: /usr/bin/gcc -- works -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- The CXX compiler identification is GNU 7.4.0 -- Check for working CXX compiler: /usr/bin/g++ -- Check for working CXX compiler: /usr/bin/g++ -- works -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Detecting CXX compile features -- Detecting CXX compile features - done -- The ASM compiler identification is GNU -- Found assembler: /usr/bin/gcc -- CPIO test cpio_reproducible_flag FAILED -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- /root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/ast.pickle is out of date. Regenerating... -- /root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/camkes-gen.cmake is out of date. Regenerating... CAmkES uses UTF-8 encoding, but your locale's preferred encoding is ansi_x3.4-1968. You can override your locale with the LANG environment variable. CMake Error at tools/seL4/cmake-tool/helpers/make.cmake:19 (file): file failed to open for reading (No such file or directory): /root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/camkes_gen/deps_1 Call Stack (most recent call first): tools/seL4/cmake-tool/helpers/make.cmake:77 (MakefileDepsToList) tools/camkes/camkes.cmake:460 (execute_process_with_stale_check) hello-camkes-0/CMakeLists.txt:13 (GenerateCAmkESRootserver) CMake Error at tools/camkes/camkes.cmake:480 (message): Failed to generate /root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/camkes-gen.cmake Call Stack (most recent call first): hello-camkes-0/CMakeLists.txt:13 (GenerateCAmkESRootserver) -- Configuring incomplete, errors occurred! See also "/root/sel4-tutorials-manifest/hello-camkes-0_build/CMakeFiles/CMakeOutput.log". Traceback (most recent call last): File "./init", line 96, in <module> File "./init", line 85, in main File "/root/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 107, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/root/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 75, in _init_build_directory return sh.cmake(args + ['..'], _cwd=directory, _out=output, _err=output) File "/usr/local/lib/python3.6/dist-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/usr/local/lib/python3.6/dist-packages/sh.py", line 774, in __init__ self.wait() File "/usr/local/lib/python3.6/dist-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/usr/local/lib/python3.6/dist-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /usr/local/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-0 -C ../settings.cmake .. STDOUT: STDERR: I am not sure if ast.pickle and camkes-gen.cmake being out of date has anything to do with deps_1 file not being present. It's not possible to copy the deps_0 file to deps_1 since calling the './init --tut hello-camkes-0' command again creates a new project directory. Is there something obvious that I am missing? Thanks, Austin

3 4

Autocorres tutorial for Isabelle/HOL beginner
by Norrathep Rattanavipanon 22 Jul '19

22 Jul '19

Hello, I have been trying to study how seL4's C code is formally verified. So I looked into Autocorres tool and had a bit of hard time understanding how to use the tool to generate Isabelle definitions from C code. I tried to follow Autocorres' quickstart but I was confused since I do not know much about Isabelle/HOL. I simply ran ``make AutoCorresTest" in l4v/tools/autocorres folder and it gave me this output: ``` Session Pure/Pure Session FOL/FOL Session HOL/HOL (main) Session HOL/HOL-Eisbach Session HOL/HOL-Library (main timing) Session HOL/HOL-Computational_Algebra (main timing) Session HOL/HOL-Algebra (main timing) Session HOL/HOL-Number_Theory (main timing) Session HOL/HOL-Statespace Session HOL/HOL-Word (main timing) Session Lib/Word_Lib (lib) Session Lib/Lib (lib) Session C-Parser/Simpl-VCG Session C-Parser/CParser Session Lib/CLib (lib) Session Unsorted/AutoCorres Session Unsorted/AutoCorresTest Building AutoCorresTest ... AutoCorresTest: theory AutoCorresTest.CustomWordAbs AutoCorresTest: theory AutoCorresTest.Test_Spec_Translation ... Finished AutoCorresTest (0:02:33 elapsed time, 0:08:14 cpu time, factor 3.23) ``` But I couldnt find any Isabelle definitions as output except "thy" files that contain: ``` theory somefile imports "AutoCorres.AutoCorres" begin external_file "somefile.c" install_C_file "somefile.c" autocorres "somefile.c" end ``` I suppose I need to invoke this file somehow using Isabelle in order to generate the definition but I'm not sure how to do that. Any help would be very appreciated. Best Regards, Norrathep -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

sel4 on the Xilinx Zynq US+ ZCU104 Evaluation Kit
by derek65 22 Jul '19

22 Jul '19

Hi, I'm interested in running sel4 on a Xilinx Zynq UltraScale+ MPSoC evaluation board. I read the great blog post about the port from DornerWorks [1] and checked the sel4 hardware support page here [2]. Since the Zynq ZCU102 Evaluation Kit listed is quite expensive, I wanted to ask if anyone tried the procedure described in the blog post on the much cheaper Xilinx US+ ZCU104 Evaluation Kit. Might this work as well? Thanks! Kind regards, - derek [1] - https://dornerworks.com/blog/hardware-security-growing-concern-sel4-ecosyst… [2] - https://docs.sel4.systems/Hardware/

4 3

CamkES support for waiting on multiple signals
by yogidk . 22 Jul '19

22 Jul '19

Hello , I would like to know if the CamkES has support for wait on multiple signal events ? I need to wait for 3 different events (say write, read and timer), I need to wait until one of these events occur. As soon as I get an event, I need to call a common function. I cannot use emitter/consumer signal events concept of CamKES here as it allows only one to one connection and not many to one connection. So in other words a single consumer_wait() for 3 different emitter events is not possible in CamkES. Any suggestions how can this be achieved using CamkES? Regards yk

3 3

Re: [seL4] Understanding Camkes Dataport Interface Access Rights
by Amit Goyal 16 Jul '19

16 Jul '19

Hi Kent, Thank you for your detailed reply. I agree that write only accesses are stored as read write mappings and reading on a write only access dataport does not give any error. I am still not very clear about the following: a) As suggested by you, I looked through the generated spec in .cdl file. I did not find the expected configuration of the dataport. Please find attached my .cdl file along with the template file. I cannot find dataport "delta" in that. Can you please help me to figure out the same. b) As far as I understood the .cdl configuration is setup by the camkes/kernel and corresponding page table mapping entries are made for each component. Later, whenever a component is scheduled by the kernel, MMU hardware will check whether it has the read or write access, based on the page table entries provided by the kernel. Please correct me if I have misunderstood it. My query is that in seL4 for communicating using endpoints a thread mints endpoint capabilities into other threads cspace and gives it the required access. I am not very clear with why the similar mechanism was not used here. I mean why a thread does not mint a frame's capability into other thread cspace with the required access. I am referring to section 7.4 of seL4 manual (http://sel4.systems/Info/Docs/seL4-manual-10.1.1.pdf) i) I feel if that would have been used, then we could take better advantage of the seL4 capability based access control guarantees and lift it to camkes. This way frame capability bits in frame capability could have been used to store/check the access rights. This way checks might have been software based rather than hardware based. ii) In case we are minting the frame in the similar way as mentioned above, can you point me towards that piece of code. iii) I hope minting is actually being used in Event connection and RPC connection. -- Thanks and Regards, Amit Goyal > On 2019-07-03 07:24, Mcleod, Kent (Data61, Kensington NSW) wrote: >> Camkes dataports on seL4 (seL4SharedData connector) are implemented as a >> shared memory mapping between the two components both pages are mapped to >> the >> same underlying frame of physical memory. The access rights are >> implemented >> via mapping attributes supported by the architecture. Your reads and writes >> through your dataport pointers are acting on this shared memory directly. >> The >> fault is generated by a hardware exception that seL4 handles by creating a >> fault and sending it to a registered fault handler (sendFaultIPC is the >> function in the kernel). There is a setting (that is enabled by default) >> that >> causes each Camkes component to set up a fault handler for all of its >> threads. >> If any of these threads cause a fault, such as by writing to read only >> memory, the fault handler will receive a message from the kernel. >> >> These mapping attributes are set when the kernel creates the page >> mapping for each component using the relevant Map invocation [1]. The >> result >> of building a Camkes system for seL4 is a system spec that contains all of >> the >> seL4 kernel objects and capabilities described by the system. Within this >> spec, dataports are described as a capability to physical memory where each >> capability has the specified access rights. When the system initialiser >> (capdl-loader-app in our case) is started by seL4 as the root task, it >> constructs the system following the spec and starts each Camkes component. >> By >> this point, the seL4 invocations for setting up the shared data page >> mappings >> have been performed. >> You can look through the generated spec in the build directory by finding >> the >> file with the .cdl extension. If you search for the name of the dataport >> you >> can find the capabilities and objects to validate that the rights are as >> you >> would expect. >> >> Hope this answers your questions. >> >> @Matthew: Write only mappings are still coerced by the capdl-loader to read >> write mappings before calling the mapping invocation. >> >> [1] https://docs.sel4.systems/ApiDoc.html#map-4

3 2

Understanding Camkes Dataport Interface Access Rights
by Amit Goyal 03 Jul '19

03 Jul '19

Hi All, I was looking at hello-camkes-2 tutorial. I understand the concept of dataports and the access rights given on dataport interfaces. I changed the configuration in hello-camkes-2.camkes.template file by adding echo.d = "R"; client.d = "W";. I did some changes in the client.c.template file to read on the dataport interface d by trying to access its contents through str/n/d pointers. Although, it only has write access on "d" in the new configuration. This leads to the fault handler being called when I simulate the build. I was just curious to find out where are such checks being done at the backend in camkes/seL4. I could find the code of fault handler in component.template.c but I could not find anywhere the code which checks that the client only has write access on dataport d and thus calling the fault handler. Can someone point me towards that piece of code or explain what is exactly happening at the backend in camkes/seL4? -- Thanks and Regards, Amit Goyal

4 4

Beaglebone Black: failed to find device frame
by KAP Benjamin 29 Jun '19

29 Jun '19

Hello I am trying to add am335x support to the pico TCP/IP stack and currently working on the following file: projects/global-components/components/Ethdriver/include/plat/am335x/plat/eth_devices.h. Current contents of this file (I am creating it step by step, thus it might be incomplete): #pragma once #define HARDWARE_ETHERNET_COMPONENT #define HARDWARE_ETHERNET_INTERFACES \ consumes Dummy EthDriver; \ emits Dummy dummy_source; #define HARDWARE_ETHERNET_COMPOSITION \ connection seL4DTBHardware ethernet_conn(from dummy_source, to EthDriver); #define HARDWARE_ETHERNET_CONFIG \ EthDriver.dtb = dtb({ "path" : "/ocp/ethernet@4a100000" }); \ EthDriver.generate_interrupts = 1; I test the implementation by using the picoserver CAmkES application. However, on boot I receive the following error: ELF-loader started on CPU: ARM Ltd. Cortex-A8 r3p2 paddr=[82000000..8262e037] No DTB found! Looking for DTB in CPIO archive... Found dtb at 820c1b84 Loaded dtb from 820c1b84 paddr=[80034000..8003cfff] ELF-loading image 'kernel' paddr=[80000000..80033fff] vaddr=[f0000000..f0033fff] virt_entry=f0000000 ELF-loading image 'capdl-loader' paddr=[8003d000..8059afff] vaddr=[10000..56dfff] virt_entry=1e4dc ELF loader relocated, continuing boot... Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Booting all finished, dropped to user space create_object@main.c:726 device frame/untyped, paddr = 0x48040000, size = 12 bits create_object@main.c:726 device frame/untyped, paddr = 0x48042000, size = 12 bits create_object@main.c:726 device frame/untyped, paddr = 0x4a100000, size = 12 bits create_object@main.c:726 device frame/untyped, paddr = 0x4a101200, size = 12 bits create_object@main.c:730 [Cond failed: err != seL4_NoError] Failed to find device frame/untyped at paddr = 0x4a101200 seL4 root server abort()ed Debug halt syscall from user thread 0xffefd600 "rootserver" halting... Kernel entry via Unknown syscall, word: 65 The am335x.dtb contains the following line in ethernet@4a100000: reg = <0x4a100000 0x00000800 0x4a101200 0x00000100>; I did find related posts (http://sel4.systems/pipermail/devel/2016-June/000850.html, http://sel4.systems/pipermail/devel/2018-July/002031.html and http://sel4.systems/pipermail/devel/2015-October/000530.html) but didn't help me that much.<http://sel4.systems/pipermail/devel/2018-July/002031.html)> If I am correct the hardware block isn't enabled but I don't know exactly how to do this. Could anyone help me out here or give me some hints? Best Regards, Kap Benjamin

3 7

seL4 devs
by James Rolevink 25 Jun '19

25 Jun '19

Hey, guys. After getting it up and running a while back, just wondering: are there any (good) seL4 app devs for hire? Engineer partner-in-crime is looking to develop apps for a smart device. Physically based in Adelaide. Cheers, James Rolevink –––––––––––––––––––––––––––––––––––––––– M: 04123 62 432 E: cybercitadel(a)icloud.com <mailto:james@cybercitadel.co> W: www.cybercitadel.co <https://www.cybercitadel.co/> L: james-r-53986189 <https://www.linkedin.com/in/james-r-53986189/> Cyber Citadel Pty Ltd ACN: 622 880 657

1 0

CMake Error
by Amit Goyal 25 Jun '19

25 Jun '19

Hi, Camkes had been working fine till now. Suddenly, it stopped working. I am running it on x86 system (i7 processor), ubuntu 16.04 on qemu. I am running the following commands: mkdir build cd build ../init --plat pc99 --tut hello-camkes-2 --solution Following error is generated: --------------------------------------------------------------------------------------------------------------------------------- Traceback (most recent call last): File "../init", line 76, in <module> sys.exit(main()) File "../init", line 62, in main result = common.init_build_directory(args.plat, args.tut, args.solution, os.getcwd()) File "/home/goyal/sel4/camkes-tutorials-manifest/projects/sel4-tutorials/common.py", line 59, in init_build_directory result = sh.cmake(args + ['..'], _cwd = directory, _out=output) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/uTraceback (most recent call last): File "../init", line 76, in <module> sys.exit(main()) File "../init", line 62, in main result = common.init_build_directory(args.plat, args.tut, args.solution, os.getcwd()) File "/home/goyal/sel4/camkes-tutorials-manifest/projects/sel4-tutorials/common.py", line 59, in init_build_directory result = sh.cmake(args + ['..'], _cwd = directory, _out=output) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 774, in __init__ self.wait() File "/usr/local/lib/python2.7/dist-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /usr/local/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL=hello-camkes-2 -DBUILD_SOLUTIONS=TRUE .. STDOUT: -- Configuring incomplete, errors occurred! STDERR: CMake Error at /opt/cmake-3.11.0-Linux-x86_64/share/cmake-3.11/Modules/CMakeDetermineSystem.cmake:100 (message): Could not find toolchain file: ../kernel/gcc.cmake Call Stack (most recent call first): CMakeLists.txt CMake Error: CMake was unable to find a build program corresponding to "Ninja". CMAKE_MAKE_PROGRAM is not set. You probably need to select a different build tool. CMake Error: CMAKE_C_COMPILER not set, after EnableLanguage CMake Error: CMAKE_CXX_COMPILER not set, after EnableLanguage --------------------------------------------------------------------------------------------------------------------------------- Can you please suggest a possible way out? -- Thanks and Regards, Amit Goyal

5 8

Checking if an endpoint is a badged version of another
by Demi Obenour 15 Jun '19

15 Jun '19

I have a server process SB that issues badged endpoints to users. Clients can invoke the endpoints to access memory and possibly other resources. Essentially, it is a version of Robigalia’s space bank. Other programs pass endpoints issued by SB to provide servers the resources needed to do their tasks, and the servers invoke the endpoints to obtain memory that they know cannot be revoked or modified by other programs. SB is part of the TCB, and is trusted by all of its clients. Clients, however, do not trust each other, and may pass forged endpoints to servers to cause servers to misbehave. Therefore, servers need to be able to ask SB if a given capability was actually issued by SB. SB can make that check by checking that the endpoint is a badged version of its master endpoint, which it never gives anyone else access to. What is the correct API function for doing this? Sincerely, Demi M. Obenour

2 1

Re: [seL4] Checking if an endpoint is a badged version of another
by Millar, Curtis (Data61, Kensington NSW) 15 Jun '19

15 Jun '19

Hi Demi, Any time you perform an seL4_Call operation on an endpoint and block waiting for a reply you are trusting that endpoint in a variety of ways. You trust that the messages will eventually get a reply and allow you to resume. You also trust that the message will eventually be received. If you want to perform an seL4_Call on an untrusted endpoint you will require a monitor thread that can handle a timeout and reset the calling thread if it is still blocked. In general, you want to avoid using endpoints where you can't trust that the message will be received and replied to in a timely manner. Asynchronous notifications do not suffer from this trust requirement so it is recommended that communication between mutually distrusting servers use shared memory and notifications. The client should seL4_Signal the server to notify a message has been sent via the shared memory and the server should signal in response to notify the client the message has been handled and the reply is in the shared memory. The problem of setting up a connection, sending the reply badged notification object to the server, acquiring a send notification object from the server, and mapping the shared memory would require either the connection being statically configured at process creation or dynamically configured by some mutually trusted shared component. Cheers, Curtis

1 0

Re: [seL4] camkes error.h include problem
by yogidk . 14 Jun '19

14 Jun '19

sorry, previous email sent by mistake. #include "sys/socket.h" actually solved the problem instead of only "socket.h" many thanks. Regards yk On Fri, Jun 14, 2019 at 10:30 AM yogidk . <yogidk(a)gmail.com> wrote: > thanks Kent and Peter, > > however if I remove > > > On Fri, Jun 14, 2019 at 2:14 AM Mcleod, Kent (Data61, Kensington NSW) < > Kent.Mcleod(a)data61.csiro.au> wrote: > >> > "../muslibc/include/sys"* // necessary for compilation as >> test_2.c has "socket.h"* >> This line shouldn't be here, and instead socket.h should be included via >> <sys/socket.h>. Otherwise many other include directives are going to match >> on the incorrect files. >> >> Kent. >> ------------------------------ >> *From:* Devel <devel-bounces(a)sel4.systems> on behalf of Chubb, Peter >> (Data61, Kensington NSW) <Peter.Chubb(a)data61.csiro.au> >> *Sent:* Friday, 14 June 2019 8:03 AM >> *To:* yogidk . >> *Cc:* devel(a)sel4.systems >> *Subject:* Re: [seL4] camkes error.h include problem >> >> >>>>> "yogidk" == yogidk <yogidk(a)gmail.com> writes: >> >> yogidk> and another file >> >> yogidk> test_2.c which includes "socket.h" >> >> yogidk> DeclareCAmkESComponent(test >> yogidk> INCLUDES "../muslibc/include/sys"* // necessary for >> yogidk> compilation as test_2.c has "socket.h"* >> >> This line means that "#include <errno.h>" picks up sys/errno.h instead >> of errno.h. >> >> Get rid of it. Instead, do '#include <sys/socket.h> instead of >> '#include <socket.h>' >> >> Peter C >> -- >> Dr Peter Chubb Tel: +61 2 9490 5852 >> http://ts.data61.csiro.au/ >> Trustworthy Systems Group Data61, CSIRO (formerly >> NICTA) >> _______________________________________________ >> Devel mailing list >> Devel(a)sel4.systems >> https://sel4.systems/lists/listinfo/devel >> >

1 0

camkes error.h include problem
by yogidk . 14 Jun '19

14 Jun '19

Hi , I have a test_1.c file which includes <camkes.h> camkes.h which is automatically generated has following includes #include <camkes/dataport.h> #include <camkes/error.h> #include <stdint.h> #include <stdlib.h> #include <utils/util.h> #include <platsupport/io.h> and another file test_2.c which includes "socket.h" In CMakeLists.txt, where I compile my test_1.c and test_2.c looks like this DeclareCAmkESComponent(test INCLUDES "../muslibc/include/sys"* // necessary for compilation as test_2.c has "socket.h"* SOURCES "test_1.c" "test_2.c" C_FLAGS -Wall -Werror LIBS seos_libs ) However when I compile , I start getting these errors: In file included from ../projects/util_libs/libplatsupport/include/platsupport/io.h:20:0, from projects/test/include/camkes.h:20, from ../projects/src/test_1.c:8: ../projects/musllibc/include/sys/errno.h:1:2: error: #warning redirecting incorrect #include <sys/errno.h> to <errno.h> [-Werror=cpp] *#warning redirecting incorrect #include <sys/errno.h> to <errno.h>* ^~~~~~~ In file included from ../projects/musllibc/include/sys/errno.h:2:0, from ../projects/util_libs/libplatsupport/include/platsupport/io.h:20, from projects/test/include/camkes.h:20, from ../projects/src/test_1.c:8: ../projects/musllibc/include/sys/errno.h:1:2: error: #warning redirecting incorrect #include <sys/errno.h> to <errno.h> [-Werror=cpp] #warning redirecting incorrect #include <sys/errno.h> to <errno.h> How could this be solved ? thanks --yk

3 2

Roadmap - Status
by Rutherford, Luke 08 Jun '19

08 Jun '19

I see these on your development road map. Any updates on the status of them? Development Roadmap Microkernel in progress 64-bit ARM virtualisation support branch Low-level Userland Status Date Feature Location planned SMP-capable virtual-machine monitor (VMM) master

3 2

Re: [seL4] xilinx ultrascale+: Spurious interrupt
by Shen, Yanyan (Data61, Kensington NSW) 05 Jun '19

05 Jun '19

Hi Leonid, One possible cause I can think of is the trigger type (level vs edge) of an interrupt is incorrect. The Linux device tree should have interrupt type for each interrupt source, so you can change the GIC init code to configure the interrupt types (GICD_ICFGR, assuming GICv2) accordingly and see if the messages disappear. Regards, Yanyan From: Devel <devel-bounces(a)sel4.systems> on behalf of Leonid Meyerovich <lmeyerovich(a)i-a-i.com> Date: Wednesday, 5 June 2019 at 4:28 am To: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: [seL4] xilinx ultrascale+: Spurious interrupt Hello Everybody, Petalinux is running on VM on the one of the core of Xilinx Ultrascale+ (A53) From time to time I see Spurious Interrupt message from seL4 kernel (handleInterruptEntry) <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff80080fa414]: Spurious interrupt!>> <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff80083e64bc]: Spurious interrupt!>> <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff800894cc98]: Spurious interrupt!>> Could somebody explain why it may happen? How to debug it? Thank you, Leonid ________________________________ 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.

1 0

xilinx ultrascale+: Spurious interrupt
by Leonid Meyerovich 05 Jun '19

05 Jun '19

Hello Everybody, Petalinux is running on VM on the one of the core of Xilinx Ultrascale+ (A53) >From time to time I see Spurious Interrupt message from seL4 kernel (handleInterruptEntry) <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff80080fa414]: Spurious interrupt!>> <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff80083e64bc]: Spurious interrupt!>> <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff800894cc98]: Spurious interrupt!>> Could somebody explain why it may happen? How to debug it? Thank you, Leonid ________________________________ 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.

1 0

回复: Devel Digest, Vol 60, Issue 18
by KIM MK 03 Jun '19

03 Jun '19

Hello Sel4 developer, Thanks for your support. Aditya and me are debugging physical memory sel4. Is there visual tool or analysis module or anything to debugging that physical memory to virtual mapping table. If you have any question, please let me know. BR, MK

2 2

Multicore for 64-bit ARM
by Rutherford, Luke 24 May '19

24 May '19

I see this on your roadmap: https://sel4.systems/Info/Roadmap/ planned Multicore for 64-bit ARM and x64 master Do you have any updates on when this will be implemented?

2 1

How to add conditional compilation in .Camkes files
by yogidk 21 May '19

21 May '19

Hi, I try to add support for UART on one platform and disable this UART for another platform. As my application is Camkes based, I need to define the UART connections (Dataport, Interface functions etc) between the 2 Camkes components. However I need to use the same application on another platform without UART support. How can this be got in .Camkes files ? I already tried including a .h file where I define something like this In main.h #ifdef PLATFORM_X #define UART 1 #else #define UART 0 #endif Then include main.h file in Camkes files using a .idl4 file . However it did not work. .Camkes file is not able to see these defines to use it further for conditional compilation in .camkes files to enable or disable UART between the two components. Is there any way to get it done ? Regards yk

2 4

Compiling seL4
by Yousif Kako 21 May '19

21 May '19

Hello, I am a student researcher, I am trying to compile seL4 using the Configuring and building an seL4 project guidelines on your website ( https://docs.sel4.systems/Developing/Building/Using) And on the site, it says that after the command "ninja", I will be given binaries in the folder "images". But, I do not get such folder nor any images. I tried re-configuring some settings using cmake-gui but still nothing. I am want to write a user-level application but I am not sure if I am going about this the right way. If you have any suggestions or if you can point me in the right direction, that would be great. Thank You

2 1

Compilation Errors for the MCS tutorial
by Zeyu Mi 21 May '19

21 May '19

Hi, I was trying the MCS tutorial but encountered a few compilation errors which I cannot resolve. And the previous tutorials can be compiled normally. The building environment is based on Docker, as recommended by the tutorials. Steps: 1. cd kernel 2. git fetch seL4 mcs-tutorials 3. git checkout mcs-tutorials 4. cd .. && ./init --tut mcs 5. cd mcs && ninja Compilation output about the errors: [79/161] Building C object projects/seL4_libs/libsel4utils/CMakeFiles/sel4utils.dir/src/elf.c.obj FAILED: projects/seL4_libs/libsel4utils/CMakeFiles/sel4utils.dir/src/elf.c.obj ccache /usr/bin/gcc --sysroot=/host/mcs_build -DHAVE_AUTOCONF -I../projects/seL4_libs/libsel4utils/include -I../projects/seL4_libs/libsel4utils/sel4_arch_include/x86_64 -I../projects/seL4_libs/libsel4utic ../projects/seL4_libs/libsel4utils/src/elf.c: In function ‘rights_from_elf’: ../projects/seL4_libs/libsel4utils/src/elf.c:35:12: error: too many arguments to function ‘seL4_CapRights_new’ return seL4_CapRights_new(false, false, canRead, canWrite); In file included from ../kernel/libsel4/include/sel4/types.h:30:0, from ../kernel/libsel4/include/sel4/sel4.h:16, from ../projects/seL4_libs/libsel4utils/src/elf.c:15: libsel4/include/sel4/shared_types_gen.h:317:1: note: declared here seL4_CapRights_new(seL4_Uint64 capAllowGrant, seL4_Uint64 capAllowRead, seL4_Uint64 capAllowWrite) [82/161] Building C object projects/seL4_libs/libsel4utils/CMakeFiles/sel4utils.dir/src/vspace/bootstrap.c.obj FAILED: projects/seL4_libs/libsel4utils/CMakeFiles/sel4utils.dir/src/vspace/bootstrap.c.obj ccache /usr/bin/gcc --sysroot=/host/mcs_build -DHAVE_AUTOCONF -I../projects/seL4_libs/libsel4utils/include -I../projects/seL4_libs/libsel4utils/sel4_arch_include/x86_64 -I../projects/seL4_libs/libsel4utic In file included from ../projects/seL4_libs/libsel4utils/src/vspace/bootstrap.c:20:0: ../projects/seL4_libs/libsel4utils/src/vspace/bootstrap.c: In function ‘common_init_post_bootstrap’: ../projects/seL4_libs/libsel4utils/include/sel4utils/vspace.h:43:43: error: ‘seL4_UserTop’ undeclared (first use in this function) #define KERNEL_RESERVED_START (ALIGN_DOWN(seL4_UserTop, PAGE_SIZE_4K)) Thanks in advance. Zeyu

2 5

Changing initial thread cnode guard
by Clifford, Alexandra - 0553 - MITLL 16 May '19

16 May '19

I am attempting to prototype an seL4 based system that ideally will have multiple threads, each with their own CSpaces which are each a tree e.g. not rooted in the initial cnode. My strategy here is to 1. chain new cnodes off of the initial cnode in the initial thread, and 2. Create a new thread TCB etc., revoke the initial cnode caps and set the new cnode cap as it’s own cnode root in that new thread. I have run into some issues at step 1 and am writing to ask if this is a viable strategy. Perhaps I am misunderstanding something but chaining in this way does not seem possible if all 32 bits are to be resolved in searching the initial cnode, so I am not certain if this strategy will work. Is it possible to configure the initial cnode guard to be something other than 32 bits? I have searched through the config of the kernel and cannot find some easily changed parameter for compile time, and for runtime I have tried to use the TCB_SetSpace and TCB_Configure on the initial thread to change the guard but this has lead to other problems. If I set it to something like 16, does this mean that all of the slot indices in the bootinfo struct are no longer valid as being set at 0x0, 0x1, etc and now will be at half word indices? It is very unclear to me from the documentation how this works but perhaps I am missing something. Setting it to something like 4 leads to an explicit TCB illegal operation and something larger like 19 returns seL4_Error 3 illegal op when I try to create new cnodes via untyped_retype from the init cnode. Is there something obvious that I am missing? I wonder if this is even possible—having cnodes not rooted in the initial cnode. Or if it is possible, is there some other mechanism to create a new cnode that is not rooted in the initial cnode? It is also probably important to note that due to constraints I am not able to use any of the nice sel4_libs provided to help with this. Thanks very much in advance for any help. Alexandra Clifford, MS 05-53 Secure Resilient Systems and Technology MIT Lincoln Laboratory 244 Wood st., Lexington MA 02421 Email: Alexandra.Clifford(a)ll.mit.edu

2 1

Possible newbie question: What are ".bf"-files belonging to the seL4 code base?
by Mike Epoch 15 May '19

15 May '19

Hi! I am new to this list so please forgive me if this question has been asked before. The seL4 code base contains a slew of files with a file type of "bf". These files seem to define packed structs that are to fit into words or d-words. An example of that would be file kernel/libsel4/mode_include/64/sel4/shared_types.bf which can be obtained (as part of an entire source tree, of course) via repo init -u https://github.com/seL4/sel4test-manifest.git followed by repo sync. What I find curious is that these files do not adhere to (common) C syntax yet they are fed into GCC and GCC swallows them. This file format appears to be an extension to GCC. I could not find any documentation on any such extension. I would be grateful if anyone could point me to some kind of documentation pertaining to it. Regards Mike

3 5

Using ARM GIC Virtualization Extensions with seL4
by dan pittman 10 May '19

10 May '19

Hi all! I'm currently trying to understand something about the use of the virtualization extensions available in the PL-400 interrupt controller in seL4. It all starts with this sentence: > The hypervisor supports virtualization also by using address translation tables to trap accesses that the virtual machines make to the virtual distributor. The hypervisor determines the effect of these accesses and might typically update the virtual interface control registers as a result. Source: http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.ddi0471b/CHDIHI… My interpretation of this is that by using the IPA which is available with arm hyp, the hardware can trap accesses to the GIC from the guest and "redirect" those accesses to the physical GIC. From this, I draw the conclusion that the need for a completely virtualized GIC when using these extensions is not necessary. However, in seL4—due to the way in which it manages interrupts by handling the hardware interactions itself and instead invoking an endpoint—the use of these extensions in this way is not possible. I'm curious if this understanding is correct, and if not, I welcome any clarity y'all can provide! cheers, dan

2 1