Devel

devel@sel4.systems

19 participants
1382 discussions

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

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel