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
…
[View More]>
> 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
>
[View Less]
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/…
[View More]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/
[View Less]
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 …
[View More]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???
[View Less]
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 …
[View More]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
[View Less]
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
…
[View More]example I could try that will help me.
Thanks.
Julien.
[View Less]
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. …
[View More]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
[View Less]
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.
…
[View More]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
[View Less]
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
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
…
[View More]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/
[View Less]
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 …
[View More]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.
[View Less]