Trustworthy Systems

Strengthening scheduling guarantees of seL4 MCS with IPC budget limits


Mitchell Johnston

    School of Computer Science and Engineering
    Sydney 2052, Australia


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

    address          = {Sydney, Australia},
    author           = {Mitchell Johnston},
    keywords         = {sel4, threshold},
    month            = nov,
    paperUrl         = {},
    school           = {School of Computer Science and Engineering},
    title            = {Strengthening scheduling guarantees of {seL4} {MCS} with {IPC} budget limits},
    year             = {2022}