Trustworthy Systems

sDDF queueing performance

Authors

Lesley Rossouw

    School of Computer Science and Engineering
    UNSW,
    Sydney 2052, Australia

Abstract

The seL4 Device Driver Framework is a high-performance driver framework for the seL4 microkernel, facilitating best-in-class driver performance. It is not clear that the current design, policy set or parameters are ideal under all conditions however, owing to complex dynamic properties. In order to evaluate the suitability of the design and to enable future analysis and optimisation, this thesis presents a discrete-event simulator for the seL4 Device Driver Framework and a suite of analysis tools to accompany it. We provide an efficient, flexible and accurate simulation capable of predicting the dynamics of given system with high accuracy. The analysis tools enable exploration of every event in the system to facilitate in-depth analysis of system configurations and policy sets. We use the combined simulation and analysis suite to explore extreme cases for the sDDF to evaluate its robustness in a variety of cases. We also use the simulation to construct empirical models of the behaviour of the network driver class and to predict optimal parameters that are capable of exceeding all current performance expectations.

BibTeX Entry

  @mastersthesis{Rossouw:be,
    address          = {Sydney, Australia},
    author           = {Lesley Rossouw},
    month            = sep,
    paperUrl         = {https://trustworthy.systems/publications/theses_public/25/Rossouw%3Abe.pdf},
    school           = {School of Computer Science and Engineering},
    title            = {{sDDF} Queueing Performance},
    type             = {{BE} Thesis},
    year             = {2025}
  }

Download