The open-source OKL4 microkernel, developed by Australia's Center of Excellence for Information and Computing Technology (NICTA), is about to receive a strong commercial push. Open Kernel (OK) Labs, a NICTA spinoff, is setting up its U.S. headquarters in Chicago and is rolling out a commercial support package for OKL4.
OKL4, under development at NICTA for the past four years, is an open-source microkernel aimed at embedded consumer and mobile devices. It claims fast performance and supports virtualization, real-time programming, software componentization, fine-grained protection domains, and dynamic resource partitioning. As a microkernel, it only contains code that executes in privileged processor mode.
According to Steve Subar, Open Kernel Labs CEO, the support staff for OKL4 includes some 45 “kernel hackers,” including both OK employees and engineers under contract at NICTA. “It's thought to be the largest group of its kind specializing and focusing in this area,” he said.
“It's been the most actively developed and researched microkernel, and it has an unchallenged performance track record for over 10 years,” claimed Gernot Heiser, OK CTO and a research director at NICTA. He said that OK and NICTA are currently working on a formal mathematical proof that will show that the kernel implementation matches its specification.
Although OK has just been launched as a U.S. company, the commercial use of OKL4 has already begun, Subar said. He said Qualcomm announced its use of OKL4 in November 2005, and that the first Toshiba handset running OKL4 went on the market in Japan last December. “Because of the collaborations we undertook, we have a number of other large commercial customers around the world, and we're launching with an initial foray into the wireless chipset and handset marketplace,” Subar said.
OKL4 is available today under an open-source license, and that will continue. The open source community has access to OKL4 source code and related technologies including a build system, cross-compilation tools for various architectures, sample projects and configurations for commercial platforms, and additional tools. OK will sell a commercial version of OKL4 that includes support, customization, processor architecture porting, and training.
A key feature of OKL4 is virtualization, which lets customers run multiple operating systems in user mode on the same processor core. Users could, for instance, run a real-time operating system (RTOS) and a high-level operating system, with isolation between the two to protect from system failures, Heiser said.
OKL4 also claims security features. It supports “fine-grained” protection domains in which application programs, system services, and device drivers can be individually encapsulated. It also supports dynamic allocation and de-allocation of resources to subsystems. OKL4 claims to support high-performance cross-domain communications.
“There's full control over resources located in various subsystems,” said Heiser. “There's full control over communications between those subsystems. In that sense you have the functionality you have in a separation kernel, but at the same time it provides high bandwidth, low latency communications between subsystems.”
OKL4 claims to have a minimal “trusted computing base” (TCB). A system with a TCB as small as 20,000 lines of code can be constructed by adding a minimal set of libraries and services, according to OK.
Heiser said that OKL4 supports hard real-time applications “in principle,” but is not defined in that way at present. “We haven't got a complete timing model and we don't claim to know our worst case latency,” he said. “A lot of people claim latencies based on benchmarking. We think the responsible way is to complete a theoretically sound investigation of the timing behavior of the kernel.” That research project is underway, he said.
OKL4 is currently available for ARM v4/v5 and x86 processors, with support for MIPS processors promised soon. Presently supported guest operating systems include Wombat, OK's virtualized Linux 2.6.10, and eCos.