Description of field of research:

Recent work in TS on building performance networking support in seL4 has shown that Linux networking performance lags significantly behind what can be achieved on seL4 with the seL4 Device Driver Framework (sDDF), despite Linux requiring far fewer mode and context switches than an seL4-based system for the same job. There is indication that this represents a performance regression in the Linux networking subsystem.

This project is to understand the nature and cause(s) of this regression. The work is to build various Linux point releases from the past 15 years and run network performance test on them. Identify the points of significant regression, and analyse the kernel changes that went into those releases. Try to understand the root causes of the regression.


Computer Science and Engineering

Research areas

Operating systems

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 describing the evaluation and analysis.