Make the definition for NULL generic, so it can be used in constants
that are shared by C and assembly code.
Signed-off-by: Axel Heider <axelheider@gmx.de>
- Provide the macro ULL_CONST() for 'unsigned long long' constants, and
use it where applicable.
- Add a verbose explanation why the 'unsigned long long' type is used
for time constants.
Signed-off-by: Axel Heider <axelheider@gmx.de>
- Reorder the macro definitions to ensure things are define before they
are used.
- provide a verbose explanation why the UL_CONST() macro is needed.
- make BIT() macro is defined generic by using UL_CONST().
Signed-off-by: Axel Heider <axelheider@gmx.de>
Also make the output more verbose in case of errors, which is
helpful when porting the kernel to new platforms.
Signed-off-by: Axel Heider <axelheider@gmx.de>
With this change, even architectures which do not use a distinct region
to map the kernel ELF will use the `kpptr_to_addr` to translate any
address from the kernel region.
This ensures that these accesses are correctly checked for bounds when
used and will make it easier to move the ELF mapping into a distinct
region of virtual address space.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Move all of the virtual to physical translation functions into a single
common file and use the updated constants.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Like SCTLR, CNTV_CTL is switched to/from hardware when we enable/disable
the VCPU, so it must be read from a saved VCPU context when that VCPU
isn't active.
Signed-off-by: Nick Spinale <nick@nickspinale.com>
The scheduler cannot correctly schedule once the timestamp exceeds
MAX_RELEASE_TIME as releases beyond this point may be subject to
overflow. For most systems this should still allow a great many years if
the timestamp starts from 0 at system boot.
Some systems currently start with a random initial timestamp and my
begin with a timestamp that prvents correct budgeting. This assert helps
to catch cases where scheduling becomes invalid due to the timestamp
exceeding the give bound.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
The proofs currently only guarantee that the system scheduler is correct
while the current time is less than INT64_MAX - 3 * MAX_PERIOD ticks.
With the MAX_PERIOD configured to almost INT64_MAX, this would imply
that the system scheduler is never correct.
To ensure that we get a large duration where the system is correct, we
take 1/8th of the TOTAL representable time as the MAX_PERIOD, ensuring
that 3 * MAX_PERIOD is still less than half of all representable time.
For a system with a 1MHz scheduling clock, this produces a valid
execution time on the order of 2^19 years.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This re-introduces the overrun handling but bounds charging of budget
such that we never calculate a refill with a start using an integer
overflow.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
A refill can still be charged if the refill list is full. This means
that we only require sufficient capacity to continue a timeslice.
Signed-off-by: Kent McLeod <kent@kry10.com>
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This replaces the refill_split_check and refill_budget_check with a
single function that chanrges the provided usage to an SC and updates
the refills.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Remove the UART handling details from the top level I/O handling that
implements printf(). The architecture's I/O handling must define how
the debug channel is implemented and what special handling is
required. This allows separating UART and SBI debug output handling.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Replace capDL() by a generic debug_capDL() where all architectures are
supposed to provide an implementation or print an error.
Signed-off-by: Axel Heider <axelheider@gmx.de>
When ksDomainTime reaches 0 the current domain expires and the next
domain is switched to. This change performs the domain time accounting
in one place, in updateTimestamp, and avoids situations where ksConsumed
is reset without also updating ksDomainTime such as in chargeBudget.
Calling rescheduleRequired in the domain expires ensures that a new
thread will be chosen in the scheduler after the domain has been
advanced. Any remaining ksConsumed will be charged to the outgoing
scheduling context when it is switched away from.
Signed-off-by: Kent McLeod <kent@kry10.com>
Rather than charge consumed time to the current thread at the point
where it is exhausted in a long-running syscall, we only check whether
checkBudget would fail and raise an exception if it would. We then
always charge after handleInvocation rather than avoid-double charging.
This is done as it is easier to add the exhaustion case in the abstract
spec in this manner (without also adding changes to the current SC).
Signed-off-by: Curtis Millar <curtis@curtism.me>
When determining whether a SC donated from the notification should be
returned, we must ensure not to try and return a NULL SC to a
notification with not bound SC.
This could occur when a passive server performs a NBSendWait/NBSendRecv
with a notification in the receive phase, where the SC for the receiver
was returned in the send phase and the notification has no bound SC.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
As this variable bounds both the period and the budget and the period
itself bounds the budget, the name for this variable would be more
appropriately named 'MAX_PERIOD'
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
See: https://sel4.atlassian.net/browse/SELFOUR-2830 for details.
On SMP configuration the `ic ialluis` instruction must be used
to ensure the I-cache on all cores is invalidated.
Signed-off-by: Ben Leslie <benno@brkawy.com>
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>
Actually divide by KHz frequency when on a platform that uses a clock
that does not have an integer MHz frequency for aarch64.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
A previous commit (9ec5df5f) to provide more efficient CLZ (count
leading zeros) and CTZ (count trailing zeros) removed the `__clzsi2` and
`__ctzsi2` symbols, due to a misunderstanding of the types of these and
other library functions expected by GCC's intrinsics. 9ec5df5f broke the
riscv32 build.
This commit corrects the misunderstanding:
- `__clzsi2` and `__ctzsi2` are reinstated with correct types.
- The types of `__clzdi2` and `__ctzdi2` are corrected.
- `__clzti2` and `__ctzti2` are removed, since seL4 contains no compiler
intrinsics that would require them.
- `clzl` and `ctzl` dispatch to the appropriate library functions based
on the size of `unsigned long`.
- Configuration options are updated to ensure that the library functions
are included in the kernel binary only when needed.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
`register_t` only needs to be able to index into the TCB user context
array, which has 35 entries. Therefore `uint8_t` is sufficient.
Using the smallest possible type for `register_t` helps with binary
verification. This shrinks static read-only data, which in turn reduces
the complexity of binary verification proof search.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
The `register_t` type was intended to be used for *indices* into the
user context, but various sbi operations in the RISC-V kernel have used
it for register *contents*. This commit changes those to use `word_t`
for register contents.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
For RISC-V platforms that do not provide machine instructions to count
leading and trailing zeros, this commit includes more efficient library
functions. For verification, we expose the bodies of the functions to
the proofs.
Kernel config options `CLZ_BUILTIN` and `CTZ_BUILTIN` allow selection of
whether compiler builtin functions should be used. These are only
supported on platforms where the builtin compiles to inline assembly. By
default, the options are on for all platforms except RISC-V.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
The binary verification tools perform inlining of C specifications, to
simulate inlining that has been performed in the binary. This means that
`DONT_TRANSLATE` and `inline` are incompatible, since the binary
verification tools require C specifications for any functions that have
been inlined in the binary.
This `DONT_TRANSLATE` annotation was added with a `MODIFIES` annotation
for proofs that the C refines the abstract specification. Those proofs
have been updated such that the annotations are no longer needed.
Reverts 1fba3d9e68 and b903cb7372.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
The RISC-V calling convention specifies that when a C function takes an
argument by value, the binary function should take the argument by
reference, if the value is larger than 2 pointer words.
For binary verification, we avoid implementing this aspect of the RISC-V
calling convention, by eliminating all such function arguments for
functions which are not inlined.
In this commit, we remove the `slot_range_t` structure altogether. For
the small number of functions which previously used this type, we unpack
the structure into three separate arguments.
Even though we are primarily concerned with RISC-V, we remove
`slot_range_t` arguments across all architectures.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
The RISC-V calling convention specifies that when a C function takes an
argument by value, the binary function should take the argument by
reference, if the value is larger than 2 pointer words.
For binary verification, we avoid implementing this aspect of the RISC-V
calling convention, by eliminating all such function arguments for
functions which are not inlined.
In this commit, we remove `extra_caps_t` function arguments. This
primarily concerns invocation decode functions. Since `loookupExtraCaps`
already stores extra caps in a global `current_extra_caps`, this
essentially amounts to eliminating many redundant structure copy
operations.
On some execution paths involving IPC, the extra caps lookup may happen
twice: first in the invocation decode, and then for cap transfer in the
performance phase of the IPC operation. Because the two phases are
entirely distinct, there is no interference in the use of a common
global variable.
Even though we are primarily concerned with RISC-V, we remove
`extra_caps_t` arguments across all architectures.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
A 'released' SC is one that has been configured with its head refill in
the past.
An 'active' checking function checks for whether an SC has been
configured.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Different microarchitectures & configurations save different sets of
VCPU registers when the current VCPU is not active. This generalises the
handling of these cases such that each microarchitecture defines which
regisers are managed in this fashion.
Fixes regression introduced in 454dfd897f
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Most of the uses of these are in functions where the cap type is
statically known and the correct branch could be used directly, but the
compiler does not know this so having these as inlines causes a large
number of accesses to bitfields of unrelated cap types in functions that
manipulate caps.
Moving this out of line makes the results of changing cap bitfields less
noisy.
Signed-off-by: Stefan O'Rear <sorear@fastmail.com>
For 64-bit, this adds a 2nd-level page table for mapping devices using
2MiB frames instead of 1GiB frames.
The boot mapping and hardware header generator have also been fixed to
correctly report the number of large frames needed for devices rather
than only reporting the first. The frame size is also specified
correctly (rather than assuming mapping with 4KiB frames).
This likely fixes an issue whereby only the first 4KiB frame of a device
was reserved but the remaining region of that kernel device could be
mapped at user level.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This is a shortcut for dealing with the inline assembly inside to
prevent the modifies analysis from picking up every part of the state.
For any future binary correctness analysis, this will need to be
removed, and instead an appeal made to inline assembly being unable to
modify the heap.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
merge the PLIC drivers for ariane and hifive
Signed-off-by: Nils Wistoff <nwistoff@iis.ee.ethz.ch>
Reviewed-by: Siwei Zhuang <siwei.zhuang@data61.csiro.au>
This makes the kernel configuration defaults public and known to the
user level. Generally shouldn't depend on these definitions outside of
code testing and benchmarking the kernel.
Signed-off-by: Curtis Millar <curtis@curtism.me>
This implements the syscall that maps the kernel log buffer for debug
and bencharking and defines the constant used to reference the buffer.
The x86_64 kernel log buffer is stored in the page directory used for
the kernel devices in the entry after the one used for the kernel device
page table.
Signed-off-by: Curtis Millar <curtis@curtism.me>
This removes the explicit CMake configuration for the kernel log buffer
and replaces it with a #define that is enabled for the required
configurations.
Signed-off-by: Curtis Millar <curtis@curtism.me>
The kernel connects ASID used in MMU and context banks used in
SMMU, and conducts TLB invalidation on context banks if a page
entry is invalidated from MMU is also used in SMMU.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Providing support to delete stream ID caps and remove any assigned
context banks to deleted stream ID caps.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Providing system calls on stream ID caps that unbinds its
context banks. Any future transaction using this stream ID
will result on faluts.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Providing a system call that removes an assigned vspace root from its
context bank. This operation causes the context bank being disabled
as it does not have a valid vspace root after the unassignment.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
The mapped attributes in both context bank and stream ID caps
are reundant for maintaining the semantics on those caps.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Providing system calls for conducting TLB invalidation operations
on all TLB entries or entries in a context bank.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Providing system calls that binds context banks to stream IDs.
Once the stream ID is bound, the transaction using that SID is
enabled.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Supporting user-level applications to assign vsapce root to context
banks through system calls. This commit also configures the context
bank according to stage 1 or stage 2 requirement.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Providing system calls on stream ID control cap and context bank
control cap for creating stream ID and context bank caps.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Adding the master control caps that are used to create transaction
and context banks caps. This commit includes the internal kernel
structure that required to manage any created transaction and
context bank caps.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
This renames the RISCV PLIC driver file hifive.h to riscv_plic0.h to
better reflect the fact that the driver could be used for a number of
platforms that use the PLIC used by SiFive and SiFive derived platforms.
Signed-off-by: Jesse Millwood <jesse.millwood@dornerworks.com>
reply_unlink takes a reply and remove the link between that reply
and its tcb. This link always exists at the call site and the tcb
information is always avaialble, or can be made available.
This commit adds this tcb as an extra argument to aid varification.
Signed-off-by: Miki Tanaka <miki.tanaka@data61.csiro.au>
- This commit largely copies the ARM way of handling
device tree blobs on to RISC-V, as they work pretty
similarly.
Signed-off-by: Michael Yoo <Michael.Yoo@data61.csiro.au>
A previous commit produced some build errors, since it converted the
`REFILL_HEAD` and `REFILL_TAIL` macros to functions returning
`refill_t`, and the results were used as lvalues. This commit returns
pointers instead, and also converts `REFILL_INDEX` to a function.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
SimplExportAndRefine can't handle the level of pointer arithmetic being
performed by `REFILL_INDEX` if it's literally inlined into a function,
however it *can* handle that arithmetic if it's in a separate function.
Signed-off-by: Edward Pierzchalski <ed.pierzchalski@data61.csiro.au>
The base pointer is wrong, and it creates some nasty corruption down the
line (only affects debug builds).
Signed-off-by: Sylvain Gauthier <sylvain.gauthier@data61.csiro.au>
The current state of MCS seL4 verification makes use of an invariant
that whenever the scheduler action is set to "resume current thread"
the current thread and the current sc are bound together. Since
maybeReturnSchedContext may unbind a thread from a scheduling context,
it should perform a check on whether it is unbinding from the current
thread, and in that case call rescheduleRequired which will (among
other things) change the scheduler action.
Signed-off-by: Mitchell Buckley <mitchell.buckley@data61.csiro.au>
If a thread is running on the SchedContext of it's bound notification,
when it next does a blocking recv/wait operation on an ep the SC is
removed. This allows the thread to return to being a passive thread to
receive the next notification or ep message.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
The capacity does not need to be passed as an argument to
refill_check_budget as all information that it was being used for can be
dertermined from the usage directly.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
We need to bound the time the user provides to configure scheduling
contexts to avoid malicious or erraneous overflows of the scheduling
math. Make the max period/budget 1 hour.
1 hour is sufficiently small that it will fit in a 32-bit error message.
1 week is sufficiently small for 64-bit platforms.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
Special debug variables that were previously stored at the end of the
tcb_t struct often cause the struct to get too large for the power-of-2
sized untyped object definition. This change moves these variables into
a new structure named debug_tcb_t that is located between the TCB CNode
and the tcb_t struct within a tcb kernel object. Because tcb_t needs to
be stored on a power-of-2 aligned boundary and the TCB CNode only
contains < 5 slots, there is easily > 512 bytes of unused data in every
tcb object. The kernel verification needs to be sure that objects don't
overlap in memory and so this space can't be easily used in a release
build at the moment, but for debug configurations using it shouldn't be
an issue.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
For each thread also track number of times scheduled, number of kernel
entries and amount of cycles spent inside the kernel. Also add
core-wide totals for each.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
Change benchmark_track_reset_utilisation to take a tcb object parameter
so that the function is more widely applicable.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
Create per-node global definitions for utilization variables.
This enables the tracking to more cleanly work on SMP configurations.
As resetting and starting the counters via SysBenchmarkResetLog only
updates the counters of the current thread and idle thread on the
current node it was not possible to accurately record utilization
statistics across multiple nodes. Now each node can have its tracking
independently started, stopped and queried. It is possible to add
additional syscalls in the future for doing this for all nodes in a
single syscall.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
