- RFC - lists.sel4.systems

[JIRA] (RFC-8) Remove support for ARMv6, i.MX31 and KZM
by Matthew Brecknell (Jira) 16 Sep '21

16 Sep '21

Matthew Brecknell ( https://sel4.atlassian.net/secure/ViewProfile.jspa?accountId=557058%3Ad9d2f… ) *updated* an issue RFCs ( https://sel4.atlassian.net/browse/RFC?atlOrigin=eyJpIjoiYzM4ZjQ2YWIzYmZkNDZ… ) / RFC ( https://sel4.atlassian.net/browse/RFC-8?atlOrigin=eyJpIjoiYzM4ZjQ2YWIzYmZkN… ) RFC-8 ( https://sel4.atlassian.net/browse/RFC-8?atlOrigin=eyJpIjoiYzM4ZjQ2YWIzYmZkN… ) Remove support for ARMv6, i.MX31 and KZM ( https://sel4.atlassian.net/browse/RFC-8?atlOrigin=eyJpIjoiYzM4ZjQ2YWIzYmZkN… ) Change By: Matthew Brecknell ( https://sel4.atlassian.net/secure/ViewProfile.jspa?accountId=557058%3Ad9d2f… ) h1. Summary This RFC proposes to remove seL4 support for KMC's KZM evaluation board, which used the freescale (now NXP) i.MX31 processor with an ARM1136 core. Since this is the only ARMv6 platform supported by seL4, this proposal would also remove support for ARMv6. h1. Motivation The KZM board has been unavailable for purchase for some years. The i.MX31 processor exited NXP's product longevity program in 2015. We previously asked the seL4 community \ [[1|https://sel4.discourse.group/t/should-we-continue-to-support-armv6-and-kzm-imx31/46],[2|https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/EQ27WYPJIN3KKRGB4VNXUZKJYL65IZ6J/],[3|https://github.com/seL4/seL4/issues/578]] if there are current users of the KZM platform. From the responses, we believe there is already consensus that there is little value in continuing support for KZM. With no known users, we are motivated to eliminate the overhead of maintaining support for KZM. Unlike all other platforms supported by seL4, KZM lacks sufficient registers for thread-local identifiers such as TLS_BASE and the IPC buffer address. For KZM alone, seL4 implements a workaround by mapping a special frame into each thread (the globals frame) to store these identifiers. As an example of the cost of maintaining support for KZM, the globals frame currently makes it difficult to uniformly describe the address space available to user-space programs. Additionally, the KZM board the seL4 Foundation has used for testing KZM support is no longer reliable, so we are currently only able to test using QEMU simulation. Although KZM was the original seL4 verification target, KZM support has not been verified since early 2016. Since we believe there is already consensus around the removal of KZM support, this RFC can be considered a formal last call for objections. h1. Guide-level explanation We propose to remove from the seL4: - * seL4 kernel build targets for the KZM board, i.MX31 processor, and ARMv6 architecture; - * any platform-specific code that is only required for those build targets, including drivers, device-tree specifications. Prior to removing support from seL4, we will remove code from other repositories that depend on seL4 support, including tests, benchmarks, and tools such as CAmkES. We propose to update the documentation on the docs.sel4.systems website, to show that the KZM board is no longer supported, and to show the last seL4 release version that included support. The impact of this change is that any current users of seL4 on the KZM board would not be able to use new releases of seL4 on the KZM board. They would most likely need to freeze the version of seL4 they use, and would therefore not be able to expect the usual level of support from the seL4 community. Since we are not aware of any users, we do not expect significant impact. h1. Reference-level explanation We have drafted a pull request to remove seL4 support for KZM, i.MX31 and ARMv6: - * [ https://github.com/seL4/seL4/pull/580 |https://github.com/seL4/seL4/pull/580] A number of related pull requests remove references from related repositories. Some of these are already merged, since the changes they make do not require an RFC process: - * [ https://github.com/seL4/seL4_libs/pull/46 |https://github.com/seL4/seL4_libs/pull/46] - * [ https://github.com/seL4/sel4test/pull/51 |https://github.com/seL4/sel4test/pull/51] - * [ https://github.com/seL4/sel4runtime/pull/13 |https://github.com/seL4/sel4runtime/pull/13] - * [ https://github.com/seL4/sel4bench/pull/7 |https://github.com/seL4/sel4bench/pull/7] * [https://github.com/seL4/camkes - tool/pull/92| https://github.com/seL4/camkes-tool/pull/92 ] - * [ https://github.com/seL4/seL4_projects_libs/pull/22 |https://github.com/seL4/seL4_projects_libs/pull/22] h1. Drawbacks Since the KZM board is the only ARMv6-based platform supported by seL4, this proposal implies the removal of ARMv6, even though later ARMv6 boards might would not require the same workaround as the KZM board. Removing ARMv6 will make it slightly harder to add a new ARMv6-based platform in the future. But it would not be prohibitively difficult, since the main difference between ARMv6 and ARMv7 support in seL4 is the workaround required for KZM. In any case, we believe that new ARM-based appliations of seL4 will most likely use ARMv7 or later, so the benefits of removing KZM support currently outweigh the drawbacks. h1. Rationale and alternatives We've already addressed the rationale for removing KZM support. One might ask why it's necessary to remove all references to ARMv6 when we remove support for KZM, since retaining ARMv6 references might make it easier to support other ARMv6 boards in the future. However, we do not think it makes sense to retain references to ARMv6 without a specific ARMv6 board to exercise them, and without a clear demand for ARMv6 support. Again, the cost of maintaining those references outweighs any clear benefit. h1. Prior art The Linux kernel removed support for the KZM board and i.MX31 processor in 2015. h1. Unresolved questions We are not aware of any unresolved questions, but welcome discussion on this RFC. ( https://sel4.atlassian.net/browse/RFC-8#add-comment?atlOrigin=eyJpIjoiYzM4Z… ) Add Comment ( https://sel4.atlassian.net/browse/RFC-8#add-comment?atlOrigin=eyJpIjoiYzM4Z… ) Get Jira notifications on your phone! Download the Jira Cloud app for Android ( https://play.google.com/store/apps/details?id=com.atlassian.android.jira.co… ) or iOS ( https://itunes.apple.com/app/apple-store/id1006972087?pt=696495&ct=EmailNot… ) This message was sent by Atlassian Jira (v1001.0.0-SNAPSHOT#100177- sha1:149c709 )

1 0

[JIRA] (RFC-8) Remove support for ARMv6, i.MX31 and KZM
by Matthew Brecknell (Jira) 16 Sep '21

16 Sep '21

1 0

[JIRA] (RFC-8) Remove support for KZM
by Matthew Brecknell (Jira) 15 Sep '21

15 Sep '21

Matthew Brecknell ( https://sel4.atlassian.net/secure/ViewProfile.jspa?accountId=557058%3Ad9d2f… ) *created* an issue RFCs ( https://sel4.atlassian.net/browse/RFC?atlOrigin=eyJpIjoiNjE4Y2IxOTJiYWU5NDl… ) / RFC ( https://sel4.atlassian.net/browse/RFC-8?atlOrigin=eyJpIjoiNjE4Y2IxOTJiYWU5N… ) RFC-8 ( https://sel4.atlassian.net/browse/RFC-8?atlOrigin=eyJpIjoiNjE4Y2IxOTJiYWU5N… ) Remove support for KZM ( https://sel4.atlassian.net/browse/RFC-8?atlOrigin=eyJpIjoiNjE4Y2IxOTJiYWU5N… ) Issue Type: RFC Assignee: Matthew Brecknell ( https://sel4.atlassian.net/secure/ViewProfile.jspa?accountId=557058%3Ad9d2f… ) Created: 15/Sep/21 7:04 PM Reporter: Matthew Brecknell ( https://sel4.atlassian.net/secure/ViewProfile.jspa?accountId=557058%3Ad9d2f… ) ******* Summary ******* This RFC proposes to remove seL4 support for KMC's KZM evaluation board, which used the freescale (now NXP) i.MX31 processor with an ARM1136 core. Since this is the only ARMv6 platform supported by seL4, this proposal would also remove support for ARMv6. ********** Motivation ********** The KZM board has been unavailable for purchase for some years. The i.MX31 processor exited NXP's product longevity program in 2015. We previously asked the seL4 community [ 1 ( https://sel4.discourse.group/t/should-we-continue-to-support-armv6-and-kzm-… ) ,[2|https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/EQ27WYPJIN3KKRGB4VNXUZKJYL65IZ6J/],[3|https://github.com/seL4/seL4/issues/578]] if there are current users of the KZM platform. From the responses, we believe there is already consensus that there is little value in continuing support for KZM. With no users, we are motivated to eliminate the overhead of maintaining support for KZM. Unlike all other platforms supported by seL4, KZM lacks sufficient registers for thread-local identifiers such as TLS_BASE and the IPC buffer address. For KZM alone, seL4 implements a workaround by mapping a special frame into each thread (the globals frame) to store these identifiers. As an example of the cost of maintaining support for KZM, the globals frame currently makes it difficult to uniformly describe the address space available to user-space programs. Additionally, the KZM board the seL4 Foundation has used for testing KZM support is no longer reliable, so we are currently only able to test using QEMU simulation. Although KZM was the original seL4 verification target, KZM support has not been verified since early 2016. Since we believe there is already consensus around the removal of KZM support, this RFC can be considered a formal last call for objections. *********************** Guide-level explanation *********************** We propose to remove from the seL4: * seL4 kernel build targets for the KZM board, i.MX31 processor, and ARMv6 architecture; * any platform-specific code that is only required for those build targets, including drivers, device-tree specifications. Prior to removing support from seL4, we will remove code from other repositories that depend on seL4 support, including tests, benchmarks, and tools such as CAmkES. We propose to update the documentation on the docs.sel4.systems website, to show that the KZM board is no longer supported, and to show the last seL4 release version that included support. The impact of this change is that any current users of seL4 on the KZM board would not be able to use new releases of seL4 on the KZM board. They would most likely need to freeze the version of seL4 they use, and would therefore not be able to expect the usual level of support from the seL4 community. Since we are not aware of any users, we do not expect significant impact. *************************** Reference-level explanation *************************** We have drafted a pull request to remove seL4 support for KZM, i.MX31 and ARMv6: * https://github.com/seL4/seL4/pull/580 A number of related pull requests remove references from related repositories. Some of these are already merged, since the changes they make do not require an RFC process: * https://github.com/seL4/seL4_libs/pull/46 * https://github.com/seL4/sel4test/pull/51 * https://github.com/seL4/sel4runtime/pull/13 * https://github.com/seL4/sel4bench/pull/7 * https://github.com/seL4/camkes-tool/pull/92 * https://github.com/seL4/seL4_projects_libs/pull/22 ********* Drawbacks ********* Since the KZM board is the only ARMv6-based platform supported by seL4, this proposal implies the removal of ARMv6, even though later ARMv6 boards might would not require the same workaround as the KZM board. Removing ARMv6 will make it slightly harder to add a new ARMv6-based platform in the future. But it would not be prohibitively difficult, since the main difference between ARMv6 and ARMv7 support in seL4 is the workaround required for KZM. In any case, we believe that new ARM-based appliations of seL4 will most likely use ARMv7 or later, so the benefits of removing KZM support currently outweigh the drawbacks. ************************** Rationale and alternatives ************************** We've already addressed the rationale for removing KZM support. One might ask why it's necessary to remove all references to ARMv6 when we remove support for KZM, since retaining ARMv6 references might make it easier to support other ARMv6 boards in the future. However, we do not think it makes sense to retain references to ARMv6 without a specific ARMv6 board to exercise them, and without a clear demand for ARMv6 support. Again, the cost of maintaining those references outweighs any clear benefit. ********* Prior art ********* The Linux kernel removed support for the KZM board and i.MX31 processor in 2015. ******************** Unresolved questions ******************** We are not aware of any unresolved questions, but welcome discussion on this RFC. ( https://sel4.atlassian.net/browse/RFC-8#add-comment?atlOrigin=eyJpIjoiNjE4Y… ) Add Comment ( https://sel4.atlassian.net/browse/RFC-8#add-comment?atlOrigin=eyJpIjoiNjE4Y… ) Get Jira notifications on your phone! Download the Jira Cloud app for Android ( https://play.google.com/store/apps/details?id=com.atlassian.android.jira.co… ) or iOS ( https://itunes.apple.com/app/apple-store/id1006972087?pt=696495&ct=EmailNot… ) This message was sent by Atlassian Jira (v1001.0.0-SNAPSHOT#100177- sha1:6b64421 )

1 0

[JIRA] (RFC-7) Removing CNode_Mutate
by Gerwin Klein (Jira) 22 Aug '21

22 Aug '21

Gerwin Klein ( https://sel4.atlassian.net/secure/ViewProfile.jspa?accountId=557058%3A53da0… ) *created* an issue RFCs ( https://sel4.atlassian.net/browse/RFC?atlOrigin=eyJpIjoiZTVmNzU0Y2NiZTc0NDk… ) / RFC ( https://sel4.atlassian.net/browse/RFC-7?atlOrigin=eyJpIjoiZTVmNzU0Y2NiZTc0N… ) RFC-7 ( https://sel4.atlassian.net/browse/RFC-7?atlOrigin=eyJpIjoiZTVmNzU0Y2NiZTc0N… ) Removing CNode_Mutate ( https://sel4.atlassian.net/browse/RFC-7?atlOrigin=eyJpIjoiZTVmNzU0Y2NiZTc0N… ) Issue Type: RFC Assignee: Gerwin Klein ( https://sel4.atlassian.net/secure/ViewProfile.jspa?accountId=557058%3A53da0… ) Created: 22/Aug/21 11:31 AM Reporter: Gerwin Klein ( https://sel4.atlassian.net/secure/ViewProfile.jspa?accountId=557058%3A53da0… ) Summary ------- This RFC proposes to remove the API seL4_CNode_Mutate() Motivation ---------- CNode_Mutate does not do what the manual describes (a combination of move and and setting badge). The only action CNode_Mutate can currently take that CNode_Move cannot take is setting the guard of a CNode , which can also be done via CNode_Mint (where CNode_Mint would be copying the cap – if you wanted the same effect, you could afterwards delete the cap it was copied from). Guide-level explanation ----------------------- seL4_CNode_Mutate() is mostly unused and has no use cases that cannot already be achieved with other API calls. The current description of seL4_CNode_Mutate() in the manual is incorrect. Drawbacks --------- I suspect there are no real drawbacks. It is theoretically possible that there is an application out there that makes extensive used of re-setting guards on CNodes while not copying the CNode caps, but that sounds unrealistic. Rationale --------- Different options would be to extend CNode_Mutate to allow changing badges, and possibly even to allow changing cap right. If we wanted to, we could even allow an in-place update. As the discussion in SELFOUR-136 indicates, mutating an existing cap is not a good fit for the cap model in general and makes reasoning about caps harder. The minimal action would be to do nothing and only update the manual to reflect that CNode_Mutate has almost no useful purpose. ( https://sel4.atlassian.net/browse/RFC-7#add-comment?atlOrigin=eyJpIjoiZTVmN… ) Add Comment ( https://sel4.atlassian.net/browse/RFC-7#add-comment?atlOrigin=eyJpIjoiZTVmN… ) Get Jira notifications on your phone! Download the Jira Cloud app for Android ( https://play.google.com/store/apps/details?id=com.atlassian.android.jira.co… ) or iOS ( https://itunes.apple.com/app/apple-store/id1006972087?pt=696495&ct=EmailNot… ) This message was sent by Atlassian Jira (v1001.0.0-SNAPSHOT#100174- sha1:8523140 )

1 0

[JIRA] (RFC-5) The seL4 Core Platform
by Gernot Heiser (Jira) 03 Jan '21

03 Jan '21

1 0

[JIRA] (RFC-5) The seL4 Core Platform
by Gernot Heiser (Jira) 03 Jan '21

03 Jan '21

1 0

[JIRA] (RFC-2) A dedicated C runtime for seL4
by Curtis Millar (Jira) 05 Apr '19

05 Apr '19

1 0

[JIRA] (RFC-3) Cross-platform thread-local storage support
by Curtis Millar (Jira) 05 Apr '19

05 Apr '19

1 0

[JIRA] (RFC-3) Cross-platform thread-local storage support
by Curtis Millar (Jira) 05 Apr '19

05 Apr '19

1 0

[JIRA] (RFC-3) Cross-platform thread-local storage support
by Curtis Millar (Jira) 25 Mar '19

25 Mar '19

1 0