- Devel - lists.sel4.systems

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

Availability of RT branch?
by Julien Delange 25 May '16

25 May '16

Hi all, Follow-up on our recent discussions on the RT branch: is the RT branch now available? How could I get it and access the related documentation? If not available, is there any idea of when it will be available? Thanks. Julien.

1 0

Getting timer info from seL4 kernel
by Will Klieber 19 May '16

19 May '16

Hi, Is there any way of obtaining the number of elapsed timer ticks from the seL4 kernel (using ARM / BeagleBoard platform)? I know the kernel uses this information internally for the scheduler, but I couldn't find any way of accessing it from userland. Specifically, my usage scenario is as follows. Two mutually distrustful programs are running, and each wants to run an action periodically. We want to temporally isolate the two programs using seL4 time domains. In this case, interacting with the hardware timer in userland seems difficult, since we want to get the updated time whenever a new timer tick arrives, but the userland device driver for the timer can only operate in exactly one of the seL4 time domains. Please let me know if I am misunderstanding something or if there might be a better way to approach this situation. Thanks, Will

5 6

Hello. I'm Kihyun-seo in South Korea.
by 서기현 17 May '16

17 May '16

Hello, I am a student of the Hanseo University in Korea. I want to create a UAV(drone) that uses Odroid XU4 Odroid XU4's Detailed Specifications = http://www.hardkernel.com/main/products/prdt_info.php?g_code=G143452239825 I want to install seL4 on the board for the security of the drones. The board has “ubuntu-15.04-robotics-odroid-xu4-201” 32bit linux version. I have two questions. First, I understood that after installing the seL4 first, and installing the linux later after seeing the 1.jpg. However, in the “https://wiki.sel4.systems/Getting%20started”. “Setting up your machine - These instructions are for Ubuntu. They assume you already know the basics of using the command line, compilers and GNU Make.” So then, Should I install the Linux(ubuntu) first, and install the seL4 later? I wonder what is correct. and I need more detailed explanation. Second, An error occurred during install the seL4 like 2.jpg. (command = "make menuconfig" in "Build ia32" part.) I need a solution about the error. Please answer my two questions.

3 2

multi-core support
by PX 17 May '16

17 May '16

Hi, Just want to double check if the seL4 under link https://github.com/seL4/sel4test supports multi-core? If so, the multi-core support is configured by default? If the sel4 does not support multi core, where can we get the experimental version supporting multi core? thanks Peng

2 1

Trusted Execution Environment on seL4
by rahul mahadev 11 May '16

11 May '16

Hi, I am Rahul Mahadev, I'm currently working on a Google Summer Of Code project with the organization lowRISC. My project is to implement a Trusted Execution Environment for the RISC-V platform. Last year's gsoc had a port of sel4 for RISC-V platform by Hesham Almatery. I plan on using seL4 for the port by either of the two methods. 1. paravirtualize OPTEE(Linaro's TEE) on top of seL4 2. implement an API similar to OPTEE for seL4 I have written a blog post explaining this, I wanted your opinion + ideas regarding this. link: http://mahadevrahul.blogspot.in/2016/05/gsoc-2016-implementing-trusted.html Thank You, Rahul Mahadev

2 1

Is the L4-embedded microkernel here means seL4
by XilongPei 20 Apr '16

20 Apr '16

Dear all, The web page http://ssrg.nicta.com.au/about/#achievements says: !$ All recent Apple iOS devices ship with a <http://www.apple.com/business/docs/iOS_Security_Guide.pdf> security processor controlled by a fork of our L4-embedded microkernel; I wonder whether the L4-embedded microkernel means seL4. thanks Xilong Pei Tongji University 2016/4/14

4 5

Problem porting sel4 into XU4
by Norrathep Rattanavipanon 19 Apr '16

19 Apr '16

Hi, I'm trying to port sel4 into ODROID-XU4 by following the wiki ( https://wiki.sel4.systems/Hardware/odriod-XU) So far I can successfully enable HYP mode as indicated by [ 0.198398] [c0] CPU: All CPU(s) started in HYP mode. [ 0.198433] [c0] CPU: Virtualization extensions available. as well as generate sel4test-driver-image-arm-exynos5 image. However, we cant do fastboot in XU4 since it doesnt have usb otg. Thus, I followed booting from sd card from https://wiki.sel4.systems/Hardware/General-ARM and copied the image into the first partition of sd card and do the following: Exynos5422 # fatload mmc 0 0x48000000 sel4test-driver-image-arm-exynos5 Exynos5422 # bootelf 0x48000000 and here's the output: ## Starting application at 0x41000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A7 r0p3 Switching CPU... ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p3 paddr=[41000000..4126401f] ELF-loading image 'kernel' paddr=[40000000..4002dfff] vaddr=[e0000000..e002dfff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[4002e000..40388fff] vaddr=[8000..362fff] virt_entry=13868 Enabling hypervisor MMU and paging Enabling MMU and paging Jumping to kernel-image entry point... �⧹I�AIq9Fy6 1)�a&I99)�6� Yq��摦P�^б��F��^/A�yyyyyyyyy�Y �)aay��XY�ǡyQ)�q��O�a@ Ia)!Fyaay �)��XY��.6I�)&FvF�6fF��VƑ�y��P�)aay��XY�ǡyQ)�q��O�a@ Ia Is it expected? or am I doing something wrong? Any help would be appreciated. Best, -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

3 6

building VMM on multi-core seL4
by PX 14 Apr '16

14 Apr '16

Dear all, I have some questions about building VMM on top of seL4. I know there is a sel4-based VMM on github (https://github.com/smaccm/sel4arm-vmm-manifest) Gernot also told me that this version of VMM does not support multi core. My questions are: 1) Can this single core version of VMM be run on top of multi-core sel4 just using one core without modification? 2) If not, what supports are missed in the multi-core version of sel4? I assume single-core version applications should be compatible with multi-core micro kernel. 3) If my assumption is wrong, what do we (as VMM developer) need to add to the VMM code to make it workable on the multi-core seL4? thanks Peng

2 1

Re: [seL4] [seL4/seL4] Real performance comparisons (#21)
by Gernot Heiser 11 Apr '16

11 Apr '16

On 11 Apr 2016, at 8:09 , fresheneesz <notifications(a)github.com<mailto:notifications@github.com>> wrote: I imagine this isn't the right place for this, but i can't find a better one. The correct one is this (devel(a)sel4.systems<mailto:devel@sel4.systems>) I see the performance comparisons at http://l4hq.org/docs/performance.php are run on all different processors. In its current form, the performance numbers here are completely useless. It would be very informative to have real performance benchmarks where the exact same processor is used for every OS in comparison. Otherwise, what am I supposed to do with those number? You’re right that comparisons across different processors are of limited power, but they aren’t useless either, especially when expressed in cycles (and ideally coupled with an understanding of the underlying hardware, eg the insane pipeline depth and speculation of the Pentium 4). However, given that these are different implementations spanning 20 years (some written in assembler), it isn’t possible to run them on the same hardware. The key observation is that no-one has ever done better on any of those processors. Gernot ________________________________ 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

i have some questions about domain and thread
by 김은영 04 Apr '16

04 Apr '16

Hi, all first, I do not speak English well. please answer to me easily. i'm studying seL4 kernel source code. i have some questions. 1. What is domain? i read manual but i don't understand well. I hope that you explain to me in detail about the domain. 2. What is the maximum number of threads that can be created in one domain? 3. Usually there is a function to create a new thread in kernel source code. but i can't find the function in seL4 kernel source code. What is the way to create a new user thread in seL4? also, what is the way to exit user thread in seL4? thanks.

2 1

Questions about Kernel Memory Mapping
by Daniel Wang 01 Apr '16

01 Apr '16

Hi all, I’m trying to understand the seL4 kernel source code. I think the memory mapping between physical memory and virtual memory is a key point since it is directly related to how kernel functions and manage badges. I noticed that the kernel turns on the paging very early. Can someone help me or point out some resources how kernel memory is allocated? Especially how during and after the booting what the kernel memory snapshot looks like and things like that. For example, I traced to map_kernel_window() function and even before that there is some pptr to paddr conversion. I would really appreciate the help. Thanks -Dan

3 2

seL4 Documentation/Tutoria
by xurongfeik 31 Mar '16

31 Mar '16

Hi folks Is there any Documentation/Tutorial about execution time for typical invocations of the seL4 system calls? Thanks! -- 许荣飞 Rongfei Xu 北京航空航天大学 Beihang University

2 1

sel4 build tutorial
by Jorge Alberto Garcia 31 Mar '16

31 Mar '16

Hi folks Is there any Documentation/Tutorial about how to do a build to start testing seL4 ? where can I find the current boards/architectures supported? Thanks!

2 2

Network Stack and Driver
by Norrathep Rattanavipanon 31 Mar '16

31 Mar '16

Hello, My name is Oak and I'm working with Prof. Gene Tsudik for remote attestation project using sel4. I know that you guys are not interested in developing network stack and drivers for sel4. But do you happen to know if anyone else has done some work with network stack and Wi-fi, Bluetooth or ethernet driver in sel4? Regards, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

答复:答复: 答复:Re: About the execution time of seL4 API
by xurongfeik 30 Mar '16

30 Mar '16

裴老师：您好！谢谢您的资料。现在我们学校有两个团队在做这方面的工作：其中我们实验室主要在模型层对seL4微内核进行建模仿真，主要是把微内核基本功能机制建模成为一个基本模型，对User Mode扩展部分以策略模型的方式与基本模型进行编织，从而建立一套在设计早期通过模型仿真验证策略的方法。目前，我们正着手建立一个能准确反映真实seL4微内核运行的模型，但是由于仿真时钟的不准确，我们希望在某一硬件环境上把seL4微内核模型下层的系统调用时间统计出来，通过时间累加计算seL4微内核模型上的应用执行过程。但是目前不知道该如何获取这些系统调用的执行时间，不知道裴老师您那边是否有相关的数据？另外一个团队主要是基于seL4微内核的操作系统开发，主要考虑分区、并发的不确定性。目前主要用于航天的应用中。如果裴老师有相关的研究，非常愿意共同合作！祝好！许荣飞在 2016-03-29 14:39:35，"XilongPei" <pei.xilong(a)kortide.com> 写道： XuRongfei: 我是同济大学电信学院老师裴喜龙，我们从事你说的这个方向好几年了。附件文件是我把seL4的说明书翻译成了中文，下面这个链接是我们做的高可用操作系统的项目工程页面。 http://elastos.org/redmine/projects/rt-elastos这个工程的源码在： https://github.com/elastos/HD-Elastos 我们基于AOP思想做的操作系统（正在开发中），官网：http://elastos.org/project-guide/ 源码开源在github: https://github.com/elastos/ElastosRDK5_0它基于AOP思想，提出一种构件技术CAR，并基于这个构件技术，实现了一… 希望国内做相关工作的人能合作，共同做一些大的工程。同济大学裴喜龙 2016年3月29日星期二发件人: Devel [mailto:devel-bounces@sel4.systems] 代表 xurongfeik 发送时间: 2016年3月29日 14:11 收件人: Thomas Sewell <thomas.sewell(a)nicta.com.au> 抄送:devel@sel4.systems 主题: [seL4] 答复:Re: About the execution time of seL4 API Thank you for your reply！ My name is XuRongfei, and I am a PHD student from China,Beijing. Now I focus on RTOS Modeling and Simulation. As we know, an important principle of microkernel design is the separation of mechanism and policy, it is what enables the construction of arbitrary systems on top of a minimal kernel. This separation of mechanism and policy is similar to AOM(Aspect-Oriented Modeling) and we can model the mechanism and policy separately. The biggest advantage is that analysis and verification of the policy applied in the implementation phase will be advanced to the design stage. As seL4 Microkernel is "the world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement". So if we want to construct an RTOS on top of seL4 Microkernel, it is necessary to simulate and analyse the policy model on the microkernel model first. To simulate the seL4 Microkernel model accurately and agree with the real situation, the execution time of seL4 typical API (such as send\receive\notify message and Resume\Suspend\Create thread) for certain platform. So how can we get the execution time of this APIs for certain platform? Is it possible? Thank you very much! At 2016-03-29 11:45:42, "Thomas Sewell" <thomas.sewell(a)nicta.com.au> wrote: Hmm, what do you mean by measuring the time? You can measure the typical execution time of various system calls easily enough by checking the CPU cycle counter. There is an internal "sel4bench" project which is similar to "sel4test" but measures timing information of some system calls. My understanding is that this will be released at some point in the near future. It's also possible to calculate the worst-case execution time of the kernel for some platforms. There's been a lot of research work on this http://ssrg.nicta.com.au/projects/TS/realtime.pml by various people at Data61/NICTA. It's probably possible to replicate for some platform of interest, but it might be quite difficult to do. Cheers, Thomas. On 29/03/16 14:06, xurongfeik wrote: Hello，everyone： When given a specific platform， is it possible to measure the execution time of seL4 API？ Anyone who has the relative data please send it to me， many thanks！！ -- 许荣飞 Rongfei Xu 北京航空航天大学 Beihang University _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel 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.

2 1

About the execution time of seL4 API
by xurongfeik 30 Mar '16

30 Mar '16

Hello，everyone： When given a specific platform， is it possible to measure the execution time of seL4 API？ Anyone who has the relative data please send it to me， many thanks！！ -- 许荣飞 Rongfei Xu 北京航空航天大学 Beihang University

3 4

Where can I get the information about Linux on seL4
by XilongPei 29 Mar '16

29 Mar '16

Hi Gernot, I found that the footer of http://ssrg.nicta.com.au/ is: Served by Apache on Linux on seL4 Whare can I get more information about Linux on seL4? Xilong Pei Tongji University 2016/3/29

2 1

Status of ARMv8 support for seL4 ?
by karim.allah.ahmed＠gmail.com 29 Mar '16

29 Mar '16

Hello, >From this roadmap [0], I can see that ARMv8 support is underway at the moment. Is this something that's going to be released soon given that the roadmap says Q1-2016 (at least 32-bit) ? [0] https://sel4.systems/Info/Roadmap -- Karim Allah Ahmed.

1 0

Porting Qubes OS to seL4 project
by Paul Vlase 28 Mar '16

28 Mar '16

No answer ... Am I doing something wrong? Beside not have patience. Could anyone tell about the status of the seL4 Qubes port project and who can I get in touch with to talk more about it? On Tue, Mar 22, 2016 at 11:35 PM, Paul Vlase <vlase.paul(a)gmail.com> wrote: > Hello, > > My name is Paul Vlase and I am following a master degree right now. I > am interested in porting the Qubes OS to seL4 project and I saw that > you are working already on it. Is there anything I can help you on > this project? > > Thank you, > Paul Vlase

2 1

sel4 in TrustZone
by Norrathep Rattanavipanon 27 Mar '16

27 Mar '16

Hi again :) Is it possible to run sel4 as a secure world OS in TrustZone? Has anyone successfully done that before? Thank you, -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

6 6

(simple?) build error?
by 谢文龙 27 Mar '16

27 Mar '16

I'm getting an error when building from Ubuntu. I'm building from: repo init -u https://github.com/seL4/sel4test-manifest.git I've configured with: make ia32_simulation_release_xml_defconfig and done "make menuconfig" accepting the defaults. Finally I run make and get errors: [KERNEL] [PBF_GEN] arch/object/structures.pbf [PBF_GEN] arch/api/shared_types.pbf [PBF_GEN] plat/machine/hardware.pbf [PBF_GEN] api/types.pbf [BF_GEN] arch/object/structures_gen.h [BF_GEN] arch/api/shared_types_gen.h [BF_GEN] plat/machine/hardware_gen.h [BF_GEN] api/types_gen.h [CPP] src/arch/x86/32/machine_asm.s [AS] src/arch/x86/32/machine_asm.o [CPP] src/arch/x86/32/traps.s [AS] src/arch/x86/32/traps.o [CPP] src/arch/x86/32/head.s [AS] src/arch/x86/32/head.o [CPP] src/arch/x86/halt.s [AS] src/arch/x86/halt.o [CPP] src/arch/x86/idle.s [AS] src/arch/x86/idle.o [TOUCH] sources_list_updated [CPP_GEN] kernel_all.c [CPP] kernel_all.c_pp [CP] kernel_final.c [CC] kernel_final.s [AS] kernel.o [LD] kernel.elf /usr/bin/ld:linker.lds_pp:5: syntax error collect2: error: ld returned 1 exit status make[1]: *** [kernel.elf] Error 1 make: *** [kernel_elf] Error 2 make V=3 mkdir -p /home/talos/seL4test/stage/x86/pc99 mkdir -p /home/talos/seL4test/build/x86/pc99 mkdir -p /home/talos/seL4test/images mkdir -p /home/talos/seL4test/stage/x86/pc99/common cp -R /home/talos/seL4test/tools/common/* /home/talos/seL4test/stage/x86/pc99/common [libs/libsel4] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4 CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4 -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4 SOURCE_DIR=/home/talos/seL4test/libs/libsel4 V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4' [GEN] include/sel4/types_gen.h [GEN] arch_include/x86/sel4/arch/invocation.h [GEN] include/sel4/shared_types_gen.h [GEN] sel4_arch_include/ia32/sel4/sel4_arch/invocation.h [HEADERS] [STAGE] api/* [STAGE] interfaces/* [STAGE] sel4/* [STAGE] interfaces/* [STAGE] sel4/* [STAGE] interfaces/* [STAGE] sel4/* [STAGE] sel4/* [STAGE] interfaces/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4' [libs/libsel4] done. [libs/libmuslc] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libmuslc CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libmuslc -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libmuslc/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libmuslc SOURCE_DIR=/home/talos/seL4test/libs/libmuslc V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libmuslc' make[1]: Nothing to be done for `default'. make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libmuslc' [libs/libmuslc] done. [libs/libcpio] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libcpio CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libcpio -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libcpio/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libcpio SOURCE_DIR=/home/talos/seL4test/libs/libcpio V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libcpio' [HEADERS] [STAGE] cpio/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libcpio' [libs/libcpio] done. [libs/libutils] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libutils CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libutils -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libutils/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libutils SOURCE_DIR=/home/talos/seL4test/libs/libutils V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libutils' [HEADERS] [STAGE] utils/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libutils' [libs/libutils] done. [libs/libsel4vka] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4vka CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4vka -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4vka/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4vka SOURCE_DIR=/home/talos/seL4test/libs/libsel4vka V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4vka' [HEADERS] [STAGE] vka/* [STAGE] vka/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4vka' [libs/libsel4vka] done. [libs/libsel4vspace] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4vspace CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4vspace -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4vspace/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4vspace SOURCE_DIR=/home/talos/seL4test/libs/libsel4vspace V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4vspace' [HEADERS] [STAGE] vspace/* [STAGE] vspace/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4vspace' [libs/libsel4vspace] done. [libs/libplatsupport] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libplatsupport CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libplatsupport -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libplatsupport/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libplatsupport SOURCE_DIR=/home/talos/seL4test/libs/libplatsupport V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libplatsupport' [HEADERS] [STAGE] platsupport/* [STAGE] platsupport/* [STAGE] platsupport/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libplatsupport' [libs/libplatsupport] done. [libs/libsel4simple] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4simple CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4simple -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4simple/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4simple SOURCE_DIR=/home/talos/seL4test/libs/libsel4simple V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4simple' [HEADERS] [STAGE] simple/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4simple' [libs/libsel4simple] done. [libs/libsel4simple-default] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4simple-default CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4simple-default -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4simple-default/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4simple-default SOURCE_DIR=/home/talos/seL4test/libs/libsel4simple-default V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4simple-default' [HEADERS] [STAGE] simple-default/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4simple-default' [libs/libsel4simple-default] done. [libs/libsel4platsupport] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4platsupport CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4platsupport -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4platsupport/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4platsupport SOURCE_DIR=/home/talos/seL4test/libs/libsel4platsupport V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4platsupport' [HEADERS] [STAGE] sel4platsupport/* [STAGE] sel4platsupport/* [STAGE] sel4platsupport/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4platsupport' [libs/libsel4platsupport] done. [libs/libelf] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libelf CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libelf -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libelf/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libelf SOURCE_DIR=/home/talos/seL4test/libs/libelf V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libelf' [HEADERS] [STAGE] elf/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libelf' [libs/libelf] done. [libs/libsel4utils] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4utils CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4utils -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4utils/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4utils SOURCE_DIR=/home/talos/seL4test/libs/libsel4utils V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4utils' [HEADERS] [STAGE] sel4utils/* [STAGE] sel4utils/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4utils' [libs/libsel4utils] done. [libs/libsel4muslcsys] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4muslcsys CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4muslcsys -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4muslcsys/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4muslcsys SOURCE_DIR=/home/talos/seL4test/libs/libsel4muslcsys V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4muslcsys' [HEADERS] [STAGE] arch_stdio.h [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4muslcsys' [libs/libsel4muslcsys] done. [libs/libsel4allocman] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4allocman CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4allocman -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4allocman/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4allocman SOURCE_DIR=/home/talos/seL4test/libs/libsel4allocman V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4allocman' [HEADERS] [STAGE] allocman/* [STAGE] allocman/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4allocman' [libs/libsel4allocman] done. [libs/libsel4test] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4test CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4test -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4test/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4test SOURCE_DIR=/home/talos/seL4test/libs/libsel4test V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4test' [HEADERS] [STAGE] sel4test/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4test' [libs/libsel4test] done. [apps/sel4test-tests] building... mkdir -p /home/talos/seL4test/build/x86/pc99/sel4test-tests CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/sel4test-tests -f /home/talos/seL4test/.config -f /home/talos/seL4test/apps/sel4test-tests/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/sel4test-tests SOURCE_DIR=/home/talos/seL4test/apps/sel4test-tests V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/sel4test-tests' [HEADERS] [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/sel4test-tests' [apps/sel4test-tests] done. [KERNEL] mkdir -p /home/talos/seL4test/build/kernel make -C /home/talos/seL4test/build/kernel -f /home/talos/seL4test/kernel/Makefile \ SOURCE_ROOT=/home/talos/seL4test/kernel O=/home/talos/seL4test/build/kernel V=3 \ TOOLPREFIX= \ CONFIG_DOMAIN_SCHEDULE= \ HAVE_AUTOCONF=1 NO_PRESERVE_TIMESTAMP=1 seL4 build options: =================== ARCH = x86 PLAT = pc99 CPU = TOOLPREFIX = PATH = /home/talos/bin:/home/talos/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games DEBUG = ASSERT = CONFIG_DEFS = CYCLE_COUNTER PERF_COUNTER=CYCLE_COUNTER DANGEROUS_CODE_INJECTION = CC = gcc CC_PATH = CPP = cpp CPP_PATH = AS = as AS_PATH = LD = ld LD_PATH = PARSER = c-parser PARSER_PATH = BF_GEN = bitfield_gen.py BF_GEN_PATH = SYSCALL_ID_GEN = syscall_header_gen.py SYSCALL_ID_GEN_PATH = INVOCATION_ID_GEN = invocation_header_gen.py INVOCATION_ID_GEN_PATH = XMLLINT_PATH = XMLLINT = xmllint.sh CFLAGS = -fno-stack-protector -m32 --std=c99 -nostdlib -nostdinc -ffreestanding -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -Wdeclaration-after-statement "-I/home/talos/seL4test/kernel/include/arch/x86/arch/32" "-I/home/talos/seL4test/kernel/include/plat/pc99/plat/32" -O2 -mno-mmx -mno-sse -mno-sse2 -mno-3dnow -DCYCLE_COUNTER -DPERF_COUNTER=CYCLE_COUNTER -DFASTPATH ASFLAGS = -Wa,--32 "-I/home/talos/seL4test/kernel/include/arch/x86/arch/32" "-I/home/talos/seL4test/kernel/include/plat/pc99/plat/32" CPPFLAGS = -DHAVE_AUTOCONF -I/home/talos/seL4test/include/generated -DARCH_X86 -DIA32 -DARCH_IA32 -D__KERNEL_32__ -DX86_32 -DPLAT_PC99 -DFASTPATH -DCYCLE_COUNTER -DPERF_COUNTER=CYCLE_COUNTER -DFASTPATH "-I/home/talos/seL4test/kernel/include/arch/x86/arch/32" "-I/home/talos/seL4test/kernel/include/plat/pc99/plat/32" LDFLAGS = -Wl,--build-id=none -Wl,-m,elf_i386 -nostdlib -nostdinc -Wl,--build-id=none -O2 make[1]: Entering directory `/home/talos/seL4test/build/kernel' [LD] kernel.elf /home/talos/seL4test/kernel/tools/changed.sh kernel.elf gcc -Wl,--build-id=none -Wl,-m,elf_i386 -nostdlib -nostdinc -Wl,--build-id=none -O2 -Wl,-T -Wl,linker.lds_pp \ -o kernel.elf src/arch/x86/32/machine_asm.o src/arch/x86/32/traps.o src/arch/x86/32/head.o src/arch/x86/halt.o src/arch/x86/idle.o kernel.o /usr/bin/ld:linker.lds_pp:5: syntax error collect2: error: ld returned 1 exit status make[1]: *** [kernel.elf] Error 1 make[1]: Leaving directory `/home/talos/seL4test/build/kernel' make: *** [kernel_elf] Error 2

2 1

sel4 benchmark
by Norrathep Rattanavipanon 25 Mar '16

25 Mar '16

Hello, What's the best way to benchmark my program inside sel4? I saw wiki page about running sel4 bench (https://wiki.sel4.systems/Benchmarking%20guide) but it wasnt filled yet. So I wonder if there's any public guide or tutorial on that? I also found this https://github.com/seL4/libplatsupport/blob/master/arch_include/x86/platsup… and tried both rdtsc_pure and rdtsc_cpuid but neither of them seems to produce reliable results. Best, -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

sel4 job offer
by Julien Delange 24 Mar '16

24 Mar '16

For information, we are looking for people to work on sel4. See https://www.appone.com/maininforeq.asp?Ad=250944&R_ID=1243309&Refer=http://… If you have any question, do not hesitate to contact me and/or apply! Julien.

1 0

Porting Qubes OS to seL4 project
by Paul Vlase 23 Mar '16

23 Mar '16

Hello, My name is Paul Vlase and I am following a master degree right now. I am interested in porting the Qubes OS to seL4 project and I saw that you are working already on it. Is there anything I can help you on this project? Thank you, Paul Vlase

1 0

[CAmkES] CAmkES 2.1.0 Release Notes
by Stephen Sherratt 22 Mar '16

22 Mar '16

CAmkES 2.1.0 Release Notes ========================== ## New Features - runner takes an `--architecture` command line argument which selects the target architecture. Valid arguments are: aarch32, arm_hyp, ia32 - added the ability to specify a hardware dataport as cached. Previously all hardware dataports were mapped uncached. This feature is intended to be used on dataports backed by DMA-able memory to improve access times. Functions to flush dataports from the cache are also provided. - support for seL4 3.0.0 ## Removed Features - `--hyp` command line argument is replaced with `--architecture arm_hyp` ## API Removals ### Unmarshalling Helpers These were intended for use in templates, but are no longer used in any internal templates: - `camkes_marshal` - `camkes_marshal_string` - `camkes_unmarshal` - `camkes_unmarshal_string` ### DMA Utilities These had been deprecated for a long period and are now being removed: - `camkes_dma_page_alloc` - `camkes_dma_page_free` You can find it at: https://github.com/seL4/camkes-tool/tree/camkes-2.1.0 A manifest for the 2.1.0 compatible versions of test and example apps: https://github.com/seL4/camkes-manifest/blob/master/default-2.1.x.xml Release notes on the wiki: https://wiki.sel4.systems/CAmkES%202.1.0 Enjoy! ________________________________ 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

What happens to the IPC buffer when you make another process within the same Vspace?
by Qiwei Wen 20 Mar '16

20 Mar '16

Hi, I'm trying to write a multithreaded seL4 application. It's to be made up of sel4util processes with different cspaces and sharing the same Vspace. I managed to achieve this, but what confuses me is that since the processes share the same Vspace, wouldn't GetIPCBuffer() return the same result for each of them? I looked at libsel4/arch_include/arm/sel4/arch/functions.h, and GetIPCBuffer() is simply: return *(seL4_IPCBuffer**)seL4_GlobalsFrame; Since seL4_GlobalsFrame is just a fixed memory location (0xffffc000) in the shared address space, why does seL4_GetIPCBuffer() return different results for different processes? Below is the output: ========================== PARENT: IPCBUFFER: 00273000 CHILD: GlobalsFrame: ffffc000, *GlobalsFrame 10076000 CHILD: setting shared to 97 PARENT: CHILD DIED, shared char: 97, MR16: 00000000 ============================= Is it that the frame ffffc000 mapping is changed on every context switch perhaps? Can I absolutely trust that IPC is still working correctly with this set up? Thanks, David

5 4

Isabelle itself proven?
by Steve VanderLeest 20 Mar '16

20 Mar '16

Since the formal verification of functional correctness of seL4 was performed using the Isabelle theorem prover, could someone tell me if Isabelle itself has been formally verified? If so, could you suggest some good references to that work? Regards, Steve Steven H. VanderLeest, Ph.D. Chief Operating Officer DornerWorks, Ltd. 3445 Lake Eastbrook Grand Rapids, MI 49546 www.dornerworks.com

3 2

Booting process
by Daniel Wang 19 Mar '16

19 Mar '16

Hi all, I’m very new to seL4 development. I’m particularly interested in understanding seL4 kernel source code. Could someone points me out how the seL4 is booted and where should I start learning? Thanks -Dan

3 2

seL4 wiki
by Anna Lyons 19 Mar '16

19 Mar '16

Hi all, We've created a public wiki for seL4 development here: https://wiki.sel4.systems/ The kernel team have put some effort into creating the initial content, but there is much more to be done. Contributions encouraged! New accounts are restricted to avoid spam, but if you have posted on this mailing list your account will be approved quickly. Otherwise contact us. Thanks, Anna Lyons seL4 Kernel Engineer | PhD Student DATA61 | CSIRO E <mailto:Brigitte.Biscotto@data61.csiro.au> Anna.Lyons(a)data61.csiro.au<mailto:Anna.Lyons@data61.csiro.au> Level 3, K17 Building, UNSW Gate 14, Barker Street, Kensington, NSW, 2033 l Locked Bag 6016, Sydney NSW 1466 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 [cid:image001.png@01D0EFD9.052ECFC0] ________________________________ 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

FYI: microkernel.info community site
by Jakub Jermář 14 Mar '16

14 Mar '16

Hello, just FYI, I have set up a simple web page[1] to promote the wider microkernel community and its goals. So far, the page comes with a brief description of the microkernel concept and an incomplete list of microkernel projects with links to each project's web. The description is made out of the first two sentences I found in the "What is XYZ" section or elsewhere on the web of the respective project. I also took the freedom to use the respective project's logo (or what I believed was the project's logo) for promoting it. I hope you will find this small web a good idea. It was inspired by a similar (though a little bit more informative) site set up by the unikernel community [2]. The sources of the [1] web are hosted on Github [3], so feel free to submit issues or PR to make the site better. Please send me a PM if there are any issues pertaining your project's cartouche that cannot be dealt with using Github. Thanks, Jakub [1] http://microkernel.info [2] http://unikernel.org/projects/ [3] https://github.com/jermar/microkernel.info

8 8

Capability faults on seL4_Send and seL4_Call
by Qiwei Wen 12 Mar '16

12 Mar '16

Hi all, I understand that capability faults for seL4_Send and seL4_Call only happen when the look-up fails, and not when illegal operations are attempted, such as calling a null cap or a piece of untyped memory. Is there another way at all, then, that such errors can be handled by user-level code? This is part of a project where the faulting process needs to surrender control to another process whenever it performs a system call on an invalid capability. Is there a way to achieve this given that fault endpoints will not work? Thanks, David

1 0

using camkesvm with qemu
by Julien Delange 10 Mar '16

10 Mar '16

Hi, I am currently trying to use the camkesvm example and run it in qemu. I am currently able to compile the c162_twovm_defconfig application. However, when running, I have the following issue (see below). So, I am wondering what would be the good arguments to start the application in qemu. I noticed that the kernel/initrd image for linux are specific in a header file, I assume this is also included in the image loaded by capdl. Any idea about how to run this example with qemu and/or how to test it? Thanks! Starting node #0 vt-x: not supported <<seL4 [decodeUntypedInvocation/193 T0xe2ff1900 "rootserver" @804afa7]: Untyped Retype: Insufficient memory or offset outside untyped>> Unmasking IOAPIC source 2 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 3 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 4 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 16 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 17 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 18 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 23 on ioapic 0 without ever setting its mode! <<seL4 [decodeCNodeInvocation/107 T0xe2ff1900 "rootserver" @804a4b2]: CNode Copy/Mint/Move/Mutate: Source slot invalid or empty.>> capDL-loader :: << Error: init_cnode_slot:1471: seL4_FailedLookup >> Ignoring call to sys_rt_sigprocmask

3 4

Recovering from cap fault?
by Qiwei Wen 10 Mar '16

10 Mar '16

Hi all, On page 26 of the manual (1.2) there's an instruction on how to restart a thread following a capability fault. The program counter where the faulting thread should pick up execution is said to be message register 0. What I'm trying to do is to restart the execution on the next instruction following the system call instruction so as to skip it. Try as I might, it will not work and the faulting thread is stuck in an endless number of faults. Below is the relevant code: seL4_Word pc = seL4_GetMR(0); printf("cap fault, pc: %08x, on %s\n",pc,seL4_GetMR(2)?"wait":"send"); //assert(!faultnum++); seL4_MessageInfo_t info = seL4_MessageInfo_new (seL4_CapFault,0,0,1); seL4_SetMR(0,pc + 4); seL4_Reply(info); It does restart, but immediately cap-faults again at the very same program counter. Is it supposed to work? What did I do wrong? Cheers, David

2 1

seL4 Tutorial Idea
by da Tyga 09 Mar '16

09 Mar '16

Hi Andrew Jackman! First of all apologies about my assumptions. In my hasty reading of your question I got the impression you were talking about yourself and not the intended audience for your tutorial material proposal. Like yourself, I too would use a practical, tutorial style guide if it were available. So I would like to give my vote for your idea. Unfortunately, I'm a one-man-show and thus not in a position to make a pledge towards a tutorial effort. Perhaps the good folks who are involved with seL4 could suggest how your proposal could come about. Reading these digests, tit would appear that there are quite a few people who are trying to come to grips with seL4. Yes, I was referring to the material that you linked. Cheers, Tyga >>> thread in reverse chrono-order: Andrew Jackman kd7nyq(a)gmail.com On Sun, Mar 6, 2016 at 11:04 AM, Jackman <kd7nyq(a)gmail.com> wrote: > Is anyone interested in tutoring on the topic of sel4? I have two > objectives: > > First, I'm interested in beginning programming, like getting through the > Hello World process. I would hope this eventually includes things like > basic driver development and practical application development. > > Second, I want to understand how virtualization works with sel4 and the > infrastructure behind it. My objective is to be able to stand up my own > virtualization host and guests. > > I'm not sure how payment would work. I'd be interested in turning our > experience into tutorials for community consumption, which may be more > valuable to some of you than the money. > > Thank you. > > Andrew Roy Jackman Hi Andrew, I don't wish to discourage you, but if you are just starting out programming and have limited knowledge of operating systems, etc ... then seL4 might be a very big undertaking to understand and learn from. There are a lot of topics you would need to come up to speed on. I suggest taking a look Gernot's course material at unsw.edu.au. > da Tyga: Thank you for writing back. I totally agree with your assessment. Permit me to elaborate a bit more on my situation. I am a professional software engineer who is primarily dedicated to writing virtualization automation software for sales demonstrations. Naturally, our department is always interested in ways in which we can improve the efficiency of our virtualization environment(s). After reading 'L4 Virtualization and Beyond' (2008, http://os.inf.tu-dresden.de/papers_ps/haertig08_l4_virtualization_and_beyon… ), I became fascinated with L4. I am here talking to you all because of the amount of press that seL4 has gotten as the proofed L4 kernel and because it appears to have the best, most easily understood documentation. Now, that does not mean that I think seL4 is well documented, just that it's the best documented of the L4 projects. The purpose of my original email was to very gently say that the introductory material to seL4 is so bad, that I'm willing to pay someone to either bring it up to date, assist me with it, or both. For example, there is a thread about RefOS, wherein Kevin wrote, "RefOS was a student project that is now no longer actively maintained." Gapry and HyperNewbie, however, provided at least some fixes, but their fixes don't appear to have gotten any attention from upstream. This was on 11 February. Nevertheless, RefOS appears to be the only seL4 project geared towards newcomers on the 'Getting Started' page ( https://sel4.systems/Info/GettingStarted/) You should note that, on that page, there is no indicator that newcomers should, in fact, stay away from that project because it's no longer maintained. I don't think requesting some attention on documentation is a bad or unjust thing. I would hope that lowering the barriers to entry to the seL4 community would increase the flow of developers, users, and sponsors to the seL4 project. In turn, I hope that would be seen as a good thing. I'm offering part-time, albeit unofficial, company sponsored development in exchange for some paid tutoring. I am not asking for a hand-out. If I didn't have to worry about ramp-up time or coming up with deliverables, I wouldn't be bugging you. Now, if you're worried about my qualifications, I'm a university educated computer scientist. While I've spent most of my career on web programming, I've studied operating systems development both at school and on my own. I began a toy kernel with the help of the osdev.org resources, and I'm happy with my progress. When I take inventory, however, I realize I don't have the desire to (re-)write an L4 kernel, nor do I think I can improve upon it. Finally, I think you're referring to Professor Gernot Heiser's page at https://www.cse.unsw.edu.au/~gernot/, and probably more specifically the CS9242 course at http://www.cse.unsw.edu.au/~cs9242/current/. If you're referring to another course, please be more specific. Thank you. Andrew Jackman kd7nyq(a)gmail.com

5 5

Tutor?
by Jackman 09 Mar '16

09 Mar '16

Is anyone interested in tutoring on the topic of sel4? I have two objectives: First, I'm interested in beginning programming, like getting through the Hello World process. I would hope this eventually includes things like basic driver development and practical application development. Second, I want to understand how virtualization works with sel4 and the infrastructure behind it. My objective is to be able to stand up my own virtualization host and guests. I'm not sure how payment would work. I'd be interested in turning our experience into tutorials for community consumption, which may be more valuable to some of you than the money. Thank you. Andrew Roy Jackman

2 2

Performce test for CAMKES or RefOS
by ぷ风过无痕?? 08 Mar '16

08 Mar '16

Hi everyone, I want to measure a variety of important aspects of system performance on CAMKES or RefOS. I know that Lmbench is an extensive suite of micro-benchmarks that give powerful insights into system performance. And lmbench is written in ANSI-C,so it is portable across a wide variety of systems and architectures. Can I measure the system performance on CAMKES or RefOS using Lmbench ? Thank you.

2 1

Re: [seL4] Devel Digest, Vol 22, Issue 1
by da Tyga 08 Mar '16

08 Mar '16

Hi Andrew, I don't wish to discourage you, but if you are just starting out programming and have limited knowledge of operating systems, etc ... then seL4 might be a very big undertaking to understand and learn from. There are a lot of topics you would need to come up to speed on. I suggest taking a look Gernot's course material at unsw.edu.au. On 7 March 2016 at 12:00, <devel-request(a)sel4.systems> wrote: > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe via the World Wide Web, visit > https://sel4.systems/lists/listinfo/devel > or, via email, send a message with subject or body 'help' to > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > > Today's Topics: > > 1. Tutor? (Jackman) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Sun, 6 Mar 2016 11:04:25 -0700 > From: Jackman <kd7nyq(a)gmail.com> > To: devel(a)sel4.systems > Subject: [seL4] Tutor? > Message-ID: > < > CAADorGK4z2oW4JoBq+K--72LDGc0d-2-1jTxUu41UxidvwjkHw(a)mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > Is anyone interested in tutoring on the topic of sel4? I have two > objectives: > > First, I'm interested in beginning programming, like getting through the > Hello World process. I would hope this eventually includes things like > basic driver development and practical application development. > > Second, I want to understand how virtualization works with sel4 and the > infrastructure behind it. My objective is to be able to stand up my own > virtualization host and guests. > > I'm not sure how payment would work. I'd be interested in turning our > experience into tutorials for community consumption, which may be more > valuable to some of you than the money. > > Thank you. > > Andrew Roy Jackman >

1 0

Can not build RefOS
by Gapry Un 08 Mar '16

08 Mar '16

Dear all, I follow the official step (https://github.com/seL4/refos-manifest) to build RefOS and it occurs the following error message. In file included from /home/chi-wai/Workspaces/microkernel/RefOS/libs/librefos/src/sync.c:16:0: ~/Workspaces/RefOS/stage/arm/imx31/include/refos/refos.h:73:1: *error: unknown type name ‘uint32_t’* ~/Workspaces/RefOS/stage/arm/imx31/include/refos/refos.h:73:23: *error: unknown type name ‘uint32_t’* In file included from /home/chi-wai/Workspaces/microkernel/RefOS/libs/librefos/src/sync.c:18:0: ~/Workspaces/RefOS/stage/arm/imx31/include/refos-util/cspace.h:44:72: *error: unknown type name ‘uint32_t’* ~/Workspaces/RefOS/libs/librefos/src/sync.c: In function ‘sync_create_mutex’: ~/Workspaces/RefOS/libs/librefos/src/sync.c:49:5: *warning*: ‘seL4_Notify’ is deprecated (declared at /home/chi-wai/Workspaces/microkernel/RefOS/stage/arm/imx31/include/sel4/deprecated.h:23): use seL4_Signal [-Wdeprecated-declarations] ~/Workspaces/RefOS/libs/librefos/src/sync.c: In function ‘sync_acquire’: ~/Workspaces/RefOS/libs/librefos/src/sync.c:65:5: *error: invalid initializer* ~/Workspaces/RefOS/libs/librefos/src/sync.c: In function ‘sync_release’: ~/Workspaces/RefOS/libs/librefos/src/sync.c:74:5: *warning*: ‘seL4_Notify’ is deprecated (declared at /home/chi-wai/Workspaces/microkernel/RefOS/stage/arm/imx31/include/sel4/deprecated.h:23): use seL4_Signal [-Wdeprecated-declarations] make[1]: *** [src/sync.o] Error 1 make: *** [librefos] Error 2 Does RefOS use the old seL4 API ? If it is, which version I need to downgrade? Thanks for any help or suggestion, Gapry. https://gapry.wordpress.com/

6 9

Re: [seL4] Devel Digest, Vol 21, Issue 11
by ぷ风过无痕?? 23 Feb '16

23 Feb '16

Hi everyone,I find an interesting problem when I read the code of endpoint(kernel\src\object\endpoint.c). In the sendIPC and receiveIPC functions , I see there are 3 states for an endpoint(Idle , send , receive). Below it is the state machine diagram. sendIPC EPState_Recv ——> EPState_Idle ——>EPState_send receiveIPC EPState_send——> EPState_Idle ——>EPState_Recv But when I add some print infomation, I find the endpoint can never reach the Send state. I think the correct state machine diagram just has two states(idle and receive). sendIPC EPState_Recv ——> EPState_Idle receiveIPC EPState_Idle ——>EPState_Recv Am I right???

2 1

Timer for AM335x
by Julien Delange 18 Feb '16

18 Feb '16

I am trying to develop a camkes application with one component having access to the timer. I got some inspiration from the time server for the kzm machine. Now, I am trying to port that to the am335x machine to execute on a beagleboard black. I dig into the code and found the appropriate platform-specific functions to call. Unfortunately, when trying to compile, it fails (see below). Anybody has an idea why this happens? Also, if you want to look at the camkes application, I put it on github at https://github.com/juli1/sel4-experiments/tree/master/camkes/pingimpl-am335x Thanks for any help! /home/sel4/test/camkes/build/arm/am335x/pingimpl/src/timer/static/components/timer/src/timer.o: In function `irq_callback': /home/sel4/test/camkes/apps/pingimpl/components/timer/src/timer.c:22: undefined reference to `dm_handle_irq' /home/sel4/test/camkes/apps/pingimpl/components/timer/src/timer.c:32: undefined reference to `dm_oneshot_relative' /home/sel4/test/camkes/build/arm/am335x/pingimpl/src/timer/static/components/timer/src/timer.o: In function `run': /home/sel4/test/camkes/apps/pingimpl/components/timer/src/timer.c:58: undefined reference to `dm_oneshot_relative' collect2: error: ld returned 1 exit status

2 2

handling timer with camkes
by Julien Delange 17 Feb '16

17 Feb '16

Dear all, I would like to build a scheduler on top of camkes. I figure that I have to get access to the timer irq and start from there (e.g. then, dispatch other tasks according to the number of elapsed ticks). I did find some relevant examples, especially in the camkes-vm ( https://github.com/seL4/camkes-vm) but nothing I can try. Is there any information about such materials? I tried to reuse the component but always got build error. I was wondering if there was an existing tutorial or an example I could try that will help me. Thanks. Julien.

2 3

Allocation of untyped memory
by Norman Feske 09 Feb '16

09 Feb '16

Hello, while moving Genode's seL4 support to seL4 version 2, I stumbled over the dynamic allocation within untyped memory regions. In the old experimental branch that I used previously, the retype-untyped operation allowed me to manually specify an offset where the new kernel object should be placed within the untyped memory region. So I was able to manage the allocation of untyped memory manually. In short, I added each initial untyped memory region to a roottask-local "phys-mem" allocator. Each time when creating a kernel object, I asked this allocator for a region of the required size and alignment, determined the untyped-memory capability that belongs to the found region, and used this capability to create the kernel object(s) at the calculated offset within the untyped-memory region. This worked very well. After switching to version 2, I found the retype-untyped operation to lack the offset argument (which admittedly was never present in the non-experimental version). Instead of accepting an offset parameter, the kernel maintains a built-in allocator per untyped-memory region. (please correct me if my understanding is wrong) The allocator is basically a simple offset value ("FreeIndex") that is increased with each allocation. Since I no longer have the chance to specify the offset explicitly, I have to rely on the allocation policy of the kernel and hit the following problem: There exists an untyped memory region of size 0x2000. Initially, the FreeIndex is 0. Now, I am creating the following kernel objects within the untyped-memory region: 1. CNode with totalObjectSize 0x400: -> The allocation increases FreeIndex to 0x400. 2. CNode with totalObjectSize 0x800: -> The FreeIndex gets aligned to 0x800 (natural alignment of the to-be-created CNode). This creates a gap between 0x400 and 0x800. -> The allocation increases FreeIndex to 0x1000. 3. seL4_IA32_4K with a totalObjectSize 0x1000: -> The allocation increases FreeIndex to 0x2000. 4. CNode with totalObjectSize 0x400: <<seL4 [decodeUntypedInvocation/209 T0xe3fc9900 "rootserver" @2013228]: Untyped Retype: Insufficient memory (1 * 1024 bytes needed, 0 bytes available).>> Since FreeIndex equals the size of the untyped memory region, the kernel concludes that untypedFreeBytes is 0. Even though there exists a gap of 0x400 within the untyped memory region that satisfies the alignment of the to-be-created kernel object, the kernel won't allow me to use it. In contrast, with the retype-untyped-at-offset operation, such a situation never occurred. Right now, I am a bit puzzled about how to proceed and have the following questions in the back of me head: * What is the rationale behind fixing the allocation policy within untyped memory regions in the kernel. Doesn't this design contradict with the principle of avoiding policy in the kernel? In my specific case, this policy seemingly makes my life much more difficult. To use the kernel in a deterministic way, I would need to model the kernel's allocation behavior in the user land. * From what I gather from the kernel's source code, the built-in allocator would not allow me to reuse parts of untyped memory regions because 'FreeIndex' is always increasing. E.g., after revoking the CNodes of steps 1 and 2, I still cannot create any new kernel objects within the untyped memory region because FreeIndex remains equal the size of the untyped memory region. Is this correct? * Is it possible to give me the retyped-untyped-at-offset operation back? ;-) e.g., in the form of a patch? Or alternatively, are there any best practices that I could follow wrt managing untyped memory? Maybe I'm just approaching the problem from the wrong angle? 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

3 5

Upgrading to Camkes 2.0
by Jeff Hieb 26 Jan '16

26 Jan '16

I was looking to upgrade to CAmkES release 2.0. but can't get an example arm configuration to compile. I did a a fresh clone using https://github.com/seL4/camkes-manifest.git and found the ia32_simple_defconfig compiles fine, but not arm_simple_defconfig make arm_simple_defconfig make [libs/libsel4] building... make[1]: *** No rule to make target `/home/sysjeff/Camkes2/libs/libsel4/sel4_arch_include/arm/interfaces/sel4arch.xml', needed by `include/interfaces/sel4_client.h'. Stop. make: *** [libsel4] Error 2 looks like the arm directory got renamed to aarch32 and part of the build system doesn't know? $ ls /home/sysjeff/Camkes2/libs/libsel4/sel4_arch_include/ aarch32/ ia32/ Is there something simple I am missing? Thanks, Jeff -- Jeffrey L. Hieb Department of Engineering Fundamentals University of Louisville Louisville Kentucky 40292 (502) 852 0465

2 2

Issue with CAmkES tutorial
by James Hasner 21 Jan '16

21 Jan '16

All, Noticed an issue with the tutorial for creating a dataport application with CAmkES components. This issue is on https://wiki.sel4.systems/CAmkES%20Tutorial within the Makefile and Kbuild section. You titled the application "helloevent" instead of hellodataport, causing the newly created application to not be able to access the header files needed. Thanks, James

2 1

Announcing Robigalia, make seL4 applications with Rust!
by Corey Richardson 07 Jan '16

07 Jan '16

Hi all, On behalf of the Robigalia project I am pleased to announce our first public release of the core libraries for using Rust on seL4. Currently, this consists of a raw interface akin to libsel4 and a higher-level "Rustic" interface. Currently, only x86 is supported. An ARM port is in progress. We have a website: https://robigalia.org/ And a mailing list: https://lists.robigalia.org/listinfo/robigalia-dev The goal of the Robigalia project is to promote Rust as a robust choice for application development on seL4 and has the long-term goal of producing Robigo, a POSIX-compatible personality on seL4. We're in the initial stages of development. We are primarily a group of students from Clarkson University, though other contributors are starting to trickle in. Currently in-progress is a port of the tutorial from the sel4-tutorials repositories and examples of doing various things using the libraries we've created. Beyond those, we're also working on x86 platform support, right now virtio and PCI bus management. (I didn't intend on posting this for another week, to finish the tutorial and high-level library, but it was scooped on HN, so I figured I might as well) -- cmr +16032392210 http://octayn.net/

2 1

Hardware Platform for sel4 and running linux as guest os
by Julien Delange 07 Jan '16

07 Jan '16

Dear all, I am looking to purchase a board for a project that will use sel4. I have the following hardware requirements: - serial port - ethernet - potentially usb Then, I want to run linux on top of sel4 and have also some native components. In the linux partition, I would like to control the usb and potentially the ethernet. In the native components, I am planning to use the serial port (communication with other components). I thought the beagleboard black would be a good match. Does anyone tried to run linux as a guest os on this platform? If yes, is there any tutorial/example to set it up? Also, any information about how to use the serial ports and other hardware components? Also, if you have an experience with any other board (x86 or ARM - the platform does not really matter), is it possible to indicate what you would recommend? Thanks for any help or suggestion, Julien.

6 6

CAmkES 2.0.0
by Ihor Kuz 06 Jan '16

06 Jan '16

The Trustworthy Systems Team at Data61 (formerly NICTA) is pleased to announce CAmkES release 2.0.0 The new release updates CAmkES to be compatible with seL4 version 2.0.0. It also marks the transition to more frequent and regular releases, as well as switching our release process to semantic versioning, so it's easy to tell which CAmkES releases are source-compatible, or will require updates to user-level code, and also with which seL4 versions they will be compatible. You can find it at: https://github.com/seL4/camkes-tool/tree/2.0.0 And a manifest for the 2.0.0 compatible versions of the CAmkES test and example apps: https://github.com/seL4/camkes-manifest/blob/master/default-2.0.x.xml Enjoy! ________________________________ 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

Extending errors to always include argument numbers
by Corey Richardson 05 Jan '16

05 Jan '16

For consistency, it seems like it'd beneficial if: seL4_RangeError seL4_AlignmentError seL4_DeleteFirst seL4_FailedLookup seL4_RevokeFirst included an indication of which argument the error applies to. For some of these errors, not every call has a unique argument which can cause the erorr. This seems like a relatively straightforward change for me to get acquainted with the full process of modifying and re-verifying the kernel. Are there tradeoffs hidden here that would make this undesirable? -- cmr +16032392210 http://octayn.net/

3 2

seL4 & camkes questions
by Julien Delange 05 Jan '16

05 Jan '16

Hello, First of all, thanks for the help you provided previously. After downloading the virtual machine, everything was fine and I was able to try seL4 and camkes by using the tutorials. Thanks also for making this documentation available publicly, it definitively helps a lot to learn the principles of this operating system. I still do have some questions regarding sel4 and camkes. - About camkes, what are the thread mapping rules. How a component is transformed into one (or several) sel4 threads? Is there a mapping 1 component = 1 thread or is it possible to have multiple threads per component? - How can I find the code generated by camkes? The idl/adl code is ultimately transformed into C code and I was wondering where I could see the code. - How the real-time requirements are handled in camkes? For example, how can I specify that a component is executed periodically every XXX ms. Does the ADL supports that? - How can we specify the scheduling constraints? Can we have an ARINC653-like scheduling where every process has a fixed time slice to be executed? Since the behavior of the system can be deduced from the execution time, allocated a fixed time slice also avoid some attacks - About scheduling, what are the policies actually supported? - How timing is handled? I tried to use nanosleep() from the libc but it seems the syscall/service is not implemented. I also tried the timer example from the sel4 tutorial but when compiling, there is an error (the function timer_handle_irq needs an IRQ as a parameter). Any idea how to fix the example and more information about how time is handled? - is it possible for the OS to load and launch multiple elf at the same time or other processes must be manually started? - How capabilities and services are associated? From the example hello-2 in the sel4 tutorial, I see that a capability is declared (with vka_alloc_endpoint(&vka, &ep_object)) but I do not understand how this is associated with the message being sent between both tasks. In other words, how is it possible to associated a capability with a service. When sending or receiving a message (for example, by using seL4_SetMR(0, MSG_DATA);), there is no use of the capability. So, how the kernel can check that the thread can effectively send a message? - Is there any efforts to support standards such as ARINC653 or MILS? (even experimental) - Is there any significant/big projects that are available online and you would recommend to learn the OS and its associated libraries? Hope you do not mind such a list of questions! I really enjoy digging into the OS and it seems very interesting. Thanks for any help/comment.

4 4

DMA
by Raymond Jennings 04 Jan '16

04 Jan '16

Is it ever possible for seL4 to run on a conventional machine without an IOMMU if any code that manipulates a DMA capable device is included as trusted or does DMA automatically void any assurance? Reason for question: Running seL4 on a system without an IOMMU.

4 8

Determining when would-have-blocked
by Corey Richardson 04 Jan '16

04 Jan '16

Looking at the manual and the C impl, it seems there is no robust way to determine if a non-blocking send failed. How should an application handle this? NBRecv sets the badge register to zero when the recv "failed" - is it expected that most/all endpoints will be badged? I'm still trying to get a feel for what a system designed for this model would look like. -- cmr +16032392210 http://octayn.net/

3 2

Tutorial error
by Julien Delange 24 Dec '15

24 Dec '15

Hello, I am trying to reproduce the tutorial. I followed the steps from the slides on https://github.com/seL4-projects/sel4-tutorials/blob/master/docs/seL4Tutori… When trying to compile, I got the following error in [1]. It seems to be a warning from the compiler, so, I edit the CFLAGS in the .config and tried to compile but then got the error in [2], which then avoid any potential compilation. Is there any special setup for the compiler? I am currently using gcc 5.2.1. Thanks for any suggestion, Julien. [1] /home/julien/tmp/sel4-tutorials/stage/x86/pc99/include/vka/object.h:286:5: warning: 'seL4_AsyncEndpointObject' is deprecated (declared at /home/julien/tmp/sel4-tutorials/stage/x86/pc99/include/sel4/objecttype.h:23): use seL4_NotificationObject [-Wdeprecated-declarations] [2] /home/julien/tmp/sel4-tutorials/kernel/src/plat/pc99/machine/acpi.c:38:13: error: size of array '__assert_failed_acpi_rsdp_packed' is negative

2 2

Camkes dependencies & development environment
by Julien Delange 23 Dec '15

23 Dec '15

Dear all, First of all, sorry if this question has been asked several times already. I am currently trying to use sel4 & camkes on a debian stable. I installed all the dependencies but I am facing an error message when trying to build the tool (see below). My version of cabal is 1.20, so, version should not be an issue. After searching, it seemed that the version of ghc might be the root cause so I upgraded to testing and/or unstable but faced other issues then. My question is then what is the best development environment to use sel4 and camkes? Any special recommendation? I would like to keep my existing debian/stable as much as possible. Thanks for any help or suggestion, Julien. [parse-capDL] building... export CONFIG_CAPDL_LOADER_MAX_IRQS=256 && cabal configure && cabal build && cp dist/build/parse-capDL/parse-capDL . Resolving dependencies... cabal: The package 'capDL-tool' requires Cabal library version -any && >=1.18 but no suitable version is installed. Makefile:45: recipe for target 'parse-capDL' failed make[1]: *** [parse-capDL] Error 1 Makefile:49: recipe for target '/home/julien/tmp/camkes/stage/arm/imx31/parse-capDL/parse-capDL' failed make: *** [/home/julien/tmp/camkes/stage/arm/imx31/parse-capDL/parse-capDL] Error 2

3 3

domain problems
by ぷ风过无痕?? 23 Dec '15

23 Dec '15

Hi everyone, I'm running the RefOS project on arm kzm board. The config file is kzm_debug_defconfig. I am tring to set two domains in the RefOS by changing the CONFIG_NUM_DOMAIN parameter from 1 to 2 in this file and rebuilt RefOS. When running RefOS it gets stucked and some servers cannot be initialized.How to resolve this bug?

1 0

domain problems
by ぷ风过无痕?? 23 Dec '15

23 Dec '15

Hi everyone, I'm running the RefOS project on arm kzm board. The config file is kzm_debug_defconfig. I am tring to set two domains in the RefOS by changing the CONFIG_NUM_DOMAIN parameter from 1 to 2 in this file and rebuilt RefOS. When running RefOS it gets stucked and some servers cannot be initialized.How to resolve this bug? The full output information is in the adjunct file.

1 0

RTEMS working with seL4
by Hesham Almatary 16 Dec '15

16 Dec '15

Hi all, I got an RTEMS port working for RISC-V architecture along with seL4. This depends on my earlier seL4 port for RISC-V. RTEMS runs with support of seL4 microkernel, and it runs in Supervisor mode (on another core). seL4 application would allocate and map memory for it from its untyped memory (userspace), before off-loading it to another core. seL4 application that loads/runs RTEMS is pretty much the same as SOS. For more details (and instructions) about how to build/run the project, see the github repo of the port [1], and/or this blog post [2] [1] https://github.com/heshamelmatary/rtems-riscv [2] http://heshamelmatary.blogspot.co.uk/2015/12/rtems-port-for-risc-v-withwith… Cheers, -- Hesham

2 2

VSpace translation?
by Ben Karel 14 Dec '15

14 Dec '15

Would any of seL4's guarantees be compromised if a Translate method were added to page directory objects (for mapping a virtual address to the underlying physical address, without exposing the intermediate page capabilities)?

4 4

Capability resolution depth mismatches
by Ben Karel 14 Dec '15

14 Dec '15

Hi all, Some capability resolution, such as for fault handling, winds up calling resolveAddressBits with n_bits = wordBits, and any remaining bits are ignored. In other cases, such as the destination slot for seL4_CNode_Copy, the user provides a resolution depth parameter, and the call to resolveAddressBits is mediated by lookupSlotForCNodeOp, which fails with a depth mismatch if there are any bits remaining. Individually these seem like reasonable choices, but it leads to code like this: seL4_CNode cspace_root = ...; // freshly allocated 256-slot CNode with no guard seL4_CPtr slot_for_copy = 0x23; // arbitrary slot we know is available seL4_CPtr slot_for_tcb = slot_for_copy << 24; seL4_CNode_Copy(cspace_root , endpoint_for_copy, 8, ...); seL4_TCB_Configure(..., endpoint_for_tcb, ...); I found it surprising that two different CPtrs are needed to describe the same slot! Is there a conceptual-model-explanation that doesn't involve appeal to the underlying implementation? Also: my current understanding is that the depth parameter is only needed to disambiguate indirections through CNode-containing slots. What goes wrong if the depth mismatch checks are relaxed?

2 2

Timing side channel via idle thread code?
by Brian Mastenbrook 12 Dec '15

12 Dec '15

While pulling up the Haskell model to respond to the previous question, I noted the following statement: "The idle thread's code is at an arbitrary location in kernel memory. For convenience in the Haskell model, we place it in the globals frame, but there is no need for it to be in user-accessible memory." Given that the globals frame is mapped cacheable, doesn't this lead to a potential timing side channel? Tasks would be able to determine whether the idle thread's code has been evicted from cache, which may or may not reveal something interesting about the state of the system as a whole. -- Brian Mastenbrook CTO Wearable Inc. Makers of AirStash

3 2

vspace_reserve_range_at
by Robert VanVossen 12 Dec '15

12 Dec '15

Hello, I am trying to map a device 1:1 in my root thread. When I try to reserve a range at the specific location, using the vspace_reserve_range_at() function I get the following error: ERROR:sel4utils_reserve_range_at_no_alloc:585: Range not available at 0xf8f00000, size 0x64000. Is there something that the kernel or the root task needs to do before this to make this range available for reservation? BTW, I am still using seL4 1.0. Thanks, Robbie VanVossen DornerWorks

2 1

vspace_reserve_range_at
by Robert VanVossen 12 Dec '15

12 Dec '15

Hello, I am trying to create a 1:1 physical to virtual mapping in my root thread. My first step in attempting this is to reserve the virtual address I need using the vspace_reserve_range_at() function, but I get the following error: ERROR:sel4utils_reserve_range_at_no_alloc:585: Range not available at 0xf8f00000, size 0x64000 Is there something I need to do in the kernel or in the root thread to actually allow this memory to be reserved? BTW, I am still using seL4 1.0. Thanks, Robbie VanVossen DornerWorks

1 0

verifying concurrency
by Gergely Buday 09 Dec '15

09 Dec '15

Hi there, what should I read if I want to understand the verification of concurrent programs related to the sel4 project? I have found https://ssrg.nicta.com.au/publications/papers/Daum-phd.pdf https://ssrg.nicta.com.au/publications/papers/Daum_DSW_08.pdf http://ssrg.nicta.com.au/projects/concurrency/ Are there others? Cheers - Gergely

3 2

Reminder: Microkernel-devroom CfP deadline is on this Sunday
by Jakub Jermar 07 Dec '15

07 Dec '15

Hi folks, the CfP deadline for the Microkernel devroom at FOSDEM 2016 is due this Sunday. See the original CfP [1] for information on what to do if you would like to give a talk about some microkernel-related topic. At the same time, I would like to encourage you to submit a talk proposal. It would be shame not to let the wider microkernel community know about the latest and greatest developments in your project. Lastly, please forward this reminder to whoever you think may want to give a talk in the devroom and is not among the recipients of this message. Thanks, Jakub [1] http://trac.helenos.org/wiki/Devroom2016

1 0

haskell on sel4
by Tim Newsham 05 Dec '15

05 Dec '15

I just noticed the web page says "we have Haskell sort-of running on seL4 (thanks or friends from Galois for their help), should be released in the near future" This is great news. Are you able to share any details such as when any of this will be public, what the porting strategy was (is this similar to HalVM?), what dependencies haskell compiled code requires, if there are sel4 bindings, etc? Tim

3 4

Initial Thread physical to Virtual Mapping
by Robert VanVossen 04 Dec '15

04 Dec '15

Hello, I am attempting to integrate the Xilinx drivers, provided through their SDK, with seL4 on the Zynq7000. In the root thread, I created a virtual mapping for the SD Card peripheral, and I pass that virtual address into the driver, so that it is reading and writing to it. The controller has a built-in DMA that gets used for data transfer. I created a buffer in the root thread's virtual space to pass to the DMA, but it needs a physical address. I calculated the virtual/physical offset from the physical and virtual addresses for the application that are given by the elfloader, but that didn't seem to be the correct mapping. Is there a good way to get that mapping, either from within the application itself or from the kernel before hand? Thanks, Robbie VanVossen DornerWorks

3 2

Assigning GPIO buffer to a new process
by Karl Apsite 02 Dec '15

02 Dec '15

Ahoy there! I'm working on a Zynq 7000 - ZC702 dev board. I've setup a capability associated with the GPIO buffer, and have successfully ran a small test in the root process that could read a button's state via GPIO. The next step is to send the capability to a second process so that it can read the button's state. I'm having some trouble understanding how I should go about using the IPC calls to achieve this transfer. I'll try to give a summary of my efforts, to clear up where I am, and what I've done so far. To start: I borrowed (heavily) from the 4th tutorial that established two separate processes Main: https://github.com/seL4-projects/sel4-tutorials/blob/master/solutions/hello… App: https://github.com/seL4-projects/sel4-tutorials/blob/master/solutions/hello… I felt inclined to inform the second process about the whereabouts of the new endpoint as opposed to making an assumption as to where it was allocated. I crammed the address into the argc/argv constructs as the process starts, and it seems to be able to continue just fine. 1. Is that an OK thing to do? I understand that I shouldn't be too willing to share vital information freely between both processes, and I'm not sure if abusing argc/argv to inform the second process is appropriate here. I left the main thread in seL4_Wait(). My idea is: other processes are expected to send a message representing a command that main can respond to. Main can check the message, badge(s), and privileges as necessary, and respond with the capability if it so desires. With the capability in hand, and a tag with extracaps set to one, I was NOT able to successfully send the cap. The second process would only receive a tag with extra caps set to zero, so it must be failing somewhere along the way. I loaded the cap into the first slot using seL4_SetCap(0, my_cap) and the cap was functioning previously, so I doubt it's erroring when I send. I expect an error on the receiving end somewhere. I have NOT been able to prepare a path for a capability in the second process, and notify seL4 of the location using seL4_GetCapReceivePath(root_node, new_cap, 32). 2. How should the second process obtain a reference to its root cnode? 3. How should the second process allocate a new cnode? I think the new_process_t structure in the main process has the addresses I'm after (to obtain the root cnode at least, and maybe allow me to a new cnode?), but I don't understand the implications of informing the second process about the information in the new_process_t structure. 4. Is the new process expected to know all of that information? 5. Is there an API to establish this sort of information (along with the IPC endpoint that I had to cram into argc/argv earlier?)

2 1

seL4 2.0.0 Release Notes
by Anna Lyons 01 Dec '15

01 Dec '15

Introducing seL4 2.0.0 ====================== Version 2.0.0 introduces more consistent terminology to manual and code, as well as API and performance improvements, including to seL4's formally verified ARMv6 version. We clarified the notion of signals and notifications vs IPC, and added a new feature to the seL4 API that allows user programs to receive notifications while waiting for IPC messages. You can now also poll notification objects. Both of these changes are aimed at simplifying user-level interaction with interrupts. In addition to the new features, seL4 has become even faster than it was before, esp. in scheduling threads. The new features and performance improvements are available on all supported platforms, and are formally verified to full sel4 standards. We have also switched our release process to semantic versioning, so it's easy to tell which seL4 releases are binary-compatible, source-compatible, or will require updates to user-level code. Terminology Changes =================== IPC vs Notifications -------------------- The old terminology of "synchronous IPC" vs "asynchronous IPC" was confusing and misleading. We changed this to reflect the fact that IPC in seL4 is always synchronous and is simply referred to as "IPC", which is enabled by "endpoint" objects. The receive operation is now more appropriately called "receive". What used to be called incorrectly "asynchronous IPC" is now called Notifications, enabled by "notification" objects. Notifications are not a form of message passing, but arrays of binary semaphores, and the new terminology describes this better. The operations on them are consequently called "signal" and "wait" New Features ============ Notification binding -------------------- A notification can be bound to a thread and is referred to as the thread's bound notification object. This is a 1:1 relationship. Whenever a thread waits for an IPC on an endpoint, it will receive any signals sent to its bound notification object, with the signal flags converted into a single-word message. Threads can also explicitly wait for signals by waiting on the notification object itself. For more details, see the 2.0.0 manual Implementation improvements =========================== * introduces the bitfield scheduler: faster scheduler (Was linear in the number of runnable threads, now log n) * improved benchmarking macros: can now specify multiple benchmarking tracepoints at once added CONFIG_RELEASE_PRINTF in addition to CONFIG_DEBUG and CONFIG_RELEASE, which enables printf in a release build API Changes =========== * seL4_Recv replaces seL4_Wait on endpoints * seL4_Wait is now only used on notification objects * Async endpoint -> notification object * sync endpoint -> endpoint * seL4_Recv on an endpoint may now return signals sent to a thread's bound notification object. API Additions ============= * seL4_NotificationObject replaces deprecated seL4_AsyncEndpointObject * seL4_NotificationBits size in bits of a notification object * seL4_IRQHandler_SetNotification replaces deprecated seL4_IRQHandler_SetEndpoint * seL4_Recv replaces seL4_Wait for endpoints * seL4_Wait used on notifications * seL4_NBRecv non-blocking (polling) receive on an endpoint, which fails if there is no message waiting. Opposite of NBSend (which silently fails if there is no receiver waiting) * seL4_Poll collects any signals from a notification objects, returns zero if there are none * seL4_Signal replaces deprecated seL4_Notify * seL4_TCB_BindNotification bind a notification to a tcb * seL4_TCB_UnbindNotification unbind a notification from a tcb Deprecations ============ * seL4_AsyncEndpointObject * seL4_Notify * seL4_IRQHandler_SetEndpoint Note on Syscall names ==================== Logically there are only two operations on capabilities, send and receive, which can take opcodes specifying sup-operations. For example, the Notification operations Signal and Wait are mapped to Send and Receive, respectively. For efficiency reasons, many kernel objects use separate kernel entry points for their operations. You must not rely on either, as this can change at any time. Instead, always use the object-specific wrapper functions. User-level repositories ======================= To simply repository management we have merged many of our user level library repositories. To see the changes please compare 1.0.4.xml and 2.0.x.xml in https://github.com/seL4/seL4test-manifest Upgrade notes ============= Calls to seL4_Wait no longer return a seL4_MessageInfo_t as seL4_Wait is intended to be used on notification objects. Calls to the prior version of seL4_Wait need to be replaced with seL4_Recv. If you don't want to upgrade yet - don't worry. Both the sel4test-manifest and verification manifest repositories have manifests titled 1.0.4.xml which point to the tips of the previously released repositories before today. All library repositories have a branch called '1.0.x-compatible' which are compatible with the 1.0.4 kernel. Note that to use the new merged repositories, you must upgrade to 2.0.0. Full changelog ============== Use git log 1.0.4..2.0.0 in https://github.com/seL4/seL4 More details ============ See the 2.0.0 manual included in the release for detailed descriptions of the new features. Or ask on this mailing list! Enjoy! ________________________________ 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

Does seL4 support periodic thread
by ぷ风过无痕?? 27 Nov '15

27 Nov '15

Hi everyone,I have some questions about seL4's timer. I know seL4 is controlling the timer device. In the current release version, scheduling is tick-based, there's a periodic interrupt that feeds into the scheduler. I wanna know if seL4 support periodic thread. I want to implement a periodic process in Refos which is above seL4 kernel.And, if seL4 does not support periodic thread, could I modify the kernel scheduler? Does it influences formal verification? I find that Refos modifies _thread_state_t enumeration-type variables (kernel\include\object\structures.h ). Does it influences formal verification? Thank you so much!!

3 2

CAmkES-vm Configuration
by Bryan Ching 24 Nov '15

24 Nov '15

Hi, I was trying to configure the CAmkES-vm to run the vmware configuration. However, I get the following error. [apps/vm] building... /home/bryan/camkes-vm/tools/camkes/camkes.mk:125: /home/bryan/camkes-vm/build/x86/pc99/vm/camkes-gen.mk: No such file or directory [GEN] camkes-gen.mk While transforming AST: /home/bryan/camkes-vm/apps/vm/vm.camkes:4: unresolved reference to VM make[1]: *** [/home/bryan/camkes-vm/build/x86/pc99/vm/camkes-gen.mk] Error 255 make[1]: *** Deleting file `/home/bryan/camkes-vm/build/x86/pc99/vm/ camkes-gen.mk' make: *** [vm] Error 2 I have seen this error before. This time, I used the "make menuconfig" command. I go to Applications --> VMM Main Application --> Configuration. I type in "vmware" to try and configure it. When I am back on the command line, I type "make vmware_defconfig" and then "make silentoldconfig" and finally "make". Where is the camkes-gen.mk file supposed to be located? Thanks, Bryan

2 4

Destroying the Root Thread
by Robert VanVossen 20 Nov '15

20 Nov '15

Hello, I was wondering if I can safely destroy my application root thread after I have setup the capabilities and memory mappings for all of my other threads in the system? Thanks, Robbie VanVossen DornerWorks

5 8

CAmkES-vm Build Question
by Bryan Ching 17 Nov '15

17 Nov '15

Hi, I was just wondering for the CAmkES-vm, where is the Makefile to build it? Also, to clone the github repository, do I use "repo" or can I use "git clone"? Thanks, Bryan

4 7

timing
by Raymond Jennings 13 Nov '15

13 Nov '15

Where does the seL4 microkernel actually get the timing information it needs to enforce scheduling decisions? I can imagine some sort of interrupt or I/O access is required to get it from the raw hardware. How does it get from the timing hardware to the scheduling code?

4 4

CAmkES Tutorial
by Bryan Ching 12 Nov '15

12 Nov '15

Hi, I am following the tutorial for CAmkES and had a few questions. There is a part in the tutorial that says to "create a dependency entry in apps/helloworld/Kbuild for your application". How exactly do you go about creating a dependency? Do you just add it to the first line of the Kconfig file? Also, for the Makefile, I needed to include the camkes.mk file. However, it was not found in the specified directory. This is the command that I included in the Makefile: include ${SOURCE_DIR}/../../tools/common/camkes.mk Where could I get that file? Or if someone had the contents of that file, I could create it myself. Thanks, Bryan

2 6

Call for Participation: NICTA Software Systems Summer School
by Gernot Heiser 11 Nov '15

11 Nov '15

tl;dr 8–9 Feb, free event, travel subsidies for AU/NZ students CALL FOR PARTICIPATION ===================================== Fourth NICTA Software Systems Summer School http://ssrg.nicta.com.au/Events/summer/16 ===================================== Supported by: ANU and UNSW Over two days, this summer school will feature lectures by international leaders in computer systems from industry and academia, interspersed with short student talks and poster sessions. We will emphasise a friendly and informal setting where students can learn and obtain feedback from experts. Topics include operating systems, hypervisors, virtual machines, databases, compilers, language implementation, memory management and security. Research students may apply for participation by submitting a summary (of no more than half a page) on their research interests, indicating how it overlaps with the topic of the summer school. They may also indicate that they would like to give a short talk, although the organisers will only select a small number of student presentations. All attending students will be able to present a poster, and are strongly encouraged to use this opportunity to get feedback from world leaders!. We will also consider submissions from final-stage undergraduate students, post-docs or academic staff, provided they explain the benefits they expect from attendance.Supervisors of attending students are particularly welcome to attend. All submitted material must fit on a single A4 page. COST Attendance is free, but subject to invitation based on the submitted abstract. We will rarely reject an application from a student. Registration includes free lunches and coffee breaks during the summer school, as well as a dinner on the evening of the first day. A limited amount of travel support will be available for students from outside NSW and the ACT. Students requesting travel support must submit a brief justification with their application. Travel support will only be available for students from Australia and New Zealand, and will not exceed the cheapest airfare from their nearest major airport to Sydney. Funds for this are limited, and we will give priority to students likely to benefit most from the summer school, i.e. students whose research is most aligned with the topic. LOCATION The workshop and associated activities will be held in the Computer Science & Engineering building on the UNSW Kensington (main) campus in Sydney. KEY DATES Abstracts Due: Monday, 23 November, 2015, via the SSSS'16 submission site Notification: Friday, 20 November, 2015 Early applications will be notified earlier to help you with planning. ACCOMMODATION For participants from outside Sydney we are holding a limited number of inexpensive rooms at a college on campus. These must be booked (and deposit paid) by the end of November. Latecomers will have to find their own accommodations (there are other colleges and backpacker hostels nearby). ORGANISERS: Gernot Heiser (NICTA and UNSW) <gernot(a)nicta.com.au> Steve Blackburn (ANU and NICTA) <Steve.Blackburn(a)anu.edu.au> PRESENTERS (tentative): • Dr Andrew Baumann, Microsoft Research, Redmond • Prof Steve Blackburn, ANU • Prof Douglas Carmean, Oregon State University • Prof Luis Ceze, University of Washington, Seattle • Prof Kevin Elphinstone, NICTA and UNSW • Prof Alan Fekete, NICTA and Sydney University • Dr Tim Harris, Oracle Labs, Cambridge • Prof Gernot Heiser FACM, NICTA and UNSW, Sydney, Australia • Prof Tony Hosking, NICTA and ANU • Prof Gabriele Keller, NICTA and UNSW • Prof Eliot Moss FACM, UMass Amherst • Dr Karin Strauss, Microsoft Research, Redmond _______________________________________________ Csprofs mailing list Csprofs(a)core.edu.au http://core.edu.au/mailman/listinfo/csprofs_core.edu.au <a href="http://core.edu.au/mailman/listinfo/csprofs_core.edu.au"> Click here to unsubscribe </a> ________________________________ 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

sel4 for armv5 architecture
by vibi sreenivasan 09 Nov '15

09 Nov '15

Hi, Can any one please let me know whether sel4 is supported on armv5 ? I am specifically looking to run sel4 on arm926ej. Thanks & Best Regards Vibi

4 4

Kernel lock
by ぷ风过无痕?? 05 Nov '15

05 Nov '15

Hi, I have a question about kernel lock in seL4. I have read all the code in sel4 kernel,but I just find one file(kernel\include\arch\ia32\kernel\lock.h) related to the lock in the sel4. I also find that the lock here is used to debug.So I think there does not exist a lock in the sel4kernel.But if the lock really does not exist ,that means the sel4 kernel is non-reentrant, does it? does seL4 really not need the lock ? ------------------ Original ------------------ From: "devel-request";<devel-request(a)sel4.systems>; Date: Wed, Nov 4, 2015 01:33 AM To: "devel"<devel(a)sel4.systems>; Subject: Devel Digest, Vol 18, Issue 4 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel or, via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Re: How is network stack implemented in sel4 (Tim Newsham) 2. Re: How is network stack implemented in sel4 (Raymond Jennings) 3. Re: How is network stack implemented in sel4 (Gernot Heiser) 4. Re: How is network stack implemented in sel4 (Raymond Jennings) 5. Re: How is network stack implemented in sel4 (Gernot Heiser) 6. Re: How is network stack implemented in sel4 (Yuxin Ren) ---------------------------------------------------------------------- Message: 1 Date: Mon, 2 Nov 2015 15:48:02 -1000 From: Tim Newsham <tim.newsham+sel4(a)gmail.com> To: Yuxin Ren <ryx(a)gwmail.gwu.edu> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: <CAGSRWbhESa8qAwNzWjVKzo7Unh=GeGWNTVTBACXbkMA=TbsVQg(a)mail.gmail.com> Content-Type: text/plain; charset="utf-8" seL4 does not provide a network stack or even network device drivers. An OS on top of seL4 would have to provide their own drivers and stack and is free to put them in a single server or in different servers and choose how to communicate between them. On Mon, Nov 2, 2015 at 2:38 PM, Yuxin Ren <ryx(a)gwmail.gwu.edu> wrote: > Hi, > > I have a few questions about network stack in sel4. > > Is network stack implemented in the kernel or user level? > If in user level, are different protocols (IP/TCP) implemented in a > single server or different servers? > If in different servers, how do they communicate with each other? > > Is there any example code to show how to use network? How to send and > receive TCP or UDP packets? > How can I set up the network environment on bare metal machine? Is > there documentation or instruction? > > Thanks a lot! > Yuxin > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20151102/34f3782d/attachmen…> ------------------------------ Message: 2 Date: Mon, 2 Nov 2015 17:58:11 -0800 From: Raymond Jennings <shentino(a)gmail.com> To: Tim Newsham <tim.newsham+sel4(a)gmail.com> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: <CAGDaZ_qNsZd+VcH8wwvPcjcq_mQR=xefgKMaR45-L4SO9VBrLQ(a)mail.gmail.com> Content-Type: text/plain; charset="utf-8" So basically L4 grants IO caps to the network card's io ports to whatever task acts as the network driver, and it's the driver task's job to bang on the card's I/O and hook up with whatever other tasks represent packet/protocol/whatever layers of the ISO 7 layer stack. On Mon, Nov 2, 2015 at 5:48 PM, Tim Newsham <tim.newsham+sel4(a)gmail.com> wrote: > seL4 does not provide a network stack or even > network device drivers. An OS on top of seL4 > would have to provide their own drivers and stack > and is free to put them in a single server or in > different servers and choose how to communicate > between them. > > > On Mon, Nov 2, 2015 at 2:38 PM, Yuxin Ren <ryx(a)gwmail.gwu.edu> wrote: > >> Hi, >> >> I have a few questions about network stack in sel4. >> >> Is network stack implemented in the kernel or user level? >> If in user level, are different protocols (IP/TCP) implemented in a >> single server or different servers? >> If in different servers, how do they communicate with each other? >> >> Is there any example code to show how to use network? How to send and >> receive TCP or UDP packets? >> How can I set up the network environment on bare metal machine? Is >> there documentation or instruction? >> >> Thanks a lot! >> Yuxin >> >> _______________________________________________ >> Devel mailing list >> Devel(a)sel4.systems >> https://sel4.systems/lists/listinfo/devel >> > > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20151102/24c77488/attachmen…> ------------------------------ Message: 3 Date: Tue, 3 Nov 2015 03:05:37 +0000 From: Gernot Heiser <gernot(a)nicta.com.au> To: Raymond Jennings <shentino(a)gmail.com> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: <E4936E28-39AA-44E9-B202-FB37401E22F9(a)nicta.com.au> Content-Type: text/plain; charset="us-ascii" On 3 Nov 2015, at 12:58 , Raymond Jennings <shentino(a)gmail.com<mailto:shentino@gmail.com>> wrote: So basically L4 grants IO caps to the network card's io ports to whatever task acts as the network driver, and it's the driver task's job to bang on the card's I/O and hook up with whatever other tasks represent packet/protocol/whatever layers of the ISO 7 layer stack. More precisely: seL4 hands all rights to all resources to the initial process, whose job is then to initialise the desired system. It would be that process that hands caps to drivers etc. Gernot ________________________________ 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. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20151103/a3a78ad4/attachmen…> ------------------------------ Message: 4 Date: Mon, 2 Nov 2015 19:46:14 -0800 From: Raymond Jennings <shentino(a)gmail.com> To: Gernot Heiser <gernot(a)nicta.com.au> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: <CAGDaZ_q=98W1c91dFMNN+zL4P1p3+iE-ETAMbfOc51ybxvFwrg(a)mail.gmail.com> Content-Type: text/plain; charset="utf-8" So the kernel itself doesn't actually "own" any capabilities, just does the bookkeeping and enforcement? On Mon, Nov 2, 2015 at 7:05 PM, Gernot Heiser <gernot(a)nicta.com.au> wrote: > On 3 Nov 2015, at 12:58 , Raymond Jennings <shentino(a)gmail.com> wrote: > > > So basically L4 grants IO caps to the network card's io ports to whatever > task acts as the network driver, and it's the driver task's job to bang on > the card's I/O and hook up with whatever other tasks represent > packet/protocol/whatever layers of the ISO 7 layer stack. > > > More precisely: seL4 hands all rights to all resources to the initial > process, whose job is then to initialise the desired system. It would be > that process that hands caps to drivers etc. > > Gernot > > ------------------------------ > > 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. > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20151102/528f68fb/attachmen…> ------------------------------ Message: 5 Date: Tue, 3 Nov 2015 03:54:58 +0000 From: Gernot Heiser <gernot(a)nicta.com.au> To: Raymond Jennings <shentino(a)gmail.com> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: <418AEC27-5994-4EAB-8AEB-2D12A7D031A7(a)nicta.com.au> Content-Type: text/plain; charset="utf-8" > On 3 Nov 2015, at 14:46 , Raymond Jennings <shentino(a)gmail.com> wrote: > > So the kernel itself doesn't actually "own" any capabilities, just does the bookkeeping and enforcement? Caps are like keys: they authenticate access. The kernel doesn?t need them for its own purposes. However, our integrity and confidentiality proofs show that the kernel will not on its own access user memory, unless on behalf of a thread who demonstrates that it is authorised by presenting an appropriate caps. Gernot ________________________________ 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. ------------------------------ Message: 6 Date: Tue, 3 Nov 2015 12:32:44 -0500 From: Yuxin Ren <ryx(a)gwmail.gwu.edu> To: Gernot Heiser <gernot(a)nicta.com.au> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: <CAAKbDrdNod7_M8h+ufyZCkdJ9bDmKeXNpRD-PpKMSCYUnwpLQQ(a)mail.gmail.com> Content-Type: text/plain; charset=UTF-8 Thank you all. But are there any projects on top of sel4 microkernel which implement network functionality? I don't think I need to build the whole network stack from bare metal. It is best for me to just refer some existing projects and run simple network application on top of it. Yuxin On Mon, Nov 2, 2015 at 10:54 PM, Gernot Heiser <gernot(a)nicta.com.au> wrote: > >> On 3 Nov 2015, at 14:46 , Raymond Jennings <shentino(a)gmail.com> wrote: >> >> So the kernel itself doesn't actually "own" any capabilities, just does the bookkeeping and enforcement? > > Caps are like keys: they authenticate access. The kernel doesn?t need them for its own purposes. However, our integrity and confidentiality proofs show that the kernel will not on its own access user memory, unless on behalf of a thread who demonstrates that it is authorised by presenting an appropriate caps. > > Gernot > > ________________________________ > > 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. > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 18, Issue 4 ************************************

4 4

How is network stack implemented in sel4
by Yuxin Ren 04 Nov '15

04 Nov '15

Hi, I have a few questions about network stack in sel4. Is network stack implemented in the kernel or user level? If in user level, are different protocols (IP/TCP) implemented in a single server or different servers? If in different servers, how do they communicate with each other? Is there any example code to show how to use network? How to send and receive TCP or UDP packets? How can I set up the network environment on bare metal machine? Is there documentation or instruction? Thanks a lot! Yuxin

5 7

Running CAmkES Sample Application on Sabre Lite Board
by Bryan Ching 02 Nov '15

02 Nov '15

I was following the CAmkES "Getting Started" tutorial on the seL4 website and followed all the instructions. Here is the link: https://sel4.systems/Info/CAmkES/GettingStarted.pml I managed to get the sample application to run in QEMU (Quick Emulator) like the instructions said. I tried loading the sample application onto the Sabre Lite Board through tftp booting using minicom. However, once I try to boot the .elf file, it displays the memory address and nothing else happens. Is there any configuration file that I need to change to make the sample application run on my Sabre Lite Board? Or is there something else that I am missing? Thanks, Bryan

3 6

Fwd: FOSDEM 2016 - Microkernel devroom CfP
by Martin Decky 28 Oct '15

28 Oct '15

Dear all, I am forwarding the Call for Participation of the Microkernel devroom at FOSDEM 2016. The original announcement did not pass the mailing list gatekeeper for some reason. Martin Decky -------- Forwarded Message -------- Subject: FOSDEM 2016 - Microkernel devroom CfP From: Jakub Jermar <jakub(a)jermar.eu> FOSDEM 2016 - Microkernel devroom CALL FOR PARTICIPATION The developers of several free and open-source microkernel-based operating systems will meet at FOSDEM 2016 [1] in Brussels, Belgium and will share a developer room. The devroom is currently looking for content in the form of talks and activities related to the area of microkernel-based operating systems. Possible topics include, but are not limited to: * project introductory and status update talks, demos * architecture, subsystem and components' design * hardware and device drivers * tools, languages and toolchains * development, debugging, testing and release engineering * best practices and learning from mistakes * trends and challenges * community and life with a microkernel project Please use the Pentabarf [2] system to submit your proposals. You do not need to create a new account if you already have one. When in doubt, please use the devroom mailing list [3]. The deadline for your CfP submissions is on 2015-12-13. Make sure to include the following in your proposal: * title of your talk * abstract (one or two paragraphs) * your full name * your short bio * a picture of yourself * duration of your talk The official devroom schedule (along with the accepted talks) will be announced on 2015-12-18 in the devroom's mailing list and the speakers will be notified via e-mail. The schedule will also be published on the FOSDEM web and in the FOSDEM booklet. The devroom will take place on Saturday of January 30, 2016 at ULB Solbosch Campus in Brussels, Belgium [4]. 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 its inception in 2012 the Microkernel devroom has been part of each FOSDEM conference. It has become a sort of an institutionalized tradition since then. To this date over a dozen projects have participated in one way or another, delivering forty talks and other contributions in total. The goal of the Microkernel devroom has been to bring the various projects together and let them share ideas, cross-pollinate and socialize. Each year the devroom is organized by one of the projects based on a system of rotating presidency from the pool of projects that opt in. In 2016 it is HelenOS' turn again. Social events It has become a tradition that the microkernel projects dine together somewhere in downtown Brussels after the devroom closes. The year 2016 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 2015-10-23 CfP 2015-12-13 CfP deadline 2015-12-18 Devroom schedule published, speakers notified 2016-01-30 Microkernel devroom takes place 2016-01-30 Microkernel family dinner Links [1] http://fosdem.org/2016 [2] https://penta.fosdem.org/submission/FOSDEM16 [3] https://lists.fosdem.org/listinfo/microkernel-devroom [4] https://fosdem.org/2016/practical/transportation/

1 0

Support for multiple levels of derived capabilities?
by Mark Jones 22 Oct '15

22 Oct '15

I have a question about the way that derived capabilities are handled in seL4. I'm posting here in the hope that somebody might be able to share some insights about this part of the design. As I understand it, early versions of seL4's Mint operation allowed multiple derived levels of capabilities. (I'm thinking, in particular, of the description of Capability Derivation Trees, or CDTs, on Pages 36-38 of Dhammika Elkaduwe's thesis.) This, for example, would make it possible to construct a system with multiple threads, A, B, and C, each holding a capability to the same object where the capability in C is a CDT child of the capability in B, which in turn is a CDT child of the capability in A. In this scenario, B would have authority to revoke the capability in C, including any further CDT children that C had created, but it wouldn't typically have authority over other children of the original capability in A. So far as I can tell, this is not possible in the current version of seL4. Specifically, the reference manual (API version 1.3, Page 11) indicates that "Ordinary original capabilities can have one level of derived capabilities" and that "Further copies of these derived capabilities will create siblings". In the scenario above, this suggests that the capabilities in B and C would be siblings and that there would be no easy way for B to track any additional sibling copies that C might have created. Can someone provide background about why this change was made? I've seen that Dhammika had a working implementation of the original design, and although it was still technically limited to 128 levels, this was not found to be an issue in practice. But perhaps there were security concerns or problems with verification? Or maybe people who worked with the original system found that it wasn't useful in practice, or that it was hard to use effectively? Or maybe I've just misunderstood some aspect of the above? Thanks and best wishes, Mark

4 5

imx6 + libethdrivers + lwip
by Andrea Sorbini 10 Oct '15

10 Oct '15

Hello, I have been experimenting on the SabreLite imx6 board and the network driver provided by libethdrivers. I've been successful in getting it to work "out of the box" and, testing with a simple UDP echo client running on Linux, I've verified that I can send and receive small UDP messages as long as they were not fragmented. I immediately noticed that the fragmentation performed by Linux was different than the one performed by lwip on seL4. Lwip was successfully reassembling a message fragmented in two, but it wasn't fragmenting it when sending it back out. The driver reports an MTU of 1536 and this is likely the reason for lwip not to perform output fragmentation. Hacking the driver slightly, I had it report an MTU of 1500 to lwip, while using the 1536 value internally to allocate buffers. This has allowed me to successfully receive and send UDP messages of up to ~2950 bytes (ie. under 3 frames). When size is increased above that amount, lwip starts behaving "suspiciously" and I can only see the two first two fragments going out, while the third one is never sent (causing the linux host to timeout on the IP reassembly). Debugging the driver, it seems the third fragment is never actually written Has anybody had any experience in getting bigger UDP messages across? Any suggestions on how to enable it if not? Thanks, -Andrea tl;dr: Got UDP working on imx6 with libethdrivers+lwip, can only send up to 2950 bytes, would like to send more, help needed. -- Andrea Sorbini Software Engineer asorbini(a)rti.com +1.408.990.7475 www.rti.com RTI - Your systems. Working as one.

1 0

Camkes MMIO Driver Failed to find device frame
by Jeff Hieb 03 Oct '15

03 Oct '15

I am working on a UART device driver in camkes for AM335x. When I load the image on the board I get this error: Creating object frame_drv_group_bin_42 in slot 596, from untyped 1f6... device frame, paddr = 0x48022000, size = 12 bits capDL-loader :: << Error: Failed to find device frame at paddr = 0x48022000 >> I am reasonably confident the address is correct, (https://github.com/seL4/libplatsupport/blob/master/plat_include/am335x/plat…) Looking at the source It seems capDL-Loader wants to find this device frame in bootinfo https://github.com/seL4/capdl-loader-app/blob/master/src/main.c#L731 Any help on how capDL-loader builds bootinfo would be appreciated. Jeff -- Jeffrey L. Hieb Department of Engineering Fundamentals University of Louisville Louisville Kentucky 40292 (502) 852 0465

4 4

We're hiring!
by Gernot Heiser 29 Sep '15

29 Sep '15

Want to be part of the seL4 team and be *paid* for having fun? We’re hiring: - proof engineers: https://ssrg.nicta.com.au/jobs/proof-engineers2015 - OS engineers: https://ssrg.nicta.com.au/jobs/OS-engineers2015 - researchers/postdocs: https://ssrg.nicta.com.au/jobs/OS-researchers2015 Gernot ________________________________ 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

libsel4cspace and IPC
by Will Korteland 27 Sep '15

27 Sep '15

Hi, I'm trying to implement a "create endpoint" syscall as a continuation of my AOS project last year. I'm using the following code to create and endpoint in the current threads's cspace (using libsel4cspace): https://gist.github.com/anonymous/8294aa47ad351e4d4066 When this code runs, seL4 prints the following during the cspace_ut_retype_addr call: <<seL4 [decodeUntypedInvocation/128 Tffeead00 @b330]: Untyped Retype: Invalid destination address.>> This error comes from inside libsel4cspace, specifically where it calls seL4_Untyped_RetypeAtOffset(). I've read the libsel4cspace documentation and enabled CSPACE_DEBUG, but nothing from the output looks amiss (I'm not an expert though, and I can post the relevant debug output). Have I done anything wrong in the code above? Thanks, - Will

1 0

How to modify timer server in refos
by ぷ风过无痕?? 27 Sep '15

27 Sep '15

I want to transplant the Refos into the ZYNQ board,Now everything is ok,except the timer server. Could you give me some advices about how to modify timer server's file device_timer.c . ------------------ Original ------------------ From: "devel-request";<devel-request(a)sel4.systems>; Date: Thu, Sep 24, 2015 10:00 AM To: "devel"<devel(a)sel4.systems>; Subject: Devel Digest, Vol 16, Issue 12 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel or, via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Reminder: Developers Day registration closes Monday (Gernot Heiser) ---------------------------------------------------------------------- Message: 1 Date: Wed, 23 Sep 2015 05:58:01 +0000 From: Gernot Heiser <gernot(a)nicta.com.au> To: seL4 <devel(a)sel4.systems> Subject: [seL4] Reminder: Developers Day registration closes Monday Message-ID: <FD16E4F0-FD7A-494C-9432-AF1C4903E750(a)nicta.com.au> Content-Type: text/plain; charset="us-ascii" Details at https://sel4.systems/Community/Devdays/ Gernot ________________________________ 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. ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 16, Issue 12 *************************************

2 1

Reminder: Developers Day registration closes Monday
by Gernot Heiser 23 Sep '15

23 Sep '15

Details at https://sel4.systems/Community/Devdays/ Gernot ________________________________ 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

Caught cap fault in send phase at address 0x0
by Andrew Shruhan 22 Sep '15

22 Sep '15

Hello, I am attempting to create a simple program opening up a serial port on the Sabrelight. Attached is the source code and below is the console output. On other sel4 blogs with this problem uboot may have been the issue. I have used the u-boot as discribed on the supported hardware->sabrelight page with the same outcome. Any help would be appreciated. Thanks, U-Boot 2009.08-dirty (Sep 17 2015 - 14:58:04) CPU: Freescale i.MX6 family TO1.2 at 792 MHz Temperature: 36 C, calibration data 0x56a4bc7d mx6q pll1: 792MHz mx6q pll2: 528MHz mx6q pll3: 480MHz mx6q pll8: 50MHz ipg clock : 66000000Hz ipg per clock : 66000000Hz uart clock : 80000000Hz cspi clock : 60000000Hz ahb clock : 132000000Hz axi clock : 264000000Hz emi_slow clock: 132000000Hz ddr clock : 528000000Hz usdhc1 clock : 198000000Hz usdhc2 clock : 198000000Hz usdhc3 clock : 198000000Hz usdhc4 clock : 198000000Hz nfc clock : 24000000Hz Board: MX6Q-SABRELITE:[ POR] Boot Device: I2C I2C: ready DRAM: 1 GB MMC: FSL_USDHC: 0,FSL_USDHC: 1 JEDEC ID: 0xbf:0x25:0x41 Reading SPI NOR flash 0xc0000 [0x2000 bytes] -> ram 0x276009b8 SUCCESS *** Warning - bad CRC, using default environment In: serial Out: serial Err: serial Net: got MAC address from IIM: 00:19:b8:01:fd:6d FEC0 [PRIME] Hit any key to stop autoboot: 0 mmc1 is current device -- Trying fat on SD 1, partition 1 reading sel4-image 344564 bytes read ## Starting application at 0x20000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10 paddr=[20000000..2004c01f] ELF-loading image 'kernel' paddr=[10000000..10031fff] vaddr=[e0000000..e0031fff] virt_entry=e0000000 ELF-loading image 'hello-1' paddr=[10032000..1003ffff] vaddr=[8000..15fff] virt_entry=803c Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Caught cap fault in send phase at address 0x0 while trying to handle: vm fault on data at address 0x0 with status 0x7 in thread 0xffdfd900 "rootserver" at address 0x804 -- -Andrew Andrew P. Shruhan Research and Development Engineer III DocBox, Inc. 320 Nevada St Newton MA, 02460 Work: 857-598-2819 ext. 117 www.docboxmed.com <http://www.docboxinc.com/>

2 1

Question about upstream
by Harish Pillay 9v1hp 20 Sep '15

20 Sep '15

Hi. I came across seL4 yesterday and have not spent too much time on it. I have not found anything specific to my question in the FAQ yet, so I am posing it here: has the work done by seL4 been accepted upstream? If not, any reason why it has not been accepted yet? Thanks. Harish

2 2

Roadmap and Developers Day announcements
by Gernot Heiser 16 Sep '15

16 Sep '15

Dear developers, Those of you who aren’t (yet) subscribed to announce(a)sel4.systems might have missed this: we announced - the seL4 roadmap: https://sel4.systems/pipermail/announce/2015/000007.html - the second Developers Day: https://sel4.systems/pipermail/announce/2015/000008.html Gernot ________________________________ 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.

2 1

Mysterious Label Before sysenter
by Corey Richardson 16 Sep '15

16 Sep '15

For example, here: https://github.com/seL4/seL4/blob/master/libsel4/arch_include/x86/sel4/arch… What use is the label? Does it align the instruction or do other ABI-important things? -- /cmr

2 2

x86-64
by Raymond Jennings 14 Sep '15

14 Sep '15

Does seL4 support x86-64 with 64-bit virtual address spaces?

2 2

Adding a Rust kernel interface generator
by Corey Richardson 11 Sep '15

11 Sep '15

Hello, As part of the robigalia [0] project I must create a Rust interface to the kernel. I'm using the XML from kernel/libsel4 and have been creating a "new" generator by copying the existing Python scripts. Should I send a patch upstream once this is suitably complete, or should I maintain this completely externally? [0] - https://github.com/robigalia -- /cmr

2 2

how to detect the number of CPUs in the system
by 杰尔米 01 Sep '15

01 Sep '15

Hi all, i want to get the number of CPUs in the system and how many cores in one CPU. how to do that? Thanks! Jeremy Li

3 2

The pt/pd/as abstraction vs software TLBs
by Raymond Jennings 01 Sep '15

01 Sep '15

Hey, quick question. This is just hypothetical, but would making management of pagetables/pagedirectories a low level literal operation hurt seL4's portability to other architectures that might not even use page tables? I could be mistaken but I think there's some archs out there that only have software TLBs (openrisc IIRC among them) Please forgive me if I'm mistaken but my recent question about memory abstraction reminded me about this.

3 2

sharing memory between processes
by Raymond Jennings 01 Sep '15

01 Sep '15

Is there an easy way for one task to share address space with another task directly or does it have to go through the kernel/os and be emulated? I noticed that support for mapping memory is mostly low level assignment of physical frames to virtual frames via page tables, unlike Mach which uses memory objects.

6 7

virtual memory abstraction
by Raymond Jennings 31 Aug '15

31 Aug '15

I noticed that unlike mach, L4 does not directly manage virtual memory, but instead farms out address space, page directory, and page table capabilities to userspace and lets userspace decide what pages to map and where. Does this imply that virtual memory abstraction is userspace responsibility?

2 1

Port I/O - Permissions Question
by Josef M. 25 Aug '15

25 Aug '15

Hi, I'm experimenting with some x86 code that involves reading from I/O ports. I noticed--much to my surprise--that I don't have to use seL4_IA32_IOPort_In8() to read from a port; my program works just as fine using the "in" assembly statement directly, without any caps. The TSS segment limit is initialized with 0x67 https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/vspace.c#L158 and the "I/O Map base address" is initialized with 0 (zero) https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/vspace.c#L43 I believe the result is that ring 3 programs can access I/O port addresses below 0x388 (0x67 * 8) without triggering a protection violation. So my question is: Shouldn't capabilities be required for all ports? Or what what is the reason or motivation behind this? Thanks, Josef

2 1

Running Linux atop sel4
by Sebastian Lau 24 Aug '15

24 Aug '15

On the sel4.systems website, it says that the site is served by the Apache web server on Linux atop sel4. How does that work and could you operate the Linux middleware just on top of sel4, maybe something like mer?

1 0

Roadmap?
by Raymond Jennings 22 Aug '15

22 Aug '15

I remember awhile ago that someone was going to post the roadmap in response to my accessed/dirty bit suggestion...but I haven't seen it yet.

2 1

Some questions about seL4 operating system
by Qing Wei 22 Aug '15

22 Aug '15

Hi, I am a beginner to seL4 as well as microkernel, and very interested in it. I think it is great in terms of its minimality and formally verified security. However, I have some questions about it, (1) How is its performance compared to other monolithic kernel, say, Linux. Could it make use of multicore, multiprocessor to enjoy the performance scalability? (2) How is its ecosystem, fox example, how to support new hardware, does it need write the driver from scratch or could it make use of Linux driver? And how to write application on it, or, could it run Linux application without modification? (3) How is its virtualization support, could it run Linux vm, and does it need any modification to the guest os? Cheers, Qing Wei

3 4

Some comments.
by Mehdi Amiri 17 Aug '15

17 Aug '15

Hi, Thank you for all your efforts and time. I believe the user community is the main success key for all open source projects. Many users and researchers, do not have enough time to read, download and evaluate all the source code in order to investigate a system to see if it is suitable for their research or usage. Usually they will go for clean systems which are easy to use, simple to understand, well documented and have a strong community beside the commercial support to ask and get help in case they had a problem. Here are some comments which may help to increase the number of users and developers for seL4: A) I suggest to add some howtos to the website. It's better to be a wiki like system so other individuals, researchers and students can help in writing some titles. Some interesting topics (at least for me as a beginner in micro-kernel) could be: 1- Running Linux/Android on top of seL4. 2- Writing a simple user application with a use case (not just the SOC). 3. Examples on real-time application. 4- Writing a service (could be a device driver, file-system, etc) for seL4. 5- Documents on using possible run-times like Genode. 6- Documents or case studies on porting an opensource software from Linux or POSIX based system to directly run om seL4. B) Providing ready to use download binary images for supported platforms can also accelerate growth of community. C) A research areas page which can suggest researchers some ideas to chose a title and do their research to expand seL4 could also be useful. Ideas like rump-kernels, lib-OS, visualization (x86/ARM), etc seems to be possible research titles on seL4. I have seen the https://sel4.systems/GettingStarted/ page and I think other than CAmkES, ports and Qubes there could be many more titles. D) I know the major development platform of seL4 has been the Arm architecture, but optimizing the code to utilize the x86 architecture including virtualization can also bring a lot of attention to this project to use seL4 as a replacement for Linux-KVM and Xen in the cloud, IoT or real time systems when stability and security is a matter. Also please note, the archive of both development ( https://sel4.systems/pipermail/devel/) and announcements ( https://sel4.systems/pipermail/announce/) mailing lists are not accessible trough the website. I'm an OS researcher and a senior system engineer (mostly Linux) with a limited time, but I can help in some parts if you think it may be useful. Thank you again! Best Regards, Mehdi

2 1

other communications
by Raymond Jennings 17 Aug '15

17 Aug '15

Is there a mailinglist or forum anywhere for people interested in using seL4? I realized this is a dev list and may not be the right place to ask technical supportr questions.

2 1

Detecting dirty/accessed page tables
by Raymond Jennings 15 Aug '15

15 Aug '15

Hey I'm just curious...how do you detect if a memory page mapped by a page table has been written to or accessed? I imagine if you're writing a filesystem task, such information would help you know when to flush data back to disk or which pages to keep around if things get tight. I hope this isn't a stupid question.

5 16