Description of field of research:
Development of operating-system functionality frequently involves performance analysis and optimisation. The seL4 microkernel presently has limited support for this. In particular, it is missing a gprof-like framework for performance analysis through statistical sampling. The project is to learn how statistical sampling is implemented in Linux and implement equivalent functionality on seL4, with generation of output suitable for post-processing by gprof.
School
Research Area
Operating systems
- Research Environment
- Expected Outcomes
- Reference Material/Links
- Our team
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.
1) Gprof-like library for statistical sampling
2) Tool that mangles the collected data into a form that can be processed by gprof
