forked from Imagelibrary/seL4
afbea15710
This adds a flags parameter to SchedControl_Configure to enable configuration of a sporadic SC. This also allows flags to be added in the future as needed without breaking the API. This allows the user to configure an SC either to be constrained as a sporadic task where accumulated time is only delayed to when a task has become runnable (implementing the sporadic server algorithm) or whenever the task becomes the current executing task (implementing the sliding-window constraint as in constant-bandwidth servers). This can be used to prevent non-realtime tasks from exceeding bandwidth under any circumstances, even in an over-committed configuration, whilst also allowing work-conserving tasks to be configured in the same system. To implement sporadic servers, we need to ensure that the suspension of a task cannot be used as a mechanism to amplify budget of a task by granting that task access to effectively multiple periods worth of replenishments within a single period. To align the implementation of SCs with the model of sporadic servers we must delay available time until the release of a task. Within seL4, a release would be any time where an SC changes from not being associated with a Running, RunningVM, or Restart thread to one that is. This can occur when an SC is bound to a new thread in such a state or when a thread changes to such a state from any non-running states. Critically, replenishments should not be delayed at the point when an SC becomes the current SC (as was the case prior to this commit). This has the effect of enforcing a continuous, constant bandwidth which is a restriction that is incompatible with standard scheduling logic. Accounting for this requires inserting a new refill_unblock_check call whenever a sporadic SC is unblocked and removing the refill_unblock_check call from when said SC is scheduled. Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
<!--
Copyright 2014, General Dynamics C4 Systems
SPDX-License-Identifier: GPL-2.0-only
-->
seL4 manual (including API). Default make target builds a PDF.
Original text from paper template README follows...
$Id: README,v 1.6 2007-03-07 15:09:26 gernot Exp $
A note on referencing:
The paper/report template can now handle the use of bibexport, and is set up to
use this method by default. In your paper or report, instead of specifying your
bibfile sources in the \bibliography{file0,file1} command, you simply specify
\bibliography{references}. Specify your source bibfiles in the Makefile as
described above.
At make time, the build system will parse your targets for citations and then
collate all the BibTeX entries in references.bib.
This is useful for several reasons. If you need to hand edit BibTeX entries to
save room in your paper, you don't need to edit the ERTOS bibfiles, or make
duplicates on entries in extras.bib. It also means that BibTeX entries are stored
with the paper in the repository.
The Makefile is smart. If you add or remove a reference to a target, the build
system will ask you whether you want to rebuild references.bib. This is to ensure
that if you have made changes by hand to any references, these aren't overwritten.
Consider updating this template when appropriate.