sel4 / docs Goto Github PK
View Code? Open in Web Editor NEWThis is the source of the seL4 docs.
Home Page: https://docs.sel4.systems
This is the source of the seL4 docs.
Home Page: https://docs.sel4.systems
The kernel compiles into about 9 k ARM instructions."
In terms of executable code size, on the 64-bit RISC-V architecture, the single-core kernel compiles into about 138 KiB. Its RAM size is about 162 KiB, which includes code, static data and the stack. Meta-data for usermode processes, incl. address spaces (page tables), thread-control blocks, capability storage etc, will add to this. (But note that in seL4โs memory-management model, such dynamic memory must be supplied to the kernel by usermode code.)
138 KiB is about 47 K RISC-V instructions, depending on the effectiveness of compression. Is RISC-V that poorly suited (no bitfield instructions, etc) to seL4 or if not what changed since 2016? So I built the spike/riscv64 kernel.
The default build following the Docker quickstart instructions with minimal changes for RISC-V (use the user_sel4-riscv
Makefile target, change stack
to sudo
in the Makefile because the riscv image does not have stack, and configure with -DPLATFORM=spike
) produces a 910KiB kernel.elf
, unstripped. The size
command reports 141KiB of text, very close to the reported number, increasing to 165 KiB including bss and data; I think this is where the numbers came from.
Disassembling and counting gives 20442 instructions occupying 60144 bytes - still a significant apparent regression, but in significant disagreement with the size
output. The size output matches the sum of the length of .boot
, .text
, .srodata
, and .rodata
; .boot
in its entirety is flagged in a text section, and because of the placement of the alignment, the full 64KiB alignment of .text
is counted against the size of .boot
.
Adjusting the linker script to separate .boot.text and .boot.data and moving the alignment outside of either results in a size
measurement of 90 KiB "text" (still includes rodata) and 115 KiB total.
The 64KiB alignment might be a fossil of ARM's large frames; reducing it to 4KiB shrinks the kernel binary by 48 KiB and does not appear to affect sel4test (this does not affect runtime memory use since it's all returned as an untyped).
The bigger problem is that this is a debug build. (For a competitor, this is a listed "benchmarking crime"). The rodata is mostly string error messages.
A -DRELEASE=TRUE
build has 14683 instructions (3614 in .boot.text, 11069 in .text) occupying 40952 (10146, 30806) bytes.
The total size of the load image as reported by objdump -p
is 46 KiB text and initialized data, 69 KiB including bss (of which 12 KiB is returned as boot memory) This is within a plausible ballpark of the 2016 numbers.
Links for patches or binaries for setting up a sabre u-boot image initially return 404 and only work after waiting a short while:
They 404'd initially, and then started resolving once I was writing up this issue.
I think there's a typo error on the "IA32 Example" where it says:
../init-build.sh -DPLATFORM=ia32 -DRELEASE=TRUE -DSIMULATION=TRUE
should say:
../../init-build.sh -DPLATFORM=ia32 -DRELEASE=TRUE -DSIMULATION=TRUE
It's not a problem at all, but if you are copy-pasting commands it breaks a bit the "magic" of the "user experience" :-)
The more things we can try of seL4, the smoother things work, the more addictive it becomes.
I stumbled upon https://docs.sel4.systems/Status through Google. I haven't been able to find this page any other way. Doesn't seem to be in this repository anywhere. The page itself looks pretty outdated and was probably left over in the process of moving stuff around or something like that.
I'd try remove it myself but I don't know how to and most likely don't have access to do so.
In the big list of devices, I think having a column for simulation supported
would be sensible. When starting to tinker, quickly finding out which platform has simulation support is good. Some (most!) of the hardware pages state this individually, but not all are clear on that. For example the Sabre Lite page contains the following phrase in the code example
# If your target binaries can be executed in an emulator/simulator, and if
# our build system happens to support that target emulator, then this script
# might work for you:
Now below, it says:
If you plan to use the ./simulate script, please be sure to add the -DSIMULATION=1 argument when running cmake.
That does not really confirm whether this target has support for simulation, or whether this is generic information on the state of affairs on simulation. Having it all in the overview list once would greatly help to quickly pick a desirable target.
Line 73 in e9e6283
Follow-up from seL4/ci-actions#185
The github CI actions in this repo should not try to deploy on forks, this will fail anyway. Especially, since this workflow is triggered regularly, the messages with errors can get really annoying after a while ;)
Follow-up from seL4/seL4#727
Document Pine64 Quartz64Board support and maintainer. Or list this an unmaintained and mention at least that a PR/branch exists with the changes.
It's not clear to me whether the page that lists supported platforms (https://docs.sel4.systems/Hardware/) is just for supported hardware or all platforms supported by seL4. E.g on RISC-V the Spike is listed but it's a purely simulated platform (to my knowledge). The page is also not named consistently, the URL is "Hardware", the title is "Supported Platforms" and the navigation bar has it listed as "Supported Hardware"
(This may wait for the Information Architecture feedback first)
The landing page has a nice overview but it's not clear that this is just a subset of the docsite content. We should make that clear.
The order and titles on the landing page and the submenus should be made consistent to avoid confusion. E.g.
The Grouping should be consistent; namely "The source code" appears in "Getting started" in the landing page but belongs to "Contributing" submenu
the "Roles" page appears in the landing page but not in the submenus. There's a question on location of this page versus having it on the website with the TSC information (see also issue 309 on website)
All the links from the tutorial section on the landing page are wrong, going to the same root Tutorials page (#206)
Can Sel4 be used to build an immutable system?
The link is here: https://docs.sel4.systems/Tutorials/mcs.html#getting-help
As discovered in #163, the docsite build is breaking with the default versions of ruby and bundler on Ubuntu 22.04.
We should update the dependencies such that they are more stable and at least work with both 20.04 and 22.04.
The RPi4 docs mention bootcode.bin
. However, the RaspberryPi documentation mentions that this file is not used on RPi4 and RPi5, so I would guess the file is inert. If that is the case, the seL4 docs should not propose to add it to the SD, that only confuses users (like me).
Line 44 in 796c552
https://github.com/SEL4PROJ/docs/blob/master/Hardware/Qemu/index.md needs to be updated to reflect current project structure and build system commands
The list on https://docs.sel4.systems/processes/release-process.html does not reflect reality:
I constructed my simple hello world project according to the first directory structure in your docs.
https://github.com/JonathonAnderson/hello-sel4
When I am in the build directory, I run the following command:
cmake -G Ninja -S ../ -DPLATFORM=x86_64 -DSIMULATION=TRUE
I receive the following output:
CMake Error at CMakeLists.txt:9 (include):
include could not find load file:
settings.cmake
-- The C compiler identification is GNU 9.2.1
-- Check for working C compiler: /usr/bin/cc
-- Check for working C compiler: /usr/bin/cc -- works
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Detecting C compile features
-- Detecting C compile features - done
-- The CXX compiler identification is GNU 9.2.1
-- Check for working CXX compiler: /usr/bin/c++
-- Check for working CXX compiler: /usr/bin/c++ -- works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- The ASM compiler identification is GNU
-- Found assembler: /usr/bin/cc
CMake Error at kernel/config.cmake:95 (include):
include could not find load file:
src/arch//config.cmake
Call Stack (most recent call first):
kernel/CMakeLists.txt:54 (include)
CMake Error at kernel/config.cmake:96 (include):
include could not find load file:
include//mode/config.cmake
Call Stack (most recent call first):
kernel/CMakeLists.txt:54 (include)
CMake Error at kernel/CMakeLists.txt:383 (add_custom_command):
add_custom_command Wrong syntax. A TARGET or OUTPUT must be specified.
-- CPIO test cpio_reproducible_flag PASSED
CMake Error at tools/elfloader-tool/CMakeLists.txt:295 (message):
no image start address computed for platform; use platform YAML file or
replace this diagnostic with a CMake custom command to generate a file ""
that hard-codes it; the same goes for ""
-- Configuring incomplete, errors occurred!
See also "/home/jonathon/hello/build/CMakeFiles/CMakeOutput.log".
I have tried the build on ubuntu, the version can be install on it is cmake 3.10.x. And another ppa is broken too (unable to find IP). Snap will fix this problem by:
snap install cmake --classic
The footer shows site modification and page modification dates, but it looks like they are always the same and might always just be when the site got last generated.
Potentially an unexpectedly recent jekyll version or similar.
See: https://github.com/seL4/docs/actions/runs/3520086041/jobs/5900677174
Liquid Exception: no implicit conversion of Hash into Integer in /home/runner/work/docs/docs/content_collections/_dependencies/l4v.md
------------------------------------------------
Jekyll 4.0.1 Please append `--trace` to the `build` command
for any additional information or backtrace.
------------------------------------------------
The minimum gcc version for building seL4 is 8 (see seL4/seL4#575 and seL4/seL4#574). This means that the currently described build host dependencies are not only out of date, but now insufficient, because Ubuntu 18 comes with gcc 7.5.
We should update the host dependencies to Ubuntu 20LTS and current Debian stable (bullseye) and document minimum gcc and clang versions.
The Arm VMs have been merged into other repos and the current doc site description is completely outdated, pointing to an archived repo.
It's not clear to me what exactly should replace it or how the description on the docsite should be merged, but it affects the following projects:
Looks like the branch 'pingerino-patch-2' got merged a while ago, if there is no reason to keep it around it should be deleted.
It talks about 2.0.x.xml
https://github.com/SEL4PROJ/docs/blob/master/Testing.md
For example:
https://docs.sel4.systems/Tutorials/capabilities.html
takes you to this page:
https://github.com/seL4/docs/edit/master/Tutorials/capabilities.md
Which just has:
{% include tutorial.md %}
It's not clear where the actual tutorial.md source is.
Makefile has:
GIT_REPOS:=$(shell (cd _data/projects && for i in `ls`; do cat $$i | ../../tools/get_repos.py ; done) | sort -u)
REPOSITORY_LIST = sel4 sel4-tutorials capdl
REPOSITORIES = $(GIT_REPOS:%=_repos/%)
But there doesn't appear to be an sel4-tutorials
repo available on github.
Hi,
I'm trying to build x86_64 example following instructions from "https://docs.sel4.systems/Hardware/IA32" and after "repo sync" I get lot of errors like:
Aborting
kernel/: leaving master; does not track upstream
error: kernel/: seL4.git checkout ed613d7d490be91f7f164ff98e09d9098de64d6e
error: Cannot checkout seL4.git
(...)
Aborting
projects/musllibc/: leaving master; does not track upstream
error: projects/musllibc/: musllibc.git checkout 9798aedbc3ee5fa3c1d7f788e9312df9203e7b0b
error: Cannot checkout musllibc.git
(...)
Aborting
projects/seL4_libs/: leaving master; does not track upstream
error: projects/seL4_libs/: seL4_libs.git checkout 043999f481d8f72f7993eb3d27f3cf3eb66b00a7
error: Cannot checkout seL4_libs.git
(...)
Aborting
projects/sel4runtime/: leaving master; does not track upstream
error: projects/sel4runtime/: sel4runtime.git checkout d935dd05da0cf959e9fd0140af913dc6fdaa0221
error: Cannot checkout sel4runtime.git
(...)
Aborting
projects/util_libs/: leaving master; does not track upstream
error: projects/util_libs/: util_libs.git checkout af6b18bd60e4f2e1a10ff1a1e687a46db02fa9db
error: Cannot checkout util_libs.git
(...)
Aborting
tools/seL4/: leaving master; does not track upstream
error: tools/seL4/: seL4_tools.git checkout df31d5a844993166c88c8a1ccce5dd42018a7296
error: Cannot checkout seL4_tools.git
Checking out: 100% (10/10), done in 0.576s
error: Unable to fully sync the tree
error: Checking out local projects failed.
Failing repos:
kernel
projects/musllibc
projects/seL4_libs
projects/sel4runtime
projects/util_libs
tools/seL4
Try re-running with "-j1 --fail-fast" to exit at the first error.
================================================================================
Repo command failed due to the following `SyncError` errors:
seL4.git checkout ed613d7d490be91f7f164ff98e09d9098de64d6e
musllibc.git checkout 9798aedbc3ee5fa3c1d7f788e9312df9203e7b0b
seL4_libs.git checkout 043999f481d8f72f7993eb3d27f3cf3eb66b00a7
sel4runtime.git checkout d935dd05da0cf959e9fd0140af913dc6fdaa0221
util_libs.git checkout af6b18bd60e4f2e1a10ff1a1e687a46db02fa9db
+1 additional errors...
I have no idea how to deal with this... I'm just following instructions... Any hint?
Edited: I missed this "Checkout the sel4test project using repo as per seL4Test". Now everything is ok, I was able to build a real hardware image for x86_64.
I've noticed some system calls that appear in the reference manual, don't appear on the API reference page (https://docs.sel4.systems/projects/sel4/api-doc.html).
Specifically:
seL4_NBSendRecv
seL4_NBSendWait
There may be more but those are the ones I've noticed so far.
Follow-up from the remark form @lsf37 in today's hangout call. The pages of with the contribution guidelines could be merged into one page. I've just stumbled over these pages
processes/contributing.md
processes/doc-contributing.md
On an Ubuntu 18.04 system, unless python3 dependencies have been installed specifically using pip3 (instead of pip), when the system has both python 2 and python 3 installed, the 'init' script of the hello-world tutorial seems to fail (with missing module errors)
The HostDependencies page instructs that both versions of python-dev and python3-dev be installed (and implicitly thus, python(2) and python3). However, the rest of the page instructs python dependencies to be installed with 'pip' (and not pip3).
This apparently causes a problem when the tutorial init scripts try to run, as this appears in an included script ( seL4-tutorials-manifest/projects/sel4-tutorials/common.py )
#!/usr/bin/env python3
Possible solution:
Once all the commands from HostDependencies were re-run with "pip3" substituted for "pip" (and additionally, the two pip install commands in Tutorials/#get-the-code likewise with pip3 substituted), the tutorial init scripts seemed to run to successful completion
xxd
is needed in elfloader-tool
in some configs. See also seL4/seL4-CAmkES-L4v-dockerfiles#70
This patch does not apply at all to the current structure found over at https://github.com/Xilinx/u-boot-xlnx
Follow-up from seL4/seL4#829
Document Avnet MaaXBoard Board support and maintainer. Or list this as unmaintained and mention at least that a PR/branch exists with the changes.
Hello, I've been having an issue with running sel4test according to the updated documentation, and shared my findings on the sel4 Discourse.
Expected Behavior: config.txt
without the dtoverlay=disable-bt
allows u-boot.bin
to load on Raspberry Pi 4B 4GB.
Actual Behavior: u-boot.bin
does not load.
Solution: Re-adding the line dtoverlay=disable-bt
causes u-boot
to load and get to the next phase, which is running sel4test
on the PI 4B
Secondary issue:
Expected Behavior: Running sel4test
with go 0x10000000
shows the testing over UART on serial0
Actual Behavior: No output is observed
Solution: Implementing the kernel patch mentioned in this revision of the documentation yields the sel4test
outputting as expected and succeeding all tests over the UART on serial0
I'd be more than happy to continue discussion, contribute a PR to the documentation or kernel if necessary. Thank you!
Is it still not supported as per documentation? PSCI is supported in elfloader, and Amlogic S905 uses PSCI. Short test with setting KernelMaxNumNodes
to 4 and specifying affinity in camkes assembly file worked. Not sure how to get the current cpu from the thread though, getcpu syscall seems to be not implemented
The current HostDependencies document advises the use of Ubuntu 18.04 in order to have an appropriately current version of CMake.
Ubuntu 18.04 's normal, out-of-the-box repositories (used by apt-get) install version 3.10.2
(at least as of the current date, July 30, 2019)
However, this version seems to be insufficient for building se4L4test. Running init-build.sh:
...
CMake Error at projects/sel4runtime/CMakeLists.txt:20 (cmake_minimum_required):
CMake 3.12.0 or higher is required. You are running version 3.10.2
I noticed that the entry level documentation pages contain several dead links and the link to the latest manual leads to a manual for v11, not v12 which appears to be the latest release
According to the RaspberryPI documentation the fixup*.dat
are matched pairs together with the start*.elf
files. Therefore I conclude that if start4.elf
is required (which is explicitly mentioned in the seL4 docs on the RPi4), then the corresponding fixup4.dat
is also required. This should be documented in the table marked below:
Lines 41 to 50 in 796c552
(This may wait for the Information Architecture feedback first)
All the links from the tutorial section on the landing page are wrong, going to the same root Tutorials page
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.