diff --git a/CAVEATS-generic.md b/CAVEATS-generic.md index 12852439798ae5d142db2efc0e93aac6c5a36f6b..2bb2942a58344bc5ccdac84691ae396a2adc59be 100644 --- a/CAVEATS-generic.md +++ b/CAVEATS-generic.md @@ -1,12 +1,12 @@ -# -# Copyright 2014, General Dynamics C4 Systems -# -# SPDX-License-Identifier: GPL-2.0-only -# +<!-- + Copyright 2014, General Dynamics C4 Systems -This file lists known caveats in the seL4 API and implementation. + SPDX-License-Identifier: GPL-2.0-only +--> -* Implementation Correctness +# Known caveats in the seL4 API and implementation + +## Implementation Correctness Only the ARMv7 version on the imx6 platform of seL4 has the full stack of correctness proofs. This proof covers the functional behaviour of the C code of @@ -37,7 +37,7 @@ Proofs for the MCS version (mixed-criticality systems) and for seL4 on the RISC-V architecture are in progress. -* Real Time +## Real Time The default version of seL4 must be configured carefully for use in real-time requirements. It has a small number of potentially long-running kernel @@ -50,7 +50,7 @@ provides principled access control for execution time, but its formal verification is currently still in progress. -* IPC buffer in globals frame may be stale +## IPC buffer in globals frame may be stale When a thread invokes its own TCB object to (re-)register its IPC buffer and the thread is re-scheduled immediately, the userland IPC buffer pointer in the @@ -58,7 +58,7 @@ globals frame may still show the old value. It is updated on the next thread switch. -* Re-using Address Spaces (ARM and x86): +## Re-using Address Spaces (ARM and x86): Before an ASID/page directory/page table can be reused, all frame caps installed in it should be revoked. The kernel will not do this automatically diff --git a/CAVEATS-ia32.md b/CAVEATS-ia32.md index 29e0c634b3c127c313a19e564accfde875c35118..834ca7db6125f65375d4ecdecbc083191ad87ca5 100644 --- a/CAVEATS-ia32.md +++ b/CAVEATS-ia32.md @@ -1,21 +1,26 @@ -# -# Copyright 2014, General Dynamics C4 Systems -# -# SPDX-License-Identifier: GPL-2.0-only -# +<!-- + Copyright 2014, General Dynamics C4 Systems -* Intel VT-d (I/O MMU) support + SPDX-License-Identifier: GPL-2.0-only +--> + +# Caveats specific to seL4 on ia32 and ia64 + +## Intel VT-d (I/O MMU) support Intel VT-d support in seL4 was tested for the following chipsets: -- Intel Q35 Express -- Intel 5500 + + - Intel Q35 Express + - Intel 5500 On other chipsets with Intel VT-d support, seL4 might: -- complain and disable IOMMU support -- hang during bootstrapping -- have some weird behaviour during runtime + + - complain and disable IOMMU support + - hang during bootstrapping + - have some weird behaviour during runtime In any case, the workaround is to disable VT-d support, either: -- in the BIOS, or -- by including "disable_iommu" into the MultiBoot (e.g. GRUB) command line - as described in the seL4 documentation + + - in the BIOS, or + - by including `disable_iommu` into the MultiBoot (e.g. GRUB) command line + as described in the seL4 documentation