This makes all daigrams have their first address at the end of the
diagram and their last address at the start of the diagram.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
kernelBase was used inconsistently between different architectures to
refer to the either of the first kernel address or the first address of
the mappings of the kernel ELF region specifically.
These have been replaced with more consistent use of constants
explicitly describing which region is being referenced.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Each architecture now only needs to describe the bounds of the three
memory regions: the 1:1 mapped physical memory region, the kernel ELF
region (which may or may not overlap the physical memory region) and the
device / kernel page table region.
The physical base address of the 1:1 mapped physcial memory region and
the kernel ELF region must also be specified.
The top of user addressable memory (where in the same virtual address
space as the kernel) is defined by USER_TOP.
The physic memory virtual mapping is described by PPTR_BASE and
PPTR_TOP. The base physical memory address is PADDR_BASE and is the
physical address used to map PPTR_BASE.
Don't use kernelBase when referring to the base of the 1:1 mapped
physical memory window.
The kernel ELF virtual address region is described by KERNEL_ELF_BASE
and extends until the virtual address of the symbol `ki_end` which is
created by the linker. KERNEL_ELF_PADDR_BASE is the base address of
the physical memory region used to map the kernel and is the address to
which KERNEL_ELF_BASE maps.
KERNEL_ELF_BASE and KERNEL_ELF_PADDR_BASE do not need to be aligned to a
page size boundary as they are approriately truncated during boot by the
`map_kernel_window` function.
KDEV_BASE describes the base virtual address of the kernel device region
and the region is assumed to extend to the end of virtual memory.
Note: The offset between PPTR_BASE and PADDR_BASE is used to translate
the virtual address of all untyped objects to physical addresses. This
includes device untyped objects or frame objects where the virtual
address does not fall within the 1:1 mapped physical memory region.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Adapted musl printf implementation using our output abstraction.
Floating point specifiers are not supported in this adaptation.
Modified the code to also match our style and make it
less unnecessarily complex.
Signed-off-by: Saer Debel <saer.debel@data61.csiro.au>
Verification requires packed C structures for reasoning. The C parser
assumes uint64_t (unsigned long long) has 8-byte alignment, thus size of
struct vcpu should be a multiple of 8. As this was not the case, we add
an extra word_t (4 bytes) for padding.
This type of manual padding is naturally fragile and will break as soon
as any field of struct vcpu changes in size by < 8 bytes.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
This register is visible to software executing at PL0 but not writeable.
Storing it in the VCPU context required custom save/restore handling as
it had to be explicitly handled when switching from a VCPU thread to a
non-VCPU thread so that it didn't become a channel. It is possible to
now update this register via seL4_TCB_WriteRegisters for software
executing at PL0.
This also fixes a bug where if a vcpu-thread is switched for a
non-vcpu-thread and then switched to a different vcpu-thread the
original vcpu-thread's copy of this register will get set to 0.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
This should not change behaviour, but makes sure we replicate the test
setup more precisely.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
The FPU enable/disable state is cached for all architectures, so
the RV64 FPU code is updated accordingly.
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
The removed while loop in ipi_send_target can cause a deadlock, if
the target of an IPI remote call enters handleIPI through the
clh_is_ipi_pending path in smp/lock.h.
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
If a TCB is being migrated to another core and it is the current
FPU owner, we reset the FPU owner to NULL.
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
When FPU is off, we first assume an illegal instruction fault
is triggered by an FPU access and retry the instruction after
switching the FPU owner. Otherwise, we handle the illegal
instruction fault.
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
lazyFPURestore is call during kernel exits. Then, the FPU is
enabled or disabled accordingly by chaning the SSTATUS
of the current thread. The SSTATUS will be written to the
physical SSTATUS CSR, and thus the FPU accesses will be
enabled or disabled.
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
These functions are called by the arch-independent functions
to save and restore FPU state lazily.
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
The F and D extensions are enabled for RV64 when KernelHaveFPU
is enabled. Note that we still use the lp64 abi: no floating-point
arguments will be passed in registers
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Two options, KernelRiscvExtD and KernelRiscvExtF, are added to
represent the D and F floating-point extensions. KernelHaveFPU
is enabled when the floating-point extensions are enabled.
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
This changes the semantics if `isBlocked` to not include the 'inactive'
state when it returns true. The old semantics for isBlocked are provided
by `isStopped`.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Every SC in the system must be configured based on the actual core on
which it will run and all time comparisons for that SC must be made
relative to that core.
When creating SCs for the system idle threads those SCs must be
configured for their target cores.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
All time for an SC should be relative to its assigned core. Any
operations which may occur on an SC on a remote core must explicitly
refer to that core.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
The starting and ready times for any SC should be relative to the core
on which the SC is running rather than the current core.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
When attempting to remap a frame, and we find a page table in the slot
we are intending to use, return DeleteFirst to the user, to match
verification specs.
This check is redundant, as lookupPTSlot does not stop on page table
PTEs.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
seL4_IllegalOperation is not the appropriate error for attempting to
supply a mismatching vaddr for a frame remap. Return
seL4_InvalidArgument with the corresponding argument number.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
In decodeRISCVFrameInvocation, in the RISCVPageMap case doing a remap,
the ASID check should check the ASID of the frame cap against the ASID
of the vspace. Currently it checks the ASID of the vspace against the
ASID of the vspace, which always succeeds.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
The thread_control_flag enum which defines which arguments should be
used to reconfigure the TCB should also be split into two sets of flags
as they are now applied to two different functions.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This changes the order in MCS of ThreadControlSched:
1. Bind the fault handler
2. Set priorities
3. Bind or unbind scheduling contexts
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This ensures that verification are not required to prove problematic
combinations of updates to a TCB that aren't even permitted by the API.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Aligning the order of setMR writes to the enum order avoids having
to prove that the operations commute.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
Sequences of memory writes that correspond to one atomic spec operation
are time consuming in the proof. This commit refactors two of these to
make verification smoother. It also sets the (unused) mapped address of
top-level PageTableCaps to 0 as expected in the proofs.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
In decodeRISCVMMUInvocation, in the asid_pool_cap case, the first extra
cap is supplied by the user. Before asking whether the page table cap is
mapped, we should check it is a page table cap.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
The basic model of seL4 system calls is decode+perform. To be a
refinement of higher-level models, we cannot in a decode decide that
everything is fine, but we will do nothing.
In this case, we need to ensure the page table being unmapped is not a
top-level page table, by looking up the ASID. A page table that isn't
mapped does not have a stored ASID. performPageTableInvocationUnmap is
capable of handling this and there is no need to early-exit from
decodeRISCVPageTableInvocation.
We proceed with performing an unmap on a non-mapped page table
regardless, and only check for being a top-level page table in the
mapped case.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
Previously, it was possible in decodeRISCVFrameInvocation for the rwx
rights of the new PTE to become 000 after masking with cap rights. This
would turn the frame PTE into a page table PTE instead, and allow the
user to create almost arbitrary mappings, including to kernel data and
code. The defect was discovered in the C verification of the RISC-V
port.
This commit changes the PTE to an invalid PTE in that situation, which
has the same effect (faulting when accessed) as mapping a PTE without
rights has on the other supported architectures.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
The function getPPtrFromHWPTE is not applicable to invalid PTEs, so
this commit refactors the loop such that the the access is guaranteed
to be guarded by the corresponding isPTEPageTable check.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
