Skip to content

Commit

Permalink
roadmap: update AARCH64 and Multikernel status
Browse files Browse the repository at this point in the history
- remove multikernel item as completed (new mk item to be added when
  funding is available)
- update AARCH64 status to FC complete, integrity ongoing
- update TX2 board status

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
  • Loading branch information
lsf37 committed Mar 29, 2024
1 parent 03d2420 commit e06f0ae
Show file tree
Hide file tree
Showing 3 changed files with 6 additions and 12 deletions.
2 changes: 1 addition & 1 deletion Hardware/JetsonTX2.md
Expand Up @@ -9,7 +9,7 @@ virtualization: "Yes"
iommu: "Yes"
soc: NVIDIA Tegra X2
cpu: Cortex-A57 Quad, Dual NVIDIA Denver
Status: "[Ongoing](/projects/sel4/verified-configurations.html#aarch64)"
Status: "FC complete, [Integrity ongoing](/projects/sel4/verified-configurations.html#aarch64)"
Contrib: Data61
Maintained: seL4 Foundation
SPDX-License-Identifier: CC-BY-SA-4.0
Expand Down
10 changes: 2 additions & 8 deletions _data/projects/l4v.yml
Expand Up @@ -25,13 +25,7 @@ roadmap:
roadmap_type: in-progress
- name: AARCH64
display_name: AArch64 port
description: Functional correctness proofs for the AArch64 port of seL4.
description: Functional correctness proofs for the AArch64 port of seL4 completed. Integrity (access control) ongoing.
assigned: Proofcraft
status: C verification to complete Q1/24
roadmap_type: in-progress
- name: Multikernel
display_name: Multikernel
description: Functional correctness proofs for static multikernel config of seL4.
assigned: Proofcraft
status: concurrency framework ongoing
status: Integrity verification to complete Q1/25
roadmap_type: in-progress
6 changes: 3 additions & 3 deletions projects/sel4/verified-configurations.md
Expand Up @@ -65,8 +65,8 @@ address translation for devices (System MMU or IOMMU), debug/profiling
interfaces, or the kernel startup at boot.

The proofs for RISCV64\_MCS/ARM\_MCS (mixed-criticality extensions to real-time
seL4 features), as well as proofs for AARCH64 are in progress. Refer to the
[roadmap](/projects/roadmap.html) for status and upcoming features.
seL4 features), as well as security proofs for AARCH64 are in progress. Refer to
the [roadmap](/projects/roadmap.html) for status and upcoming features.

## ARM Sabre Lite

Expand Down Expand Up @@ -121,7 +121,7 @@ Mixed-Criticality-Systems API | Yes
| Platform | Tegra X2 (Jetson TX2)
| Floating-point support | Yes
| Hypervisor mode | Yes
| **Verified properties** | in progress
| **Verified properties** | functional correctness, incl fast path completed; integrity proof in progress

## RISCV64

Expand Down

0 comments on commit e06f0ae

Please sign in to comment.