LionsOS is a new seL4-based OS for embedded systems under development at TS. It uses a modular device-driver model that passes I/O data via shared-memory, zero-copy data structures. LionsOS I/O outperforms Linux.
However, the LionsOS driver model is incompatible with that of legacy systems, making it necessary to re-write drivers from scratch. While this is ok for selected, performance- or security-critical devices, and made approachable by the simplicity of the model, it is unfeasible to write all drivers from scratch.
LionsOS supports re-use of unmodified Linux drivers by encapsulating a driver into a minimally configured Linux kernel hosted in a per-device driver VM, which appears to the rest of the system like a native driver. While efficient in terms of engineering cost, this comes at a significant performance cost.
This project is to evaluate and analyse the overheads of driver VMs and investigate how far they can be reduced. While we cannot expect driver VMs to perform at par with native drivers, we are interested in minimising overheads for complex yet important device classes, such as Wifi, USB and graphics. Native Linux will serve as the performance baseline.
School
Computer Science and Engineering
Research Area
Operating systems
Suitable for recognition of Work Integrated Learning (industrial training)?
Yes
- Research environment
- Expected outcomes
- Supervisory team
- Reference material/links
The Trustworthy Systems (TS) Group is the pioneer in formal (mathematical) correctness and security proofs of computer systems software. Its formally verified seL4 microkernel, now backed by the seL4 Foundation, is deployed in real-world systems ranging from defence systems via medical devices, autonomous cars to critical infrastructure. The group's vision is to make verified software the standard for security- and safety-critical systems. Core to this a focus on performance as well as making software verification more scalable and less expensive.
- Report analysing driver VM overheads for several device classes, identifying optimisation opportunities, and achieved improvements;
- Pull requests against the respective sDDF/LionsOS repositories
