Hi
I played with the demo cd and it works great..
Just a few questions which I am having a hard time understanding:
1. L4 is itself a API/ABI reference, right?
2. Are L4.Pistachio and L4.Fiasco are 2 different implementations of L4?
3. Is L4.Pistachio is the current official reference implementation? Do both of them only differ in internal code only?
3. What is the difference between L4.Pistachio and L4.Fiasco? Why are there 2 separate implementations ie. why not just one codebase? Are you able to merge these 2 together or plan to?
4. Is L4.Sec official and already in the process of being implemented? Is L4.Pistachio and L4.Fiasco going to be replaced by L4.Sec?
Thanks Shams
Shams wrote:
Hi
I played with the demo cd and it works great..
Just a few questions which I am having a hard time understanding:
- L4 is itself a API/ABI reference, right?
L4 is a family of microkernels. There are two main APIs: L4-X.2 (aka L4-V.4) and L4-V.2, which include a binary interface (ABI) for each supported processor architecture. In addition there are two experimental APIs: L4.Sec and seL4 (see the Nicta homepage).
- Are L4.Pistachio and L4.Fiasco are 2 different implementations of L4?
Yes, Pistachio implements the L4-X.2 API. Fiasco implements an improved version of L4-V.2 that incorporates some extensions inspired by L4-X.2 (e.g., UTCBs) and by our local work here (e.g., support for real-time scheduling).
- Is L4.Pistachio is the current official reference implementation?
When you look for a reference implementation for L4-X.2 maybe yes.
Both Fiasco and Pistachio origin from experiments but are right now widely used even by some industry partners.
Do both of them only differ in internal code only?
No, they also differ in the API version they implement.
- What is the difference between L4.Pistachio and L4.Fiasco?
Why are there 2 separate implementations ie. why not just one codebase?
We have two code bases primarily for historic reasons. Fiasco was implemented in C++ at the time when the main stream L4 kernel was Jochen Liedke's assembler kernel implementing the L4-V2 API. Pistachio was developed later. One of the design goals was to restructure the code base to better support porting the kernel to different architectures. Fiasco was later on re-factored to support multiple architectures as well.
Are you able to merge these 2 together or plan to?
Technically yes, but why should we do so? One can only learn from having two alternative implementations.
- Is L4.Sec official and already in the process of being implemented?
We have a partial implementation of the L4.Sec API but there are no near term plans to release it.
Is L4.Pistachio and L4.Fiasco going to be replaced by L4.Sec?
Probably not. The main objective of L4.Sec was to experiment with capabilities and kernel memory management.
Marcus
Hi Marcus,
Thanks for the info.
1. Since L4.Pistachio and L4.Fiasco both are now implemented in C++ and L4.Pisctatio implements the "latest" L4 API ie. L4-X.2 (L4-V.4), does this conclude that L4.Pistachio is more superior implementation than L4.Fiasco?
3. With L4.Linux is this just a virtualised version of Linux to run on either L4.Pistachio or L4.Fiasco or is this just another implementation of Linux that implements the L4 API?
4. If I want to use L4 for research purposes should I be using L4.Pistachio or L4.Fiasco or L4.Linux?
Thanks Shams
Hi,
On Sun Jun 03, 2007 at 19:44:04 +1200, Shams wrote:
- Since L4.Pistachio and L4.Fiasco both are now implemented in C++ and
L4.Pisctatio implements the "latest" L4 API ie. L4-X.2 (L4-V.4), does this conclude that L4.Pistachio is more superior implementation than L4.Fiasco?
Fiasco implements an interface that has been modified and enhanced in many ways from the original interface. Also, Pistachio and kernels based on Pistachio undergo further development. It is not up to me to judge if there is a 'superior' implementation. Both have their merits.
- With L4.Linux is this just a virtualised version of Linux to run on
either L4.Pistachio or L4.Fiasco or is this just another implementation of Linux that implements the L4 API?
L4Linux is a version of Linux running on L4 as a user space application.
- If I want to use L4 for research purposes should I be using L4.Pistachio
or L4.Fiasco
That's up to you. This also depends on what you specifically want to do and what might suit you more.
Adam
On Sun, 3 Jun 2007 19:44:04 +1200, "Shams" shams@orcon.net.nz said:
S> Hi Marcus, S> Thanks for the info.
S> 1. Since L4.Pistachio and L4.Fiasco both are now implemented in C++ and S> L4.Pisctatio S> implements the "latest" L4 API ie. L4-X.2 (L4-V.4), does this conclude that S> L4.Pistachio S> is more superior implementation than L4.Fiasco?
There are presently 3 actively-maintained versions, Fiasco, Pistachio and OKL4 (a descendent of Pistachio). The APIs are evolving as R&D is progressing (although I guess it's fair to say that OKL4 is evolving most rapidly, for better or worse).
S> 3. With L4.Linux is this just a virtualised version of Linux to run on S> either L4.Pistachio or L4.Fiasco S> or is this just another implementation of Linux that implements the L4 API?
L4.Linux is a para-virtualised Linux on L4, but it isn't the only one. Karlsruhe has their afterburned Linux that runs on Pistachio, and NICTA/OK have Wombat, which is a portable para-vitrualised Linux that runs on OKL4 on several architectures (x86, ARM and MIPS).
S> 4. If I want to use L4 for research purposes should I be using L4.Pistachio S> or L4.Fiasco S> or L4.Linux?
L4Ka::Pistachio and Fiasco (like the OKL4 kernel) are microkernels, L4Linux isn't (it's a paravirtualised Linux on L4, as is Wombat).
You can use either of the three for research, including OKL4 (just because it's commercial doesn't mean it cannot be used for research purposes, to the contrary, it's a very mature platform given that it is running in consumer products).
Gernot
Hi,
Regarding OKL4: http://www.ok-labs.com/products/
1. Is OKL4 is a commercial implementation of L4?
2. Is OKL4 based on the L4.Pistachio code base and still open-source but with a separate source tree?
3. The OKL4 roadmap http://www.ok-labs.com/products/product_roadmap mentions "High-security API" and "Formal correctness proof".
Does this mean that L4.Sec may or is already getting implemented in OKL4?
Thanks Shams
Hi Shams,
On 6/3/07, Shams shams@orcon.net.nz wrote:
- Is OKL4 is a commercial implementation of L4?
I'm not sure about what you mean by commercial, but OKL4 is still BSD licensed, As far as I understand, Open kernel labs is a son of NICTA, with the purpose of commercializing ERTOS research program developments, you may find more information about this at NICTA's web site.
2. Is OKL4 based on the L4.Pistachio code base and still open-source
but with a separate source tree?
L4.Pistachio is developed and maintained by the System Architecture Group at the University of Karlsruhe, people from U of new south wales used it to make their l4.embedded, and added a minimal OS personality called iguana, the L4.embedded API has changed a lot in the last year, and it is now released under the name of OKL4, by open kernel labs. OKL4=OKL4 microkernel + iguana + wombat
3. The OKL4 roadmap http://www.ok-labs.com/products/product_roadmap
mentions "High-security API" and "Formal correctness proof".
What I understand is that the formal correctness proof its being worked in team with NICTA, using Isabelle.
Does this mean that L4.Sec may or is already getting implemented in OKL4?
I think they are two different things.
Well hope it helps.
Thanks
Shams
l4-hackers mailing list l4-hackers@os.inf.tu-dresden.de http://os.inf.tu-dresden.de/mailman/listinfo/l4-hackers
On Sun, 3 Jun 2007 19:53:08 +1200, "Shams" shams@orcon.net.nz said:
S> Hi, S> Regarding OKL4: S> http://www.ok-labs.com/products/
S> 1. Is OKL4 is a commercial implementation of L4?
OKL4 is "commercial" in that it is professionally developed and supported by Open Kernel Labs, and that it is deployed in commercial products. Eg Qualcomm ships wireless chipsets where the firmware is based on OKL4, and Toshiba sells a mobile phone handset that runs OKL4. There are many other deployments that aren't public yet.
S> 2. Is OKL4 based on the L4.Pistachio code base and still open-source S> but with a separate source tree?
OKL4 is based on the L4Ka::Pistachio code base, but has deviated substantially from it, both in API and implementation. It is still distributed under a BSD license.
S> 3. The OKL4 roadmap http://www.ok-labs.com/products/product_roadmap S> mentions "High-security API" and "Formal correctness proof".
S> Does this mean that L4.Sec may or is already getting implemented in OKL4?
The high-security API is that of the seL4 project, which is quite different from L4.Sec. There is plenty of information, including several very recent publications showing the liveness of the project on the seL4 website, http://ertos.nicta.com.au/research/sel4/ There is a prototype implementation, and an executable version of the specification. The latter will be published as soon as we get our lawyers to agree to it. We also have formal proofs of certain security properties of the seL4 API.
The formal correctness proof is targeting the seL4 implementation, details can be found on the L4.verified web page http://ertos.nicta.com.au/research/l4.verified/
The OKL4 API is converging towards seL4 in small steps, to ensure a migration path for existing OKL4e customers.
Gernot
Thanks for the info.
1. After reading up on http://www.ok-labs.com/ I still couldn't find the following info.
Does OKL4 only run on ERTOS or can it run on other architectures like L4.Pistachio eg. PowerPC, IA32, IA64, see: http://l4ka.org/projects/pistachio/?
2. Since OKL4 is evolving as a commercial project (and being a descendant of L4.Pistachio) how much contribution is OKL4 making back to the L4 community in particular L4.Pistachio in terms of API, ABI, Architecture, Documentation etc, I mean for significant commercial improvements to OKL4 are most/some of them integrated back into L4-V4/.Pistachio?
3. Also if L4-V4/L4.Pistachio evolves then doe the changes get followed through into OKL4.
4. So OKL4 can be used commercially or in a research environment (free of charge) but if one wants commercial support/development then they have to pay for it, right? Sorry just getting my BSD license understanding clarified.
Thanks Shams
On Mon, 4 Jun 2007 07:43:12 +1200, "Shams" shams@orcon.net.nz said:
S> Thanks for the info. S> 1. After reading up on http://www.ok-labs.com/ I still couldn't find the S> following info.
S> Does OKL4 only run on ERTOS or can it run on other architectures like S> L4.Pistachio S> eg. PowerPC, IA32, IA64, see: http://l4ka.org/projects/pistachio/?
not sure what you mean with "only run on ERTOS".
OKL4 presently is supported on x86, ARM and MIPS. Others will be released in the future. Some Pistachio ports (like Alpha, Itanium) aren't presently maintained by anyone. In fact, I don't think anyone is really maintaining Pistachio on anything but x86 (but I could be mistaken).
S> 2. Since OKL4 is evolving as a commercial project (and being a descendant of S> L4.Pistachio) S> how much contribution is OKL4 making back to the L4 community in particular S> L4.Pistachio S> in terms of API, ABI, Architecture, Documentation etc, I mean for S> significant commercial S> improvements to OKL4 are most/some of them integrated back into S> L4-V4/.Pistachio?
Given that OKL4 has forked from L4Ka::Pistachio a couple years ago, there is a limit to what code can be contributed back. However, OKL4 is distributed under a compatible license, so people are welcome to take stuff back into Pistachio.
As far as API is concerned, I don't think that the KA Pistachio maintainers want to go the way OKL4 is going.
S> 3. Also if L4-V4/L4.Pistachio evolves then doe the changes get followed S> through into S> OKL4.
Maybe, maybe not. KA changes are motivated by different deployment scenarios, and the code and API has diverged significantly.
S> 4. So OKL4 can be used commercially or in a research environment (free of S> charge) but if one S> wants commercial support/development then they have to pay for it, right? S> Sorry just getting my S> BSD license understanding clarified.
OKL4 is presently licensed under a straight BSD license. You can do with it pretty much whatever you can do with Pistachio. In addition, you can get commercial support (services such as porting, system architecture, training etc). Also, OK has code which builds on OKL4 that is under proprietary licenses.
In addition, while the KA folks have always maintained very high standards of code quality, they are a research team and cannot possibly put as much effort into QA as Open Kernel does.
Gernot
Many thanks for the info.
With ERTOS I mean embedded real time OS.
1. But you say it supports OKL4 supports x86 so thats means that it should be possible to run OKL4 on an x86-32/x86-64 server/desktop/laptop computer just like I can take L4.Pistaschio and run it on my 64-bit desktop computer?
2. Is seL4 only for embedded systems? I mean when OKL4 incorporates seL4 would these seL4 features also be available on OKL4 for x86-32/x86-64?
3. Also briefly why did OK choose seL4 rather than L4.Sec for OKL4?
Thanks Shams
On Fri, 8 Jun 2007 12:51:45 +1200, "Shams" shams@orcon.net.nz said:
S> Many thanks for the info. S> With ERTOS I mean embedded real time OS.
S> 1. But you say it supports OKL4 supports x86 so thats means that it should S> be possible S> to run OKL4 on an x86-32/x86-64 server/desktop/laptop computer just like I S> can S> take L4.Pistaschio and run it on my 64-bit desktop computer?
Yes, but because we target embedded systems there isn't a lot of emphasis on making everything work on standard PC platforms. Specific questions are best directed to the OKL4 developers mailing list, see http://portal.ok-labs.com/
S> 2. Is seL4 only for embedded systems? I mean when OKL4 incorporates S> seL4 would these seL4 features also be available on OKL4 for x86-32/x86-64?
Sure. These features are generally independent of the processor architecture. Once rolled out in OKL4, the features will be available on all supported architectures. There are a large number of embedded systems using x86 processors :-)
However, the seL4 prototype (to be released once we beat sense into NICTA lawyers) presently only supports ARM.
S> 3. Also briefly why did OK choose seL4 rather than L4.Sec for OKL4?
Open Kernel Labs grew out of NICTA, and seL4 is a NICTA project, so that's natural. seL4 was started at about the same time as L4.Sec, but if you look at it you'll see that they go quite different ways. seL4 is a much more radical approach, where L4.Sec is relatively incremental. Obviously we think that the seL4 approach is better ;-) but judge for yourself.
Although I admit that checking is a bit difficult given the lack of a release. But check out the several papers written about it, see http://ertos.nicta.com.au/research/sel4/
Gernot
Hi,
1. Also is OKL4 the one and only commercially implementaed and supported version of L4?
2. I believe OK is using gcc to build OKL4. However is this a custom version of gcc or just the normal 4.x version thats available for everyone else?
Thanks Shams
On Fri, 8 Jun 2007 13:05:36 +1200, "Shams" shams@orcon.net.nz said:
S> Hi, S> 1. Also is OKL4 the one and only commercially implementaed S> and supported version of L4?
Depends what you call "commercially implementaed". I understand that Pistachio and Fiasco are used in some commercial projects, and there are commercial (closed-source) L4 clones. However, I'm not aware of any company specifically providing professional support for any other open-source L4 versions.
S> 2. I believe OK is using gcc to build OKL4. However is this S> a custom version of gcc or just the normal 4.x version thats S> available for everyone else?
Standard GNU tool chains, but other tool chains (eg ARM compilers) are also supported. Again, check the Open Kernel Labs web site http://portal.ok-labs.com/
Gernot
Gernot Heiser wrote:
On Fri, 8 Jun 2007 13:05:36 +1200, "Shams" shams@orcon.net.nz said:
S> Hi, S> 1. Also is OKL4 the one and only commercially implementaed S> and supported version of L4?
Depends what you call "commercially implementaed". I understand that Pistachio and Fiasco are used in some commercial projects, and there are commercial (closed-source) L4 clones. However, I'm not aware of any company specifically providing professional support for any other open-source L4 versions.
There is another commercial version of L4, which however only implements a subset of the API: P4. This is a closed source solution by SysGo: At www.sysgo.com follow the PikeOS link in Products for more information.
Marcus
Hi Marcus
Am Freitag, 8. Juni 2007 09:08 schrieb Marcus Voelp:
Gernot Heiser wrote:
> On Fri, 8 Jun 2007 13:05:36 +1200, "Shams" shams@orcon.net.nz > said:
S> Hi, S> 1. Also is OKL4 the one and only commercially implementaed S> and supported version of L4?
Depends what you call "commercially implementaed". I understand that Pistachio and Fiasco are used in some commercial projects, and there are commercial (closed-source) L4 clones. However, I'm not aware of any company specifically providing professional support for any other open-source L4 versions.
There is another commercial version of L4, which however only implements a subset of the API: P4. This is a closed source solution by SysGo: At www.sysgo.com follow the PikeOS link in Products for more information.
Thanks for bringing this up. In fact, P4 (which is also referred to as the "PikeOS microkernel" in more recent documents) is a subset to L4 in some respects as well as a superset in some others -- it's just "different".
I presented a paper at the MIKES 2007 Workshop about the kernel's evolution from a full L4 V2.0 API clone to what it is today. The proceedings of the workshop (including that paper) are on NICTA's web site:
www.ertos.nicta.com.au/publications/ papers/Kuz_Petters_07.pdf
Cheers
Rob
l4-hackers@os.inf.tu-dresden.de
-
Adam Lackorzynski -
Gernot Heiser -
Jorge Torres -
Marcus Voelp -
Robert Kaiser -
Shams