This commit adds support for building the seL4 kernel, loader, monitor,
and libmicrokit with LLVM (Clang, LLVM and ld.lld). Passing --llvm
should instruct the tool to build everything with with LLVM.
Clang/RISC-V don't implement or need -mstrict-align
Also fix a trivial error adding single quotes within a string.
Signed-off-by: Hesham Almatary <heshamalmatary@capabilitieslimited.co.uk>
This would otherwise give the warning
platform maaxboard supports multiple architectures, none was given
defaulting to: aarch64
on platforms which support multiple architectures, for instance, the
maaxboard which can be built for aarch64 and aarch32. This seems to have
been fine because the first option is always the 64-bit option, but this
is probably unlikely to be guaranteed.
For the CMake Builds for sel4test et al, this is set in
cmake-tool/helpers/application_settings.cmake.
Signed-off-by: julia <git.ts@trainwit.ch>
Previously I did not turn this option on by default because
I thought it would make the kernel proofs not apply anymore.
In reality this is only true really when a user makes use
of the SMC feature. Most users probably will never have to enable
it and the ones that that do will no longer have to patch Microkit
to enable it.
I've added a warning about using SMC calls in the manual to make users
aware of the implications of using this feature.
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
With the changes to seL4 regarding reserving the SBI region
properly [1] it means we can no longer use 0x80200000
as a loader link address for this platform.
[1]: cf3a64b44c
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
One of the things the tool has to do is emulate the kernel boot process,
this involves getting a layout of all memory and putting into two
categories, 'device' memory and 'normal' memory as defined by the
kernel.
The way we do this currently is by looking at certain symbols in the
kernel ELF that encode this information. This doesn't work well when
the compiler decides to optimise that symbol out and instead embed
the information directly into where it's being used in the kernel code.
So, instead we use the `platform_gen.json` file that gets generated by
the kernel build system to get the same information.
There should be no difference at all in terms of what the tool actually
spits out at the end, it just means that the process of doing this
emulation is less fragile.
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
The current way examples are done in the repository and
shipped in the SDK does not make sense when you have many
boards in my opinion so this restructure moves examples that
are not specific to any particular platform (e.g hello world)
to be generic to every platform supported by Microkit.
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
People tend to rename the SDK etc and so it helps to have
this file so they know what version they're on.
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
Instead of hard-coding invocation numbers, we now
get them from a file generated by the seL4 kernel
build.
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
We will always have an official, 'supported' C toolchain but it has
become apparent that:
1. GCC toolchain triples are a complete, inconsistent mess.
2. People may have vendored toolchains that they must use when compiling
from source.
Therefore, we introduce arguments to the build_sdk.py script that allows
overriding the default prefixes.
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
Rust's cross-compiling is limited so this only works from
a Linux host, if you're on macOS it won't work.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
This will be used by CI for builds on each commit of Microkit,
which will be useful for getting prebuillt SDKs between official
releases.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
It was seen on larger Microkit systems that the loader data was
overlapping with the code for the loader itself when the loader
attempted to copy the data to the appropriate location before
jumping to seL4 and starting the system.
I believe the root cause of this problem is not gone and will involve
changing the tool to be smarter with how it allocates physical memory,
my current attempts to do so lead to other issues. I'll have to make a
follow up fix to prevent this from happening again, but for now this
will allow users of the MaaXBoard to run larger Microkit systems.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
This changes the behaviour of virtual machines to see the
architectural timer change even when it is not running.
I do not understand why this option applies to all vCPUs
in the kernel, instead of being behaviour that depends on
the configuration of a particular vCPU.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
We are compiling libmicrokit with hardware floating extensions
which means that user-code must also be compiled with hardware
floating extensions.
This meant that before this patch user programs that make use of
floating point instructions would crash as the kernel has the FPU
disabled.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
The manual says that the loader should not print on release mode,
so this patch just makes that true.
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
This patch adds a new configuration for each platform called
'benchmark'.
The purpose of this is to enable Microkit systems to leverage the
benchmark configuration of seL4 that tracks things like kernel entries
and CPU utilisation. This also exports the PMU to user-space.
This is not ideal, which is why RFC-16 exists.
However, we need to be able to do benchmarking for projects like the
seL4 Device Driver Framework in the meantime. It may take a while
to get the RFC approved and implemented which is why we are adding
this 'temporary' configuration.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
The QEMU virt platform does not have a timer and so the only
way to get a timer driver working is to use the architectural
timer.
Exporting the architectural timer to user-space can be problematic
as it means any user-space program can access it, including ones
you may not trust. However, as this platform is only intended for
development purposes, this is not an issue.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
Change the permissions to be owner-writeable. This means we no
longer need `sudo` to move or remove the SDK after unpacking the
tar.
I can't know the original reason for doing this, but I imagine it
was to prevent users from accidentally removing the SDK unless they
really wanted to.
However, the user-experience of this is poor and in not worth it in
my opinion.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
This PR adds support for running seL4 in hypervisor mode as well as
a new 'virtual machine' abstraction.
This commit message says 'initial support' as features such as
multi-vCPU/core support for VMs are not yet implemented. However,
with this patch, we can run guest operating systems such as Linux
on a Microkit system.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
This commit rewrites the entire Microkit tool from Python to Rust.
This is was done for the following reasons:
* The current tool was difficult to build from source. It took too long,
did not have any cache for rebuilds, and sometimes would not reliably
build/link with musl.
* While perhaps not as extensive as C, Rust does have some verification
tooling surrounding it, meaning it is possible for us to verify the
Microkit tool in the future. Although at this time there are no
concrete plans to verify the tool.
This rewrite, while not significantly reducing our dependencies in
general, does improve the situation. We are no longer dependent on
pyoxidizer, which was causing most of the issues with the tool.
We introduce a dependency on the Rust toolchain. The tool itself has
two dependencies (for XML parsing). No other dependencies are needed,
and it was a conscious decision to re-invent the wheel where the Rust
standard library was lacking (compared to the Python standard library).
The other programming languages considered for the rewrite were Zig and
Go. While they both have their benefits and costs (as does Rust), they
were not chosen due to them not being in any other seL4 Foundation
supported projects meaning that it could have been difficult to continue
maintaining the tool in the future.
The main cost of rewriting the tool in Rust is that it has undoubtedly
become more complicated and harder to understand. This could potentially
result in a higher barrier to entry for contributors. However, most
contributions such as adding platform support will not need to touch the
tool.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
Hesham Almatary