seL4的编译和运行(OdroidXU3)

2023-05-16

seL4支持平台

seL4所在的git如下:
https://github.com/seL4/seL4.git

不过我们编译和运行seL4一般不只是用这个git,而是借助seL4test(seL4的测试框架):
https://github.com/seL4/sel4test.git

seL4提供了各种平台上的配置文件,也提供了用于测试seL4的app。


seL4指定了可以运行的平台,按照下面的匹配来编译它(当然还有其他的匹配)。

ARCHPLATARMVCPU
armimx31armv6arm1136jf-s
armomap3armv7-acortex-a8
armam335xarmv7-acortex-a8
ia32pc99

另外在seL4官方文档中,指出下列平台也可以运行seL4:

  • Intel platforms

    1. a PC99-style Intel Architecture 32-bit x86 (ia32)
    2. There is also experimental support for the 64-bit Intel x86_64 architecture.
  • ARM platforms

    1. The Arndale dual core A15 ARM development board
    2. The Beagleboard, Omap 3530
    3. The Inforce IFC6410 development board, running a Qualcomm Krait processor that is like an A15.
    4. The KZM-ARM11-01. The kernel for this board is the one that is formally verified.
    5. The Odroid-X Exynos4412 board
    6. The Odroid-XU Exynos 5 board
    7. The Sabre Lite i.mx6 board.
    8. The Beaglebone Black is a community-supported port.

选择OdroidXU3编译seL4

根据seL4官方文档所说明的支持平台,并参照seL4test工程中的配置文件,我们选择OdroidXU3开发板来运行seL4。下面就是OdroidXU3:
OdroidXU3

这个平台采用Samsung Exynos5422 Cortex™-A15 2.0Ghz quad core and Cortex™-A7 quad core CPUs。而exynos5422在seL4的支持序列当中。同时这个板子支持的操作系统如下:Ubuntu 14.04 + OpenGL ES + OpenCL on Kernel LTS 3.10和Android 4.4.2 on Kernel LTS 3.10。因此是一款能满足时下开发的较新的开发板。
关于它的相信信息,可以到官网上去查看:
Hardkernel Odroid


通过repo获得seL4test工程。工程根目录下有一个configs文件夹,里面就是根据具体平台所设置的配置文件,我们根据我们的板子,选择 odroidxu3_release_xml_defconfig。把它拷贝到seL4test工程根目录下。
在工程根目录下执行命令: $ make menuconfig
出现如下界面:
这里写图片描述

进入“Load an Alternate Configuration File”,输入刚才拷贝的配置文件的名字:
这里写图片描述

ok后,回到上面的界面,进入“Save an Alternate Configuration File”,直接ok。最后Exit退出menuconfig。

然后运行命令: $ make

这样你就会在images目录下发现新生成的seL4的elf格式的镜像文件:
sel4test-driver-image-arm-exynos5

编译成功!


制作OdroidXU3的SD卡启动盘

OdroidXU3默认是eMMC启动,也就是说厂商在eMMC中烧写了u-boot和ubuntu的镜像,我们想通过SD卡启动,所以需要做:

  1. 将OdroidXU3的启动方式改为SD卡启动
  2. 制作SD卡启动盘

对于1,看下面的图:
这里写图片描述

板子上有如图所示的开关,左数第一个开关就是控制启动方式:

开关状态启动方式
ONeMMC
OFFMICROSD

下面制作SD卡启动盘:

  • 根据OdroidXU3提供的分区表烧写u-boot
  • 对SD卡分区并拷贝seL4镜像

下面是OdroidXU3的eMMC卡或microSD卡的分区表:
这里写图片描述

如果我们不按照平台指定的SD卡的分区表来烧写u-boot,是不能正确烧写并启动u-boot的。

OdroidXU3官方也提供了如何编译u-boot的手册和烧写u-boot的shell脚本:
xu3 building u-boot

注意:
首先确认目录 u-boot/sd_fuse/hardkernel/下是否存在 bl1.bin.HardKernel、bl2.bin.HardKernel、tzsw.bin.hardkernel,和配置文件sd_fusing.sh。 将自带的u-boot.bin.hardkernel删掉。
安装手册会在根目录编译生成u-boot/u-boot.bin,需要将它拷贝到u-boot/sd_fuse/hardkernel目录下,并重命名为u-boot.bin.hardkernel。

按照手册所说的利用sd_fusing.sh脚本将u-boot烧写到SD卡中。

我们使用minicom在xubuntu下进行串口调试(minicom配置信息采用默认即可),查看板子启动信息,如果u-boot烧写成功,启动后会出现如下界面:
这里写图片描述

进入u-boot命令模式。


接下来我们先要将上面生成的seL内核镜像放到SD卡中,我们不是用烧写u-boot时的脚本将内核也烧进SD卡中,而是要将SD卡进行分区,然后直接拷贝。

将SD卡分区需要注意以下两点:
1. 第一分区位置要从地址3072开始。原因:MBR的需要占用第一个512byte,fwbl1区需要占用1-30 共15KB,bl2区需要占用31-62 共 16KB,u-boot镜像需要占用63-718 共238KB,tzsw.bin需要占用719-1230,共256KB,u-boot的运行环境需要占用1231-1263 共16KB,u-boot的环境变量需要占用1263-3071。而第一分区存储的是SEL4的内核镜像,为保证u-boot运行,以及不干扰第一分区的读写操作,所以地址设定为3072。
2. 我们将SD卡分为两区(非必须),文件系统类型分别为FAT16(vfat)、LINUX 文件系统(ext4),第一分区应留出足够的空间存储SEL4的内核镜像,至少为3MB以上。

分好区后,将SD卡插入电脑就可以挂载识别了,我们将seL4的内核镜像sel4test-driver-image-arm-exynos5拷贝到SD卡的第一个分区中(为了下面启动seL4内核的方便,我们将内核重命名为sel4)。

大功告成!现在试一下是否可以在OdroidXU3上点亮seL4。


点亮seL4

在u-boot命令模式下,依次输入如下命令:

这里写图片描述

这里显示的是SD卡第一个分区中存放的文件,我们的内核镜像是sel4。

然后将内核加载到内存指定位置:
这里写图片描述

其中0x48000000就是内核在内存中的指定位置。

最后启动:
这里写图片描述

这里写图片描述

由于我们使用的是seL4test这个官方提供的框架,编译生成的seL4内核镜像包含了一个叫seL4test-driver的app,所以运行所出的信息实际上是这个app在运行,最后会出现“All is well in the universe”。

至此我们已经在OdroidXU3上成功点亮seL4。

本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)

seL4的编译和运行(OdroidXU3) 的相关文章

  • C++的编译过程详解

    C C 43 43 编译过程 C C 43 43 编译过程主要分为4个过程 编译预处理编译 优化阶段汇编过程链接程序 一 编译预处理 xff08 1 xff09 宏定义指令 xff0c 如 define Name TokenString x
  • BA(Basic authentication)认证实践

    1 概念介绍 Basic authentication xff1a 是一种最简单的对Web资源进行访问控制的方法 xff0c 属应用层的安全保障手段 常用的签名算法有 xff1a base64 HmacSHA1 1 xff09 优点 xff
  • 累加校验和C语言实现

    发送方 xff1a 对要数据累加 xff0c 得到一个数据和 xff0c 对和求反 xff0c 即得到我们的校验值 然后把要发的数据和这个校验值一起发送给接收方 接收方 xff1a 对接收的数据 包括校验和 进行累加 xff0c 如果得到0
  • C++项目工程在Linux环境开发、部署和运行问题

    背景 当我们自己开发的项目程序需要在linux上进行部署 调试时 xff0c 项目代码完整拷贝过去之后 xff0c 直接运行我们自己的可执行程序 xff0c 往往提示找不到所相关的 so库 xff0c 会报错 这是因为 xff0c 系统只会
  • Jetson Xavier NX上安装ROS、Cartographer、基于D435i的Yolov5+TensorRT7的流程及问题解决

    主要记录下自己在Jetson Xavier NX上运行ROS Cartographer 基于D435i的Yolov5 43 TensorRT的系统环境配置流程 xff0c 经过了无数次在ARM上的安装 xff0c 这次是最流畅的一次环境配置
  • 计算机进制转换:二进制、八进制、十进制、十六进制

    一 什么是进制 在生活中 xff0c 我们通常都是使用阿拉伯数字计数的 xff0c 也就是10进制 xff0c 以10为单位 xff0c 遇10进一 xff0c 所以是由0 xff0c 1 xff0c 2 3 4 5 6 7 8 9组成的
  • 摘要认证,使用HttpClient实现HTTP digest authentication

    文章目录 前言一 四个过程二 过程细节三 HttpClient 代码示例 前言 今天工作需要做了摘要认证 xff08 digest authentication xff09 xff0c 下面就工作中遇到的问题及过程做一个总结 一 四个过程
  • C语言之带参数的宏

    这两天在学习C语言 xff0c 发现宏定义挺有意思 xff0c 可以减少代码量 带参宏定义 的一般形式为 define 宏 名 形参表 字符串 带参宏调用 的一般形式为 xff1a 宏 名 实参表 xff1b define M X Y X
  • visual studio升级

    visual studio升级 概述升级步骤温馨提示 概述 有时处于开发要求或者安全要求 xff0c 需要将visual studio升级到最新的版本 本篇文章记录一下如何升级 升级步骤 1 找到visual studio的安装路径下的安装
  • STL中那些好用的东西!(持续更新)

    一 数据结构部分 1 set amp map xff08 后续持续更新 xff09 2 queue xff08 priority queue xff09 queue lt int gt a 定义 a push i 压入 a pop 弹出 a
  • 工业机器人虚拟仿真设计

  • HTTP详解

    一 什么是HTTP xff1f HTTP xff08 HyperText Transfer Protocol xff0c 超文本传输协议 xff09 是一个简单的请求 响应协议 xff0c 它通常运行在TCP之上 xff08 应用层 xff
  • android练习之为 TextView 添加监听器 ,添加后退按钮 ,从按钮到图标按钮

    为 TextView 添加监听器 NEXT按钮不错 xff0c 但如果用户单击应用的TextView文字区域 xff08 地理知识问题 xff09 xff0c 也可以跳转 到下一道题 xff0c 用户体验会更好 添加后退按钮 为GeoQui
  • ORA-01918: 用户 'SCOTT' 不存在 解决方法

    SQL gt alter user scott account unlock alter user scott account unlock 第 1 行出现错误 ORA 01918 用户 SCOTT 不存在 找到scott sql 文件 S
  • idea 里form表单action提交servlet文件出现报错

    由于在action的字符串中加了空格 xff0c 导致于于url pattern不匹配 xff0c 所以报错
  • 数据结构——二维数组

    二维数组可以理解为数组的数组 二维数组组织为矩阵 xff0c 可以表示为行和列的集合 但是 xff0c 创建二维数组以实现关系数据库外观相似的数据结构 它提供了一次容纳大量数据的便利性 xff0c 可以在任何需要的地方传递给任意数量的功能
  • 数据结构——链表

    链表是一种随机存储在内存中的节点的对象集 节点包括两个字段 xff0c 即存储在该地址的数据和包含下一节点地址的指针 链表的最后一个节点包含指向null的指针 1 链表的用途 链表不需要连续存在于存储器中 节点可以是存储器中任何位置并链接在
  • 多线程学习笔记--第一章 多线程技能(1)

    1 什么是进程 xff1f 进程是操作系统结构的基础 xff0c 是一次程序的执行 xff1b 是一个程序及其数据在处理机上顺序执行时所发生的活动 xff1b 是程序在一个数据集合上运行的过程 xff0c 它是系统进行资源分配和调度的一个独
  • 多线程学习笔记--第一章 多线程技能(2)

    1 currentThread方法 该方法返回代码段正在被哪个线程调用的信息 2 isAlive方法 判断当前线程是否处于活动状态 活动状态是线程已经启动且尚未终止 线程处于运行或准备开始运行的状态 如果将线程对象以构造参数的方式传递给Th
  • Qt编程过程中若给定一些数,把它们四舍五入后,保留两位小数

    double类型的数进行四舍五入后保留两位小数 场景实现方式方法一 方法二总结 场景 开发的过程中需要显示一些double类型的数 xff0c 但是又不能直接显示 xff0c 需要四舍五入之后保留两位小数 如 xff1a 0 124567

随机推荐