Global Information Lookup Global Information

L4 microkernel family information


L4 microkernel family
DeveloperJochen Liedtke
Written inAssembly language, then C, C++
OS familyL4
Working stateCurrent
Source modelOpen source, closed source
Initial release1993; 31 years ago (1993)
Marketing targetReliable computing
Available inEnglish, German
PlatformsIntel i386, x86, x86-64, ARM, MIPS, SPARC, Itanium, RISC-V
Kernel typeMicrokernel
LicenseSource code, proofs: GPLv2
Libraries, tools: BSD 2-clause
Preceded byEumel
Official websiteos.inf.tu-dresden.de/L4

L4 is a family of second-generation microkernels, used to implement a variety of types of operating systems (OS), though mostly for Unix-like, Portable Operating System Interface (POSIX) compliant types.

L4, like its predecessor microkernel L3, was created by German computer scientist Jochen Liedtke as a response to the poor performance of earlier microkernel-based OSes. Liedtke felt that a system designed from the start for high performance, rather than other goals, could produce a microkernel of practical use. His original implementation in hand-coded Intel i386-specific assembly language code in 1993 created attention by being 20 times faster than Mach.[1] The follow-up publication two years later[2] was considered so influential that it won the 2015 ACM SIGOPS Hall of Fame Award. Since its introduction, L4 has been developed to be cross-platform and to improve security, isolation, and robustness.

There have been various re-implementations of the original L4 kernel application binary interface (ABI) and its successors, including L4Ka::Pistachio (implemented by Liedtke and his students at Karlsruhe Institute of Technology), L4/MIPS (University of New South Wales (UNSW)), Fiasco (Dresden University of Technology (TU Dresden)). For this reason, the name L4 has been generalized and no longer refers to only Liedtke's original implementation. It now applies to the whole microkernel family including the L4 kernel interface and its different versions.

L4 is widely deployed. One variant, OKL4 from Open Kernel Labs, shipped in billions of mobile devices.[3][4]

  1. ^ Liedtke, Jochen (December 1993). "Improving IPC by kernel design". 14th ACM Symposium on Operating System Principles. Asheville, NC, USA. pp. 175–188.
  2. ^ Liedtke, Jochen (December 1995). "On µ-Kernel Construction". Proceedings 15th ACM Symposium on Operating Systems Principles (SOSP). pp. 237–250. Archived from the original on 25 October 2015.
  3. ^ "Hypervisor Products: General Dynamics Mission Systems". General Dynamics Mission Systems. Archived from the original on 15 November 2017. Retrieved 26 April 2018.
  4. ^ "Open Kernel Labs Software Surpasses Milestone of 1.5 Billion Mobile Device Shipments" (Press release). Open Kernel Labs. 19 January 2012. Archived from the original on 11 February 2012.

and 18 Related for: L4 microkernel family information

Request time (Page generated in 0.868 seconds.)

L4 microkernel family

Last Update:

L4 is a family of second-generation microkernels, used to implement a variety of types of operating systems (OS), though mostly for Unix-like, Portable...

Word Count : 3982

Microkernel

Last Update:

minimality and are specialized to supporting virtual machines; the L4 microkernel frequently finds use in a hypervisor capacity. Early operating system...

Word Count : 5726

L4

Last Update:

submarine L-4 L4 microkernel family, a family of operating system kernels L4, the transport layer in the OSI model of computer communications L4, the fourth...

Word Count : 310

Jochen Liedtke

Last Update:

computer scientist, noted for his work on microkernel operating systems, especially in creating the L4 microkernel family. In the mid-1970s Liedtke studied for...

Word Count : 995

GNU Hurd

Last Update:

various efforts were launched to port the Hurd to more modern microkernels. The L4 microkernel was the original choice in 2004, but progress slowed to a halt...

Word Count : 2488

Eumel

Last Update:

orthogonal persistence. EUMEL was followed by the L3 microkernel, and later the L4 microkernel family. Liedtke, Jochen (December 1993). "A persistent system...

Word Count : 271

Trusted computing base

Last Update:

verification of seL4, a member of the L4 microkernel family, proving functional correctness of the C implementation of the kernel. This makes seL4 the first operating-system...

Word Count : 1632

Linux Foundation

Last Update:

Archived from the original on 2023-01-24. Retrieved 2020-12-31. "seL4 Microkernel Optimized for Security Gets Support of Linux Foundation". 7 April 2020...

Word Count : 2731

Fiasco

Last Update:

designed to create a Coen-brothers-style story Fiasco, an open-source L4 microkernel family operating system developed at TU Dresden FIASCO, the name used by...

Word Count : 203

PikeOS

Last Update:

environment (IDE) for embedded systems. It is a commercial clone of the L4 microkernel family. PikeOS has been developed for safety and security-critical applications...

Word Count : 786

L4Linux

Last Update:

that is altered to the extent that it can run paravirtualized on an L4 microkernel, where the L4Linux kernel runs a service. L4Linux is not a fork but...

Word Count : 199

Comparison of operating system kernels

Last Update:

support for memory protection, so the strong isolation goals of the microkernel design could not be achieved.[citation needed] "Chapter 14. Security"...

Word Count : 1162

List of operating systems

Last Update:

in Haskell and C ILIOS – Research OS designed for routing L4 – second generation microkernel Mach – from OS kernel research at Carnegie Mellon University;...

Word Count : 8243

REX OS

Last Update:

is a combination of two operating systems: L4Ka::Pistachio embedded microkernel and Iguana, with extensive modifications and extensions by Qualcomm and...

Word Count : 264

Hypervisor

Last Update:

Parallels Workstation, and a "DIAGNOSE code" in IBM VM. Some microkernels, such as Mach and L4, are flexible enough to allow paravirtualization of guest...

Word Count : 2766

OpenVMS

Last Update:

on top of the L4 microkernel and supported the x86-64 architecture. Prior work investigating the implementation of VMS using a microkernel-based architecture...

Word Count : 9044

List of important publications in computer science

Last Update:

significant impact on the design of the Windows NT kernel and modern microkernels like L4. In addition, its memory-mapped files feature was added to many monolithic...

Word Count : 5931

Raspberry Pi

Last Update:

operating systems can also run on the Raspberry Pi. The formally verified microkernel seL4 is also supported. There are several ways of installing multiple operating...

Word Count : 18191

PDF Search Engine © AllGlobal.net