sel4 / capdl Goto Github PK
View Code? Open in Web Editor NEWCapability Distribution Language tools for seL4
Home Page: https://sel4.systems
Capability Distribution Language tools for seL4
Home Page: https://sel4.systems
I'm trying to set the stack, but I get the following error
$ cd tools/capDL
$ make sandbox
stack setup
No information found for ghc-8.0.1.
Supported versions for OS key 'linux64-nopie': GhcVersion 8.0.2, GhcVersion 8.2.1, GhcVersion 8.2.2
Makefile:37: recipe for target 'sandbox' failed
make: *** [sandbox] Error 1
find_device_object
searches through the device untypeds, and then when it reaches the correct object, retypes a single page until the proper physical address is found. This isn't a huge deal on ARM platforms, where device objects are defined by the device tree. However, on x86, there exists a region of memory defined as device memory from the end of RAM to the PaddrUserTop value (1 << 47 on x86_64).
The problem with this setup is that x86 processor cards can seemingly arbitrarily place MMIO regions into this memory. For example, this is a snippet of a PCI scan for a COTS Ice Lake processor card:
Region 0: Memory at 20fffaf0000 (64-bit, non-prefetchable) [size=16K]
Region 0: Memory at 20fffaec000 (64-bit, non-prefetchable) [size=16K]
Region 0: Memory at 20fffae8000 (64-bit, non-prefetchable) [size=16K]
Region 0: Memory at 20fffae4000 (64-bit, non-prefetchable) [size=16K]
Trying to give one of these regions causes find_device_object
to take so long the system is unusable:
[[email protected]:817](mailto:[email protected]:817) Creating object vm0_mmio_frame_2267737452544 in slot 31572, from untyped 7b16...
[[email protected]:682](mailto:[email protected]:682) device frame/untyped, paddr = 0x20fffaf7000, size = 12 bits
[[email protected]:507](mailto:[email protected]:507)
[[email protected]:532](mailto:[email protected]:532) 8000000000 408000000000
In my case, it would take ~419 million calls to get to that memory. And it could even be worse, if the memory was even higher.
I'm not sure if I can release my code, but I was able to come up with a solution where I retyped Huge Pages instead of single pages. This reduced the time it took to find the proper physical address, but the whole function could use a look through to make things more optimized.
https://github.com/seL4/capdl/blob/master/capdl-loader-app/src/main.c#L502
I'm a but confused about what commit e08dbb4 added. Looking at
capdl/capdl-loader-app/include/capdl.h
Lines 169 to 185 in e082ee7
CONFIG_VTX
within a CONFIG_ARCH_ARM
block. Looks to me as if CDL_VCPU
is never declared on CONFIG_ARCH_X86
at all then?parse-capDL --dot ...
creates invalid dot file. Seems the problem is, that there are lines containing a quoted filename within a quoted string, which dot
can't process.
"frame_ticker_group_bin_0000" [label = "{<Object> frame_ticker_group_bin_0000 \n frame (64k, fill: [{0 65536 CDL_FrameFill_FileData "ticker_group_bin" 0}])}"];
The inner quotes must be escaped as \"
.
I'm not familiar with Haskell but I would think that it supports compiling static binaries. I tried to do so with stack build --fast --ghc-options '-optl-static'
and it resulted in:
Building all executables for `capDL-tool' once. After a successful build of all of them, only specified executables will be rebuilt.
capDL-tool> configure (exe)
Configuring capDL-tool-1.0.0.1...
capDL-tool> build (exe)
Preprocessing executable 'parse-capDL' for capDL-tool-1.0.0.1..
Building executable 'parse-capDL' for capDL-tool-1.0.0.1..
[ 1 of 17] Compiling CapDL.Matrix
[ 2 of 17] Compiling CapDL.Model
[ 3 of 17] Compiling CapDL.AST
[ 4 of 17] Compiling CapDL.ParserUtils
[ 5 of 17] Compiling CapDL.Parser
[ 6 of 17] Compiling CapDL.DumpParser
[ 7 of 17] Compiling CapDL.STCC
[ 8 of 17] Compiling CapDL.State
[ 9 of 17] Compiling CapDL.PrintUtils
[10 of 17] Compiling CapDL.PrintXml
[11 of 17] Compiling CapDL.PrintModel
[12 of 17] Compiling CapDL.PrintJSON
[13 of 17] Compiling CapDL.PrintDot
[14 of 17] Compiling CapDL.PrintC
[15 of 17] Compiling CapDL.PrintIsabelle
[16 of 17] Compiling CapDL.MakeModel
[17 of 17] Compiling Main
Linking .stack-work/dist/x86_64-linux/Cabal-3.6.3.0/build/parse-capDL/parse-capDL ...
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_cond_broadcast.o)(.note.stapsdt+0x14): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_cond_destroy.o)(.note.stapsdt+0x14): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_cond_init.o)(.note.stapsdt+0x14): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_cond_signal.o)(.note.stapsdt+0x14): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_cond_wait.o)(.note.stapsdt+0x14): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_cond_wait.o)(.note.stapsdt+0x60): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_cond_wait.o)(.note.stapsdt+0xac): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_join_common.o)(.note.stapsdt+0x14): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_join_common.o)(.note.stapsdt+0x5c): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_mutex_cond_lock.o)(.note.stapsdt+0x14): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_mutex_cond_lock.o)(.note.stapsdt+0x5c): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_mutex_cond_lock.o)(.note.stapsdt+0xa0): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_mutex_destroy.o)(.note.stapsdt+0x14): error: relocation refers to local symbol "" [1], which is defined in a discarded section
/usr/lib/gcc/x86_64-linux-gnu/12/../../../x86_64-linux-gnu/libc.a(pthread_mutex_init.o)(.note.stapsdt+0x14): error: relocation refers to local symbol "" [1], which is defined in a discarded section
collect2: error: ld returned 1 exit status
`gcc' failed in phase `Linker'. (Exit code: 1)
Error: [S-7282]
Stack failed to execute the build plan.
While executing the build plan, Stack encountered the following errors:
[S-7011]
While building package capDL-tool-1.0.0.1 (scroll up to its section to see the error) using:
/home/ivanv/.stack/setup-exe-cache/x86_64-linux/Cabal-simple_SvXsv1f__3.6.3.0_ghc-9.2.8 --verbose=1 --builddir=.stack-work/dist/x86_64-linux/Cabal-3.6.3.0 build exe:parse-capDL --ghc-options " -fdiagnostics-color=always"
Process exited with code: ExitFailure 1
If someone familiar with the tool or Haskell could help that would be great. I cannot find any documentation for building a static binary with stack.
I notice that in
capdl/python-capdl-tool/capdl/Object.py
Lines 375 to 395 in f7ef9ca
fault_ep_slot
in the capDL spec generated can be anything.
However, I notice in the capDL initialiser in this repository:
capdl/capdl-loader-app/src/main.c
Line 1044 in f7ef9ca
It is expecting that the fault endpoint is in a specific slot.
Is this a restriction of the initialiser itself or of CapDL in general?
do branch maintenance (update/delete):
I'm getting this warning when compiling a CAmkES system for RISC-V rv32 (spike):
Building C object .../capdl/capdl-loader-app/src/main.c.obj
.../capdl/capdl-loader-app/src/main.c: In function 'init_level_1':
.../capdl/capdl-loader-app/src/main.c:1565:51: warning: left shift count >= width of type [-Wshift-count-overflow]
1565 | uintptr_t base = level_1_base + (obj_slot << (CDL_PT_LEVEL_2_IndexBits + CDL_PT_LEVEL_3_IndexBits + seL4_PageBits));
| ^~
.../capdl/capdl-loader-app/src/main.c: In function 'init_level_0':
.../capdl/capdl-loader-app/src/main.c:1585:52: warning: left shift count >= width of type [-Wshift-count-overflow]
1585 | uintptr_t base = (level_0_base + obj_slot) << (CDL_PT_LEVEL_1_IndexBits + CDL_PT_LEVEL_2_IndexBits +
| ^~
The python-capdl-tool
uses the package nose
for running its (small) test suite. This package is now unmaintained, and as of python 3.10 does not work any more for python-capdl-tool
.
This issue is to replace nose
with something more recent such as pytest.
PR #30 is temporarily switching off testing on python 3.10, but this is a stop-gap only. As time goes on python >= 3.10 will become the default.
The capdl_spec.c file is generated by capDL-tool and is compiled into the capdl-loader-app program to define the system that the loader will load. The file is supposed to only be a C-language representation of the capDL spec for a particular system.
Currently, the header files required to compile this spec file introduces dependencies on a C library, and libraries from seL4/util_libs and seL4/sel4_libs including libsel4utils and libutils (and any libraries they depend on).
The spec itself doesn't inherently require any type definitions other than what's provided by libsel4, and so it shouldn't require these additional dependencies.
The file generated by the capDL-tool only has the following header file dependencies:
capdl_spec.h
:
#include <capdl.h>
#include <sel4/sel4.h>
capdl.h
:
#include <autoconf.h>
#include <capdl_loader_app/gen_config.h>
#include <sel4/types.h>
// These should all be removed
#include <sel4utils/mapping.h>
#include <limits.h>
#include <stdbool.h>
#include <stdlib.h>
#include <utils/util.h>
These are the following non-libsel4 types in the capDL spec and how they can be replaced:
uint8_t
-> seL4_Uint8
bool
-> seL4_Bool
uint64_t
-> seL4_Uint64
size_t
-> seL4_Word
(All usages of size_t are for non-negative integers and so unsigned long is safe)uint32_t
-> seL4_Uint32
seL4_ARCH_VMAttributes
-> unsigned
(The CDL_Cap struct definition uses an unsigned 3 bitfield definition already.)In addition some constructions the spec uses can be manually defined:
#include <sel4/bootinfo_types.h>
#define BIT(x) (1lu << x)
#define PACKED __attribute__((packed))
#if defined(CONFIG_ARCH_ARM)
#define CDL_VM_CacheEnabled seL4_ARM_Default_VMAttributes
#define CDL_VM_CacheDisabled 0
#elif defined (CONFIG_ARCH_X86)
#define CDL_VM_CacheEnabled seL4_X86_Default_VMAttributes
#define CDL_VM_CacheDisabled seL4_X86_CacheDisabled
#elif defined (CONFIG_ARCH_RISCV)
#define CDL_VM_CacheEnabled seL4_RISCV_Default_VMAttributes
#define CDL_VM_CacheDisabled 0
#else
#error "Unsupported architecture"
#endif
And a small update to the capDL-tool's C generation:
diff --git a/capDL-tool/CapDL/PrintC.hs b/capDL-tool/CapDL/PrintC.hs
index 290b1c8..c058176 100644
--- a/capDL-tool/CapDL/PrintC.hs
+++ b/capDL-tool/CapDL/PrintC.hs
@@ -142,7 +142,7 @@ showCap objs (FrameCap id rights _ cached maybe_mapping) _ is_orig _ =
", .is_orig = " ++ is_orig ++
", .rights = " ++ showRights rights ++
", .vm_attribs = " ++
- (if cached then "seL4_ARCH_Default_VMAttributes" else "CDL_VM_CacheDisabled") ++
+ (if cached then "CDL_VM_CacheEnabled" else "CDL_VM_CacheDisabled") ++
", .mapping_container_id = " ++
(case maybe_mapping of
Just (mapping_container, _) -> showObjID objs mapping_container;
@@ -216,7 +216,7 @@ showSlots objs obj_id (x:xs) irqNode cdt ms =
where
index = fst x
slot = showCap objs (snd x) irqNode is_orig ms
- is_orig = if Map.notMember (obj_id, index) cdt then "true" else "false"
+ is_orig = if Map.notMember (obj_id, index) cdt then "1" else "0"
memberSlots :: Map ObjID Int -> ObjID -> CapMap Word -> IRQMap -> CDT -> ObjMap Word -> String
memberSlots objs obj_id slots irqNode cdt ms =
@@ -451,7 +451,7 @@ showUntypedDerivations :: AllocationType -> Map ObjID Int -> CoverMap -> String
showUntypedDerivations DynamicAlloc{} _ untypedCovers
| all null (Map.elems untypedCovers) =
".num_untyped = 0," +++
- ".untyped = NULL,"
+ ".untyped = 0,"
| otherwise = error $
"refusing to generate spec for dynamic allocation because the " ++
"following untypeds already have children:\n" ++
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.