The C semantics used by our binary correctness mechanism understand
uninitialised variables as non-deterministic assignment. The translation
to a simplified form suitable for further analysis occurs on a
per-function basis which does not support non-determinism. This means
uninitialised local variables must not be used for decision making in
any function.
In infer_cpu_gic_id, 'target' is initialised in the loop, which will not
be executed if nirqs <= 0, after which the uninitialised 'target' is
examined. We address this by initialising 'target' to 0.
The overall C code is still safe, as infer_cpu_gic_id is only called
once in dist_init, where 0 < nirqs.
The CPU target ID can be calculated from the GIC by reading the
interrupt target registers for private interrupts that are RO and are
guaranteed to return the current target ID.
Specifically, what happens when a TCB is bound to a notification,
and that notification gets signaled while in the TCB is in the middle
of waiting during seL4_Call's receive phase.
The TLS_BASE stored in the globals frame needs to refer to the TLS_BASE
of the current thread and so must be maintained across all context
switches. (This was only being maintained on the slow path).
So far this is only implemented for the GIC, which most of our platforms
use. Error if this invocation is made on another platform, and guard
calls to the trigger function if it is not supported.
- renamed an architecture label so that it begins with ARM.
- changed setIRQTrigger so that it takes a boolean value instead of an int.
- Arch_decodeIRQControlInvocation converts the second argument (trigger)
to a boolean immediately.
Add a new invocation which allows an irq handler capability to be
obtained with a specific trigger method (edge or level). Obtaining
this capability modifies the GIC state.
While the RISC-V ISA says to that a VMFENCE before a write to the
satp may be necessary, vm faults occur with this ordering when
running on the Rocket Chip. Placing the VMFENCE after the satp write
resolves these faults.
This is also the ordering used in the RISC-V port of Linux when
switching MMU contexts.
Change-Id: I1ec794651d080a5e7a987fa8b2062dc01daeb683
This commit adds a cmake variable for the Clock Frequency used
in the rdtime instruction, which is used for the scheduling tick.
The resetTimer and initTimer functions were updated to use a
calculated cycle count, which is based on the clock frequency and
the timer tick variable.
Change-Id: I130013003ed2c4aec8d5d294624413ee05477d58
Even if we are building for x86_64, we still need a cross compiler to be able to
build ELF binaries.
OS X cross compilers can be installed via brew from here:
https://github.com/SergioBenitez/homebrew-osxct
add_config_library for sel4 adds sel4_Gen custom target. Having two targets with
names that only differ in case results in strange build problems on systems with
case insensitive file systems (I've seen it only on OS X but I assume Win is
affected too).
The stack is loaded on the preceding lines of code from
TPIDRPRW, regardless of SMP being enabled or not. Loading ksCurThread
into r7 is from the previous approach of loading the kernel stack and is
not longer used.
Modified the behaviour of the EXACT_INPUT option within the
CPPFile helper function. Now named EXACT_NAME, the option
copies the input file to a temporary file. The name of the
temporary file is also passed in by the caller. This
step in necessary in getting the CPP step to correctly
depend on the targets given by the caller
(through EXTRA_DEPS). Also updated the CPP generation of the
kernel_all.i file to reflect the change.
Added an "ignore" argument to the circular_includes script. This
allows the caller to specify files for the script to ignore when
it parses the source file. Rather than creating a special
ignore case for "kernel_all.c" in the script itself, the user
parses the file as an argument (plus others if needed). Updated
the kernels cmake file to reflect the change.
This patch moves the 'outer' chunk of lockTLBEntry into C rather
than handwritten assembly. The outer chunk accesses a global
counter and does arithmetic. The inner chunk (lockTLBEntryCritical)
writes to the registers, must be specially aligned, and is generally
special.
The change reduces unnecessary handwritten assembly, and also avoids
a special case that was problematic for binary verification.
It has become clear that the 'packed' GCC attribute affects the
memory semantics of C in a way that the verification tools do not
understand. The bootinfo types are used by kernel boot code (not
currently verified, but covered by binary verification) and should
not use this attribute.
This is a source-compatible but not binary-compatible change.
Added small bash scripts to run astyle, pylint and xmllint
checks over the kernel source. These style checks were ported
from the old Make build system.
Leaves the last entry in the top level page table free so that it can be used for mapping
devices in the future. This moves the kernel image down to the second last entry in the
top level page table. Leaving the last entry in the top level page table also matches the
rv64 design.
Only a single level 2 page table is now used for mapping the kernel image so this simplifies
the state data to only allocate a single PT and removes the now out of date description.
