# RFC discussion

**URL:** https://sel4.discourse.group/c/rfc-discussion/9.md

[Latest](https://sel4.discourse.group/latest.md) · [Categories](https://sel4.discourse.group/categories.md) · [Tags](https://sel4.discourse.group/tags.md)

---

## [About the RFC discussion category](https://sel4.discourse.group/t/about-the-rfc-discussion-category/143)

<div class="topic-metadata">

**Author:** [@curtis](https://sel4.discourse.group/u/curtis)\
**Replies:** 0

</div>

RFC discussions are used to discuss changes to the seL4 ecosystem that would need to follow the RFC Process. Topics of discussion for this category include: the discussions necessary before proposing an RFC to determi…

---

## [Pre-RFC: change MCS API from us to ticks](https://sel4.discourse.group/t/pre-rfc-change-mcs-api-from-us-to-ticks/1011)

<div class="topic-metadata">

**Author:** [@gerwin.klein](https://sel4.discourse.group/u/gerwin.klein)\
**Replies:** 12\
**Last updated:** [December 31, 2025, 10:39pm UTC](https://sel4.discourse.group/t/pre-rfc-change-mcs-api-from-us-to-ticks/1011 "2025-12-31T22:39:49Z")

</div>

The current MCS user-facing API for instance for setting budget and period or reporting consumed time takes its arguments in micro seconds (us, time\_t), but internally represents all times in timer ticks (ticks\_t). The …

---

## [Pre-RFC: Arm: Add TCB policy support for controlling user level access to certain system registers](https://sel4.discourse.group/t/pre-rfc-arm-add-tcb-policy-support-for-controlling-user-level-access-to-certain-system-registers/507)

<div class="topic-metadata">

**Author:** [@kent-mcleod2](https://sel4.discourse.group/u/kent-mcleod2)\
**Replies:** 5\
**Last updated:** [March 22, 2024, 12:09pm UTC](https://sel4.discourse.group/t/pre-rfc-arm-add-tcb-policy-support-for-controlling-user-level-access-to-certain-system-registers/507 "2024-03-22T12:09:28Z")

</div>

Summary: There are system registers that are useful to be able to access from user level. Two examples are system registers related to the Arm Generic Timer and registers related to the Performance Monitor Unit. There …

---

## [Pre-RFC: To effortlessly develop seL4 systems in rust](https://sel4.discourse.group/t/pre-rfc-to-effortlessly-develop-sel4-systems-in-rust/539)

<div class="topic-metadata">

**Author:** [@BenPH](https://sel4.discourse.group/u/BenPH)\
**Replies:** 73\
**Last updated:** [December 9, 2022, 5:00pm UTC](https://sel4.discourse.group/t/pre-rfc-to-effortlessly-develop-sel4-systems-in-rust/539 "2022-12-09T17:00:09Z")

</div>

There are a number of project out there that involve developing on seL4 using Rust. This RFC is an exploration of what can/needs to be done within the seL4 project itself to allow full advantage of rust tooling and langu…

---

## [RFC-13: MCS: Improve constraints on grant via reply](https://sel4.discourse.group/t/rfc-13-mcs-improve-constraints-on-grant-via-reply/622)

<div class="topic-metadata">

**Author:** [@mbrcknl](https://sel4.discourse.group/u/mbrcknl)\
**Replies:** 0\
**Last updated:** [November 22, 2022, 10:07am UTC](https://sel4.discourse.group/t/rfc-13-mcs-improve-constraints-on-grant-via-reply/622 "2022-11-22T10:07:20Z")

</div>

I have posted a new RFC. It proposes a change to the semantics of reply invocations in the MCS kernel. If accepted, the ability to grant capabilities when replying would be controlled primarily by endpoint capability gra…

---

## [RFC-12: seL4 Device Driver Framework](https://sel4.discourse.group/t/rfc-12-sel4-device-driver-framework/600)

<div class="topic-metadata">

**Author:** [@gerwin.klein](https://sel4.discourse.group/u/gerwin.klein)\
**Replies:** 0\
**Last updated:** [October 6, 2022, 2:59pm UTC](https://sel4.discourse.group/t/rfc-12-sel4-device-driver-framework/600 "2022-10-06T14:59:25Z")

</div>

A new RFC has just landed on the seL4 Device Driver Framework: \[RFC-12\] - Jira If you have any feedback, please comment there. Cheers, Gerwin

---

## [RFC-11: fault+timeout parameters in TCBConfigure (MCS)](https://sel4.discourse.group/t/rfc-11-fault-timeout-parameters-in-tcbconfigure-mcs/548)

<div class="topic-metadata">

**Author:** [@gerwin.klein](https://sel4.discourse.group/u/gerwin.klein)\
**Replies:** 1\
**Last updated:** [July 25, 2022, 8:08am UTC](https://sel4.discourse.group/t/rfc-11-fault-timeout-parameters-in-tcbconfigure-mcs/548 "2022-07-25T08:08:16Z")

</div>

I’d like to solicit discussion on the new RFC-11 on setting fault and timeout handler parameters while configuring TCBs (MCS only). The idea is to make the API more consistent, and it looks fairly uncontroversial, so i…

---

## [Pre RFC: Re-implement inline assembly functions in Rust, publish as stand-alone crate](https://sel4.discourse.group/t/pre-rfc-re-implement-inline-assembly-functions-in-rust-publish-as-stand-alone-crate/540)

<div class="topic-metadata">

**Author:** [@BenPH](https://sel4.discourse.group/u/BenPH)\
**Replies:** 4\
**Last updated:** [July 17, 2022, 11:42pm UTC](https://sel4.discourse.group/t/pre-rfc-re-implement-inline-assembly-functions-in-rust-publish-as-stand-alone-crate/540 "2022-07-17T23:42:08Z")

</div>

Summary To define in-line assembly functions, such as those found in libsel4/sel4\_arch\_include/aarch64/sel4/sel4\_arch/syscalls.h, using rust code. Motivation In the context of there being a desire to see development of …

---

## [Pre-RFC: Exposing Cross-Component TCBs via CAmkES Template](https://sel4.discourse.group/t/pre-rfc-exposing-cross-component-tcbs-via-camkes-template/479)

<div class="topic-metadata">

**Author:** [@jshackleton](https://sel4.discourse.group/u/jshackleton)\
**Replies:** 7\
**Last updated:** [May 18, 2022, 10:36pm UTC](https://sel4.discourse.group/t/pre-rfc-exposing-cross-component-tcbs-via-camkes-template/479 "2022-05-18T22:36:01Z")

</div>

Summary We recently developed a userland scheduled for MCS within the CAmKES service framework. In the process, we encountered an obstacle: The scheduling component itself must have access to the TCBs and SCs of the oth…

---

## [PreRFC external tools](https://sel4.discourse.group/t/prerfc-external-tools/481)

<div class="topic-metadata">

**Author:** [@ratmice](https://sel4.discourse.group/u/ratmice)\
**Replies:** 6\
**Last updated:** [March 8, 2022, 6:39pm UTC](https://sel4.discourse.group/t/prerfc-external-tools/481 "2022-03-08T18:39:43Z")

</div>

Hello, I have been messing around with the prospect of running external tools over the kernel xml, during the kernel build, with the external tools being written in other languages, and generating bindinfs for other la…

---

## [Pre-RFC: ProtectN](https://sel4.discourse.group/t/pre-rfc-protectn/478)

<div class="topic-metadata">

**Author:** [@alwin-joshy](https://sel4.discourse.group/u/alwin-joshy)\
**Replies:** 15\
**Last updated:** [February 11, 2022, 4:54am UTC](https://sel4.discourse.group/t/pre-rfc-protectn/478 "2022-02-11T04:54:28Z")

</div>

Summary This RFC discusses the implementation of a new mapping primitive, protectN (and by extension unmapN), as well as changes to page\_map which enables more seamless use of stale capabilities, which are utilized by t…

---

## [Pre-RFC: FPU as an object](https://sel4.discourse.group/t/pre-rfc-fpu-as-an-object/475)

<div class="topic-metadata">

**Author:** [@andyb](https://sel4.discourse.group/u/andyb)\
**Replies:** 2\
**Last updated:** [February 11, 2022, 2:34am UTC](https://sel4.discourse.group/t/pre-rfc-fpu-as-an-object/475 "2022-02-11T02:34:19Z")

</div>

Summary This proposes to introduce a new object that represents the FPU into seL4. Motivation Currently, seL4 treats the FPU as part of the thread context, saved in the TCB on preemption. As FPU state is large, the kern…

---

## [RFC-9: Add new capability for seL4 SMC Forwarding](https://sel4.discourse.group/t/rfc-9-add-new-capability-for-sel4-smc-forwarding/431)

<div class="topic-metadata">

**Author:** [@gerwin.klein](https://sel4.discourse.group/u/gerwin.klein)\
**Replies:** 0\
**Last updated:** [November 9, 2021, 9:51pm UTC](https://sel4.discourse.group/t/rfc-9-add-new-capability-for-sel4-smc-forwarding/431 "2021-11-09T21:51:51Z")

</div>

I’d like to solicit discussion on the new RFC on forwarding Secure Monitor Calls on Arm: https://sel4.atlassian.net/browse/RFC-9 Relevant Arm documentation (SMC calling conventions): https://developer.arm.com/document…

---

## [Pre-RFC: Build interface](https://sel4.discourse.group/t/pre-rfc-build-interface/294)

<div class="topic-metadata">

**Author:** [@curtis](https://sel4.discourse.group/u/curtis)\
**Replies:** 7\
**Last updated:** [September 4, 2021, 2:15am UTC](https://sel4.discourse.group/t/pre-rfc-build-interface/294 "2021-09-04T02:15:26Z")

</div>

Summary This proposes to introduce a well-defined process for generating a kernel image for a given configuration as well as producing a bootable image from a kernel image and user-level image. Motivation The discussion…

---

## [RFC-7: remove CNode\_Mutate](https://sel4.discourse.group/t/rfc-7-remove-cnode-mutate/399)

<div class="topic-metadata">

**Author:** [@gerwin.klein](https://sel4.discourse.group/u/gerwin.klein)\
**Replies:** 0\
**Last updated:** [August 22, 2021, 1:34am UTC](https://sel4.discourse.group/t/rfc-7-remove-cnode-mutate/399 "2021-08-22T01:34:37Z")

</div>

Sparked by Mark Jones’ question on the mailing list and SELFOUR-136. See also https://sel4.atlassian.net/browse/RFC-7

---

## [Pre-RFC: CAmkES pre\_init() and pre\_post() need a return code](https://sel4.discourse.group/t/pre-rfc-camkes-pre-init-and-pre-post-need-a-return-code/364)

<div class="topic-metadata">

**Author:** [@axel](https://sel4.discourse.group/u/axel)\
**Replies:** 0\
**Last updated:** [June 9, 2021, 11:33pm UTC](https://sel4.discourse.group/t/pre-rfc-camkes-pre-init-and-pre-post-need-a-return-code/364 "2021-06-09T23:33:35Z")

</div>

The CAmkES function pre\_init() and pre\_post() need a return code, so any initialization error can be reported back to the CAmkES runtime. The runtime shall then stop any further activities like calling post\_init() or ena…

---

## [Pre-RFC: TrustZone support on AArch64](https://sel4.discourse.group/t/pre-rfc-trustzone-support-on-aarch64/250)

<div class="topic-metadata">

**Author:** [@nspin](https://sel4.discourse.group/u/nspin)\
**Replies:** 14\
**Last updated:** [May 30, 2021, 6:50am UTC](https://sel4.discourse.group/t/pre-rfc-trustzone-support-on-aarch64/250 "2021-05-30T06:50:16Z")

</div>

The purpose of this thread is to discuss what TrustZone support for the AArch64 seL4 kernel might look like, and whether that’s worth the cost. TrustZone background The security of a TrustZone-enabled system is achieved…

---

## [Pre-RFC: Allow per-thread access to system counter on Aarch64](https://sel4.discourse.group/t/pre-rfc-allow-per-thread-access-to-system-counter-on-aarch64/347)

<div class="topic-metadata">

**Author:** [@bennoleslie](https://sel4.discourse.group/u/bennoleslie)\
**Replies:** 1\
**Last updated:** [May 14, 2021, 5:30am UTC](https://sel4.discourse.group/t/pre-rfc-allow-per-thread-access-to-system-counter-on-aarch64/347 "2021-05-14T05:30:15Z")

</div>

Currently the default compile does not allow a thread to access the system counter register on ARM. There is a compile option that does allow threads to account the counter (all threads). It would be preferable if this…

---

## [Pre-RFC: make explicit names for connections in CAmkES optional](https://sel4.discourse.group/t/pre-rfc-make-explicit-names-for-connections-in-camkes-optional/327)

<div class="topic-metadata">

**Author:** [@axel](https://sel4.discourse.group/u/axel)\
**Replies:** 1\
**Last updated:** [March 24, 2021, 10:55pm UTC](https://sel4.discourse.group/t/pre-rfc-make-explicit-names-for-connections-in-camkes-optional/327 "2021-03-24T22:55:18Z")

</div>

Currently, every connection must be given a name in the CAmkES system definition. However, in many cases the name is not used anywhere by the user. It would be convenient, if the name could be omitted and the builder pic…

---

## [Pre-RFC: Boot Interface](https://sel4.discourse.group/t/pre-rfc-boot-interface/295)

<div class="topic-metadata">

**Author:** [@curtis](https://sel4.discourse.group/u/curtis)\
**Replies:** 8\
**Last updated:** [February 19, 2021, 12:44am UTC](https://sel4.discourse.group/t/pre-rfc-boot-interface/295 "2021-02-19T00:44:42Z")

</div>

Summary This adds a well-defined interface for the kernel to boot itself in a manner that allows any pre-boot software to be readily interchanged on any platform. elfloader will then be modified to use this interface to …

---

## [Pre-RFC: Supported kernel configurations](https://sel4.discourse.group/t/pre-rfc-supported-kernel-configurations/284)

<div class="topic-metadata">

**Author:** [@bennoleslie](https://sel4.discourse.group/u/bennoleslie)\
**Replies:** 4\
**Last updated:** [February 8, 2021, 1:48am UTC](https://sel4.discourse.group/t/pre-rfc-supported-kernel-configurations/284 "2021-02-08T01:48:37Z")

</div>

Below is a proposal that comes out of the postponed/abandoned RFC-6 proposal for seL4 core. This is not written in the RFC format as it is intended to be structured in a way to support discussion around the idea and moti…

---

## [Pre-RFC: interface specifications](https://sel4.discourse.group/t/pre-rfc-interface-specifications/241)

<div class="topic-metadata">

**Author:** [@DemiMarie](https://sel4.discourse.group/u/DemiMarie)\
**Replies:** 1\
**Last updated:** [November 11, 2020, 10:36pm UTC](https://sel4.discourse.group/t/pre-rfc-interface-specifications/241 "2020-11-11T22:36:16Z")

</div>

It would be nice if there were standardized interfaces, such as for block and network drivers, between seL4 components. Some of the interfaces I would like to see are: Filesystems Block devices; the Xen PV API is like…

---

## [Pre-RFC: Specify a fixed kernel ABI for each architecture](https://sel4.discourse.group/t/pre-rfc-specify-a-fixed-kernel-abi-for-each-architecture/145)

<div class="topic-metadata">

**Author:** [@lazycandle55](https://sel4.discourse.group/u/lazycandle55)\
**Replies:** 21\
**Last updated:** [November 10, 2020, 12:40am UTC](https://sel4.discourse.group/t/pre-rfc-specify-a-fixed-kernel-abi-for-each-architecture/145 "2020-11-10T00:40:05Z")

</div>

Note: This discussion is continued from this thread. Currently, the seL4 kernel ABI – the enumerations, structures, types, system calls, and object invocations needed to communicate between the kernel and user space – c…

---

## [Pre-RFC: Binding notifications to endpoints](https://sel4.discourse.group/t/pre-rfc-binding-notifications-to-endpoints/233)

<div class="topic-metadata">

**Author:** [@DemiMarie](https://sel4.discourse.group/u/DemiMarie)\
**Replies:** 11\
**Last updated:** [November 9, 2020, 1:21am UTC](https://sel4.discourse.group/t/pre-rfc-binding-notifications-to-endpoints/233 "2020-11-09T01:21:17Z")

</div>

Currently, a service that needs to receive many notifications has a problem. The only scalable way to do so is to use an endpoint, but it is a bad idea for to make an IPC call to an untrusted endpoint, so this only work…
