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>
Fix tk1 smmu cmake config variables.
Fix platforn_gen for tk1.
Add separate hardware.yml for tk1.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
ndks_boot, rootserver and rootserver_mem don't contain any non-zero init
values and can be moved to bss so they don't take up space in the ELF.
ndks_boot contains a sparse struct that is > 4MiB on x86_64 and so this
change allows the x86_64 ELF to return to < 200KiB.
Signed-off-by: Kent McLeod <kent@kry10.com>
A slot in the top level VSpace page table is used to hold the number of
SMMUv2 ContextBanks that are assigned to a VSpace. This means a
reduction of available virtual addresses at userlevel as the slot cannot
be used for holding regular mappings.
Signed-off-by: Kent McLeod <kent@kry10.com>
Remove unused cases and add break in switch statements.
Add conditions to sel4arch.xml.
Change guard in capdl printing to correct TK1_SMMU.
Set KernelArmSMMU default to off.
Add types to aarch32 syscall_stub_gen.py.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
- Add a chapter in the Hardware I/O Section
- Link API documentation back to chapter.
Co-authored-by: Qian Ge <Qian.Ge@data61.csiro.au>
Signed-off-by: Kent McLeod <kent@kry10.com>
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 the two control caps: the
stream ID control cap and the context bank control cap.
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>
The initial thread's CNode guard size is calculated so that the CNode
resolves the number of bits in the architecture word size.
Signed-off-by: Jimmy Brush <code@jimmah.com>
Allow rockpro64 to be built with MCS. Sets the kernel WCET to 10u.
Sel4test passes when running on a pinebook pro.
CLK_MAGIC and CLK_SHIFT were not set as this platform is not enabled for
32-bit arm.
Sel4test was built and executed using this procedure:
mkdir sel4test
cd sel4test
repo init -u https://github.com/seL4/sel4test-manifest.git \
-b refs/tags/11.0.0
repo sync
cd kernel
git checkout master
cd ../tools/seL4
git checkout master
cd ../..
mkdir build
cd build
../init-build.sh -DPLATFORM=rockpro64 -DSIMULATION=false -DSMP=on \
-DNUM_NODES=6 -DMCS=on -DLibUtilsDefaultZfLogLevel=0
ninja
cd images
../../tools/seL4/cmake-tool/helpers/make-uimage \
/usr/bin/aarch64-linux-gnu-objcopy \
../elfloader/elfloader \
arm64 \
sel4test-driver-image-arm-rockpro64-uboot
Note that sel4test was built from 11.0.0 with a master kernel and
seL4-tools due to the issue at seL4/sel4test#25.
Signed-off-by: Jimmy Brush <code@jimmah.com>
Add error messages for seL4_DebugSnapshot for platforms that are
not currently supported by capDL Kernel Printing
Signed-off-by: Jingyao Zhou <Jingyao.Zhou@data61.csiro.au>
The RISC-V ISA manual requires supervisor code to execute a dummy sc
instruction to clear reservations "during a preemptive context switch".
Failure to do so allows a lr/sc sequence in one user thread to be
interleaved with a non-atomic write to the same address in another
thread without causing the sc to fail.
This is not necessary on the fastpath for functional correctness since
user threads do not perform ipc in the middle of lr/sc sequences. I
believe it is not needed there for dataflow reasons either, as the
reservation can be considered a message register (although impossible to
use gainfully on most implementations).
This is likely unobservable for Rocket-based implementations as they
time out reservations after at most 80 cycles and there is no path
through the scheduler in less than that; it could be an issue for Ariane
which does not appear to time out reservations.
Signed-off-by: Stefan O'Rear <sorear@fastmail.com>
- 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>
