L4Ka Pistachio实验性内核参考手册

3星 · 超过75%的资源需积分: 10 84 浏览量更新于2024-07-30 收藏 779KB PDF 举报

本篇文档是关于L4Ka-Pistachio微内核的实验性规范手册（L4eXperimentalKernel Reference Manual），由SystemArchitectureGroup, Department of Computer Science, Karlsruhe Institute of Technology (L4Ka团队)发布，版本为X.2。该手册提供了对L4微内核体系结构的深入理解和详细描述，适用于研究者、开发者和对L4技术感兴趣的读者。 L4Ka-Pistachio是一个轻量级的、安全性极高的微内核系统，特别强调了最小化攻击面和高效性能。它遵循版权协议，允许无限制地复制和分发文档，但不允许未经许可进行修改或创建衍生作品，L4Ka团队保留随时更新规格的权利，最新版本可在<http://l4ka.org/>获取。手册首先介绍了手册的目的和读者需要了解的关键信息。读者应具备基本的系统架构知识，并理解文档中的专业术语。章节一"BasicKernelInterface"是核心部分，分为两个子节： 1.1 **Kernel Interface Page** 这部分详细解释了L4Ka-Pistachio微内核的基本接口，包括如何与内核进行交互，以及提供的服务和功能。这些接口通常涉及进程通信、系统调用、中断处理和内存管理等关键操作，设计上强调了简洁性和安全隔离，使得应用程序和内核之间的交互尽可能地简单且受控。 1.2 **"...** （此处缺失部分内容，可能是对特定接口或功能的深入讨论，如异常处理、线程管理或同步机制等）。这部分可能包含具体的接口函数定义、参数说明以及使用示例，以便开发者在实际项目中参考和实现。通过阅读此文档，用户可以深入了解L4微内核设计原则，学习如何构建基于L4Ka-Pistachio的系统，以及如何处理安全性和性能优化。这对于从事嵌入式系统、安全操作系统或微内核研究的人员来说是一份宝贵的参考资料。同时，文档的修订历史也能帮助追踪技术演进和新特性添加，确保开发者始终与最新进展保持同步。

4 KERNEL INTERFACE PAGE

r w x

Identiﬁes the supported access rights (read, write, execute) that can be set independently of

other access rights. A 1-bit signals that the right can be set and reset on a mapped page. For

rwx = 010, only write permission could be controlled orthogonally. The processor would

implicitly permit read and execute access on any mapped page. For rwx = 111, all three rights

could be set and reset independently.

ThreadInfo

UserBase

(12)

SystemBase

(12)

(8)

Number of valid thread-number bits. The thread number ﬁeld may be larger but only bits

0 . . . t − 1 are signiﬁcant for this kernel. Higher bits must all be 0.

UserBase

Lowest thread number available for user threads (see page 14). The ﬁrst three thread numbers

will be used for the initial thread of σ

, σ

, and root task respectively (see page 92). The version

numbers (see page 14) for these initial threads will equal to one.

SystemBase

Lowest thread number used for system threads (see page 14). Thread numbers below this value

denote hardware interrupts.

ClockInfo

SchedulePrecision

(16)

ReadPrecision

(16)

ReadPrecision

Speciﬁes the minimal time difference 6= 0 that can be detected by reading the system clock

through the SYSTEMCLOCK system call. Basically, this is the precision of the system clock

when reading it.

SchedulePrecision

Speciﬁes the maximal jitter (±) for a scheduled thread activation based on a wakeup time (pro-

vided that no thread of higher or equal priority is active and timer interrupts are enabled).

Precisions are given as time periods (see page 30).

UtcbInfo

∼

(10/42)

(6)

(10)

The minimal area size for an address space’s UTCB area is 2

. The size of the UTCB area limits

the total number of threads k to 2

mk ≤ 2

UTCB size multiplier.

The UTCB location must be aligned to 2

. The total size required for one UTCB is 2

KipAreaInfo

∼

(26/58)

(6)

The size of the kernel interface page area is 2

BootInfo

Prior to kernel initialization a boot loader can write an arbitrary value into the BootInfo ﬁeld of

the kernel conﬁguration page (see page 92). Post-initialization code, e.g., a root server can later

read the ﬁeld from the kernel interface page. Its value is neither changed nor interpreted by the

kernel. This is a generic method for passing system information across kernel initialization.

Processor Description

ProcDescPtr

Points to an array containing a description for each system processor. The ProcessorInfo ﬁeld

contains the dimension of the array. ProcDescPtr is given as an address relative to the kernel

interface page’s base address.

ExternalFreq

External Bus frequency in kHz.

KERNELINTERFACE 7

1.2 KERNELINTERFACE [Slow Systemcall]

−→ void* kernel interface page

Word API Version

Word API Flags

Word KernelId

Delivers base address of the kernel interface page, API version, and API ﬂags. The latter two values are copies of the

corresponding ﬁelds in the kernel interface page. The API information is delivered in registers through this system call (a)

to enable unrestricted structural changes of the kernel interface page in future versions, and (b) to enable secure detection

of the kernel’s endian mode (little/big) and word width (32/64).

The structure of the kernel interface page is described on page 2. The page is a microkernel object. It is directly

mapped through the microkernel into each address space upon address-space creation. It is not mapped by a pager, can

not be mapped or granted to another address space and can not be unmapped. The creator of a new address space can

specify the address where the kernel interface page has to be mapped. This address will remain constant through the

lifetime of that address space.

Any thread can determine the address of the kernel interface page through this system call. Since the system call may

be slow it is highly recommended to store the address in a static variable for further use.

It is also possible to use a unique address for the kernel interface page in all address spaces of a (sub)system. Then,

the kernel interface page can be accessed by ﬁxed absolute addresses without using the current system call.

Besides other things, the page describes the current API, ABI, and microkernel version so that a server or an application

can ﬁnd out whether and how it can run on the current microkernel. Since the kernel interface page also contains API-

and ABI-speciﬁc data for most other system calls the page’s base address is typically required before any other system

call can be used.

To enable version detection independently of the API and ABI, the current system call is guaranteed to work in all L4

versions. The systemcall code will never change and will be the same on compatible processors. (If a processor is upward

compatible to multiple incompatible processors the kernel should offer multiple systemcall codes for this function.)

Output Parameters

kernel interface page

Ver X.1 and above

base address

(32/64)

Kernel interface page address, always page aligned. 0 is no valid address.

Ver X.0 and below

(32/64)

Older versions (2, X.0, etc.) do not include the kernel interface page as a kernel mapped page.

No address is delivered.

API Version

version

(8)

subversion

(8)

∼

(16)

see page 3, “Kernel Interface Page”

API Flags

∼

(28/60)

ww ee

see page 3, “Kernel Interface Page”

剩余197页未读，继续阅读

三壮

粉丝: 18
资源: 4

L4Ka Pistachio实验性内核参考手册

imapi2.dll

前端开源库-pistachio2

基于微信小程序的学习资料销售平台设计与实现.docx

java基于ssm+jsp二手交易平台网站管理系统源码 带毕业论文

weixin218“校园资料分享微信小程序”的设计与实现springboot.rar

jdk - 22.0.2 - linux

java基于ssm+jsp旅游信息网站系统源码 带毕业论文+PPT

仿ios音量调节的效果.zip

基于springboot的校园疫情防控系统设计与实现.docx

Sigrity-System Explorer User Guide.rar

最新资源

java基于ssm+jsp二手交易平台网站管理系统源码带毕业论文

java基于ssm+jsp旅游信息网站系统源码带毕业论文+PPT