SEL4编译

简介: SEL4编译

1. 编译脚本执行

mkdir build_aarch64
cd build_aarch64
../init-build.sh -DPLATFORM=qemu-arm-virt -DSIMULATION=true

1.0 -DPLATFORM=qemu-arm-virt

PLATFORM选择:进入如下目录,可以看到支持的一些平台信息

cd sel4/kernel/src/plat
allwinnerA20  apq8064  bcm2711  exynos4  fvp     hikey  imx7       maaxboard  odroidc4  pc99       qemu-arm-virt    quartz64    rockpro64  tk1          tx1  zynq7000
am335x        ariane   bcm2837  exynos5  hifive  imx6   imx8m-evk  odroidc2   omap3     polarfire  qemu-riscv-virt  rocketchip  spike      tqma8xqp1gb  tx2  zynqmp

我们选择qemu-arm-virt

1.1 -DCROSS_COMPILER_PREFIX=arm-linux-gnueabi-

定义交叉编译工具链是arm-linux-gnueabi-。

1.2 -DCMAKE_TOOLCHAIN_FILE=…/kernel/gcc.cmake

定义cmake通toolchain文件,设置编译工程的编译器,链接器。

1.3 -DRELEASE

设置true or false,编译出来的版本是否有debug信息。

1.4 -DSMP

设置true or flase, 默认配置中最大支持4核,如果支持更多核,需要设置-DKernelMaxNumNodes=<YOUR_PREFERENCE>

1.5 定义ARM体系架构

-DAARCH32=TRUE: Tells the build system that you are building for a 32-bit ARM target. This will cause the build system to assume that

you have a cross compiler installed which targets a system with the

triplet name arm-linux-gnueabi-.


-DAARCH32HF=TRUE: Tells the build system you’re building for a 32-bit ARM target which has hardware floating point support. Assumes you

have a cross- compiler installed which targets arm-linux-gnueabihf-.


-DAARCH64=TRUE: Tells the build system you’re building for a 64-bit ARM target. Assumes you have a cross-compiler installed which targets

aarch64-linux-gnu-.

2. 编译脚本解析

#!/bin/sh
#设置编译遇到错误就停止,遇到未定义报错
set -eu
#脚本执行路径/home/xxxx/data/source/opensource/sel4/
SCRIPT_PATH=${0%/*}
#执行脚本名称/home/xxxx/data/source/opensource/sel4/
SCRIPT_NAME=${0##*/}
#判断当前路径与脚本路径是否一致,可以看到不一致,所以下边if不生效
if [ "$PWD" = "$SCRIPT_PATH" ]
then
    echo "\"$SCRIPT_NAME\" should not be invoked from top-level directory" >&2
    exit 1
fi
if [ -e CMakeLists.txt ]
then
    echo "\"$SCRIPT_NAME\" should be invoked from a build directory and not" \
        "source directories containing a CMakeLists.txt file" >&2
    exit 1
fi
if [ -d "$HOME/.sel4_cache" ]
then
    CACHE_DIR="$HOME/.sel4_cache"
else
    CACHE_DIR="$SCRIPT_PATH/.sel4_cache"
fi
#判断脚本文件路径是否存在CMakeLists.txt文件,可以看到不存在
if [ -e "$SCRIPT_PATH/CMakeLists.txt" ]
then
    cmake -DCMAKE_TOOLCHAIN_FILE="$SCRIPT_PATH"/kernel/gcc.cmake -G Ninja "$@" \
        -DSEL4_CACHE_DIR="$CACHE_DIR" -C "$SCRIPT_PATH/settings.cmake" "$SCRIPT_PATH"
else
    # 进入else执行
    # real_easy_settings是/home/xxxx/data/source/opensource/sel4/projects/sel4test/easy-settings.cmake
    # 注意:$SCRIPT_PATH/easy-settings.cmake是一个链接文件
    real_easy_settings="$(realpath $SCRIPT_PATH/easy-settings.cmake)"
    # project_dir是/home/xxxx/data/source/opensource/sel4/projects/sel4test/
    project_dir="$(dirname $real_easy_settings)"
    #cmake -G: 选择生成器是Ninja
    #cmake -C: **没太理解ccache有什么用处,带更新**
    cmake -G Ninja "$@" -DSEL4_CACHE_DIR="$CACHE_DIR" -C "$project_dir/settings.cmake" "$project_dir"
fi

2.1 projects/sel4test/CMakeLists.txt解析(待注释)

#
# Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
#
# SPDX-License-Identifier: BSD-2-Clause
#
cmake_minimum_required(VERSION 3.7.2)
include(settings.cmake)
project(sel4test C CXX ASM)
find_package(seL4 REQUIRED)
find_package(elfloader-tool REQUIRED)
# Set the roottask CNode size to be large enough for DTB, timer caps, etc
# Note that this works for the platforms that we have at the moment, and may
# need to be increased in the future
set(KernelRootCNodeSizeBits 13 CACHE INTERNAL "")
# Set our custom domain schedule
set(KernelDomainSchedule "${CMAKE_CURRENT_LIST_DIR}/domain_schedule.c" CACHE INTERNAL "")
sel4_import_kernel()
if((NOT Sel4testAllowSettingsOverride) AND (KernelArchARM OR KernelArchRiscV))
    # Elfloader settings that correspond to how Data61 sets its boards up.
    ApplyData61ElfLoaderSettings(${KernelPlatform} ${KernelSel4Arch})
endif()
elfloader_import_project()
add_subdirectory(apps/sel4test-driver)
if(SIMULATION)
    include(simulation)
    if(KernelSel4ArchX86_64)
        SetSimulationScriptProperty(MEM_SIZE "3G")
    endif()
    if(KernelPlatformQEMUArmVirt)
        SetSimulationScriptProperty(MEM_SIZE "2G")
    endif()
    GenerateSimulateScript()
endif()

2.2projects/sel4test/settings.cmake解析(待注释)

#
# Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
#
# SPDX-License-Identifier: BSD-2-Clause
#
cmake_minimum_required(VERSION 3.7.2)
set(project_dir "${CMAKE_CURRENT_LIST_DIR}/../../")
file(GLOB project_modules ${project_dir}/projects/*)
list(
    APPEND
        CMAKE_MODULE_PATH
        ${project_dir}/kernel
        ${project_dir}/tools/seL4/cmake-tool/helpers/
        ${project_dir}/tools/seL4/elfloader-tool/
        ${project_modules}
)
set(NANOPB_SRC_ROOT_FOLDER "${project_dir}/tools/nanopb" CACHE INTERNAL "")
set(OPENSBI_PATH "${project_dir}/tools/opensbi" CACHE STRING "OpenSBI Folder location")
set(SEL4_CONFIG_DEFAULT_ADVANCED ON)
include(application_settings)
include(${CMAKE_CURRENT_LIST_DIR}/easy-settings.cmake)
correct_platform_strings()
find_package(seL4 REQUIRED)
sel4_configure_platform_settings()
set(valid_platforms ${KernelPlatform_all_strings} ${correct_platform_strings_platform_aliases})
set_property(CACHE PLATFORM PROPERTY STRINGS ${valid_platforms})
if(NOT "${PLATFORM}" IN_LIST valid_platforms)
    message(FATAL_ERROR "Invalid PLATFORM selected: \"${PLATFORM}\"
Valid platforms are: \"${valid_platforms}\"")
endif()
# Declare a cache variable that enables/disablings the forcing of cache variables to
# the specific test values. By default it is disabled
set(Sel4testAllowSettingsOverride OFF CACHE BOOL "Allow user to override configuration settings")
if(NOT Sel4testAllowSettingsOverride)
    # We use 'FORCE' when settings these values instead of 'INTERNAL' so that they still appear
    # in the cmake-gui to prevent excessively confusing users
    if(ARM_HYP)
        set(KernelArmHypervisorSupport ON CACHE BOOL "" FORCE)
    endif()
    if(KernelPlatformQEMUArmVirt OR KernelPlatformQEMURiscVVirt OR KernelPlatformSpike)
        set(SIMULATION ON CACHE BOOL "" FORCE)
    endif()
    if(SIMULATION)
        ApplyCommonSimulationSettings(${KernelSel4Arch})
    else()
        if(KernelArchX86)
            set(KernelIOMMU ON CACHE BOOL "" FORCE)
        endif()
    endif()
    # sel4test specific config settings.
    if(SIMULATION)
        set(Sel4testSimulation ON CACHE BOOL "" FORCE)
        set(Sel4testHaveCache OFF CACHE BOOL "" FORCE)
    else()
        set(Sel4testSimulation OFF CACHE BOOL "" FORCE)
        set(Sel4testHaveCache ON CACHE BOOL "" FORCE)
    endif()
    if(KernelPlatformQEMUArmVirt)
        if(KernelArmExportPCNTUser AND KernelArmExportPTMRUser)
            set(Sel4testHaveTimer ON CACHE BOOL "" FORCE)
        else()
            set(Sel4testHaveTimer OFF CACHE BOOL "" FORCE)
        endif()
    elseif(
        KernelPlatformZynqmp
        OR KernelPlatformPolarfire
        OR KernelPlatformQuartz64
        OR (SIMULATION AND (KernelArchRiscV OR KernelArchARM))
    )
        # Frequency settings of the ZynqMP make the ltimer tests problematic
        # Polarfire does not have a complete ltimer implementation
        # Quartz64 does not have a complete ltimer implementation
        set(Sel4testHaveTimer OFF CACHE BOOL "" FORCE)
    else()
        set(Sel4testHaveTimer ON CACHE BOOL "" FORCE)
    endif()
    # Check the hardware debug API non simulated (except for ia32, which can be simulated),
    # or platforms that don't support it.
    if(((NOT SIMULATION) OR KernelSel4ArchIA32) AND NOT KernelHardwareDebugAPIUnsupported)
        set(HardwareDebugAPI ON CACHE BOOL "" FORCE)
    else()
        set(HardwareDebugAPI OFF CACHE BOOL "" FORCE)
    endif()
    ApplyCommonReleaseVerificationSettings(${RELEASE} ${VERIFICATION})
    if(BAMBOO)
        set(LibSel4TestPrintXML ON CACHE BOOL "" FORCE)
    else()
        set(LibSel4TestPrintXML OFF CACHE BOOL "" FORCE)
    endif()
    if(DOMAINS)
        set(KernelNumDomains 4 CACHE STRING "" FORCE)
    else()
        set(KernelNumDomains 1 CACHE STRING "" FORCE)
    endif()
    if(SMP)
        if(NUM_NODES MATCHES "^[0-9]+$")
            set(KernelMaxNumNodes ${NUM_NODES} CACHE STRING "" FORCE)
        else()
            set(KernelMaxNumNodes 4 CACHE STRING "" FORCE)
        endif()
    else()
        set(KernelMaxNumNodes 1 CACHE STRING "" FORCE)
    endif()
    if(MCS)
        set(KernelIsMCS ON CACHE BOOL "" FORCE)
    else()
        set(KernelIsMCS OFF CACHE BOOL "" FORCE)
    endif()
endif()

3 参考

链接: Configuring and building seL4 projects

链接: Incorporating the build system into a project

相关文章
|
存储 Shell 编译器
makefile 变量赋值方式
makefile 变量赋值方式
224 1
|
Kubernetes 安全 网络协议
【K8S系列】深入解析k8s网络插件—Calico
【K8S系列】深入解析k8s网络插件—Calico
4760 0
|
Java 中间件 应用服务中间件
慎重!springboot中用undertow踩坑记
场景:准备基于springboot的静态资源实现mp4资源的播放,不同版本的springboot下效果不一样,可能导致正常的资源不可用。本文测试了几个版本,也针对这种情况提出了解决建议,希望对你的工作有所帮助。
2100 0
慎重!springboot中用undertow踩坑记
SEL4 for aarch64 on qemu编译运行
SEL4 for aarch64 on qemu编译运行
429 0
|
10月前
|
缓存 物联网 数据库
InfluxDB vs TDengine :2025 年了,谁家用的数据库还不能高效读缓存?
在工业互联网和物联网的大数据应用场景中,实时数据的写入和查询性能至关重要。如何快速获取最新设备状态并实时处理数据,直接影响到业务的高效运转。本文将深入分析 TDengine 和 InfluxDB 在缓存机制上的差异,帮助读者更好地理解这两款主流时序数据库在性能优化方面的优劣。
877 1
|
12月前
|
机器学习/深度学习 前端开发 JavaScript
WebAssembly:让前端性能突破极限的秘密武器
WebAssembly(简称 WASM)作为前端开发的性能加速器,能够让代码像 C++ 一样在浏览器中高速运行,突破了 JavaScript 的性能瓶颈。本文详细介绍了 WebAssembly 的概念、工作原理以及其在前端性能提升中的关键作用。通过与 JavaScript 的配合,WASM 让复杂运算如图像处理、3D 渲染、机器学习等在浏览器中流畅运行。文章还探讨了如何逐步集成 WASM,展示其在网页游戏、高计算任务中的实际应用。WebAssembly 为前端开发者提供了新的可能性,是提升网页性能、优化用户体验的关键工具。
5207 2
WebAssembly:让前端性能突破极限的秘密武器
|
12月前
|
网络架构 CDN
|
Unix Linux Shell
不同RTOS中POSIX接口的实现差异
本文探讨了在开发实时应用时使用POSIX API来实现跨平台和可移植性的策略。
269 1
不同RTOS中POSIX接口的实现差异
|
分布式计算 DataWorks API
dataworks常见问题之如何获取oss文件大小
DataWorks是阿里云提供的一站式大数据开发与管理平台,支持数据集成、数据开发、数据治理等功能;在本汇总中,我们梳理了DataWorks产品在使用过程中经常遇到的问题及解答,以助用户在数据处理和分析工作中提高效率,降低难度。
459 4