Trustworthy Systems

Strengthening scheduling guarantees of seL4 MCS with IPC budget limits

Authors

Mitchell Johnston

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

Abstract

This thesis evaluates some areas for improvement regarding the scheduling behaviour of the seL4 MCS kernel, improving its applicability to mixed-criticality read-time systems. It proposes a set of changes that, when configured correctly, improve system scheduling behaviour regarding budget expiry and budget overrun.

BibTeX Entry

  @mastersthesis{Johnston:be,
    address          = {Sydney, Australia},
    author           = {Mitchell Johnston},
    keywords         = {sel4, threshold},
    month            = nov,
    paperUrl         = {https://trustworthy.systems/publications/theses_public/22/Johnston%3Abe.pdf},
    school           = {School of Computer Science and Engineering},
    title            = {Strengthening scheduling guarantees of {seL4} {MCS} with {IPC} budget limits},
    year             = {2022}
  }

Download