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-…
[View More]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.
[View Less]
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 …
[View More]_thread_state_t enumeration-type variables (kernel\include\object\structures.h ). Does it influences formal verification? Thank you so much!!
[View Less]
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/…
[View More]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
[View Less]
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
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
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?
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}/../../…
[View More]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
[View Less]
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 …
[View More]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.
[View Less]
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";&…
[View More]lt;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
************************************
[View Less]
