- Devel - lists.sel4.systems

Syscall errors with musl
by Rinat Dobrokhotov 21 Nov '16

21 Nov '16

Hi all, I have written simple programme which gets system time. I get syscall errors when programm is calling gettimeofday function: *main.c:* #include <time.h> #include <sys/time.h> #include <stdlib.h> #include <stdio.h> int main(int argc, char *argv[]) { int iterations = 1000000; struct timeval start, end; gettimeofday(&start, NULL); for (int i = 0; i < iterations; i++) { } gettimeofday(&end, NULL); printf("%ld\n", ((end.tv_sec * 1000000 + end.tv_usec) - (start.tv_sec * 1000000 + start.tv_usec))); return 0; *Errors:* libsel4muslcsys: Error attempting syscall 263 libsel4muslcsys: Error attempting syscall 78 Could you tell me where I mistook? -- Best regards, Rinat Dobrokhotov

2 1

seL4RPC vs seL4RPCCall?
by Andrew Gacek 18 Nov '16

18 Nov '16

What's the difference between seL4RPC and seL4RPCCall in CAmkES? Is there documentation on the various connectors somewhere? Thanks, Andrew

2 1

Send input to seL4 in QEMU
by Andrew Gacek 18 Nov '16

18 Nov '16

Hi, We are developing an seL4 application that will process UDP packets coming in over a network connection. Eventually, we'll be running this on real hardware with real drivers, but for now we are using QEMU. We have a python script that can generate packet payloads. Is there a way to send this information into QEMU so that we can develop our seL4 application without having the drivers and hardware in place? If it matters, we are using CAmkES as well. Thanks, Andrew

2 3

seL4 Kernel Profiler
by Chris Guikema 18 Nov '16

18 Nov '16

Hello, I am working on a Code Profiler for use in seL4 Systems. I see that the Kernel already has some form of profiling/benchmarking functionality built in. However, I do not see anything in the documentation that covers how this is used. Is there a guide that I can follow to get the kernel profile functional? Thanks Chris Guikema

2 1

Will seL4_Word ever be anything but uintptr_t?
by Corey Richardson 17 Nov '16

17 Nov '16

I guess this is a somewhat philosophical question. It's come up a bit in the Rust libs I've been writing. Casting from pointer-sized things to *specifically* u32/u64 is bit tiresome for the places where I can't abstract over that. -- cmr http://octayn.net/ +16038524272

2 1

seL4 on i.MX53
by Yevgeny Lavrov 15 Nov '16

15 Nov '16

Hello. I've multiple ARM devices at my disposal that I want to use to experiment with seL4, one of them is USB Armory (Architecture: ARMv7 Cortex-A8 Processor: i.MX53 800MHz). Before I get into it, I would like to know if seL4 supports this ARM device. Thanks

2 1

Unable To Map Physical Frame
by Mark Reus 13 Nov '16

13 Nov '16

Hi I want to map the arm global timer which is located at memory location 0xF8F00200 . However, when I am trying to get the physical frame using : error = simple_get_frame_cap(&simple, (void*)global_timer_paddr, 12, &ep_cap_path); if (error) { ZF_LOGE("Failed to find frame at paddr %p\n", global_timer_paddr); return error; } I get the Error Statement on stduout as "main@main.c:209 Failed to find frame at paddr 0xf8f00200" If i print the bootinfo during bootup, I can see that I have access to this region 0xf8000000 | 00000012 | [520 <--> 521 ] Can someone help me as why this issue may be caused? I know that this global timer is said to be mapped in the private region. But I do not what exactly that means and if we cannot do it. Regards Mark

2 1

malloc and SCHED0004
by Vasily A. Sartakov 05 Nov '16

05 Nov '16

Greetings. I am keep working, and now I would like to discuss my second memory-related issue. In contrast with first one, the second issue happens only in SCHED004 test, in malloc function: helper_thread_t **threads = (helper_thread_t **) malloc(sizeof(helper_thread_t*) * NUM_PRIOS); malloc dies because there is no record inside TLB. someone tries to write something to an address, for example, 0x54f1c8. This address is important because it is located outside of the virtual memory allocated for the test. Previous, elf_loader allocates a region and the region ends exactly on 0x54efff. I have experimented with different setups, added some debug functions, and each time I saw the same picture: malloc dies because tries to write to next page outside the allocated region. I know what is the function tries to write. It is a pretrim, part of libmuslc: static int pretrim(struct chunk *self, size_t n, int i, int j) { size_t n1; struct chunk *next, *split; /* We cannot pretrim if it would require re-binning. */ if (j < 40) return 0; if (j < i+3) { if (j != 63) return 0; n1 = CHUNK_SIZE(self); if (n1-n <= MMAP_THRESHOLD) return 0; } else { n1 = CHUNK_SIZE(self); } if (bin_index(n1-n) != j) return 0; next = NEXT_CHUNK(self); printf("next - %x, n1 = %x\n", next, n1); split = (void *)((char *)self + n); <————— the split points outside the allocated region split->prev = self->prev; <————— here we die split->next = self->next; split->prev->next = split; split->next->prev = split; split->psize = n | C_INUSE; split->csize = n1-n; next->psize = n1-n; self->csize = n | C_INUSE; return 1; } As a previous, I would like to ask, should I keep in mind something platform specific? maybe you have modified, like a_and asm functions or something else in libmuslc? Also, malloc itself raises questions: void *malloc(size_t n) { struct chunk *c; int i, j; if (adjust_size(&n) < 0) return 0; <….> i = bin_index_up(n); for (;;) { uint64_t mask = mal.binmap & -(1ULL<<i); mal.binmap is used uninitialised. also, when we set up bits inside it? Moreover, I have different values on ARM (0x80000000000) and MIPS (0x8000000000000000), I am not sure that it is ok Thank you! -- Vasily A. Sartakov sartakov(a)ksyslabs.org

2 6

Timer for Performance Measurement
by Andrew Mine 04 Nov '16

04 Nov '16

Hi Is there any inbuilt library to get the time like get_time in seL4? I want to measure IPC performance and overheads for my tasks. Regards Andrew

1 0

Does anyone use recycle?
by Adrian.Danis＠data61.csiro.au 03 Nov '16

03 Nov '16

Hi All, If you do not know what recycle is and/or have not used it then you can probably ignore this e-mail. We are considering removing the recycle operation from cnodes, and replacing it with a 'revoke badges' operation. Currently the semantics of recycle are ill defined but can generally be summed up as "put an object back into its initial state". It turns out this is not particularly useful, and is completely unused by us. The proposal is to remove this and have an invocation that will only operate on endpoints and will remove any badged versions of that endpoint, hence the name 'revoke badges'. This is the current semantics of recycling an endpoint, and we see this as the only useful thing recycle does, hence the desire to keep it around. Whilst we do not use recycle we would like to first find out if anybody in the community is using recycle, or has a strong argument for why they would like it to stay. If this is you, please let us know, otherwise we will continue with our plans for removal. Adrian

5 11

need ideas
by Vasily A. Sartakov 02 Nov '16

02 Nov '16

Hello. I have a problem. It is a very complicated problem. I understand that It is hard to give an advice without looking into the sources. But I am stuck and need some ideas in ‘brainstorm’ format as an input for me. So, here is the problem: There are many tests from sel4test suit are working. This is how does it look like: http://pastebin.com/vvnDaUe9 Unfortunately, I found several configurations of the tests, which causes crashes with stable and different symptoms. One of them is looking following: 11 #include <sel4test/test.h> 12 #include "../test.h" 13 #include "../helpers.h" 14 15 #define MIN_EXPECTED_ALLOCATIONS 100 16 17 18 19 20 21 22 23 int test_allocator(env_t env) 24 { 25 /* Perform a bunch of allocations and frees */ 26 vka_object_t endpoint; 27 int error; 28 29 for (int i = 0; i < MIN_EXPECTED_ALLOCATIONS; i++) { 30 error = vka_alloc_endpoint(&env->vka, &endpoint); 31 test_assert(error == 0); 32 test_assert(endpoint.cptr != 0); 33 vka_free_object(&env->vka, &endpoint); 34 } 35 36 return sel4test_get_result(); 37 } 38 DEFINE_TEST(TRIVIAL0001, "Ensure the allocator works", test_allocator) 39 DEFINE_TEST(TRIVIAL0002, "Ensure the allocator works more than once", test_allocator) as you might see, this is little bit modified version of trivial.c tests. Usual, when I am testing all tests, there is no problem with this test. But when I am running this file alone, I have a problem. Also, you might see, that there are several free lines with numbers from 16 to 22. I made this not accidental, it is a source of error. If the test_allocator(env_t env) is lockated in the 23rd line, this tests has no problem. But if I add one more free line, I have an error like this: Starting test suite sel4test Starting test 0: TEST_TRIVIAL0001 TEST_TRIVIAL0001 726:trap!, address error on store! $0 : 0 fffffff8 7 10089000 $4 : 6a6ffc 3f 0 ffffffff $8 : 1 7 1 20 $12 : 70f 0 2 6ae $16 : 6a6ffc 5a6a50 ffffff30 6a6ffc $20 : 3f 5a6e58 5a6a50 6a6fdc $24 : 20 41bab0 0 0 $28 : 0 100848d8 fffffffe 41faf0 Hi : 20 Lo : 0 epc : 41f818 fi : 41f814 ra : 41faf0 Status: 20000002 Cause : 414 Config: 80008482 BadVaddr: f which means, that the test-drivers (I know the ASID) tries to store something to the address 0x0000000f by the instruction located in the 0x41f818 (EPC). Also, it is failed before the starting of trivial.c test! This is what I on the address: 0041f7b4 <unbin>: 41f7b4: 8c83000c lw v1,12(a0) 41f7b8: 27bdffd8 addiu sp,sp,-40 41f7bc: 8c820008 lw v0,8(a0) 41f7c0: afb0001c sw s0,28(sp) 41f7c4: 00808021 move s0,a0 41f7c8: afbf0024 sw ra,36(sp) 41f7cc: 1462000e bne v1,v0,41f808 <unbin+0x54> 41f7d0: afb10020 sw s1,32(sp) 41f7d4: 00a03021 move a2,a1 41f7d8: 00002021 move a0,zero 41f7dc: 0c107afa jal 41ebe8 <.pic.__ashldi3> 41f7e0: 24050001 li a1,1 41f7e4: 3c04005a lui a0,0x5a 41f7e8: 00022827 nor a1,zero,v0 41f7ec: 24846a50 addiu a0,a0,27216 41f7f0: 0c107dac jal 41f6b0 <a_and> 41f7f4: 00038827 nor s1,zero,v1 41f7f8: 3c04005a lui a0,0x5a 41f7fc: 02202821 move a1,s1 41f800: 0c107dac jal 41f6b0 <a_and> 41f804: 24846a54 addiu a0,a0,27220 41f808: 8e030008 lw v1,8(s0) 41f80c: 8e02000c lw v0,12(s0) 41f810: 8fbf0024 lw ra,36(sp) 41f814: 8fb10020 lw s1,32(sp) 41f818: ac430008 sw v1,8(v0) I am quite sure that there is no problem here with unbin function, and the problem somewhere with contexts, or alignment or something else. Also, I am mapping this area RO, so I am also sure that there is no corruption of the user-space regions. Also, I see, that there is a correlation between size of the image and faults: 1349892 ./sel4test-tests.bin_23 1349900 ./sel4test-tests.bin_24 The border line is 1349900 if I have a size of the image below the value -- there is no problem. Unfortunately, 1349900 is not a 'round' value, somehow related to TLB sizes of something else what I know. Also, I should mention, that 'key' variable wich changes when I add new line is an argument of _sel4test_failure: mips-mti-linux-gnu-objdump -d sel4test-tests.bin_23 > bin23.asm mips-mti-linux-gnu-objdump -d sel4test-tests.bin_24 > bin24.asm diff -ua bin23.asm bin24.asm Disassembly of section .init: @@ -3143,7 +3143,7 @@ 4030f0: 3c050043 lui a1,0x43 4030f4: 2484c248 addiu a0,a0,-15800 4030f8: 24a5c964 addiu a1,a1,-13980 - 4030fc: 2406001f li a2,31 + 4030fc: 24060020 li a2,32 403100: 0c107b51 jal 41ed44 <_sel4test_failure> 403104: 0000f021 move s8,zero 403108: 8fbf0074 lw ra,116(sp) @@ -3383,7 +3383,7 @@ 4034b0: 2484c950 addiu a0,a0,-14000 4034b4: 24a5c964 addiu a1,a1,-13980 4034b8: 0c107b51 jal 41ed44 <_sel4test_failure> - 4034bc: 24060020 li a2,32 + 4034bc: 24060021 li a2,33 4034c0: 03c01021 move v0,s8 4034c4: 8fbf0074 lw ra,116(sp) 4034c8: 8fbe0070 lw s8,112(sp) That is all that I have now. Any ideas? Now I do not see any other choice but to gradually reduce the amount of code with keeping this 'border' situation, until I will not have very small set of system functions. Thank you -- Vasily A. Sartakov sartakov(a)ksyslabs.org

2 3

Configuring Process Issue
by Andrew Mine 28 Oct '16

28 Oct '16

Hi I am working with Zynq based seL4 and currently have written an app which configures two processes using sel4utils_configure_process. Both my other processes are apps that are also elf files generated during the build. I have noticed that when I am configuring two processes in the root task as 102: sel4utils_process_t process1,process2; 103: error = sel4utils_configure_process(&process1, &vka, &vspace, seL4_MaxPrio, PROCESS1_IMAGE_NAME); 104: assert(error == 0); 105: 106: error = sel4utils_configure_process(&process2, &vka, &vspace,seL4_MaxPrio, PROCESS2_IMAGE_NAME); 107: assert(error == 0); The code compiles but I get a runtime error as _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark vka_alloc_object@object.h:51 Failed to allocate object of size 4096, error 1 _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark new_pages_at_vaddr@vspace.c:325 Failed to allocate page load_segment@elf.c:82 ERROR: failed to allocate frame by loadee vka: 10 _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark sel4utils_elf_load_record_regions@elf.c:272 Failed to load segment sel4utils_configure_process_custom@process.c:550 Failed to load elf file _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark sel4utils_configure_process_custom@process.c:593 Could not clean up vspace Assertion failed: error == 0 (latest-sel4-tutorial/apps/zynq-comm/src/main.c: main: 107) If I remove any one of the process from the root process, it actually works and my process gets launched. I am assuming there is some conflict when the elf is being loaded as both processes are elf files. Regards Andrew

1 0

CallWithMRs is an unexercised code path
by Jeff Waugh 27 Oct '16

27 Oct '16

Hi all, Last night I opened two pull requests to begin fixing the CallWithMRs code path on x86_64 and aarch32. syscall_stub_gen.py couldn't generate x86_64 stubs for the CallWithMRs / non-IPCBuffer path. That didn't surprise me too much, as x86_64 support is relatively new. Then I discovered that libsel4 *always* [1] uses the IPCBuffer path. Hrm. Changing that prompted a quick fix to aarch32's apparently unused, long since even built CallWithMRs. (Similar fixes might be needed in some of the other functions.) The test suite failed with it on aarch32, which I could poke at in more depth, but it worked fine for x86_64. So… what's the status of the *WithMRs functions? Based on my understanding of the source (particularly the new helper functions) and assembly output, they're destined for the chopping block, right? Thanks, Jeff [1] hard coded --buffer parameter to syscall_stub_gen.py in libsel4/Makefile, since late 2015

2 6

Build Error
by Andrew Mine 27 Oct '16

27 Oct '16

Hi I have used sel4-tutorial branch earlier and was able to build and run earlier. I realized that my branch is way behind, so I have cloned the new branch into a separate folder and am compiling for zynq device. I get the following build error: [apps/hello-1] building... [HEADERS] [STAGE] autoconf.h [CC] src/main.o [CC] src/util.o [LINK] hello-1.elf sel4tutorials/stage/arm/zynq7000/lib/libsel4.a: error adding symbols: Archive has no index; run ranlib to add one collect2: error: ld returned 1 exit status make[1]: *** [hello-1.elf] Error 1 make: *** [hello-1] Error 2 Is anyone else facing this issue? I am using arm-none-eabi-gcc for compiling. Regards Andrew

2 1

Allocman Error
by Neelesh Vemula 26 Oct '16

26 Oct '16

Hi I have created a new process from the root/init task. In the new process I have the following code for initializing the allocman as below: vka_t vka; allocman_t *allocman; vspace_t vspace; #define ALLOCATOR_STATIC_POOL_SIZE ((1 << seL4_PageBits) * 10) UNUSED static char allocator_mem_pool[ALLOCATOR_STATIC_POOL_SIZE]; #define ALLOCATOR_VIRTUAL_POOL_SIZE ((1 << seL4_PageBits) * 100) int main(int argc, char **argv) { allocman = bootstrap_use_current_1level(SEL4UTILS_CNODE_SLOT, CONFIG_SEL4UTILS_CSPACE_SIZE_BITS, 0, (1u << CONFIG_SEL4UTILS_CSPACE_SIZE_BITS), ALLOCATOR_STATIC_POOL_SIZE, allocator_mem_pool); allocman_make_vka(&vka, allocman); vka_object_t ep_object = {0}; error = vka_alloc_endpoint(&vka, &ep_object); ZF_LOGF_IFERR(error, "Failed to allocate new endpoint object.\n"); I have the following definition structure shared as enum sel4utils_cspace_layout { /* * The root cnode (with appropriate guard) */ SEL4UTILS_CNODE_SLOT = 1, /* The slot on the cspace that fault_endpoint is put if * sel4utils_configure_process is used. */ SEL4UTILS_ENDPOINT_SLOT = 2, SEL4UTILS_PD_SLOT = 3, FREE_SLOT = 4, }; This particular program has compiled for zynq-7000 platform and when running it I get the following output in the stdout : Just entered the user function vka_alloc_object@object.h:51 Failed to allocate object of size 16, error 1 Assertion failed: error == 0 (/apps/zynq-comm-user/src/main.c: main: 71) I have been not able to figure out why this error is occurring. I can only guess that the allocman was not initialized properly. Can someone help me with what I may have done wrong? Regards Neelesh Vemula

2 1

Exynos Arndale 5420 support
by Yevgeny Lavrov 26 Oct '16

26 Oct '16

Hello. Exynos Arndale 5250 is listed as seL4 supported ARM devices. I would like to know if seL4 also supports Exynos Arndale 5420 board, and if it does, then would the process of mounting seL4 onto Arndale 5420 be the same as with 5250? Thanks

2 1

seL4 Call Issue
by Chris Guikema 26 Oct '16

26 Oct '16

Hello, I am working on a lock system using templates (based on what is found here: https://github.com/seL4/camkes/tree/master/apps/mutex) This system can work, but there are some issues with the components just going back and forth when calling the locks. I believe this is an issue with multiple components using the same endpoint to communicate with the "lock server" and the calls getting pre-empted by other threads. Here are the system calls that are used to hit the endpoint with the (un)lock request. seL4_Send(/*? ep ?*/, info); info = seL4_Recv(/*? ep ?*/, NULL); And in the lock server: seL4_MessageInfo_t info = seL4_Recv(/*? ep ?*/, &sender); ...do locking things seL4_Send(/*? ep ?*/, info); So in order to prevent preempting by other threads, I went and changed the (un)lock request system call to info = seL4_Call(/*? ep ?*/, info); Using print statements, I was able to determine that the lock server receives the proper message on the endpoint and performs the locking operations. However, when it reaches the seL4_Send operation, the system locks up. This shouldn't be the case, because one component is waiting on the endpoint with the seL4_Call, and the other is sending information on the same endpoint, especially when having separate Send & Recv statements works. Am I doing something incorrect? Thanks for your help, Chris Guikema

1 0

Starting Threads in New seL4Utils processes.
by Richard Habeeb 25 Oct '16

25 Oct '16

Hello all, I am using seL4Utils to create some new processes. For these I am also transferring capabilities to some untyped kernel memory so that those processes can start their own worker threads and make endpoints. I've managed to get those threads started; however, I am a bit confused about how the CSpace is laid out now. My problem is that I want these worker threads to have capabilities to an endpoint created by the child process, but I can't figure out how to copy the cap. This is my TCB configure line. error = seL4_TCB_Configure(THREAD_2_CAP, seL4_CapNull, seL4_MaxPrio, SEL4UTILS_CNODE_SLOT, seL4_NilData, SEL4UTILS_PD_SLOT, seL4_NilData, ipc_buffer_vaddr, THREAD_2_IPC_BUF_CAP); Any guidance is appreciated. Thanks. -- Richard Habeeb Research Assistant, Computer Science, USF http://habeebr.bitbucket.org/

1 1

timers in seL4
by Horace Blanc 24 Oct '16

24 Oct '16

Hi, I am trying to understand the timer design of both seL4 as a kernel and as a hypervisor on ARM architecture. I understand that in both cases, seL4 uses a timer in order to preempt its threads. This means that seL4 must keep the control over that timer and cannot let threads use it directly. I also understand that seL4 does not provide any timer API to its threads. It seems then that the intended use is to implement a timer driver in userland in order for other application to access timing functions. But this timer driver cannot access the same timer as seL4. Does this mean that at least two physical timers (or at least two physical timer interfaces) are necessary? ARM virtualization extensions offers a virtual timer to be used by VMs and which is implemented with an offset register. They also offer different timers (one for an hypervisor, one for kernel/application and one for the virtual timer). It seems that the current seL4 as a hypervisor project does not use these extenstions. Do they? If not why? Thank you for your answers

1 0

Freelance
by Marco Reus 22 Oct '16

22 Oct '16

Hi I apologize if this is not the right platform to reach people. But I am looking for a freelancer who has some expereince in working with seL4 kernel. I need some aid in implementation of a project. Regards Vicky

1 0

Larger badges on 64-bit?
by Corey Richardson 21 Oct '16

21 Oct '16

Is there a future in which we recover the extra 32+ bits of padding on 64-bit systems for use in badges? In Robigalia, 28 bit badges are extremely limiting for what we want to use them for. -- cmr http://octayn.net/

2 1

CAmkES Groups
by Robert VanVossen 19 Oct '16

19 Oct '16

Hello, I have been trying to get groups with CAmkES 2.2 working, but it doesn't look like it will build correctly. At first, when I place components in a group, I get that there is an unresolved reference to one of the components during compilation. I was able to get past this by moving the function assign_address_spaces in camkes/camkes/runner/Transforms.py from POST_RESOLUTION to PRE_RESOLUTION, but after that I still ran into some issues: [LD] MyGroup_group_bin if [ 2 -eq 1 ]; then cp "comp1.instance-copy.bin" " MyGroup_group_bin"; else /usr/bin/ccache arm-xilinx-eabi-gcc comp1.instance-copy.bin comp2.instance-copy.bin -Wl,--build-id=none -L<stage_dir>/lib -Wall -nostdinc -std=gnu11 -O2 -D_XOPEN_SOURCE=700 -marm -Wtrampolines -mcpu=cortex-a9 -g -Wno-main -fno-stack-protector -Wl,--start-group -lsel4 -lsel4debug -lc -lsel4muslccamkes -lsel4camkes -lsel4sync -lutils -lsel4vka -lsel4utils -lsel4platsupport -lplatsupport -lsel4vspace -lgcc -Wl,--end-group -static -nostdlib -u _camkes_start -e _camkes_start -o MyGroup_group_bin; fi <stage_dir>/lib/libsel4camkes.a(crt0.o): In function `_camkes_start': (.text+0x6c): undefined reference to `_start' Any insight on this? Are groups supported yet? Thanks, Robbie VanVossen

2 1

SDHC driver in Sabre Lite
by Norrathep Rattanavipanon 19 Oct '16

19 Oct '16

Is there any example on how to use sdhc driver in ( https://github.com/SEL4PROJ/projects_libs/tree/master/libsdhcdrivers)? Currently, I'm struggling to read a block of data from micro-sd in seL4. I use the following code (assertions are omitted here for readability) to instantiate the driver : ps_io_mapper_t io_mapper = {0}; error = sel4platsupport_new_io_mapper(simple, vspace, vka, &io_mapper); ps_dma_man_t dma_man = {0}; error = sel4utils_new_page_dma_alloc(&vka, &vspace, &dma_man); ps_io_ops_t io_ops = { .io_mapper = io_mapper, .dma_manager = dma_man }; sdio_host_dev_t* dev = (sdio_host_dev_t*) malloc(sizeof(*dev)); assert(dev != NULL); memset(dev,0, sizeof(*dev)); enum sdio_id id = sdio_default_id(); error = sdio_init(id, &io_ops, dev); mmc_card_t* mmc_card = (mmc_card_t*) malloc(sizeof(*mmc_card)); error = mmc_init(dev, &io_ops, mmc_card); void* vaddr = (void*) 0x1980000; uintptr_t paddr = (uintptr_t) 0x119a7000; long read_len = mmc_block_read(*mmc_card, 0, 5, vaddr, paddr, NULL, NULL); And the code's stuck in mmc_block_read function where interrupt status (BRR and BWR) are never on. Thanks in advance, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

3 5

Missing untypeds on x86?
by Jeff Waugh 19 Oct '16

19 Oct '16

Hi all, Using x86 master on qemu with 2G memory, the kernel's map looks good: Parsing GRUB physical memory map Physical Memory Region from 0 size 9fc00 type 1 Physical Memory Region from 9fc00 size 400 type 2 Physical Memory Region from f0000 size 10000 type 2 Physical Memory Region from 100000 size 7fee0000 type 1 Adding physical memory region 0x100000-0x1fc00000 Physical Memory Region from 7ffe0000 size 20000 type 2 Physical Memory Region from fffc0000 size 40000 type 2 But the largest physical address of non-device untyped I get from bootinfo is 0x1faf9000. Same at 1G to 3G, though it does the right thing at 128M. On the other hand, x86_64 looks fine with 0x7ffc0000, and adapts to more. btw, very exciting to see x86_64 code land! Working well so far. Thanks, Jeff

2 1

question about adding device to ARM VM linux
by PX 18 Oct '16

18 Oct '16

Hi, all I have a question about adding a device to ARM VM linux. When a device is added to the vmlinux, two functions, map_device () and map_ram () are invoked. I don't understand the purpose of map_ram(). In map_device(), the capacity to the device is used to set up the mapping between a virtual address and the MMIO (of the device). Then, in the map_ram (), a capacity to the virtual address is allocated. I am confused because the virtual address is already mapped to the mmio of the device. why do we need to allocate a capacity for the virtual address? Should the capacity be the same as the one for the device? Thanks Peng

1 0

Benchmark results?
by Corey Richardson 18 Oct '16

18 Oct '16

Hello, Are there any public results from sel4bench, or should I get my own numbers for some hardware? -- cmr http://octayn.net/

2 1

adding code to the main.c for ARM VMM
by PX 18 Oct '16

18 Oct '16

Hi, I have posted this question before and my problem is not totally solved because I am not familiar with Makefile. I try to make my question more specific as follows. I want to add new code, which is already organized under a directory, say, test. I want to add the directory test to main.c file for ARM VMM, located at ~/projects/vm/apps/vm/components/VM/src/main.c. In the program, we want to refer to the sub-directories by relative path to the directory test. what is the easy to do that? How can we add the directory test to the search path so that we can include the header files by the relative path to the directory test, say include "test1/test1.h"? We tried to modify the makefile at ~projects/vm/apps/vm, but we have to add all the sub-directories, and there are problems for the files with the same name under different directories. thanks Peng

2 1

Re: [seL4] endpoint.c
by Vasily A. Sartakov 18 Oct '16

18 Oct '16

> we take address that causes syscall from the ksCurThread and set them back. Thus, FaultInstruction should point to something different, right? > I have add FaultInstruction in the same manner as it made in ARM platform: sub lr, lr, #4 /* Store FaultInstruction */ str lr, [sp, #(PT_FaultInstruction - PT_LR_svc)] I am tacking address of an instruction causes exception, subtract 4 from the value, and save it into the FauiltInstruction. Now get* and set* functions are: word_t PURE getRestartPC(tcb_t *thread) { return getRegister(thread, FaultInstruction); } void setNextPC(tcb_t *thread, word_t v) { setRegister(thread, CP0_EPC, v); } Also, Faultinstruction is part of frameRegisters and «linked» with cp0_epc of seL4_UserContext (sel4arch.xml) Now both tests are passed: Starting test 27: TEST_RECYCLE0001 TEST_RECYCLE0001 Running test RECYCLE0001 (Basic endpoint recycle testing.) <<seL4 [decodeInvocation/609 T0x8fee3f00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #101.>> <<seL4 [decodeInvocation/609 T0x809a1500 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #163.>> <<seL4 [decodeInvocation/609 T0x809a1700 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #230.>> <<seL4 [decodeInvocation/609 T0x809a1900 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #303.>> <<seL4 [decodeInvocation/609 T0x809a1b00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #364.>> <<seL4 [decodeInvocation/609 T0x809db100 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #428.>> <<seL4 [decodeInvocation/609 T0x809db300 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #491.>> <<seL4 [decodeInvocation/609 T0x809db500 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #564.>> <<seL4 [decodeInvocation/609 T0x809db700 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #619.>> <<seL4 [decodeInvocation/609 T0x809db900 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #694.>> <<seL4 [decodeInvocation/609 T0x809dbb00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #761.>> <<seL4 [decodeInvocation/609 T0x809dbd00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #828.>> <<seL4 [decodeInvocation/609 T0x809dbf00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #831.>> <<seL4 [decodeInvocation/609 T0x8fe29100 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #898.>> <<seL4 [decodeInvocation/609 T0x8fe29300 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #965.>> <<seL4 [decodeInvocation/609 T0x8fe29500 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1032.>> <<seL4 [decodeInvocation/609 T0x8fe29700 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1099.>> <<seL4 [decodeInvocation/609 T0x8fe29900 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1170.>> <<seL4 [decodeInvocation/609 T0x8fe29b00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1221.>> <<seL4 [decodeInvocation/609 T0x80a13100 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1295.>> <<seL4 [decodeInvocation/609 T0x80a13300 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1354.>> <<seL4 [decodeInvocation/609 T0x80a13500 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1427.>> <<seL4 [decodeInvocation/609 T0x80a13700 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1490.>> <<seL4 [decodeInvocation/609 T0x80a13900 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1563.>> <<seL4 [decodeInvocation/609 T0x80a13b00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1628.>> <<seL4 [decodeInvocation/609 T0x80a13d00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1635.>> <<seL4 [decodeInvocation/609 T0x80a13f00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1698.>> <<seL4 [decodeInvocation/609 T0x80aa1100 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1765.>> <<seL4 [decodeInvocation/609 T0x80aa1300 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1828.>> <<seL4 [decodeInvocation/609 T0x80aa1500 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1897.>> <<seL4 [decodeInvocation/609 T0x80aa1700 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1966.>> <<seL4 [decodeInvocation/609 T0x80aa1b00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #2033.>> Test RECYCLE0001 passed Starting test 28: TEST_RECYCLE0002 TEST_RECYCLE0002 Running test RECYCLE0002 (Recycle deletes caps) <<seL4 [decodeInvocation/609 T0x809a1500 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #165.>> <<seL4 [decodeInvocation/609 T0x809a1500 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #165.>> <<seL4 [decodeInvocation/609 T0x809a1700 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #231.>> <<seL4 [decodeInvocation/609 T0x809a1500 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #165.>> <<seL4 [decodeInvocation/609 T0x809a1700 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #231.>> <<seL4 [decodeInvocation/609 T0x809a1900 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #297.>> <<seL4 [decodeInvocation/609 T0x809a1500 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #165.>> <<seL4 [decodeInvocation/609 T0x809a1700 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #231.>> <<seL4 [decodeInvocation/609 T0x809a1900 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #297.>> <<seL4 [decodeInvocation/609 T0x809a1b00 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #361.>> <<..> <<seL4 [decodeInvocation/609 T0x80a90700 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #2003.>> <<seL4 [decodeInvocation/609 T0x80a90900 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #2073.>> <<seL4 [decodeInvocation/609 T0x80a90b00 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #2131.>> <<seL4 [decodeInvocation/609 T0x80a90f00 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #2203.>> Test RECYCLE0002 passed Can you please tell me something about the Faultinstruction context field, and, in general, what the assumptions about the behaviour of CPU you put into the design. For example, in MIPS, in a case of a trap, EPC points on instruction causes a trap, but in a case of an interrupt, PC and further EPC points on next instruction. Should I take this into the account somewhere in the kernel? > >> Hope that helps. >> >> Regards, >> Hesham >> ________________________________________ >> From: Devel <devel-bounces(a)sel4.systems> on behalf of Vasily A.Sartakov <sartakov(a)ksyslabs.org> >> Sent: Friday, October 14, 2016 12:33 AM >> To: devel(a)sel4.systems >> Subject: [seL4] endpoint.c >> >> Hello. >> >> I have a problem with endpoint.c test (RECYCLE0001): >> >> Error: seL4_MessageInfo_get_label(tag) == seL4_InvalidCapability at line 50 of file /long/path/apps/sel4test-tests/src/tests/endpoints.c >> >> I am reading MR(0) in call_func above this check and see, that seL4_Call returns values that were sent before. For example, 100 for the first thread, 101 for the second and etc. Thus, as far I understand, cnode_recycle does not work at all. I am pretty sure that my seL4_Call syscall was implemented properly. I have looked inside the kernel, and tried to track everything related to cteRecycle and do not see anything platform specific. I know that it is a complicated question, but any ideas or hints where to look?

2 2

Fwd: Microkernels / Component-based OSes devroom - Call for Participation
by Vasily A. Sartakov 18 Oct '16

18 Oct '16

Just want to invite you to FOSDEM’17 > The developers of several free and open-source microkernel-based > operating systems will meet at FOSDEM 2017 [1] in Brussels, Belgium > and will share a developer room on Saturday of February 04, 2017 [2]. > The devroom is currently looking for content in the form of talks and > activities related to the area of microkernel-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 > * Enabling support for hardware (architectures, device drivers) > * Used languages and tools > * Maintainance and testing > * Security and robustness > * Trends and challenges > * Use cases, experiences, lessons learned and demos > > Please use the Pentabarf [3] system to submit your proposals and file it > under the track “Microkernels and Component-based OS”. You do not need > to create a new account if you already have one. When in doubt, please > use the devroom mailing list [4]. If you do not want to give a talk > yourself, you may still send suggestions for what else you would like to > see, or do in the devroom. Please send your suggestions to the mailing > list. The deadline for your proposal is on December the 4th. > > 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 (please, at least 25 and no longer than 45 min) > > The official devroom schedule (along with the accepted talks) will be > announced on December the 11th on the devroom's mailing list and the > speakers will be notified via e-mail. The schedule will also be published > on the FOSDEM website. > > > 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. > > > About the devroom > > Since the first Microkernel devroom in 2012 this devroom has been part of > each following FOSDEM. By now it has become a somewhat institutionalized > tradition for the micro kernel 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 differend > solutions. Therefore, the goal of the Microkernel 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 downtown Brussels after the devroom closes. The year 2017 > will not be any different, so there is going to be a microkernel family > dinner on Saturday night. The exact location and time will be specified > 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. > > > Important dates recap > > * 04.12.2016: Deadline for submissions > * 11.12.2016: Schedule published and speakers notified of acceptance > * 04.02.2017: The devroom takes places > > > Links > > [1] http://fosdem.org/ > [2] https://fosdem.org/2017/practical/transportation/ > [3] https://fosdem.org/submit > [4] https://lists.fosdem.org/listinfo/microkernel-devroom -- Vasily A. Sartakov sartakov(a)ksyslabs.org

1 0

General Questions
by Mark Reus 17 Oct '16

17 Oct '16

Hi I have recently started with working on sel4 and I have a couple of questions. i) Can a process be spawned or configured only from the root task? (using sel4_configure_process) ii) How to enable or locate prints of ZF_LOGE in kernel? I have enabled kernel prints and debug in make menuconfig. iii) I have followed the tutorial for IPC between a spawned process and root task. The setup is done as follows from the root task: /* create an endpoint */ vka_object_t ep_object = {0}; error = vka_alloc_endpoint(&vka, &ep_object); assert(error == 0); /* * make a badged endpoint in the new process's cspace. This copy * will be used to send an IPC to the original cap */ /* make a cspacepath for the new endpoint cap */ cspacepath_t ep_cap_path; seL4_CPtr new_ep_cap; vka_cspace_make_path(&vka, ep_object.cptr, &ep_cap_path); /* copy the endpont cap and add a badge to the new cap */ new_ep_cap = sel4utils_mint_cap_to_process(&new_process, ep_cap_path, seL4_AllRights, seL4_CapData_Badge_new(EP_BADGE)); assert(new_ep_cap != 0); However, I want to establish communication between two spawned processes. In that case I need to copy the badged endpoint capability of one process into another process. But in the spawned process I wouldn't have access to the pointer (sel4utils_process_t of new process), so how can i use mint_cap_to_process. Can someone help me with these. Thanks in advance. Regards Mark

3 2

endpoint.c
by Vasily A. Sartakov 14 Oct '16

14 Oct '16

Hello. I have a problem with endpoint.c test (RECYCLE0001): Error: seL4_MessageInfo_get_label(tag) == seL4_InvalidCapability at line 50 of file /long/path/apps/sel4test-tests/src/tests/endpoints.c I am reading MR(0) in call_func above this check and see, that seL4_Call returns values that were sent before. For example, 100 for the first thread, 101 for the second and etc. Thus, as far I understand, cnode_recycle does not work at all. I am pretty sure that my seL4_Call syscall was implemented properly. I have looked inside the kernel, and tried to track everything related to cteRecycle and do not see anything platform specific. I know that it is a complicated question, but any ideas or hints where to look? Thank you -- Vasily A. Sartakov sartakov(a)ksyslabs.org

2 2

sel4 hypervisor communication
by Horace Blanc 13 Oct '16

13 Oct '16

Hi, 1) Is there a mechanism for inter VM communication with seL4 as a hypervisor? 2) If the VMMs run in kernel mode (PL1), as I was told, does it mean they use hvc commands instead of swi/svc commands when sending messages to seL4 as hypervisor? Thank you in advance,

2 1

syscall.c
by Vasily A. Sartakov 11 Oct '16

11 Oct '16

Greetings. I have moved forward to tests in my our MIPS port. Some of them work fine, but not all. Now I have a question about syscall.c test. What exactly we test here? In ARM-based part I see initialisation of 12 registers, performing syscall with further checking that our initialised registers have original values. So, as far I understand, these registers should be modified in a syscall’s inline, thus, they should be allocated on the stack and reloaded after the end of syscall. Right? My issue here is that I have much many than 12 registers and my compiler chooses them randomly (for me). For example, sometimes it uses only S0-S7 with some T0-T9 registers, sometimes all T0-T9 with some S0-S7 registers. Moreover, I cannot put more than 30 asm instructions in one inline (gcc error), thus, maybe I should specify proper register name here. But for that, I should be sure that I understand this test correct. Can we help me? Thank you -- Vasily A. Sartakov sartakov(a)ksyslabs.org

2 2

Spawn new process
by Andrew Mine 11 Oct '16

11 Oct '16

Hi I am working with sel4-tutorials and wanted to spawn a new process using int sel4utils_configure_process_custom(sel4utils_process_t *process, vka_t *target_vka, vspace_t *spawner_vspace, sel4utils_process_config_t config); However, I am not able to understand some of the details required to initialize the parameter config used in the function. Can someone give me link to an example of sorts where this is used. Regards Andrew Mine

1 0

adding new code to VMM on TK1
by PX 11 Oct '16

11 Oct '16

Hi, Please forgive my ignorance. I want to add new code to the seL4-based VM for TK1. However, I find it is hard to add new directories. The newly added directories are always ignored or can not be found by compiler. What's the correct way to add new directories? which scripts we should look into? thanks Peng

3 4

questions about the device driver in virtual machine on ARM seL4 (TK1 board)
by PX 06 Oct '16

06 Oct '16

Hi, I have questions about the device drivers in the virtual machine on ARM seL4. The virtual machine on TK1 board is located on the physical memory starting at 0xb0000000. However, the MMIOs used by the device drivers in the VM are below 0xb0000000. 1.If my understanding is correct, does that mean that a device driver in the VM can actually access a memory block outside of the VM's boundary even though it is mmio. 2. If the device driver actually uses the mmio outside of the VM's memory boundary, do the page tables (including EPT) need to map to this mmio? However, I can not find any code doing the mapping. Do I miss something? Thanks Peng

2 4

Post-mutikernel approach to multiprocessor support?
by Jeff Waugh 04 Oct '16

04 Oct '16

Hi all, Is there anything that can be shared so far about seL4's post-multikernel approach to multiprocessor support? (I couldn't see anything new or upcoming on the publications pages, and figured a paper or two might land before code aimed for Q4'16.) Thanks, Jeff

2 5

Possible seL4 developer day Dec 15–16 in Malibu
by Gernot.Heiser＠data61.csiro.au 04 Oct '16

04 Oct '16

Dear seL4 Community, Part of the Data61 seL4 Team will be in Malibu in mid December and we are considering running another Developer Day. As in the past, this would actually run over 1.5 days, from the morning of the 15th to about mid-day on the 16th and be a combination of lectures and hands-on sessions. As usually we’ll try to make this a free event, provided that our friends at HRL Labs can host us. We have been discussing the possibility of providing an advanced stream besides the “newbie” version we had been running in the past. Right now, we are gauging interest in this. So, if you are interested in participating on those two days, would you please let Ihor know 1) how many participants you expect from your organisation 2) whether you are interested in the newbie or an advanced version, 3) if advanced, what topics you would like covered Examples of advanced materials - advanced driver writing/porting, eg how to port a real Linux driver - advanced real-time topics: eg building stuff from scratch rather than filling in templates - locking and synchronisation - architecting seL4-based systems - process for building real systems: throw everything into a VM, and then extract bits into native components - anything specific you are interested in We’d imagine the advanced stream to be less structured, emphasising largely independent work on a specific problem, with people around to help. It could even be solving a particular problem you have (but we’d need to understand what you’re trying to build beforehand). Gernot & Ihor

1 0

Why send-only IPC doesn't and shouldn't return a success indicator
by Gernot.Heiser＠data61.csiro.au 29 Sep '16

29 Sep '16

We have just received this comment on github, which I think merits some explanation: > There are times when IPC needs to happen, but a sending process cannot wait around for another process to be receiving. seL4_NBSend is basically the system call for this, but it never provides any feedback whether or not IPC took place. Summary: I accept that this is a valid use case, but the suggested solution is not the right one. There are two reasons why I’m saying this: 1) the current behaviour of send-only IPC is correct and cannot be changed, 2) send-only IPC is the wrong way to address this use case. Re (1): Anyone who tried to use seL4_Send() or seL4_NBSend() will likely have noticed that they are of very little use, because you don’t know whether the message was transferred. So, why can't we return at least a boolean value, indicating whether a message has been delivered or it was dropped on the floor? It’s simple: this would violate the dataflow guarantees provided by seL4. Send-only IPC is there to enable one-way information flow, and consequently can be invoked using a send-only cap. But a send-only cap must not allow any information flow from the receiver to the sender (or else all our isolation proofs would break down). Basically, a return status that can be influenced by the receiver constitutes a back channel that is not authorised by a cap, and as such is verboten. This means that send-only IPC is of very little practical use, except where you really want one-way information transfer, or you have a higher-level protocol that lets you get away with not knowing whether the message was lost. (Eg if the receiver being not ready is a protocol violation by the receiver, and it has only itself to blame for losing the message.) So, could we make send-only IPC a bit more useful by changing the semantics slightly? For example, we could have a return value that indicates successful message delivery if the send was invoked with a send+receive cap, but will always return false if the invocation used a send-only cap? In principle that would be doable without violating security requirements. The cost would be extra checking. It would also be somewhat unsystematic if the semantics of a send-only operation would depend on whether your cap has receive rights as well. It’d be arguably misleading, as you’re doing more than sending. This gets me to (2): send-only IPC is the wrong way to solve the problem. The above use case is clearly one where info flow is inherently two-way: you send something and need an acknowledgment of receipt. This means call-type IPC is the right mechanism, it does exactly that. And on top of that it is more efficient than separate send-receiver, and avoids (thanks to reply caps) the need to set up a separate reply channel. The problem, of course, is that seL4_Call() is always blocking, there is no polling variant of this syscall. Should there be an seL4_NBCall()? Arguably yes, just as the RT branch already provides a seL4 SignalRecv() syscall, which is the non-blocking equivalent of seL4_ReplyRecv(). Will it happen? Possibly, but not in mainline the near future. The reason is that to add this (fairly simple) feature to the mainline kernel will require verifying it, and our verification engineers are presently very busy delivering on contracted milestones. We’ll discuss this internally. In the meantime I’ve added some explanation of the semantics of seL4_Send()/seL4NBSend() to the FAQ on the seL4 wiki. Gernot

4 6

quesion about TK1 Linux irq
by PX 27 Sep '16

27 Sep '16

Hi, I have questions about the irqs defined for TK1 guest linux. 1. The linux_pt_irqs[] defined in tk1_vmlinux.h lists all the IRQs for I/O devices, but why they are different from TK1 manual? Does seL4 perform some mapping for guest Linux? 2. what 's the Physical address for Ethernet card on TK1 board? Thanks Peng

2 1

Fwd: [Fwd: quesion about TK1 Linux irq]
by Jason.Butler＠data61.csiro.au 27 Sep '16

27 Sep '16

The irq numbers are remapped in: kernel/include/plat/tk1/plat/machine.h Jason ? -------- Forwarded Message -------- From: PX <seawolf.peng(a)gmail.com> To: devel(a)sel4.systems Subject: [seL4] quesion about TK1 Linux irq Date: Mon, 26 Sep 2016 17:38:47 -0400 Hi, I have questions about the irqs defined for TK1 guest linux. 1. The linux_pt_irqs[] defined in tk1_vmlinux.h lists all the IRQs for I/O devices, but why they are different from TK1 manual? Does seL4 perform some mapping for guest Linux? 2. what 's the Physical address for Ethernet card on TK1 board? Thanks Peng _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel

1 0

Why send-only IPC doesn't and shouldn't return a success indicator
by Matt Rice 26 Sep '16

26 Sep '16

Gernot.Heiser wrote: > We have just received this comment on github, which I think merits some explanation: >> There are times when IPC needs to happen, but a sending process cannot wait around for another process to be receiving. seL4_NBSend is basically the system call for this, but it never provides any feedback whether or not IPC took place. ... >This gets me to (2): send-only IPC is the wrong way to solve the problem. > >The above use case is clearly one where info flow is inherently two-way: you send >something and need an acknowledgment of > receipt. This means call-type IPC is the right mechanism, it does exactly that. And on top of that it is more efficient than > separate send-receiver, and avoids (thanks to reply caps) the need to set up a separate reply channel. New to sel4 and the list (so sorry for stuffing up the threading) Couldn't at the expense of an extra notification send, use a notification where the receiver of the notification then should call the then do a non-blocking reply. I didn't see reply being non-blocking described in the manual so please correct me if i am wrong. This only works one party is willing to block correct, and there is no way to short circuit the call if an incoming message could be delivered to the call'ing process before the call can be completed? Although it would seem to take some amount of gymnastics to balance sending and receiving... so if really neither are willing to wait there is always notifications+shared memory?

3 4

Questions about Capability model
by Daniel Wang 21 Sep '16

21 Sep '16

Hi all, I’m new to the capability concept of seL4. Please correct me if I’m wrong. My understand of the capability is that it is a reference to a chunk of memory that allocated for specific purpose. Say if I want to do IPC between two threads A and B, I will need to apply an chunk of memory as endpoint, which give me a capability that I can pass from thread A to thread B is that correct? Also it is ok to assume the message passing mechanism in IPC is a producer-consumer model? The reason I ask it because I’m thinking is it possible for three (or more) threads that need to communicate with each other using the same endpoint, or it has to be paired for each two of those threads to use an endpoint? Thanks -Dan

3 4

developing a Ethernet card server for seL4
by PX 20 Sep '16

20 Sep '16

Hi, all, We want to develop a networking service on top of seL4, which works as a hypervisor, on Jetson TK1. We know that there is source code for lwip under /projects/util_libs/libethdrivers, but there is no support for TK1. We want to know how much effort needed to port the code to TK1 platform? Is it straightforward? Is there any TK1 ethernet driver source code available? Peng

3 3

How to run seL4 as a hypervisor?
by Daniel Wang 19 Sep '16

19 Sep '16

Hi all, Is there any document/tutorial about using seL4 as a hypervisor to running Linux on top? Appreciate for your help. Thanks -Dan

2 1

General Questions
by sixpackgurkenwasser＠use.startmail.com 15 Sep '16

15 Sep '16

Hello, I've got several questions. 1. Is there a simple way to relate a virtual address in the initial threads address space to the corresponding frame cap in the BootInfo? 2. In 8.2.2 of the manual it is stated in that "seL4 provides no way to obtain the physical address of a page from its capability". Isn't that exactly what the GetAddress method of a Page object does(10.4.14)? Cheers, Steve

3 2

Re: [seL4] General seL4 Kernel Questions
by Kofidoku.Atuah＠data61.csiro.au 13 Sep '16

13 Sep '16

Hey, welcome: ? > 1) Once the kernel boots, the control is given to a root task which we define. Does this root task have all permissions and capabilities or do we still need to assign it capabilities? The root task is given capabilities to all kernel objects , and it has full permissions (Read-write-grant) on all of them -- you needn't do any work to cause the root task to have permissions/control over the initial objects. Just need to read and parse the BootInfo struct that describes how they are laid out in your CSpace. >2) Who is in-charge of scheduling or thread suspend (We can start new threads from root task), is it also responsibility in root task to manage and schedule it? Who is in charge of migrating the tasks, flushing CPUs loading new stack etc? The kernel handles scheduling in the main, but threads can be suspended as needed by any other thread that has a capability to the TCB of the thread that you want to manage. Mainline seL4 currently doesn't support multicore, so there is no thread migration, and I do not know what form the multicore extensions will take, with regards to CPU affinity configuration as yet. It's not easy to speculate either, since the entire scheduler is going to undergo intrusive changes when the Real Time extensions are released. >3) While spawning a new thread? Who allocates virtual memory to it? And is the virtual memory allocated equal to 4 GB like in linux kernel where all applications get same Virtual Memory size but different mappings? A new thread is initially a blank TCB -- to associate a virtual address space (VSpace) with it, you'd need to create a VSpace (seL4_Untyped_Retype), and then pass that to the kernel while configuring the TCB (seL4_TCB_Configure). The VSpace is also just a blank page directory, so you have to then create the page tables for the address space, and then create frames to map into the page tables, etc. The VSpace object is a light wrapper around hardware page tables, so yes, they cover a 4GiB address range, but like Linux, seL4 takes up some of that 4GiB for itself. >4) What are the default things loaded into Virtual Memory of a thread? Only the Cspace maybe made available via CNode_mutates? or something else? Nothing -- the day that comes after the darkest night has the greatest number of possibilities -- or something like that: what I'm trying to say is that because no policy is enforced by the kernel (not even executable format) you have the greatest range of flexibility to do what you want with the new thread's VSpace. When you create a new VSpace there is nothing in it at all. The only exception is that when the kernel creates the root task's VSpace, it also then goes on to put the bootinfo struct into it, and in addition it allocates a stack and IPC buffer, and expands the root task's ELF image -- this is a special case because the root task is special. Kofi Doku Atuah Kernel engineer DATA61 | CSIRO E kofidoku.atuah(a)data61.csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 ________________________________

3 2

Re: [seL4] General seL4 Kernel Questions
by Andrew Mine 13 Sep '16

13 Sep '16

Hi Thanks a lot for the responses. It is much clearer now. I will delve a little bit more into this. Regards Andrew Mine On Mon, Sep 12, 2016 at 2:07 AM, <Kofidoku.Atuah(a)data61.csiro.au> wrote: > Hey, welcome: > > > 1) Once the kernel boots, the control is given to a root task which we > define. Does this root task have all permissions and capabilities or do we > still need to assign it capabilities? > > The root task is given capabilities to all kernel objects , and it has > full permissions (Read-write-grant) on all of them -- you needn't do any > work to cause the root task to have permissions/control over the initial > objects. Just need to read and parse the BootInfo struct that describes how > they are laid out in your CSpace. > > >2) Who is in-charge of scheduling or thread suspend (We can start new > threads from root task), is it also responsibility in root task to manage > and schedule it? Who is in charge of migrating the tasks, flushing CPUs > loading new stack etc? > > The kernel handles scheduling in the main, but threads can be suspended as > needed by any other thread that has a capability to the TCB of the thread > that you want to manage. Mainline seL4 currently doesn't support multicore, > so there is no thread migration, and I do not know what form the multicore > extensions will take, with regards to CPU affinity configuration as yet. > It's not easy to speculate either, since the entire scheduler is going to > undergo intrusive changes when the Real Time extensions are released. > > >3) While spawning a new thread? Who allocates virtual memory to it? And > is the virtual memory allocated equal to 4 GB like in linux kernel where > all applications get same Virtual Memory size but different mappings? > > A new thread is initially a blank TCB -- to associate a virtual address > space (VSpace) with it, you'd need to create a VSpace > (seL4_Untyped_Retype), and then pass that to the kernel while configuring > the TCB (seL4_TCB_Configure). The VSpace is also just a blank page > directory, so you have to then create the page tables for the address > space, and then create frames to map into the page tables, etc. The VSpace > object is a light wrapper around hardware page tables, so yes, they cover a > 4GiB address range, but like Linux, seL4 takes up some of that 4GiB for > itself. > > >4) What are the default things loaded into Virtual Memory of a thread? > Only the Cspace maybe made available via CNode_mutates? or something else? > > Nothing -- the day that comes after the darkest night has the greatest > number of possibilities -- or something like that: what I'm trying > to say is that because no policy is enforced by the kernel (not even > executable format) you have the greatest range of flexibility to do what > you want with the new thread's VSpace. When you create a new VSpace there > is nothing in it at all. > > The only exception is that when the kernel creates the root task's VSpace, > it also then goes on to put the bootinfo struct into it, and in addition it > allocates a stack and IPC buffer, and expands the root task's ELF image -- > this is a special case because the root task is special. > > Kofi Doku Atuah > Kernel engineer > DATA61 | CSIRO > E kofidoku.atuah(a)data61.csiro.au > www.data61.csiro.au > > CSIRO's Digital Productivity business unit and NICTA have joined forces to > create digital powerhouse Data61 > ------------------------------ > > >

1 0

General seL4 Kernel Questions
by Andrew Mine 12 Sep '16

12 Sep '16

Hi I need help with some basic questions which I am getting confused of how seL4 is working. I am currently using the tutorials-seL4 branch. 1) Once the kernel boots, the control is given to a root task which we define. Does this root task have all permissions and capabilities or do we still need to assign it capabilities? 2) Who is in-charge of scheduling or thread suspend (We can start new threads from root task), is it also responsibility in root task to manage and schedule it? Who is in charge of migrating the tasks, flushing CPUs loading new stack etc? 3) While spawning a new thread? Who allocates virtual memory to it? And is the virtual memory allocated equal to 4 GB like in linux kernel where all applications get same Virtual Memory size but different mappings? 4) What are the default things loaded into Virtual Memory of a thread? Only the Cspace maybe made available via CNode_mutates? or something else? I am sorry if the questions are silly, but I am getting confused. Thanks and Regards Andrew Mine

1 0

seL4 GDB
by Chris Guikema 09 Sep '16

09 Sep '16

Hello everyone, DornerWorks has developed a GDB-stub system for the ARMv7 platform (specifically Zynq 7000) that can be found at the following repos: https://github.com/dornerworks/gdbstub-app https://github.com/dornerworks/gdbstub-app-manifest If you have any questions, feel free to ask.

1 0

CAmkES Question
by Chris Guikema 02 Sep '16

02 Sep '16

Hello Ihor, My name is Chris Guikema, and I am an embedded systems engineer at DornerWorks, located in Grand Rapids Michigan. I am currently working on a project that requires the use of the CAmkES system, and I would like some help, if you are willing to. The project is to allow for debugging using CAmkES. The debugging process was successfully implemented in a simple seL4 program by using the init thread to set up an exception thread and setting up the exception endpoint, which was mapped to the init thread. The init thread was then used to implement a bad assembly code, which fired an exception. The exception handler thread was waiting on something to appear at the endpoint, and then grabbed the program counter and the stack of the init thread and sent it to a GDB function, which allowed debugging. My job is to replicate the debugging using CAmkES. However, CAmkES doesn't seem to want the application to utilize any of the seL4 system calls, and I don't believe the application knows its root cspace and vspace, so any attempt to initialize a debug thread and setup an exception endpoint just don't work. What steps do I need to take to 1, set up an endpoint that I could map to the exception endpoint (the simple libraries cause a vm fault), and 2, set up a thread that waits on the application to throw an exception and allow the debugging to occur. Any help you could send me would be appreciated. I look forward to hearing from you. Thanks Chris Guikema

2 1

sel4 as hypervisor
by Horace Blanc 01 Sep '16

01 Sep '16

Hi, I would like to have more information concerning the design of the hypervisor functionality in the sel4 project on ARMv7 architectures. >From what I read (FAQ/announcement from Adrian Danis in this mailing list), sel4 can run an application called VMM which adds that functionality. Here are my questions: 1) Did the design of this functionality require any change in the sel4 microkernel or is it just the VMM in userland that permits it? (what was in the arm_hyp branch that is now in master?) 2) Does this mean that it is a type-2 hypervisor? Do the guest OS run on top of the VMM? 3) How are the virtualization extentions of ARM used? More precisely what runs on the different protection levels (PL0, PL1 and PL2)? 4) To what extent is this hypervisor design pure? Do the guest OS know that it is running on top of seL4? Best, Horace BLANC

2 1

Genode 16.08 supports dynamic workloads on seL4
by Alexander Boettcher 31 Aug '16

31 Aug '16

Hello, we are proud to announce that the just released version 16.08 of the Genode OS Framework brings vastly extended seL4 support, which allows interactive and dynamic system scenarios to run directly on the x86 version of the seL4 kernel. With the new version, users of seL4 can compose dynamic operating systems from a plethora of ready-to-use Genode components. First, there are our time-tested device drivers and protocol stacks: - VESA driver (based on x86emu of XOrg) - Intel graphics driver (based on Linux 4.4.3), e.g., to drive external connectors - Intel wireless stack (based on Linux 4.4.3) including WPA supplicant - Network driver (based on iPXE) - AHCI, PS/2, PIT, ACPI driver - Audio driver (ported from OpenBSD 5.9) - USB driver (based on Linux 4.4.3) with hot-plug support - lwIP - light weight TCP/IP stack - Linux TCP/IP Stack (ported from Linux 4.4.3) - File-system support, e.g., ext2 based on Rump kernels Also, Genode includes a range of low-complexity resource multiplexers: - Secure GUI multiplexer - Nitpicker - Highly configurable and dynamical window manager - Audio mixer - Virtual networking components - Virtual file-system support For application development, there are several runtime environments and high-level libraries: - Noux - UNIX-like subsystem to run command-line-based GNU software like bash, vim, coreutils, gcc/g++, ... - Environments for the Rust, Python, and Lua programming languages - Base libraries like libc, standard C++ library, pthreads, OpenSSL, Readline etc. - Qt5 libraries and applications, including Webkit There's a lot more to explore and - in the pure microkernel way - each of these components are executed in user mode as separate protection domains on seL4. More details about version 16.08 can be found in the extensive release documentation: https://genode.org/documentation/release-notes/16.08 and, for the impatient, a life demo scenario of Genode on seL4 can be downloaded: https://www.genode.org/documentation/release-notes/16.08#Try_Genode_seL4_at… Best regards, -- Alexander Boettcher Genode Labs http://www.genode-labs.com · http://genode.org Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

1 0

Kernel extensions and userspace options
by Jonathan C Day 30 Aug '16

30 Aug '16

Hi, I am very interested in SEL4, partly because I was assured it was impossible to use Formal Methods in kernel development, partly because it's a fascinating project in its own right, but right now because there are some embedded applications that could do with the high level of reliability and security that provable correctness implies. Unfortunately, said applications need a comprehensive network stack and a powerful packet filtering/mangling engine. The latter could imaginably be done in the kernel, as it's deterministic, but I don't see any obvious value. Nonetheless, if someone has coded such a system as a third-party add-on, I would be very interested. There are good arguments for why the former can't be done, in a way that can be proven, and I really want the correctness. In terms of userspace, I believe I could use something like L4Linux (as long as it is still maintained), and I think there's one supplied, but are there other options? Has anyone ported OpenBSD to it? To be honest, I'm not sure I need a multitasking userspace, but I do absolutely need the network stack and packet filter. Everything else can be ported, albeit with difficulty. However, network operating systems are thin on the ground and tend to be proprietary, exactly what I don't want. For those curious, I'm looking to end up with a system with strong bounds on robustness and security, and that can handle things like multipath TCP, network failover, QoS and OpenFlow. However, all of these requirements boil down to a sequential process. Unnecessary complexity is where you end up with problems. If current wisdom says that there's nothing suitable in userspace, then does anyone know if there are there any existing Coloured Petri Nets that I could use to build what I need into the kernel? Even if I can't get better than a quasi-guarantee, it would be something.

3 6

Re: [seL4] Devel Digest, Vol 27, Issue 16 - High Assurance Hardware
by Tyga 30 Aug '16

30 Aug '16

> > Re: > > ------------------------------ > Date: Mon, 29 Aug 2016 23:01:45 +0000 > From: <Gernot.Heiser(a)data61.csiro.au> > <snip> > You may *think* that the manufacturers don?t make changes to the more > conventional bits of the hardware, and thus they are ?correct", but that > isn?t true, of course. And on top of that we know that there are > intentional backdoors in commercial hardware. > The only way around this is high-assurance hardware, and this doesn?t come > at an affordable cost. > > I think it?s an illusion to think one can partition hardware into trusted > and untrusted bits. In the end, the OS is at the mercy of the hardware, if > it?s faulty then you lose, there?s no way around it. A key attraction of seL4 is the trustworthiness of the microkernel. Running it on hardware with known bugs or features (e.g. recent Intel CPUs) that compromise the kernel's trustworthiness counteracts the perceived advantages. Perhaps, it would be possible to list CPUs (and possibly boards) that are recognised for being free of known potential attack vectors. I would certainly not want to invest time and effort into making seL4 run on hardware that could have be reasonably known to be of low assurance.

2 1

IA32 syscall bindings
by Norman Feske 26 Aug '16

26 Aug '16

Dear seL4 developers, first, I'd like to thank you for publishing seL4 under GPL. I am very happy that I can finally get my hands dirty with working with the kernel of your group. :-) Currently, I am taking the first baby steps to bring the Genode OS framework (http://genode.org) to seL4. For reference, I am using the experimental branch. The first smallish issue I stumbled upon stems from the fact that Genode is written in C++. By compiling the seL4 syscall bindings with a C++ compiler, I got the following error: error: inconsistent operand constraints in an ‘asm’ It can be reproduced by putting the following code snippet into a cc file and compiling it with 'g++ -m32 -c' (tested with the Genode tool chain as well as with GCC 4.8.1): typedef enum { seL4_SysDebugPutChar = -9, _enum_pad_seL4_Syscall_ID = (1U << ((sizeof(int)*8) - 1)) } seL4_Syscall_ID; void seL4_DebugPutChar(char c) { asm volatile ( "pushl %%ebp \n" "movl %%esp, %%ecx \n" "leal 1f, %%edx \n" "1: \n" "sysenter \n" "popl %%ebp \n" : : "a" (seL4_SysDebugPutChar), "b" (c) : "%ecx", "%edx", "%esi", "%edi", "memory" ); } When compiling the same code snippet with 'gcc' instead of 'g++', everything is fine. It turns out that the C++ compiler does not like the enum value to be specified as input argument. I found the following ways to circumvent this problem: * Changing the enum value 'SysDebugPutChar' to a positive value, * Removing the definition of '_enum_pad_seL4_Syscall_ID', * Casting 'seL4_SysDebugPutChar' to an integer: : "a" ((int)seL4_SysDebugPutChar), In any case, I seem to have to change the bindings. Do you see a way around it? If not, would you consider one of the solutions above for the seL4 headers? On another note, I noticed that the bindings use the EBX register. Unfortunately, this makes it impossible to compile seL4 userland software as position-independent code (PIC). E.g., when compiling the above code snippet via 'g++ -m32 -fPIC -c', the following error occurs: error: inconsistent operand constraints in an ‘asm’ However, PIC is required in order to use shared libraries. The solution would be to not use EBX to pass arguments to the 'asm' statements, save EBX on the stack prior moving the respective kernel argument to the register, and, of course, restoring it after sysenter returns. Before I start changing the bindings, I'd like to know: is there anyone else working on the same problem? Would you be open to accept a change of the bindings to become PIC compliant on the costs of a few added instructions? Or do you have another suggestion how I should go about it? Best regards Norman -- Dr.-Ing. Norman Feske Genode Labs http://www.genode-labs.com · http://genode.org Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

4 7

syscalls and tlb
by Vasily A. Sartakov 26 Aug '16

26 Aug '16

Greetings. I am working on MIPS port of seL4. Now I can run very simple hello world application which reads and dumps bootinfo page. In other words, I modified elfloader, added platform and architecture support to the kernel, add _sel4_start for mips in libsel4platsupport, adopted mips support of libmuslc to work with __sysinfo in mips and more. Now I have some questions. I see that for different ‘syscalls' muslc uses different routes but with the same end. For example, SYS_ioctl from __stdout_write uses __syscall, provided by libmuslc/arch/<arch>/syscall_arch.h (implemented as CALL_SYSINFO). In the same time, syscall_cp function from __stdio_write is implemented inside libmuslc/src/internal/<arch>/syscall.s which uses __sysinfo in turn. So, that question is why? The second question is about the kernel. Now I am using static configuration of TLB in kerne: I have one region for rootserver aligned to 2MB, and one region for boot info page (also aligned). Thus, I do not have tlb traps since everything is in the TLB. In future, of course, I should add a processing of TLB misses somewhere in the plat/arch part of kernel. I am not familiar with memory support in seL4 yet, is there any syscall for delivery tlb traps? (I see nothing similar) Is there any check inside, for example, SEND call, about a presence of page in TLB? thank you. -- Vasily A. Sartakov sartakov(a)ksyslabs.org

4 5

Does anyone pay attention to Google's new operating system fuchsia
by XilongPei 24 Aug '16

24 Aug '16

Hi, Google has announced a new operating system fuchsia, https://github.com/fuchsia-mirror Its kernel is called Magenta, Magenta has a capability-based security model, this is very similar to seL4. Does anyone pay attention to Google's new operating system fuchsia? Xilong Pei Tongji University Shanghai, China 2016/8/24

3 3

x86: loosing edge triggered interrupts when using I/O APIC
by Alexander Boettcher 24 Aug '16

24 Aug '16

Hi, we are using as user level timer driver the PIT on Genode/seL4 and experience situations that the driver does not get IRQs after a while. It happens on Qemu as also on native x86 hardware. We tracked down the problem to the masking of edge-triggered IRQs on the I/O APIC in the seL4 kernel. According to Intel, [0] chapter 3.2.4 "Interrupt Mask R/W", edge interrupts on a masked interrupt pin gets ignored and are not held pending. On [2] there are also some discussion about this topic too. We solved/workaround the issue by this patch [1]. I looked additionally into two other microkernels using the I/O APIC and they don't mask edge level triggered I/O APIC interrupts. I wonder if anybody already stumbled about the issue on seL4/x86? If not, please take the patch or give advices to adapt the patch so that it may get upstream. Thanks, Alexander Boettcher. [0] http://www.intel.com/design/chipsets/datashts/29056601.pdf [1] https://github.com/genodelabs/genode/blob/master/repos/base-sel4/patches/io… [2] http://yarchive.net/comp/linux/edge_triggered_interrupts.html

2 1

New to seL4
by Andrew Mine 22 Aug '16

22 Aug '16

Hi I have just started looking at seL4 and I was wondering where can I find some documentation explaining the features and difference between seL4 and other kernels. I have gone through the manual and tutorial documents but nothing majorly explains how seL4 is different and its features. Any guidance towards any documentation will be helpful. Thanks Andrew

2 1

next seL4 developers day on Sep 6?
by Gerwin.Klein＠data61.csiro.au 16 Aug '16

16 Aug '16

We’re contemplating running a seL4 developers day in conjunction with the DARPA HACMS PI meeting in Pittsburgh on Tue, Sep 6 2016. If you would be interested in attending, please drop me a short email by Thursday night of your local time zone. If enough people register interest we will try to organise one. Cheers, Gerwin -- Prof Gerwin Klein, Research Group Leader, Trustworthy Systems DATA61 | CSIRO gerwin.klein(a)data61.csiro.au T +61 2 8306 0578 http://data61.csiro.au NICTA and CSIRO’s Digital Productivity business unit have joined forces to create the digital powerhouse Data61

1 0

Interrupt in seL4
by Norrathep Rattanavipanon 14 Aug '16

14 Aug '16

I have a few questions about how interrupts work in seL4. 1) Is it possible to enable/disable interrupt (i.e. __enable_irq or __disable_irq for ARM) in the userspace code of sel4? We want to make sure that the execution of the code in the initial process does not get interrupt. 2) My understanding is that the scheduling mechanism in seL4 is priority-based first and round-robin if two processes/threads have the same priority. Assume process A is the initial process spawned by kernel. 2.0) is my understanding about sel4 scheduling correct? 2.1) Is the initial process guaranteed to have the maximum priority in seL4? 2.2) If another process, say process B, is created by process A with lower priority. Is it possible for process B to interrupt process A and execute code in B instead while A is executing? Thanks, -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

4 6

up-to-date formal verification
by Horace Blanc 09 Aug '16

09 Aug '16

Hi, I would like to know if the verification of the seL4 is up-to-date with the newest version of the sel4 microkernel (3.2.0). If so, how do I access it? When I run make ASpec in l4v, I get a pdf with the Abstract Formal Specification in version 1.3. Does it refer to the seL4 microkernel version 1.3 or has the Abstract Formal Specification its own versions? Also, what is the best way to explore this specification in Isabelle/jedit? thanks in advance Horace Blanc

2 1

on Zynq
by Neelesh Vemula 08 Aug '16

08 Aug '16

Hi all, I am completely new with seL4, embedded systems as well as the fpga world. I am working on installing seL4 on Zynq fpga and use it. I have successfully able to boot up a "hello world" application using uboot(sd card bootup) on the zynq device. However, I have no clue as in how to setup communication between the sel4 logic and the PL(fpga fabric). If I am correct some sort of device driver has to be written or is there anything that is inbuilt or someone else who has worked on a similar project. Any guidance in this regard will be utmost helpful. Thanks a ton! Neelesh Vemula

2 1

capDL configuration file
by Norrathep Rattanavipanon 03 Aug '16

03 Aug '16

So I was reading capDL paper and it mentions about having a human-readable XML file for configuration of the initial thread which allows the system initialize into a know state. I assume this is not specific to camkes. so is there any way I can see/get the XML file and the code that generates it in the regular seL4? Thanks, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

memory map/unmap performance
by Yuxin Ren 02 Aug '16

02 Aug '16

Hi all, I am curious memory mapping/unmapping performance. Are there any applications that stress the memory mapping and unmapping utility? Thanks a lot! Yuxin

4 4

beaglebone ethernet support
by Julien Delange 27 Jul '16

27 Jul '16

Hello, I noticed that there is some source code to support the ethernet driver of the beaglebone black. I look especially in projects/seL4_libs/libsel4platsupport/src/plat/am335x/cpsw_beaglebone.c According to https://github.com/seL4/seL4_libs/blob/master/libsel4platsupport/src/plat/a… the file has been introduced by NICTA - I am wondering if there is any existing example/support for it. In a nutshell, I am trying to use the ethernet driver. I started to integrate the startcode from TI on a camkes application before discovering this code. So, is there any sample application to use it? It is supported/working? Thanks for any help, Julien.

1 0

sel4 on Hikey board
by rahul mahadev 26 Jul '16

26 Jul '16

Hi , I'm trying to run sel4 on a hikey board, I'm following this wiki https://wiki.sel4.systems/Hardware/HiKey . I'm having issues as the link to the linaro-edk2 patch does not work(asks for some auth) , can someone provide another link or direct me . Thank you

2 1

Image lies outside of usable physical memory
by Alexander Boettcher 22 Jul '16

22 Jul '16

Hi, I want to boot seL4 (x86) 3.2.0 on a native machine (Lenovo X201) and I get a message like: End of loaded userland image lies outside of usable physical memory seL4 called fail at sel4/src/arch/x86/kernel/boot_sys.c: in function boot_sys, saying "boot_sys failed for some reason :( (Full log below attached) It seems that our used bootloader put the image to high in physical memory for seL4 (the other x86 kernels we use don't complain so far). Is this right that only memory below PPTR_TOP (0x1fc00000 on x86 3.2.0) can be used for the initial boot modules? Can this be changed or should we not try to touch this define (it seems to be derived from various other defines). Is there maybe a description about the required physical memory layout of the kernel and why it has to be as it is? Just in order to understand better the constraints we probably have to apply to our bootloader ;-) Thanks in advance, Alex. Parsing GRUB physical memory map Physical Memory Region from 0 size 89000 type 1 Physical Memory Region from 89000 size 17000 type 2 Physical Memory Region from d2000 size 2000 type 2 Physical Memory Region from dc000 size 24000 type 2 Physical Memory Region from 100000 size bb17c000 type 1 Adding physical memory region 0x100000-0x1fc00000 Physical Memory Region from bb27c000 size 6000 type 2 Physical Memory Region from bb282000 size dd000 type 1 Physical Memory Region from bb35f000 size 12000 type 2 Physical Memory Region from bb371000 size 81000 type 4 Physical Memory Region from bb3f2000 size 1d000 type 2 Physical Memory Region from bb40f000 size 60000 type 1 Physical Memory Region from bb46f000 size 1f9000 type 2 Physical Memory Region from bb668000 size 80000 type 4 Physical Memory Region from bb6e8000 size 27000 type 2 Physical Memory Region from bb70f000 size 8000 type 1 Physical Memory Region from bb717000 size 8000 type 2 Physical Memory Region from bb71f000 size 4c000 type 1 Physical Memory Region from bb76b000 size c000 type 4 Physical Memory Region from bb777000 size 3000 type 3 Physical Memory Region from bb77a000 size 7000 type 4 Physical Memory Region from bb781000 size 1000 type 3 Physical Memory Region from bb782000 size 9000 type 4 Physical Memory Region from bb78b000 size 1000 type 3 Physical Memory Region from bb78c000 size 13000 type 4 Physical Memory Region from bb79f000 size 60000 type 3 Physical Memory Region from bb7ff000 size 1000 type 1 Physical Memory Region from bb800000 size 800000 type 2 Physical Memory Region from bc000000 size 4000000 type 2 Physical Memory Region from e0000000 size 10000000 type 2 Physical Memory Region from feaff000 size 1000 type 2 Physical Memory Region from fec00000 size 10000 type 2 Physical Memory Region from fed00000 size 0 type 2 Physical Memory Region from fed1c000 size 4000 type 2 Physical Memory Region from fed20000 size 70000 type 2 Physical Memory Region from fee00000 size 1000 type 2 Physical Memory Region from ff000000 size 1000000 type 2 Physical Memory Region from 0 size 38000000 type 1 Kernel loaded to: start=0x100000 end=0x147000 size=0x47000 entry=0x10003e ACPI: RSDP paddr=0xf68e0 ACPI: RSDP vaddr=0xdfcf68e0 ACPI: RSDT paddr=0xbb7f07a2 ACPI: RSDT vaddr=0xdfff07a2 ACPI: DMAR paddr=0xbb781000 ACPI: DMAR vaddr=0xdff81000 ACPI: IOMMU host address width: 36 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1d fun=0x0 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1a fun=0x0 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x2 fun=0x0 ACPI: 3 IOMMUs detected ACPI: MADT paddr=0xbb7feb45 ACPI: MADT vaddr=0xdfffeb45 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_APIC apic_id=0x1 ACPI: MADT_APIC apic_id=0x4 ACPI: MADT_APIC apic_id=0x5 ACPI: MADT_IOAPIC ioapic_id=1 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd ACPI: 4 CPU(s) detected Detected 4 CPUs. Only just 1 Detected 1 boot module(s): module #0: start=0x7fc7a000 end=0x7ffff338 size=0x385338 name='/image.elf' ELF-loading userland images from boot modules: size=0x385000 v_entry=0x2000000 v_start=0x2000000 v_end=0x2385000 p_start=0x80000000 p_end=0x80385000

2 1

3.1.0 to 3.2.0 (x86) upgrade issue
by Alexander Boettcher 22 Jul '16

22 Jul '16

Hello, after upgrading the seL4 kernel (x86) from 3.1.0 to 3.2.0 we get for the very first invocation of seL4_X86_Page_Map an errorcode of *3* (seL4_IllegalOperation). We bisected the commits between 3.1.0 and 3.2.0 and [0] is the first bad commit for us. If we use the 3.2.0 release with [0] reverted on top than everything works as before - so no changes to Genode/seL4 as used for the 3.1.0 kernel are necessary. It's a know issue, or maybe something changed which must be adjusted in userland/roottask ? Thanks, Alex. [0] https://github.com/seL4/seL4/commit/c8819792d76ae5aecd89bcff656ca561e62959a5

2 2

Re: [seL4] [sel4utils question] stack size of the second process
by Kofidoku.Atuah＠data61.csiro.au 21 Jul '16

21 Jul '16

Hi, Our malloc currently uses mmap() for large allocations (and therefore the matching munmap() for freeing those large allocations). See https://github.com/seL4/musllibc/blob/sel4/src/malloc/malloc.c#L352. So while the mmap() call is implemented, the munmap() call is not, and this is why you're seeing this issue with "syscall 91" not being successful: https://github.com/seL4/musllibc/blob/sel4/arch/i386/bits/syscall.h#L92 https://github.com/seL4/musllibc/blob/sel4/arch/arm/bits/syscall.h#L67 ? Usually you allocate such a big chunk of memory for private use and management, so free() probably isn't a mission critical thing here (for the tutorials), unless there are factors I can't see -- let me know if this was helpful -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO E kofidoku.atuah(a)csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61

1 0

[sel4utils question] stack size of the second process
by Norrathep Rattanavipanon 21 Jul '16

21 Jul '16

Hi, So I followed hello-4 example. I can create a static array inside a second process (hello-4-app) and the second process works fine. However, when I try to increase the size of an array to 80,000 bytes, the second process wont start. I tried to increase ALLOCATOR_VIRTUAL_POOL_SIZE but it still does not work. Any help would be appreciated. Thanks, -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

1 1

Re: [seL4] [sel4utils question] stack size of the second process
by Kofidoku.Atuah＠data61.csiro.au 20 Jul '16

20 Jul '16

Hi, Thanks for popping by! The answer to the question in the subject line of your email (stack size of processes spawned by sel4utils_configure_process()) is that sel4utils_configure_process() calls sel4utils_configure_thread(), which allocates the stack using vspace_new_pages(), found here: (https://github.com/seL4/seL4_libs/blob/master/libsel4vspace/include/vspace/…) The stack size is determined by CONFIG_SEL4UTILS_STACK_SIZE, which can be set in your `make menuconfig` settings. Try: `make menuconfig` -> select "seL4 Libraries" -> "libsel4utils" and change the stack size as desired. That said, > However, when I try to increase the size of an array to 80,000 bytes, the second process wont start. I tried to increase ALLOCATOR_VIRTUAL_POOL_SIZE but it still does not work. Sorry, I'll need to know a bit more about what's going on here: could you post some more detailed output, or maybe a diff, so I can try to aid you? --Yours truly, Kofi

1 0

Cortex-M port?
by Stefan Wallentowitz 18 Jul '16

18 Jul '16

Hi, I was wondering if anyone ever started a port to a v7-M platform? Cheers, Stefan

2 1

3.2.0 release issues?
by Jeff Waugh 18 Jul '16

18 Jul '16

Hey there, I noticed the wiki "latest" links now point to 3.2.0. I haven't seen an announcement for 3.2.0 yet, so perhaps this is all a matter of staging, but the current sel4test manifest points to 3.2.x-compatible tags that don't exist in most of the repos. Just thought I'd mention it as I imagine it's the primary way people acquire new releases. Thanks, Jeff

2 4

RELEASE: seL4 3.2.0 release
by Parthasarathi Susarla 18 Jul '16

18 Jul '16

We are pleased to announce the release of 3.2.0 of seL4. This release contains the following changes: * ARM Hypervisor support. * ARM Jetson-TK1: Cleanup. * Benchmarking now supports tracking of syscalls. * Support for XSAVE feature set for x86 CPUs. * Simplified ARM platform selection during configuration. = ABI Changes = * seL4_BootInfo has a new entry for IOSpace caps for ARM SMMU. The release tarballs can be directly downloaded from: https://github.com/seL4/seL4/archive/3.2.0.tar.gz 7210ecc65f0f8a04490605e92f7b89b4 3.2.0.tar.gz The manual for this release can be downloaded here: http://sel4.systems/Info/Docs/seL4-manual-3.2.0.pdf Please let us know of any issues that you run into by creating an issue in the issue tracker: https://github.com/seL4/seL4/issues -- Partha Susarla <parthasarathi.susarla(a)nicta.com.au> ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

verification requirements
by Gergely Buday 13 Jul '16

13 Jul '16

Hi, what are the requirements for running the whole sel4 verification proof? Is 32G RAM and 20G disk space enough? How about the processor needs? I guess what is enough in batch mode will be enough for interactive development. - Gergely

2 1

Frame buffer
by Rinat Dobrokhotov 09 Jul '16

09 Jul '16

Hello, Could you tell me if framebuffer is released for seL4? -- Best Regards, Rinat Dobrokhotov

6 7

[sel4] persistent storage / file system
by rahul mahadev 06 Jul '16

06 Jul '16

Hi, I wanted to know if persistent storage/ file system have been tried on sel4 before ,if so can I have more details on it. Regards , Rahul S Mahadev

5 5

Capabilities of binary images
by Norrathep Rattanavipanon 06 Jul '16

06 Jul '16

Hi, I need to access the user image from a user application for verifying that the binary is installed correctly. So I found in bootinfo.h that it contains userImageFrames and its supposed to be the one I'm looking for but it gave me an error when I map the frames via vspace_map_pages(vspace, info->userImageFrames.start, ...) at the root task. The error is : ERROR:sel4utils_map_page_pd:223: Error mapping pages, bailing: 2 What am I doing wrong here? Best, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

3 2

Get real time clock data (and timer) from I.MX6
by Norrathep Rattanavipanon 30 Jun '16

30 Jun '16

Hi, I was wondering if there's any real time clock implementation for I.MX6 in sel4. And if there isnt any, what would be the best way to use a timer in sel4 (since I saw many implementations of those)? through sel4platsupport_get_default_timer? Best, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 5

ARM Hypervisor extensions in master
by Adrian Danis 28 Jun '16

28 Jun '16

The ARM hypervisor extensions are now supported in the master seL4 kernel. This support has existed on a public development branch (arm_hyp) for some time, but this marks the beginning of proper support and a verification target. What is done: * Hypervisor extensions supported on odroid-xu and Jetson TK1 platforms * SystemMMU supported on Jetson TK1 platform Limitations: * Currently any usage of hyp extensions or SystemMMU is *not* verified * SystemMMU contains work around currently for the VMM to map in large amounts of memory (fix for this relies on a kernel change currently being verified) You can use the manifest https://github.com/seL4proj/camkes-arm-vm-manifest to get the project https://github.com/seL4proj/camkes-arm-vm and then use one of the two default configs for the TK1 and odroid-xu platforms. Adrian ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

camkes-VM with QEMU and virutal PCI device
by Samuel Weiser 28 Jun '16

28 Jun '16

Hi again, I'm playing around with camkes-vm in QEMU+KVM. I want to add a virtual PCI device to Linux, which is running as vm0 on top of seL4. However, I got stuck with some errors during system boot. My setup is as follows: QEMU is configured to share a 1MB memory region between the host and the QEMU guest (seL4). Here's what QEMU sets up: (qemu): info mtree ... 00000000fe000000-00000000fe0fffff (prio 1, RW): ivshmem-bar2-container 00000000fe000000-00000000fe0fffff (prio 0, RW): ivshmem.bar2 00000000febf1000-00000000febf10ff (prio 1, RW): ivshmem-mmio ... (qemu): info pci ... Bus 0, device 4, function 0: RAM controller: PCI device 1af4:1110 IRQ 11. BAR0: 32 bit memory at 0xfebf1000 [0xfebf10ff]. BAR2: 64 bit prefetchable memory at 0xfe000000 [0xfe0fffff]. id "" ... I adapted a previously working configuration (optiplex9020.camkes) accordingly with what I thought should be correct. Especially, I added vm0_config.pci_devices_iospace and vm0_config.pci_devices as well as the PCI irq. Here's the configuration: configuration { VM_CONFIGURATION_DEF() VM_PER_VM_CONFIG_DEF(0, 2) vm0.simple_untyped24_pool = 12; vm0.heap_size = 0; vm0.guest_ram_mb = 1536; vm0.kernel_cmdline = VM_GUEST_CMDLINE; vm0.kernel_image = C162_KERNEL_IMAGE; vm0.kernel_relocs = C162_KERNEL_IMAGE; vm0.initrd_image = C162_ROOTFS; vm0.iospace_domain = 0x00; vm0_config.ram = [ [ 0x20800000, 23 ], [ 0x21000000, 24 ], [ 0x22000000, 25 ], [ 0x24000000, 26], [ 0x28000000, 27], [0x30000000, 28], [0x40000000, 29] , [0x60000000, 30], [0xa0000000, 28]]; vm0_config.ioports = [ {"start":0x2f8, "end":0x2ff, "pci_device":0, "name":"COM2 Serial Port"}, {"start":0x2e8, "end":0x2ef, "pci_device":0, "name":"COM4 Serial Port"} ]; vm0_config.irqs = [ {"name":"Serial", "source":3, "level_trig":0, "active_low":0, "dest":3}, {"name":"PCI", "source":11, "level_trig":1, "active_low":1, "dest":11} ]; vm0_config.pci_devices_iospace = 1; vm0_config.pci_devices = [ {"name":"PCI", "bus":0, "dev":0x04, "fun":0, "irq":"PCI", "memory":[ {"paddr":0xfe000000, "size":0x100000, "page_bits":12}, ], }, ]; } However, after creating the MMIO frames and doing some other stuff, the boot process fails, as shown below. The error also occurs if I change or completely remove just the "memory" definition of my PCI device. I also tried different values for "iospace_domain" (QEMU should use 0 as default PCI domain). Thanks in advance for any hints and ideas! Best, Sammey Starting Loader... Parsing bootinfo... 1041793 free cap slots, from 6783 to 1048576 Untyped memory (24) 0x0000000000100000 - 0x0000000000108000 0x0000000000108000 - 0x0000000000109000 0x0000000003000000 - 0x0000000004000000 0x0000000004000000 - 0x0000000008000000 0x0000000008000000 - 0x0000000010000000 0x0000000010000000 - 0x0000000018000000 0x0000000018000000 - 0x000000001c000000 0x000000001c000000 - 0x000000001e000000 0x000000001e000000 - 0x000000001f000000 0x000000001f000000 - 0x000000001f800000 0x000000001f800000 - 0x000000001fc00000 0x0000000001b6b000 - 0x0000000001b6c000 0x0000000001b6c000 - 0x0000000001b70000 0x0000000001b70000 - 0x0000000001b80000 0x0000000001b80000 - 0x0000000001c00000 0x0000000001c00000 - 0x0000000001e00000 0x0000000001e00000 - 0x0000000001f00000 0x0000000001f00000 - 0x0000000001f80000 0x0000000001f80000 - 0x0000000001fc0000 0x0000000001fc0000 - 0x0000000001fe0000 0x0000000001fe0000 - 0x0000000001ff0000 0x0000000001ff0000 - 0x0000000001ff2000 0x0000000001ff2000 - 0x0000000001ff3000 0x0000000001ff3000 - 0x0000000001ff3800 Loader is running in domain 0 Device untyped memory (30) 0x0000000000001000 - 0x0000000000002000 0x0000000000002000 - 0x0000000000004000 0x0000000000004000 - 0x0000000000008000 0x0000000000008000 - 0x0000000000010000 0x0000000000010000 - 0x0000000000020000 0x0000000000020000 - 0x0000000000040000 0x0000000000040000 - 0x0000000000080000 0x0000000000080000 - 0x0000000000100000 0x000000001fc00000 - 0x0000000020000000 0x0000000020001000 - 0x0000000020002000 0x0000000020002000 - 0x0000000020004000 0x0000000020004000 - 0x0000000020008000 0x0000000020008000 - 0x0000000020010000 0x0000000020010000 - 0x0000000020020000 0x0000000020020000 - 0x0000000020040000 0x0000000020040000 - 0x0000000020080000 0x0000000020080000 - 0x0000000020100000 0x0000000020100000 - 0x0000000020200000 0x0000000020200000 - 0x0000000020400000 0x0000000020400000 - 0x0000000020800000 0x0000000020800000 - 0x0000000021000000 0x0000000021000000 - 0x0000000022000000 0x0000000022000000 - 0x0000000024000000 0x0000000024000000 - 0x0000000028000000 0x0000000028000000 - 0x0000000030000000 0x0000000030000000 - 0x0000000040000000 0x0000000040000000 - 0x0000000060000000 0x0000000060000000 - 0x00000000a0000000 0x00000000a0000000 - 0x00000000e0000000 0x00000000e0000000 - 0x0000000000000000 Sorting untypeds... Untyped 0 (cptr=1a39) is of size 15. Placing in slot 17... Untyped 1 (cptr=1a3a) is of size 12. Placing in slot 20... Untyped 2 (cptr=1a3b) is of size 24. Placing in slot 5... Untyped 3 (cptr=1a3c) is of size 26. Placing in slot 2... Untyped 4 (cptr=1a3d) is of size 27. Placing in slot 0... Untyped 5 (cptr=1a3e) is of size 27. Placing in slot 1... Untyped 6 (cptr=1a3f) is of size 26. Placing in slot 3... Untyped 7 (cptr=1a40) is of size 25. Placing in slot 4... Untyped 8 (cptr=1a41) is of size 24. Placing in slot 6... Untyped 9 (cptr=1a42) is of size 23. Placing in slot 7... Untyped 10 (cptr=1a43) is of size 22. Placing in slot 8... Untyped 11 (cptr=1a44) is of size 12. Placing in slot 21... Untyped 12 (cptr=1a45) is of size 14. Placing in slot 18... Untyped 13 (cptr=1a46) is of size 16. Placing in slot 15... Untyped 14 (cptr=1a47) is of size 19. Placing in slot 11... Untyped 15 (cptr=1a48) is of size 21. Placing in slot 9... Untyped 16 (cptr=1a49) is of size 20. Placing in slot 10... Untyped 17 (cptr=1a4a) is of size 19. Placing in slot 12... Untyped 18 (cptr=1a4b) is of size 18. Placing in slot 13... Untyped 19 (cptr=1a4c) is of size 17. Placing in slot 14... Untyped 20 (cptr=1a4d) is of size 16. Placing in slot 16... Untyped 21 (cptr=1a4e) is of size 13. Placing in slot 19... Untyped 22 (cptr=1a4f) is of size 12. Placing in slot 22... Untyped 23 (cptr=1a50) is of size 11. Placing in slot 23... Creating objects... ... Creating object conn1_mmio_frame_4261412864 in slot 6808, from untyped 1a3c... device frame, paddr = 0xfe000000, size = 12 bits Creating object conn1_mmio_frame_4261416960 in slot 6809, from untyped 1a3c... device frame, paddr = 0xfe001000, size = 12 bits Creating object conn1_mmio_frame_4261421056 in slot 6810, from untyped 1a3c... device frame, paddr = 0xfe002000, size = 12 bits ... Creating object vm_vm0_pre_init_ep in slot 10275, from untyped 1a3c... Creating object conn1_iospace_32 in slot 10276, from untyped 1a3c... <=== This is ignored! Creating object conn4_iport_760_767 in slot 10276, from untyped 1a3c... ... Populating slot 21 with cap to conn1_iospace_32... minting (with badge/guard 0x20)... <<seL4 [decodeCNodeInvocation/107 T0xe1ff3900 "rootserver" @804a911]: CNode Copy/Mint/Move/Mutate: Source slot invalid or empty.>> capDL-loader :: << Error: init_cnode_slot:1689: seL4_FailedLookup >>

2 1

Autocorres Error.
by Dan DaCosta 24 Jun '16

24 Jun '16

seL4 Developers: I apologize in advance if this is not the correct place for this email. I am experimenting with Autocorres as an intern at Rockwell Collin's Advanced Technology Center in Minnesota. My latest experiment is in building a small verified library for manipulation and analysis of adjacency lists. My initial work towards this end generated the following error: exception CTERM raised (line 948 of "~/development/rockwellcollins/verification/l4v/tools/autocorres/utils.ML"): autocorres: Internal var uu_::"int" is exposed. Please notify the AutoCorres maintainers of this failure. In the meantime, use "autocorres [keep_going]" to ignore the failure. I am using the latest version of Autocorres and Isabelle. The c and theory file that generated this error can be found here: https://github.com/chaosape/autocorresexperiments/tree/master/graph Thanks! Dan DaCosta

3 3

Resolving issue using camkes-vm with qemu
by Samuel Weiser 20 Jun '16

20 Jun '16

Hi, I just want to share some information which I needed to run camkes-vm with qemu, especially addressing one issue which prevented the guest vm to boot. I basically follow the recommendations of Adrian in [1] and only focus on the simple case without vt-d. 1. use the 'optiplex9020_onevm' configuration as it basically just specifies physical RAM. 2. enable nested KVM [2,3] 3. run QEMU with enough RAM: qemu-system-i386 -nographic \ -m 3GB \ -enable-kvm \ -cpu host \ -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-experimental-image-ia32-pc99 Following the above steps gives you a booting camkes vmm, however it fails to eventually activate Intel vt-x, needed to run the guest vm. The reason for that is that the seL4 kernel requires the IA32_FEATURE_CONTROL MSR to have VMXON enabled (bit 2) and locked (bit 0) (i.e. a value of 5). Normally, it's the job of the BIOS to do so, however I couldn't find an appropriate QEMU BIOS ROM which does so. The quick workaround is to enable VMXON within the seL4 kernel itself. The corresponding diff is attached. With this minor change, the recompiled kernel works like a charm. PS: One could consider making a separate option in Kconfig for that purpose. Best, Sammey [1] https://sel4.systems/pipermail/devel/2016-March/000717.html [2] http://www.rdoxenham.com/?p=275 [3] https://wiki.archlinux.org/index.php/QEMU#Enabling_KVM

2 1

Rust application support
by Kent.Mcleod＠data61.csiro.au 20 Jun '16

20 Jun '16

Using rust (https://www.rust-lang.org) in user applications on top of seL4 with existing C libaries and apps now has limited support. See here for more information: https://wiki.sel4.systems/Rust What you can do: + Build system support for using a rust cargo project as a library or app on seL4 + Use most core libraries (core, alloc, collections, rustc_unicode, and a limited std) + Use rust dependencies from crates.io on seL4 + Use rust to implement camkes components + Using rust's FFI support it is possible to call rust from C and C from rust. Two sample apps are located here: https://github.com/SEL4PROJ/rust-camkes-samples Instructions for building and running are on the wiki page. Has been tested on x86 i386 and arm kzm both in qemu and hardware. Caveats: + Rust's libstd functionality is limited by which muslc syscalls are supported on seL4. + Rust's libstd requires muslc thread local storage support which is not currently available on seL4. We currently use a muslc branch called rust that uses a global TLS struct. Kent McLeod Kernel engineer / Thesis Student DATA61 | CSIRO

1 0

WIll seL4 support any Unikernel
by XilongPei 16 Jun '16

16 Jun '16

Hi, According to wikipedia.org, Unikernels are specialised, single address space machine images constructed by using library operating systems. A developer selects, from a modular stack, the minimal set of libraries which correspond to the OS constructs required for their application to run. These libraries are then compiled with the application and configuration code to build sealed, fixed-purpose images (unikernels) which run directly on a hypervisor or hardware without an intervening OS such as Linux or Windows. Will seL4 support any unikernel, such as Drawbridge or MirageOS, in the future? Xilong Pei Tongji University Shanghai, China 2016/6/13

3 2

Beaglebone black/CAmkES issue
by Julien Delange 16 Jun '16

16 Jun '16

I am using the second serial interface of the beaglebone black. According to the source code (in libsel4platsupport/plat_include/am335x/sel4platsupport/plat/hw/soc_AM335x.h), the address is 0x48022000). The following line is found in the source #define SOC_UART_1_REGS (0x48022000) So, in CAmkES, I configure the hardware component that represents the serial hardware component with the following attributes: drv.mem_attributes = "0x48022000:0x1000"; The application compiles fine. However, when launching the image on the target, I have the following issue. Any idea about how to solve this? Does anybody successfully used UART1 on the beaglebone black? Or have any idea/suggestion to investigate? Thanks. Julien. Creating object conn1_frame__timer_0 in slot 728, from untyped 29b... device frame, paddr = 0x48040000, size = 12 bits Creating object conn2_frame__Cons_PingMe_0 in slot 729, from untyped 29b... device frame, paddr = 0x48022000, size = 12 bits capDL-loader :: << Error: Failed to find device frame at paddr = 0x48022000 >> Ignoring call to sys_rt_sigprocmask Ignoring call to sys_gettid sys_tkill assuming self kill

4 8

Tidying and real-time
by Jeff Waugh 16 Jun '16

16 Jun '16

This commit… https://github.com/seL4/seL4/commit/c5b6a6a58aae75129cdf5a83f861bdacddbf51d6 … is pleasing. As is the RT API. Passive servers! A seemingly viable and sensible approach to user-space scheduling! Just a quick thumbs up for recent progress. :-)

1 0

CAmkES parsing issue
by Julien Delange 11 Jun '16

11 Jun '16

Hi, I am trying to build a camked application with a UART driver. When trying to build the application, I got the following error: While rendering uart_mem.from.source: 'drv' However, the component is well define. How can I try to get more information/debug of the camkes assembly and find out what is wrong? Thanks! Note: the project can be found there: https://drive.google.com/file/d/0Bxl72qH3r6BjRGxYSXd2LUllcDQ/view?usp=shari…

3 6

camkes arm vm I/0 devices
by Josh Tuttle 08 Jun '16

08 Jun '16

Hey, We have been playing around with the busybox for tk1 that was included in the build. While trying to verify all the I/0 devices, we noticed that the Ethernet device would not come up. Looking though dmesg, it seems to load a driver but never initializes a device. Ifconfig just errors when trying to bring up eth0. Has anyone verified the I/0 devices on tk1 using this build? Not being familiar with busybox, can we follow this: http://elinux.org/Jetson/Busybox_RootFS guide to building a busybox image to include all appropriate drivers? Thanks, Josh

2 1

seL4 benchmarks available
by Anna Lyons 07 Jun '16

07 Jun '16

Hi all, I've just finished pushing the seL4 benchmarking suite out to github. Get it: * manifest: https://github.com/seL4/sel4bench-manifest * explore the applications: https://github.com/seL4/sel4bench. Cheers, -- Anna Lyons Kernel engineer / PhD Student DATA61 | CSIRO E anna.lyons(a)nicta.com.au<mailto:anna.lyons@nicta.com.au> www.data61.csiro.au<http://www.data61.csiro.au> CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

Unable to build camkes-vm
by Samuel Weiser 07 Jun '16

07 Jun '16

Hello, didn't manage to build camkes-vm. Is there any working setup available or did I make something wrong? 1.) I tried to build c162_twovm_defconfig with the "default.xml" manifest 1a.) I get compile errors regarding some definitions of seL4_X86.... It seems that seL4_libs (March 2016) are inconsistent with the kernel version (Dec 2015). Updating to a newer kernel, i.e. 3.1.0 solves this issue but creates new ones: 1b.) The bootinfo struct is too big to fit one page. I get the error: compile_assert(bi_size, sizeof(seL4_BootInfo) <= BIT(BI_FRAME_SIZE_BITS)) So I reduced the max. no of bootinfo untyped caps from 800 to 167 1c.) Error: No rule to make target 'libsel4simple-default', needed by 'libsel4platsupport-y' Since the kernel is not stable, it falls back to default but does not manage to correctly reference the default lib. First, I added the missing symlink in libs. Then, I added the default lib to the main Kconfig and the apps/c162_twovm/Kbuild. 1d.) The next error is: x86/pc99/include/vmm/guest_state.h:60:44: error: unknown type name ‘seL4_VCPUContext’ ... 2.) I also tried building with the "working.xml" manifest, which already failed to fetch the correct revisions 2a.) In the working.xml, I fixed the seL4_libs upstream to 'master' Also, the kernel revision is broken, seL4.git points to an experimental commit, which couldn't be fetched. I changed it to kernel 3.1.0. 2b.) The same error as in 1d) appears. This is where I gave up. Any hints? Thanks in advance, Sammey

2 1

VM on SeL4 for TK1
by Joshua Tuttle 06 Jun '16

06 Jun '16

Hi, I am working with Peng Xie to run the vm for tk1 code that Adrian gave out a couple of days ago, located at https://github.com/seL4proj/camkes-arm-vm-manifest. We have successfully been able to build and run on our tk1 board, but are met with a buildroot login prompt. What is the username and password, we should be using? Also, is this a para-virtualized or fully-virtualized environment? Thanks, Josh Tuttle Research Engineer Intelligent Automation, Inc. 15400 Calhoun Dr., Suite 109 Rockville, MD 20855 Ph: (301) 795-2706 jtuttle(a)i-a-i.com<mailto:jtuttle@i-a-i.com> ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

2 1

Latest experimental RT kernel released
by Anna Lyons 03 Jun '16

03 Jun '16

= Latest experimental RT kernel released = The RT kernel provides + periodic scheduling, + temporal isolation, + support for criticality and criticality mode changes, + temporal exceptions, .. and more. == Caveats == The RT kernel does not compile or run on all platforms, we currently support: + x86: ia32 platforms with TSC_DEADLINE mode + ARM: Sabre lite, Beagle board, and Odroid-xu (all armv7-a). The RT kernel is not verified, and as such we provide no guarantees, and there's likely still some bugs hiding in there. The other platforms require driver work at user level and in the kernel. If you are keen to get a certain platform working, contributions are welcome! == Available == + *Kernel branch* on github: https://github.com/seL4/seL4/tree/rt + *Release notes* (detailed API changes from current seL4 latest release): https://wiki.sel4.systems/seL4%201.0.0-rt-dev + *RT kernel manual* http://sel4.systems/Info/Docs/seL4-manual-1.0.0-rt-dev.pdf + *whitepaper* http://arxiv.org/abs/1606.00111 == Try it == Check out the rt branch of sel4test-manifest with repo: $ repo init -u https://github.com/seL4/sel4test-manifest.git -b rt Feedback on the API would be *extremely* valued. Enjoy! -- Anna Lyons Kernel engineer / PhD Student DATA61 | CSIRO E anna.lyons(a)nicta.com.au<mailto:anna.lyons@nicta.com.au> www.data61.csiro.au<http://www.data61.csiro.au> CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

3 3

Memory allocation & threads
by Доброхотов Ринат 03 Jun '16

03 Jun '16

Hello, I don't understand how static and virtual pool's size related to thread's available working space. I got the example app from the sel4-tutorials project with process creation (app-4). A static pool and a virtual pool are created in this app. I have done experiments with size of this pools and size of arrays in the second thread. For example I set size of virtual pool to zero, as I understand this pool need to create kernel objects. Also I define the test array size of (1 << 23)~8,3Mb. If test array is static, static pool size must be equal to ((1 << seL4_PageBits) * 100) ~0,4Mb. If test array is no static, static pool size not limited. Why is it so? -- Best Regards, Rinat Dobrokhotov

4 4

Will the codes in branch rt be merged into master
by XilongPei 02 Jun '16

02 Jun '16

Hi, I got information from https://wiki.sel4.systems/seL4%201.0.0-rt-dev , the development branch for the seL4 realtime extensions. My question is that will the codes in branch rt be merged into master, and add some build option. If a working tree always not in the master branch, it will be very difficult to be managed. Xilong Pei Tongji University 2016/6/1

2 1

RT branch questions
by Julien Delange 27 May '16

27 May '16

I am currently trying the RT branch and have some questions: 1. What emulator to use in order to try the examples? I am trying to use x86 with qemu but it seems that it does not work. I got the following trace at execution Starting node #0 APIC: unsupported platform, TSC-deadline mode is not supported seL4 called fail at /home/sel4/camkes-sc-tests/kernel/src/arch/x86/kernel/boot_sys.c:451 in function boot_sys, saying "boot_sys failed for some reason :( So, is there an emulator (for any supported platform) to try it? 2. In the RT-camkes extensions, I have the following new attributes: _period _budget _priority What is the semantics of these attributes? Any information about them? How they are supposed to be isolated from each other then? How to define the scheduling plan for the system then? Also, how these attributes apply to all thread: a thread is created for each interface of the component, so, how can we then define the priority/budget of each thread? Do these attributes apply to all the components of the thread? Thanks for any help/clarification. Julien. assembly { composition { component Client client1; component Client client2; } configuration { client1._priority = 100; client1._period = 10000; client1._budget = 7500; client2._priority = 50; client2._period = 10000; client2._budget = 7500; } }

3 6

Advice on camkes and regular seL4 for driver components
by Norrathep Rattanavipanon 27 May '16

27 May '16

Hello, I currently had codes, implemented as regular seL4, since camkes does not support some features (i.e. transferring capabilities or accessing address space outside the process), Everything is fine up to this point but now I want to create several drivers. And I found that the best and easiest way to do that is to use camkes. So is it possible to use existing regular codes in conjunction with camkes? Or would the best way be to implement drivers as regular seL4 codes? Thanks, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

building VMM on Jetson TK1 board
by PX 26 May '16

26 May '16

Hi, all we want to build the seL4-based VMM from https://github.com/smaccm/sel4arm-vmm.git on Jetson TK1 board. However, the seL4 kernel in that project does not support TK1 board. We want to use the new version seL4 version (arm_hyp) at https://github.com/seL4/seL4.git. My questions are: 1) It is feasible to do that? 2) If so, what are the correct steps to do that? 3) we try to compile these source code, but failed. We do the following modifications: A) we add TK1 source codes (i.e. TK1 folders from https://github.com/seL4/seL4.git) to the corresponding libraries in the VMM source code from https://github.com/smaccm/sel4arm-vmm.git; and B) we add relevant config definitions to the VMM code. Currently, we can successfully compile the seL4 kernel code, but have trouble to compile the VMM libraries. Do we miss something here? thanks Peng

2 1