From c6bcf9e453081cbbc984508ca82a43c4ef4490e1 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@data61.csiro.au>
Date: Tue, 10 Mar 2020 17:44:05 +0800
Subject: [PATCH] converted CAVEAT file content into .md

Adjusted headlines and comment syntax to markdown.
---
 CAVEATS-generic.md | 20 ++++++++++----------
 CAVEATS-ia32.md    | 33 +++++++++++++++++++--------------
 2 files changed, 29 insertions(+), 24 deletions(-)

diff --git a/CAVEATS-generic.md b/CAVEATS-generic.md
index 128524397..2bb2942a5 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 29e0c634b..834ca7db6 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
-- 
GitLab