Merge remote-tracking branch 'spacebeaker/upstream' into update

Change-Id: I5e036b1b8f7408c644f1dfeac6e4bb04ae2e0cac
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 25cddb5..1e29fe1 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -11,14 +11,19 @@
 jobs:
   run-tests:
     strategy:
-      matrix: 
+      matrix:
         build-type: [ debug, release ]
         board: [ sail, ibex-safe-simulator ]
         include:
+          - sonata: false
           - build-type: debug
             build-flags: --debug-loader=y --debug-scheduler=y --debug-allocator=y -m debug
           - build-type: release
             build-flags: --debug-loader=n --debug-scheduler=n --debug-allocator=n -m release --stack-usage-check-allocator=y --stack-usage-check-scheduler=y
+          - board: sonata-simulator
+            build-type: release
+            build-flags: --debug-loader=n --debug-scheduler=n --debug-allocator=n -m release --stack-usage-check-allocator=y --stack-usage-check-scheduler=y --testing-model-output=y
+            sonata: true
       fail-fast: false
     runs-on: ubuntu-latest
     container:
@@ -26,7 +31,7 @@
       options: --user 1001
     steps:
     - name: Checkout repository and submodules
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         submodules: recursive
     - name: Build tests
@@ -35,6 +40,8 @@
         xmake f --board=${{ matrix.board }} --sdk=/cheriot-tools/ ${{ matrix.build-flags }}
         xmake
     - name: Run tests
+      # Test suite needs HyperRAM support to be added to RTOS because SRAM is not big enough.
+      if: ${{ !matrix.sonata }}
       run: |
         cd tests
         xmake run
@@ -47,7 +54,7 @@
           xmake f --board=${{ matrix.board }} --sdk=/cheriot-tools/ ${{ matrix.build-flags }}
           xmake
         done
-    - name: Run examples 
+    - name: Run examples
       run: |
         set -e
         for example_dir in $PWD/examples/*/; do
@@ -73,7 +80,7 @@
       options: --user 1001
     steps:
     - name: Checkout repository and submodules
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         submodules: recursive
     - name: Run clang-format and clang-tidy
diff --git a/README.md b/README.md
index d5da6b3..1491256 100644
--- a/README.md
+++ b/README.md
@@ -108,8 +108,8 @@
 
 ## Trademarks
 
-This project may contain trademarks or logos for projects, products, or services. Authorized use of Microsoft 
-trademarks or logos is subject to and must follow 
+This project may contain trademarks or logos for projects, products, or services. Authorized use of Microsoft
+trademarks or logos is subject to and must follow
 [Microsoft's Trademark & Brand Guidelines](https://www.microsoft.com/en-us/legal/intellectualproperty/trademarks/usage/general).
 Use of Microsoft trademarks or logos in modified versions of this project must not cause confusion or imply Microsoft sponsorship.
 Any use of third-party trademarks or logos are subject to those third-party's policies.
diff --git a/SECURITY.md b/SECURITY.md
index e138ec5..9dc6316 100644
--- a/SECURITY.md
+++ b/SECURITY.md
@@ -14,7 +14,7 @@
 
 If you prefer to submit without logging in, send email to [secure@microsoft.com](mailto:secure@microsoft.com).  If possible, encrypt your message with our PGP key; please download it from the [Microsoft Security Response Center PGP Key page](https://aka.ms/opensource/security/pgpkey).
 
-You should receive a response within 24 hours. If for some reason you do not, please follow up via email to ensure we received your original message. Additional information can be found at [microsoft.com/msrc](https://aka.ms/opensource/security/msrc). 
+You should receive a response within 24 hours. If for some reason you do not, please follow up via email to ensure we received your original message. Additional information can be found at [microsoft.com/msrc](https://aka.ms/opensource/security/msrc).
 
 Please include the requested information listed below (as much as you can provide) to help us better understand the nature and scope of the possible issue:
 
diff --git a/SUPPORT.md b/SUPPORT.md
index cd36070..967091d 100644
--- a/SUPPORT.md
+++ b/SUPPORT.md
@@ -2,14 +2,14 @@
 

 This project is open sourced as an ongoing research project to facilitate wider collaboration.

 

-## How to file issues and get help  

+## How to file issues and get help

 

-This project uses GitHub Issues to track bugs and feature requests. Please search the existing 

-issues before filing new issues to avoid duplicates.  For new issues, file your bug or 

+This project uses GitHub Issues to track bugs and feature requests. Please search the existing

+issues before filing new issues to avoid duplicates.  For new issues, file your bug or

 feature request as a new Issue.

 

 For help and questions about using this project, please use the GitHub Discussions tab.

 

-## Microsoft Support Policy  

+## Microsoft Support Policy

 

 Support for this project is limited to the resources listed above.

diff --git a/examples/04.temporal_safety/README.md b/examples/04.temporal_safety/README.md
index 23911b3..b07a370 100644
--- a/examples/04.temporal_safety/README.md
+++ b/examples/04.temporal_safety/README.md
@@ -42,9 +42,9 @@
 
 This is the expected set for heap memory.
 Any of these can be cleared from a copy of the pointer before passing it to other code if you wish to restrict what can be done to an object with that pointer.
-For example, if you remove `W` and `M` permissions from a pointer that you pass as a parameter then you have a guarantee that nothing reachable from the pointer will be mutated.
-Similarly, if you remove `G` and `L` then you have the guarantee that nothing reachable from the pointer will be captured.
-If you remove `G` but not `L` then you have the weaker guarantee that the pointer that you passed will not be captured but pointers reachable from it might be.
+For example, if you remove `W` and `m` permissions from a pointer that you pass as a parameter then you have a guarantee that nothing reachable from the pointer will be mutated.
+Similarly, if you remove `G` and `g` then you have the guarantee that nothing reachable from the pointer will be captured.
+If you remove `G` but not `g` then you have the weaker guarantee that the pointer that you passed will not be captured but pointers reachable from it might be.
 
 The next three use cases show the handling of a sub-object, a capability that references a sub-range of the allocation.
 
diff --git a/examples/10.audit/README.md b/examples/10.audit/README.md
index cd8d379..8bc4c62 100644
--- a/examples/10.audit/README.md
+++ b/examples/10.audit/README.md
@@ -15,7 +15,7 @@
 Note: For all of the `cheriot-audit` examples, we'll assume that you're running a command something like this:
 
 ```sh
-$ cheriot-audit --board=../../sdk/boards/sail.json --firmware-report=build/cheriot/cheriot/release/caesar_example.json --module=caesar.rego  --query '{query}' | jq
+$ cheriot-audit --board=../../sdk/boards/sail.json --firmware-report=build/cheriot/cheriot/release/audit.json --module=caesar.rego  --query '{query}' | jq
 ```
 
 You may need to specify a full path to cheriot-audit (it is in `/cheriot-tools/bin` in the dev container).
diff --git a/examples/10.audit/xmake.lua b/examples/10.audit/xmake.lua
index 71cb288..df3934a 100644
--- a/examples/10.audit/xmake.lua
+++ b/examples/10.audit/xmake.lua
@@ -23,7 +23,7 @@
     add_files("consumer.cc")
 
 -- Firmware image for the example.
-firmware("caesar_example")
+firmware("audit")
     -- Both compartments require memcpy
     add_deps("freestanding", "debug", "string")
     add_deps("entry", "caesar")
diff --git a/scripts/model_output/sonata-simulator/examples/audit.txt b/scripts/model_output/sonata-simulator/examples/audit.txt
new file mode 100644
index 0000000..f2abe0c
--- /dev/null
+++ b/scripts/model_output/sonata-simulator/examples/audit.txt
@@ -0,0 +1,3 @@
+Producer: Encrypting message 'Hello, World!'
+Entry compartment: Received encrypted message: 'Ifmmp-!Xpsme"' (13 bytes)
+Consumer: Decrypted message: 'Hello, World!'
diff --git a/scripts/model_output/sonata-simulator/examples/error_handling.txt b/scripts/model_output/sonata-simulator/examples/error_handling.txt
new file mode 100644
index 0000000..ed3cf77
--- /dev/null
+++ b/scripts/model_output/sonata-simulator/examples/error_handling.txt
@@ -0,0 +1,5 @@
+UART compartment: Message provided by caller: hello
+UART compartment: Detected BoundsViolation(0x1) trying to write to UART.  Register CS0(0x8) contained invalid value: 0x101b10 (v:1 0x101b0b-0x101b10 l:0x5 o:0x0 p: - RWcgml -- ---)
+UART compartment: Message provided by caller: 
+UART compartment: Detected PermitLoadViolation(0x12) trying to write to UART.  Register CS0(0x8) contained invalid value: 0x101b0b (v:1 0x101b0b-0x101b10 l:0x5 o:0x0 p: - -W---- -- ---)
+UART compartment: Message provided by caller: Non-malicious string
diff --git a/scripts/model_output/sonata-simulator/examples/hello_compartment.txt b/scripts/model_output/sonata-simulator/examples/hello_compartment.txt
new file mode 100644
index 0000000..31e3a2a
--- /dev/null
+++ b/scripts/model_output/sonata-simulator/examples/hello_compartment.txt
@@ -0,0 +1,2 @@
+UART compartment: Hello world
+UART compartment: Hello from the stack
diff --git a/scripts/model_output/sonata-simulator/examples/hello_safe_compartment.txt b/scripts/model_output/sonata-simulator/examples/hello_safe_compartment.txt
new file mode 100644
index 0000000..0ec9819
--- /dev/null
+++ b/scripts/model_output/sonata-simulator/examples/hello_safe_compartment.txt
Binary files differ
diff --git a/scripts/model_output/sonata-simulator/examples/hello_world.txt b/scripts/model_output/sonata-simulator/examples/hello_world.txt
new file mode 100644
index 0000000..bcb68d3
--- /dev/null
+++ b/scripts/model_output/sonata-simulator/examples/hello_world.txt
@@ -0,0 +1 @@
+Hello world compartment: Hello world
diff --git a/scripts/model_output/sonata-simulator/examples/javascript.txt b/scripts/model_output/sonata-simulator/examples/javascript.txt
new file mode 100644
index 0000000..6fc8329
--- /dev/null
+++ b/scripts/model_output/sonata-simulator/examples/javascript.txt
@@ -0,0 +1,10 @@
+Hello, World!
+array[0] = 2
+array[1] = 4
+array[2] = 6
+array[3] = 8
+array[4] = 10
+JavaScript hello compartment: Microvium is using 0x1a6 bytes of memory, including 0x60 bytes of heap
+JavaScript hello compartment: Running GC
+JavaScript hello compartment: Microvium is using 0x86 bytes of memory, including 0x14 bytes of heap
+JavaScript hello compartment: Peak heap used: 0x60 bytes, peak stack used: 0x32 bytes
diff --git a/scripts/model_output/sonata-simulator/examples/memory_safety.txt b/scripts/model_output/sonata-simulator/examples/memory_safety.txt
new file mode 100644
index 0000000..4ebed1f
--- /dev/null
+++ b/scripts/model_output/sonata-simulator/examples/memory_safety.txt
@@ -0,0 +1,17 @@
+Memory safety compartment: Demonstrate memory safety
+Memory safety compartment: Trigger stack linear overflow
+Memory safety compartment: Detected error in instruction 0x107cac (v:0 0x107820-0x108820 l:0x1000 o:0x0 p: G R-cgm- X- ---)
+Memory safety compartment: Detected BoundsViolation(0x1): Register CA1(0xb) contained invalid value: 0x101ad0 (v:1 0x101ad0-0x101b10 l:0x40 o:0x0 p: - RWcgml -- ---)
+Memory safety compartment: Trigger heap linear overflow
+Memory safety compartment: Detected error in instruction 0x107ab2 (v:0 0x107820-0x108820 l:0x1000 o:0x0 p: G R-cgm- X- ---)
+Memory safety compartment: Detected BoundsViolation(0x1): Register CA0(0xa) contained invalid value: 0x109910 (v:1 0x109910-0x109a10 l:0x100 o:0x0 p: G RWcgm- -- ---)
+Memory safety compartment: Trigger heap nonlinear overflow
+Memory safety compartment: Detected error in instruction 0x107b0c (v:0 0x107820-0x108820 l:0x1000 o:0x0 p: G R-cgm- X- ---)
+Memory safety compartment: Detected BoundsViolation(0x1): Register CA0(0xa) contained invalid value: 0x109a18 (v:1 0x109a18-0x109b18 l:0x100 o:0x0 p: G RWcgm- -- ---)
+Memory safety compartment: Trigger heap use after free
+Memory safety compartment: Detected error in instruction 0x107a58 (v:0 0x107820-0x108820 l:0x1000 o:0x0 p: G R-cgm- X- ---)
+Memory safety compartment: Detected TagViolation(0x2): Register CA0(0xa) contained invalid value: 0x109b20 (v:0 0x109b20-0x109c20 l:0x100 o:0x0 p: G RWcgm- -- ---)
+Memory safety compartment: Trigger storing a stack pointer 0x101ad0 (v:1 0x101ad0-0x101ae0 l:0x10 o:0x0 p: - RWcgml -- ---) into global
+Memory safety compartment: tmp: 0x101ad0 (v:0 0x101ad0-0x101ae0 l:0x10 o:0x0 p: - RWcgml -- ---)
+Memory safety compartment: Detected error in instruction 0x107a28 (v:0 0x107820-0x108820 l:0x1000 o:0x0 p: G R-cgm- X- ---)
+Memory safety compartment: Detected TagViolation(0x2): Register CS0(0x8) contained invalid value: 0x101ad0 (v:0 0x101ad0-0x101ae0 l:0x10 o:0x0 p: - RWcgml -- ---)
diff --git a/scripts/model_output/sonata-simulator/examples/producer-consumer.txt b/scripts/model_output/sonata-simulator/examples/producer-consumer.txt
new file mode 100644
index 0000000..7a77111
--- /dev/null
+++ b/scripts/model_output/sonata-simulator/examples/producer-consumer.txt
@@ -0,0 +1,203 @@
+Consumer: Queue set to 0x10a720 (v:1 0x10a720-0x10a778 l:0x58 o:0xb p: G RWcgm- -- ---)
+Producer: Starting producer loop
+Consumer: Waiting for messages
+Consumer: Read 1 from queue
+Consumer: Read 2 from queue
+Consumer: Read 3 from queue
+Consumer: Read 4 from queue
+Consumer: Read 5 from queue
+Consumer: Read 6 from queue
+Consumer: Read 7 from queue
+Consumer: Read 8 from queue
+Consumer: Read 9 from queue
+Consumer: Read 10 from queue
+Consumer: Read 11 from queue
+Consumer: Read 12 from queue
+Consumer: Read 13 from queue
+Consumer: Read 14 from queue
+Consumer: Read 15 from queue
+Consumer: Read 16 from queue
+Consumer: Read 17 from queue
+Consumer: Read 18 from queue
+Consumer: Read 19 from queue
+Consumer: Read 20 from queue
+Consumer: Read 21 from queue
+Consumer: Read 22 from queue
+Consumer: Read 23 from queue
+Consumer: Read 24 from queue
+Consumer: Read 25 from queue
+Consumer: Read 26 from queue
+Consumer: Read 27 from queue
+Consumer: Read 28 from queue
+Consumer: Read 29 from queue
+Consumer: Read 30 from queue
+Consumer: Read 31 from queue
+Consumer: Read 32 from queue
+Consumer: Read 33 from queue
+Consumer: Read 34 from queue
+Consumer: Read 35 from queue
+Consumer: Read 36 from queue
+Consumer: Read 37 from queue
+Consumer: Read 38 from queue
+Consumer: Read 39 from queue
+Consumer: Read 40 from queue
+Consumer: Read 41 from queue
+Consumer: Read 42 from queue
+Consumer: Read 43 from queue
+Consumer: Read 44 from queue
+Consumer: Read 45 from queue
+Consumer: Read 46 from queue
+Consumer: Read 47 from queue
+Consumer: Read 48 from queue
+Consumer: Read 49 from queue
+Consumer: Read 50 from queue
+Consumer: Read 51 from queue
+Consumer: Read 52 from queue
+Consumer: Read 53 from queue
+Consumer: Read 54 from queue
+Consumer: Read 55 from queue
+Consumer: Read 56 from queue
+Consumer: Read 57 from queue
+Consumer: Read 58 from queue
+Consumer: Read 59 from queue
+Consumer: Read 60 from queue
+Consumer: Read 61 from queue
+Consumer: Read 62 from queue
+Consumer: Read 63 from queue
+Consumer: Read 64 from queue
+Consumer: Read 65 from queue
+Consumer: Read 66 from queue
+Consumer: Read 67 from queue
+Consumer: Read 68 from queue
+Consumer: Read 69 from queue
+Consumer: Read 70 from queue
+Consumer: Read 71 from queue
+Consumer: Read 72 from queue
+Consumer: Read 73 from queue
+Consumer: Read 74 from queue
+Consumer: Read 75 from queue
+Consumer: Read 76 from queue
+Consumer: Read 77 from queue
+Consumer: Read 78 from queue
+Consumer: Read 79 from queue
+Consumer: Read 80 from queue
+Consumer: Read 81 from queue
+Consumer: Read 82 from queue
+Consumer: Read 83 from queue
+Consumer: Read 84 from queue
+Consumer: Read 85 from queue
+Consumer: Read 86 from queue
+Consumer: Read 87 from queue
+Consumer: Read 88 from queue
+Consumer: Read 89 from queue
+Consumer: Read 90 from queue
+Consumer: Read 91 from queue
+Consumer: Read 92 from queue
+Consumer: Read 93 from queue
+Consumer: Read 94 from queue
+Consumer: Read 95 from queue
+Consumer: Read 96 from queue
+Consumer: Read 97 from queue
+Consumer: Read 98 from queue
+Consumer: Read 99 from queue
+Consumer: Read 100 from queue
+Consumer: Read 101 from queue
+Consumer: Read 102 from queue
+Consumer: Read 103 from queue
+Consumer: Read 104 from queue
+Consumer: Read 105 from queue
+Consumer: Read 106 from queue
+Consumer: Read 107 from queue
+Consumer: Read 108 from queue
+Consumer: Read 109 from queue
+Consumer: Read 110 from queue
+Consumer: Read 111 from queue
+Consumer: Read 112 from queue
+Consumer: Read 113 from queue
+Consumer: Read 114 from queue
+Consumer: Read 115 from queue
+Consumer: Read 116 from queue
+Consumer: Read 117 from queue
+Consumer: Read 118 from queue
+Consumer: Read 119 from queue
+Consumer: Read 120 from queue
+Consumer: Read 121 from queue
+Consumer: Read 122 from queue
+Consumer: Read 123 from queue
+Consumer: Read 124 from queue
+Consumer: Read 125 from queue
+Consumer: Read 126 from queue
+Consumer: Read 127 from queue
+Consumer: Read 128 from queue
+Consumer: Read 129 from queue
+Consumer: Read 130 from queue
+Consumer: Read 131 from queue
+Consumer: Read 132 from queue
+Consumer: Read 133 from queue
+Consumer: Read 134 from queue
+Consumer: Read 135 from queue
+Consumer: Read 136 from queue
+Consumer: Read 137 from queue
+Consumer: Read 138 from queue
+Consumer: Read 139 from queue
+Consumer: Read 140 from queue
+Consumer: Read 141 from queue
+Consumer: Read 142 from queue
+Consumer: Read 143 from queue
+Consumer: Read 144 from queue
+Consumer: Read 145 from queue
+Consumer: Read 146 from queue
+Consumer: Read 147 from queue
+Consumer: Read 148 from queue
+Consumer: Read 149 from queue
+Consumer: Read 150 from queue
+Consumer: Read 151 from queue
+Consumer: Read 152 from queue
+Consumer: Read 153 from queue
+Consumer: Read 154 from queue
+Consumer: Read 155 from queue
+Consumer: Read 156 from queue
+Consumer: Read 157 from queue
+Consumer: Read 158 from queue
+Consumer: Read 159 from queue
+Consumer: Read 160 from queue
+Consumer: Read 161 from queue
+Consumer: Read 162 from queue
+Consumer: Read 163 from queue
+Consumer: Read 164 from queue
+Consumer: Read 165 from queue
+Consumer: Read 166 from queue
+Consumer: Read 167 from queue
+Consumer: Read 168 from queue
+Consumer: Read 169 from queue
+Consumer: Read 170 from queue
+Consumer: Read 171 from queue
+Consumer: Read 172 from queue
+Consumer: Read 173 from queue
+Consumer: Read 174 from queue
+Consumer: Read 175 from queue
+Consumer: Read 176 from queue
+Consumer: Read 177 from queue
+Consumer: Read 178 from queue
+Consumer: Read 179 from queue
+Consumer: Read 180 from queue
+Consumer: Read 181 from queue
+Consumer: Read 182 from queue
+Producer: Producer sent all messages to consumer
+Consumer: Read 183 from queue
+Consumer: Read 184 from queue
+Consumer: Read 185 from queue
+Consumer: Read 186 from queue
+Consumer: Read 187 from queue
+Consumer: Read 188 from queue
+Consumer: Read 189 from queue
+Consumer: Read 190 from queue
+Consumer: Read 191 from queue
+Consumer: Read 192 from queue
+Consumer: Read 193 from queue
+Consumer: Read 194 from queue
+Consumer: Read 195 from queue
+Consumer: Read 196 from queue
+Consumer: Read 197 from queue
+Consumer: Read 198 from queue
+Consumer: Read 199 from queue
diff --git a/scripts/model_output/sonata-simulator/examples/sealing.txt b/scripts/model_output/sonata-simulator/examples/sealing.txt
new file mode 100644
index 0000000..f6d7fd9
--- /dev/null
+++ b/scripts/model_output/sonata-simulator/examples/sealing.txt
@@ -0,0 +1,5 @@
+Identifier service: Allocated identifier, sealed capability: 0x109410 (v:1 0x109410-0x109420 l:0x10 o:0xb p: G RWcgm- -- ---)
+unsealed capability: 0x109418 (v:1 0x109418-0x109420 l:0x8 o:0x0 p: G RWcgm- -- ---)
+Caller compartment: Allocated identifier to hold the value 42: 0x109410 (v:1 0x109410-0x109420 l:0x10 o:0xb p: G RWcgm- -- ---)
+Caller compartment: Value is 42
+Caller compartment: Dangling pointer: 0x109410 (v:0 0x109410-0x109420 l:0x10 o:0xb p: G RWcgm- -- ---)
diff --git a/scripts/model_output/sonata-simulator/examples/temporal_safety.txt b/scripts/model_output/sonata-simulator/examples/temporal_safety.txt
new file mode 100644
index 0000000..37f990e
--- /dev/null
+++ b/scripts/model_output/sonata-simulator/examples/temporal_safety.txt
@@ -0,0 +1,52 @@
+Allocating compartment: ----- Simple Case -----
+Allocating compartment: Allocated: 0x109910 (v:1 0x109910-0x109940 l:0x30 o:0x0 p: G RWcgm- -- ---)
+Allocating compartment: Use after free: 0x109910 (v:0 0x109910-0x109940 l:0x30 o:0x0 p: G RWcgm- -- ---)
+Allocating compartment: ----- Sub object -----
+Allocating compartment: Allocated : 0x109948 (v:1 0x109948-0x1099b0 l:0x68 o:0x0 p: G RWcgm- -- ---)
+Allocating compartment: Sub Object: 0x109961 (v:1 0x109961-0x109993 l:0x32 o:0x0 p: G RWcgm- -- ---)
+Allocating compartment: heap quota: 3984
+Allocating compartment: After free of sub object
+Allocating compartment: Allocated : 0x109948 (v:1 0x109948-0x1099b0 l:0x68 o:0x0 p: G RWcgm- -- ---)
+Allocating compartment: Sub Object: 0x109961 (v:1 0x109961-0x109993 l:0x32 o:0x0 p: G RWcgm- -- ---)
+Allocating compartment: heap quota: 3984
+Allocating compartment: After free of allocation
+Allocating compartment: Allocated : 0x109948 (v:0 0x109948-0x1099b0 l:0x68 o:0x0 p: G RWcgm- -- ---)
+Allocating compartment: Sub Object: 0x109961 (v:0 0x109961-0x109993 l:0x32 o:0x0 p: G RWcgm- -- ---)
+Allocating compartment: heap quota: 4096
+Allocating compartment: ----- Sub object with a claim -----
+Allocating compartment: Allocated : 0x1099b8 (v:1 0x1099b8-0x109a20 l:0x68 o:0x0 p: G RWcgm- -- ---)
+Allocating compartment: Sub Object: 0x1099d1 (v:1 0x1099d1-0x109a03 l:0x32 o:0x0 p: G RWcgm- -- ---)
+Allocating compartment: heap quota: 3984
+Allocating compartment: heap quota after claim: 3968
+Allocating compartment: After free of allocation
+Allocating compartment: Allocated : 0x1099b8 (v:1 0x1099b8-0x109a20 l:0x68 o:0x0 p: G RWcgm- -- ---)
+Allocating compartment: Sub Object: 0x1099d1 (v:1 0x1099d1-0x109a03 l:0x32 o:0x0 p: G RWcgm- -- ---)
+Allocating compartment: heap quota: 3968
+Allocating compartment: After free of sub object
+Allocating compartment: Allocated : 0x1099b8 (v:0 0x1099b8-0x109a20 l:0x68 o:0x0 p: G RWcgm- -- ---)
+Allocating compartment: Sub Object: 0x1099d1 (v:0 0x1099d1-0x109a03 l:0x32 o:0x0 p: G RWcgm- -- ---)
+Allocating compartment: heap quota: 4096
+Allocating compartment: ----- Sub object with a fast claim -----
+Allocating compartment: Allocated : 0x109a38 (v:1 0x109a38-0x109aa0 l:0x68 o:0x0 p: G RWcgm- -- ---)
+Allocating compartment: Sub Object: 0x109a51 (v:1 0x109a51-0x109a83 l:0x32 o:0x0 p: G RWcgm- -- ---)
+Allocating compartment: heap quota: 3984
+Allocating compartment: After free
+Allocating compartment: Allocated : 0x109a38 (v:0 0x109a38-0x109aa0 l:0x68 o:0x0 p: G RWcgm- -- ---)
+Allocating compartment: Sub Object: 0x109a51 (v:0 0x109a51-0x109a83 l:0x32 o:0x0 p: G RWcgm- -- ---)
+Allocating compartment: heap quota: 4096
+Allocating compartment: ----- Claim in another compartment -----
+Allocating compartment: Allocated : 0x109aa8 (v:1 0x109aa8-0x109ab8 l:0x10 o:0x0 p: G RWcgm- -- ---)
+Allocating compartment: heap quota: 4072
+Claimant compartment: Initial quota: 4096
+Claimant compartment: Make Claim : 0x109aa8 (v:1 0x109aa8-0x109ab8 l:0x10 o:0x0 p: G RWcgm- -- ---)
+Claimant compartment: heap quota: 4056
+Allocating compartment: After free: 0x109aa8 (v:1 0x109aa8-0x109ab8 l:0x10 o:0x0 p: G RWcgm- -- ---)
+Allocating compartment: heap quota: 4096
+Claimant compartment: Show Claim : 0x109aa8 (v:1 0x109aa8-0x109ab8 l:0x10 o:0x0 p: G RWcgm- -- ---)
+Claimant compartment: Initial quota: 4056
+Claimant compartment: Make Claim : 0x109ad0 (v:1 0x109ad0-0x109ae0 l:0x10 o:0x0 p: G RWcgm- -- ---)
+Claimant compartment: heap quota: 4056
+Allocating compartment: After make claim
+Allocating compartment: x: 0x109aa8 (v:0 0x109aa8-0x109ab8 l:0x10 o:0x0 p: G RWcgm- -- ---)
+Allocating compartment: y: 0x109ad0 (v:1 0x109ad0-0x109ae0 l:0x10 o:0x0 p: G RWcgm- -- ---)
+Claimant compartment: Show Claim : 0x109ad0 (v:1 0x109ad0-0x109ae0 l:0x10 o:0x0 p: G RWcgm- -- ---)
diff --git a/scripts/run-sonata-sim.sh b/scripts/run-sonata-sim.sh
new file mode 100755
index 0000000..1b4c1a3
--- /dev/null
+++ b/scripts/run-sonata-sim.sh
@@ -0,0 +1,51 @@
+#!/bin/bash
+
+set -e
+
+# Specify the default environment variables if they haven't been already.
+: "${SONATA_SIMULATOR:=/cheriot-tools/bin/sonata_simulator}"
+: "${SONATA_SIMULATOR_BOOT_STUB:=/cheriot-tools/elf/sonata_simulator_boot_stub}"
+: "${SONATA_SIMULATOR_UART_LOG=uart0.log}"
+
+if [ -z "$1" ] ; then
+	echo You must specify an elf file to run.
+	exit 1
+fi
+
+if [ ! -x "${SONATA_SIMULATOR}" ] ; then
+	echo Unable to locate Sonata simulator, please set SONATA_SIMULATOR to the full path of the simulator.
+	exit 2
+fi
+
+if [ ! -x "${SONATA_SIMULATOR_BOOT_STUB}" ] ; then
+	echo Unable to locate Sonata simulator boot stub, please set SONATA_SIMULATOR_BOOT_STUB to the full path of the boot stub.
+	exit 3
+fi
+
+# Remove old uart log
+rm -f "${SONATA_SIMULATOR_UART_LOG}"
+
+# If a second argument is provided, check content of UART log.
+if [ -n "$2" ] ; then
+	# Run the simulator in the background.
+	${SONATA_SIMULATOR} -E "${SONATA_SIMULATOR_BOOT_STUB}" -E "$1" &
+	LOOP_TRACKER=0
+	while (( LOOP_TRACKER <= 60 ))
+	do
+		sleep 1s
+		# Returns 0 if found and 1 if not.
+		MATCH_FOUND=$(grep -q -F -f "$2" "${SONATA_SIMULATOR_UART_LOG}"; echo $?)
+		if (( MATCH_FOUND == 0 )) ; then
+			# Match was found so exit with success
+			pkill -P $$
+			exit 0
+		fi
+		LOOP_TRACKER=$((LOOP_TRACKER+1))
+	done
+	# Timeout was hit so no success.
+	pkill -P $$
+	exit 4
+else
+	# If there is no second argument, run simulator in foreground.
+	${SONATA_SIMULATOR} -E "${SONATA_SIMULATOR_BOOT_STUB}" -E "$1"
+fi
diff --git a/sdk/boards/ibex-safe-simulator.json b/sdk/boards/ibex-safe-simulator.json
index 0331598..87ac417 100644
--- a/sdk/boards/ibex-safe-simulator.json
+++ b/sdk/boards/ibex-safe-simulator.json
@@ -40,8 +40,8 @@
         "IBEX_SAFE"
     ],
     "driver_includes" : [
-        "../include/platform/generic-riscv",
-        "../include/platform/ibex"
+        "../include/platform/ibex",
+        "../include/platform/generic-riscv"
     ],
     "timer_hz" : 100000,
     "tickrate_hz" : 10,
diff --git a/sdk/boards/sail.json b/sdk/boards/sail.json
index 2e102c8..95e1689 100644
--- a/sdk/boards/sail.json
+++ b/sdk/boards/sail.json
@@ -27,7 +27,10 @@
             "priority": 2
         }
     ],
-    "defines" : "SAIL",
+    "defines" : [
+        "SAIL",
+        "RISCV_HTIF"
+    ],
     "driver_includes" : [
         "../include/platform/generic-riscv"
     ],
diff --git a/sdk/boards/sonata-prerelease.json b/sdk/boards/sonata-prerelease.json
index 01b4058..bd07567 100644
--- a/sdk/boards/sonata-prerelease.json
+++ b/sdk/boards/sonata-prerelease.json
@@ -2,11 +2,15 @@
     "devices": {
         "shadow" : {
             "start" : 0x30000000,
-            "end"   : 0x30004000
+            "end"   : 0x30000800
         },
         "pwm": {
             "start" : 0x80001000,
-            "length": 0x00001000
+            "end"   : 0x80001030
+        },
+        "pwm_lcd": {
+            "start" : 0x80001030,
+            "end"   : 0x80001038
         },
         "rgbled" : {
             "start" : 0x80009000,
@@ -47,17 +51,17 @@
     },
     "instruction_memory": {
         "start": 0x00101000,
-        "end":   0x00140000
+        "end":   0x00120000
     },
     "heap": {
-        "end": 0x00140000
+        "end": 0x00120000
     },
     "revokable_memory_start": 0x00100000,
     "defines" : [
         "IBEX",
         "SUNBURST",
         "SUNBURST_SHADOW_BASE=0x30000000",
-        "SUNBURST_SHADOW_SIZE=0x4000",
+        "SUNBURST_SHADOW_SIZE=0x800",
         "ipconfigDRIVER_INCLUDED_RX_IP_CHECKSUM=1",
         "ipconfigDRIVER_INCLUDED_TX_IP_CHECKSUM=1"
     ],
diff --git a/sdk/boards/sonata-simulator.json b/sdk/boards/sonata-simulator.json
new file mode 100644
index 0000000..c2073f7
--- /dev/null
+++ b/sdk/boards/sonata-simulator.json
@@ -0,0 +1,142 @@
+{
+    "devices": {
+        "shadow" : {
+            "start" : 0x30000000,
+            "end"   : 0x30000800
+        },
+        "pwm": {
+            "start" : 0x80001000,
+            "length": 0x00001000
+        },
+        "rgbled" : {
+            "start" : 0x80009000,
+            "end"   : 0x80009020
+        },
+        "revoker": {
+            "start" : 0x8000A000,
+            "length": 0x00001000
+        },
+        "adc": {
+            "start" : 0x8000B000,
+            "length": 0x00001000
+        },
+        "clint": {
+            "start" : 0x80040000,
+            "end"   : 0x80050000
+        },
+        "uart": {
+            "start" : 0x80100000,
+            "end"   : 0x80100034
+        },
+        "uart1": {
+            "start" : 0x80101000,
+            "end"   : 0x80101034
+        },
+        "uart2": {
+            "start" : 0x80102000,
+            "end"   : 0x80102034
+        },
+        "usbdev": {
+            "start" : 0x80400000,
+            "end"   : 0x80401000
+        },
+        "plic": {
+            "start" : 0x88000000,
+            "end"   : 0x88400000
+        }
+    },
+    "instruction_memory": {
+        "start": 0x00101000,
+        "end":   0x00120000
+    },
+    "heap": {
+        "end": 0x00120000
+    },
+    "revokable_memory_start": 0x00100000,
+    "defines" : [
+        "IBEX",
+        "SUNBURST",
+        "SUNBURST_SHADOW_BASE=0x30000000",
+        "SUNBURST_SHADOW_SIZE=0x800",
+        "ipconfigDRIVER_INCLUDED_RX_IP_CHECKSUM=1",
+        "ipconfigDRIVER_INCLUDED_TX_IP_CHECKSUM=1"
+    ],
+    "driver_includes" : [
+        "../include/platform/sunburst",
+        "../include/platform/ibex",
+        "../include/platform/generic-riscv"
+    ],
+    "timer_hz" : 40000000,
+    "tickrate_hz" : 100,
+    "revoker" : "hardware",
+    "stack_high_water_mark" : true,
+    "simulator" : "${sdk}/../scripts/run-sonata-sim.sh",
+    "simulation": true,
+    "interrupts": [
+        {
+            "name": "RevokerInterrupt",
+            "number": 1,
+            "priority": 2
+        },
+        {
+            "name": "EthernetInterrupt",
+            "number": 2,
+            "priority": 3
+        },
+        {
+            "name": "UsbDevInterrupt",
+            "number": 3,
+            "priority": 3
+        },
+        {
+            "name": "Uart0Interrupt",
+            "number": 8,
+            "priority": 3
+        },
+        {
+            "name": "Uart1Interrupt",
+            "number": 9,
+            "priority": 3
+        },
+        {
+            "name": "Uart2Interrupt",
+            "number": 10,
+            "priority": 3
+        },
+        {
+            "name": "I2c0Interrupt",
+            "number": 16,
+            "priority": 3
+        },
+        {
+            "name": "I2c1Interrupt",
+            "number": 17,
+            "priority": 3
+        },
+        {
+            "name": "SpiLcdInterrupt",
+            "number": 24,
+            "priority": 3
+        },
+        {
+            "name": "SpiEthmacInterrupt",
+            "number": 25,
+            "priority": 3
+        },
+        {
+            "name": "Spi0Interrupt",
+            "number": 26,
+            "priority": 3
+        },
+        {
+            "name": "Spi1Interrupt",
+            "number": 27,
+            "priority": 3
+        },
+        {
+            "name": "Spi2Interrupt",
+            "number": 28,
+            "priority": 3
+        }
+    ]
+}
diff --git a/sdk/core/allocator/alloc.h b/sdk/core/allocator/alloc.h
index 69f2726..9560be0 100644
--- a/sdk/core/allocator/alloc.h
+++ b/sdk/core/allocator/alloc.h
@@ -1207,6 +1207,7 @@
 			           "quota is {})",
 			           header->size_get(),
 			           quota);
+			heapFreeSize += header->size_get();
 			mspace_free_internal(header);
 			return AllocationFailureQuotaExceeded{};
 		}
@@ -2385,8 +2386,10 @@
 	 * Move a chunk back onto free lists.
 	 *
 	 * Note that this chunk does not have to come from quarantine, because it
-	 * can come from initialisation or splitting a free chunk.  Assumes that the
-	 * revocation shadow bits are clear in either case.
+	 * can come from initialisation or splitting a free chunk.  Thus, it is
+	 * the caller's responsibility to appropriately account heapFreeSize.
+	 *
+	 * Assumes that the revocation shadow bits are clear in either case.
 	 *
 	 * Initializes the linkages of p.
 	 */
@@ -2394,8 +2397,6 @@
 	{
 		ok_in_use_chunk(p);
 
-		heapFreeSize += p->size_get();
-
 		if (!p->is_prev_in_use())
 		{
 			// Consolidate backward
@@ -2581,6 +2582,7 @@
 			fore->metadata_clear();
 
 			heapQuarantineSize -= foreHeader->size_get();
+			heapFreeSize += foreHeader->size_get();
 
 			/* Clear the shadow bits that marked this region as quarantined */
 			revoker.shadow_paint_range<false>(foreHeader->body().address(),
@@ -2774,6 +2776,7 @@
 			 *   mspace_malloc does not displace into the chunk it finds from
 			 *   the free pool, but, in principle, it could.
 			 */
+			// This chunk is already free; do not adjust heapFreeSpace
 			mspace_free_internal(p);
 			p = r;
 		}
@@ -2796,6 +2799,7 @@
 			 *   to trim our tail, so it may well have trimmed the chunk
 			 *   it used to satisfy our request.
 			 */
+			// This chunk is already free; do not adjust heapFreeSpace
 			mspace_free_internal(r);
 		}
 
diff --git a/sdk/core/allocator/main.cc b/sdk/core/allocator/main.cc
index b5336ce..bb21962 100644
--- a/sdk/core/allocator/main.cc
+++ b/sdk/core/allocator/main.cc
@@ -923,10 +923,14 @@
 	return 0;
 }
 
-__cheriot_minimum_stack(0xf0) int heap_can_free(SObj  heapCapability,
-                                                void *rawPointer)
+__cheriot_minimum_stack(0x260) int heap_can_free(SObj  heapCapability,
+                                                 void *rawPointer)
 {
-	STACK_CHECK(0xf0);
+	// This function requires much less space, but we claim that we require as
+	// much as `heap_free` so that a call to `heap_free` will not fail due to
+	// insufficient stack immediately after `heap_can_free` has said that it's
+	// fine.
+	STACK_CHECK(0x260);
 	LockGuard g{lock};
 	return heap_free_internal(heapCapability, rawPointer, false);
 }
@@ -934,6 +938,7 @@
 __cheriot_minimum_stack(0x260) int heap_free(SObj  heapCapability,
                                              void *rawPointer)
 {
+	// If this value changes, update `heap_can_free` as well.
 	STACK_CHECK(0x260);
 	LockGuard g{lock};
 	int       ret = heap_free_internal(heapCapability, rawPointer, true);
diff --git a/sdk/core/loader/boot.cc b/sdk/core/loader/boot.cc
index bc67535..20ff56f 100644
--- a/sdk/core/loader/boot.cc
+++ b/sdk/core/loader/boot.cc
@@ -1212,6 +1212,10 @@
 	// it a normal import will require a small compiler change.  It is now
 	// exposed as a normal export, which enables exporting other things from
 	// the switcher later.
+	//
+	// Despite being exposed as a normal export, we still build the sentry by
+	// hand and, at the moment, ignore its IRQ disposition flags in favor of
+	// hardcoding the value here.
 	Debug::log("Setting compartment switcher");
 	auto switcherEntry =
 	  build<ExportEntry>(imgHdr.switcher.exportTable.start() + 20,
diff --git a/sdk/core/loader/types.h b/sdk/core/loader/types.h
index 3b96b39..90e190e 100644
--- a/sdk/core/loader/types.h
+++ b/sdk/core/loader/types.h
@@ -1070,6 +1070,24 @@
 		static constexpr uint8_t InterruptStatusMask = uint8_t(0b11)
 		                                               << InterruptStatusShift;
 
+		static constexpr uint8_t InterruptStatusSwitcherMask =
+		  uint8_t(0b10) << InterruptStatusShift;
+
+		/*
+		 * The switcher tests the high bit of the InterruptStatus word of
+		 * compartment-crossing calls through export entries by masking the
+		 * ExportEntry::flags field with InterruptStatusSwitcherMask.  Assert
+		 * that its understanding is correct.
+		 */
+		static_assert(
+		  ((int(InterruptStatus::Enabled) << InterruptStatusShift) &
+		   InterruptStatusSwitcherMask) == 0,
+		  "Switcher interpretation of InterruptStatus no longer correct");
+		static_assert(
+		  ((int(InterruptStatus::Disabled) << InterruptStatusShift) &
+		   InterruptStatusSwitcherMask) != 0,
+		  "Switcher interpretation of InterruptStatus no longer correct");
+
 		/**
 		 * The flag indicating that this is a fake entry used to identify
 		 * sealing types.  No import table entries should refer to this
diff --git a/sdk/core/scheduler/common.h b/sdk/core/scheduler/common.h
index ea9ccfd..0c43380 100644
--- a/sdk/core/scheduler/common.h
+++ b/sdk/core/scheduler/common.h
@@ -51,10 +51,17 @@
 	 * Subclasses must implement a static `sealing_type` method that returns
 	 * the sealing key.
 	 */
-	template<bool IsDynamic>
+	template<bool IsDynamicArg>
 	struct Handle
 	{
 		/**
+		 * Some Handle types must reside in static memory, and some may be built
+		 * on the fly, and in particular in the shared heap, at runtime.  Is
+		 * this type among the latter?
+		 */
+		static constexpr bool IsDynamic = IsDynamicArg;
+
+		/**
 		 * Unseal `unsafePointer` as a pointer to an object of the specified
 		 * type.  Returns nullptr if `unsafePointer` is not a valid sealed
 		 * pointer to an object of the correct type.
diff --git a/sdk/core/scheduler/main.cc b/sdk/core/scheduler/main.cc
index 678c784..d4d36a8 100644
--- a/sdk/core/scheduler/main.cc
+++ b/sdk/core/scheduler/main.cc
@@ -26,30 +26,15 @@
 using namespace CHERI;
 
 #ifdef SIMULATION
-/**
- * This is a special MMIO register. Writing an LSB of 1 terminates
- * simulation. The upper 31 bits can pass extra metadata. We use all 0s
- * to indicates success.
- *
- * This symbol doesn't need to be exported. The simulator is clever
- * enough to find it even if it's local.
- */
-volatile uint32_t tohost[2];
+#	include <platform-simulation_exit.hh>
 
 /**
  * Exit simulation, reporting the error code given as the argument.
  */
 void simulation_exit(uint32_t code)
 {
-	// If this is using the standard RISC-V to-host mechanism, this will exit.
-	tohost[0] = 0x1 | (code << 1);
-	tohost[1] = 0;
-	// If we didn't exit with to-host, try writing a non-ASCII character to the
-	// UART.  This is how we exit the CHERIoT Ibex simulator for the SAFE
-	// platform.
-	MMIO_CAPABILITY(Uart, uart)->blocking_write(0x80 + code);
+	platform_simulation_exit(code);
 }
-
 #endif
 
 /**
@@ -390,20 +375,24 @@
 
 	/// Helper to safely deallocate an instance of `T`.
 	template<typename T>
-	int deallocate(SObjStruct *heapCapability, void *object)
+	int deallocate(SObjStruct *heapCapability, void *objectPtr)
 	{
+		static_assert(T::IsDynamic);
+
 		// Acquire the lock and hold it. We need to be careful of two attempts
 		// to free the same object racing, so we cause others to back up behind
 		// this one.  They will then fail in the unseal operation.
 		LockGuard g{deallocLock};
-		return typed_op<T>(object, [&](T &unsealed) {
-			if (int ret = heap_can_free(heapCapability, &unsealed); ret != 0)
+		return typed_op<T>(objectPtr, [&](T &unsealed) {
+			SObj object = static_cast<SObj>(objectPtr);
+			if (int ret = token_obj_can_destroy(
+			      heapCapability, T::sealing_type(), object);
+			    ret != 0)
 			{
 				return ret;
 			}
 			unsealed.~T();
-			heap_free(heapCapability, &unsealed);
-			return 0;
+			return token_obj_destroy(heapCapability, T::sealing_type(), object);
 		});
 	}
 
diff --git a/sdk/core/scheduler/thread.h b/sdk/core/scheduler/thread.h
index 4ed345b..ea88756 100644
--- a/sdk/core/scheduler/thread.h
+++ b/sdk/core/scheduler/thread.h
@@ -363,6 +363,7 @@
 		{
 			Debug::log("Thread {} exited, {} threads remaining", current->threadId, threadCount - 1);
 			current->list_remove(&priorityList[current->priority]);
+			current->priority_map_remove();
 			current->state = ThreadState::Exited;
 			return (--threadCount) == 0;
 		}
diff --git a/sdk/core/switcher/entry.S b/sdk/core/switcher/entry.S
index b139892..6e6bcfc 100644
--- a/sdk/core/switcher/entry.S
+++ b/sdk/core/switcher/entry.S
@@ -77,6 +77,7 @@
  *
  *  - "LIVE IN:", a list of live (in) registers at this point of the code and/or
  *    - "*": the entire general purpose register file (no CSRs or SCRs implied)
+ *    - "callee-save": the psABI callee-save registers
  *    - "mcause"
  *    - "mtdc"
  *    - "mtval"
@@ -89,6 +90,27 @@
  * continue onto adjacent lines.
  *
  */
+/*
+ * Multiple points in the switcher are exposed to callers via sentries (either
+ * forward-arc sentries manufactured elsewhere or backwards-arc sentries
+ * manufactured by CJALRs herein.  Sentries can have their GL(obal) permission
+ * cleared by the bearer, but nothing here relies on PCC being GL(obal): we
+ * never store anything derived from our PCC to memory, much less through an
+ * authority not bearing SL permission.
+ *
+ * Similarly, the switcher communicates with the outside world by means of
+ * sealed data capabilities (to TrustedStacks and compartment export tables).
+ * These, too, can have their GL(obal) bit cleared by bearers, but again, it
+ * does not much matter for switcher correctness; see comments marked with
+ * "LOCAL SEAL" notes in the code below.
+ *
+ * We do rely on PCC having L(oad)G(lobal) permission -- which is under seal in
+ * sentries and so not mutable by the caller, even if a sentry is loaded
+ * through an authority without LG -- so that, in particular, the sealing
+ * authorities used herein are GL(obal) and so the sealed capabilities that
+ * result are also GL(obal).
+ */
+
 
 switcher_code_start:
 
@@ -142,7 +164,7 @@
 .endm
 
 /// Spill a single register to a trusted stack pointed to by csp.
-.macro spillOne, reg
+.macro trustedSpillOne, reg
 	csc \reg, TrustedStack_offset_\reg(csp)
 .endm
 
@@ -150,12 +172,12 @@
  * Spill all of the registers in the list (in order) to a trusted stack pointed
  * to by csp.
  */
-.macro spillRegisters reg1, regs:vararg
-	forall spillOne, \reg1, \regs
+.macro trustedSpillRegisters reg1, regs:vararg
+	forall trustedSpillOne, \reg1, \regs
 .endm
 
 /// Reload a single register from a trusted stack pointed to by csp.
-.macro reloadOne, reg
+.macro trustedReloadOne, reg
 	clc \reg, TrustedStack_offset_\reg(csp)
 .endm
 
@@ -163,8 +185,8 @@
  * Reload all of the registers in the list (in order) to a trusted stack pointed
  * to by csp.
  */
-.macro reloadRegisters reg1, regs:vararg
-	forall reloadOne, \reg1, \regs
+.macro trustedReloadRegisters reg1, regs:vararg
+	forall trustedReloadOne, \reg1, \regs
 .endm
 
 /**
@@ -216,8 +238,9 @@
 	/*
 	 * FROM: cross-call
 	 * FROM: malice
-	 * IRQ ASSUME: deferred (exposed as IRQ-deferring sentry; see the 'export'
-	 *             macro at the end of this file)
+	 * IRQ ASSUME: deferred (loader/boot.cc constructs only IRQ-deferring
+	 *             sentries to this function; the export entry at the end
+	 *             of this file is somewhat fictitious)
 	 * LIVE IN: mtdc, ra, sp, gp, s0, s1, t0, t1, a0, a1, a2, a3, a4, a5
 	 *          (that is, all registers except tp and t2)
 	 *
@@ -273,26 +296,39 @@
 	 * populating the error return values in a0 and a1, are required.
 	 */
 	/*
+	 * __Z26compartment_switcher_entryz is exposed to callers directly as a
+	 * forward-arc interrupt-disabling sentry via the somewhat lengthy chain
+	 * of events involving...
+	 *   - the .compartment_import_table sections defined in
+	 *     compartment.ldscript,
+	 *   - the export table defined below (.section .compartment_export_table),
+	 *   - firmware.ldscript.in's use of that export table to define
+	 *     .switcher_export_table,
+	 *   - the firmware image header (loader/types.h's ImgHdr), in particular
+	 *     ImgHdr::switcher::exportTable and, again, firmware.ldscript.in's
+	 *     use of .switcher_export_table to populate that field, and
+	 *   - loader/boot.cc:/populate_imports and its caller's computation of
+	 *     switcherPCC.
+	 */
+	/*
 	 * TODO: We'd like to relax the interrupt posture of the switcher where
 	 * possible.  Specifically, unless both the caller and callee are running
 	 * and to be run with interrupts deferred, we'd like the switcher, and
 	 * especially its stack-zeroing, to be preemtable.
 	 */
-	cincoffset        ct2, csp, -SPILL_SLOT_SIZE
 .Lswitch_entry_first_spill:
 	/*
 	 * FROM: above
 	 * ITO: .Lswitch_just_return (via .Lhandle_error_in_switcher)
 	 */
-	csc               cs0, SPILL_SLOT_cs0(ct2)
-	csc               cs1, SPILL_SLOT_cs1(ct2)
-	csc               cgp, SPILL_SLOT_cgp(ct2)
-	csc               cra, SPILL_SLOT_pcc(ct2)
-	cmove             csp, ct2
+	csc               cs0, (SPILL_SLOT_cs0-SPILL_SLOT_SIZE)(csp)
+	cincoffset        csp, csp, -SPILL_SLOT_SIZE
+	csc               cs1, SPILL_SLOT_cs1(csp)
+	csc               cgp, SPILL_SLOT_cgp(csp)
+	csc               cra, SPILL_SLOT_pcc(csp)
 	/*
 	 * Atlas update:
 	 *  ra, gp, s0, s1: dead (presently, redundant caller values)
-	 *  t2: dead (presently, a copy of csp)
 	 */
 
 	/*
@@ -308,8 +344,8 @@
 	 * surviving the stores above.
 	 *
 	 * TODO for formal verification: it should be the case that after these
-	 * tests and the size checks below, no csp-authorized instruction in the
-	 * switcher can fault.
+	 * tests and the size checks below, no instruction in the switcher
+	 * authorized by the capability now in sp can fault.
 	 */
 //.Lswitch_csp_check:
 	cgetperm           t2, csp
@@ -449,7 +485,7 @@
 	 *  s0, t2, gp: dead (again)
 	 */
 
-	// Fetch the sealing key, using gp as a scratch scalar
+	// Fetch the sealing key
 	LoadCapPCC         cs0, .Lunsealing_key_import_tables
 	// Atlas update: s0: switcher sealing key
 	/*
@@ -469,6 +505,14 @@
 	 *      .Lhandle_error_in_switcher.
 	 */
 	/*
+	 * LOCAL SEAL: If it happened that the export table reference given to us
+	 * is not GL(obal), then the result of unsealing above, now in t1, will
+	 * also be not GL(obal).  This reference is stored to the TrustedStack frame
+	 * through a SL-bearing authority (because the TrustedStack also holds our
+	 * register spill area, and so must have SL) but neither it or any monotone
+	 * progeny otherwise escape the switcher's private register file.
+	 */
+	/*
 	 * Load the entry point offset.  If cunseal failed then this will fault and
 	 * we will force unwind; see .Lhandle_error_switcher_pcc_check.
 	 */
@@ -574,9 +618,11 @@
 
 	/*
 	 * Enable interrupts if the interrupt-disable bit is not set in flags.  See
-	 * loader/types.h's InterruptStatus and ExportEntry::InterruptStatusMask
+	 * loader/types.h's InterruptStatus and ExportEntry::InterruptStatusMask.
+	 * InterruptStatus::Inherited is prohibited on export entries, so we need
+	 * look only at one bit.
 	 */
-	andi               t1, tp, 0x10
+	andi               t1, tp, ExportEntryInterruptStatusSwitcherMask
 	bnez               t1, .Lswitch_skip_interrupt_enable
 	csrsi              mstatus, 0x8
 .Lswitch_skip_interrupt_enable:
@@ -592,6 +638,25 @@
 	 *  tp, t1, t2, s0, s1: dead
 	 */
 	/*
+	 * There is an interesting narrow race to consider here.  We're preemptable
+	 * and in the switcher.  That means someone could call
+	 * __Z25switcher_interrupt_threadPv on us, and when we came back on core,
+	 * we'd jump ahead to switcher_after_compartment_call, via...
+	 *
+	 *   - .Lexception_scheduler_return_installed
+	 *   - .Lhandle_injected_error
+	 *   - .Lhandle_error
+	 *   - .Lhandle_error_switcher_pcc
+	 *   - .Lhandle_error_in_switcher
+	 *   - .Lcommon_force_unwind
+	 *
+	 * That is, rather than invoking the callee's compartment's error handler,
+	 * and letting it service the MCAUSE_THREAD_INTERRUPT, we'll return to the
+	 * caller with -ECOMPARTMENTFAIL.
+	 *
+	 * TODO: https://github.com/CHERIoT-Platform/cheriot-rtos/issues/372
+	 */
+	/*
 	 * Up to 10 registers are carrying state for the callee or are properly
 	 * zeroed.  Clear the remaining 5 now.
 	 */
@@ -633,7 +698,8 @@
 	/*
 	 * Pop a frame from the trusted stack, leaving all registers in the state
 	 * expected by the caller of a cross-compartment call.  The callee is
-	 * responsible for zeroing argument and temporary registers.
+	 * responsible for zeroing unused return registers; the switcher will zero
+	 * other non-return argument and temporary registers.
 	 *
 	 * This unwind path is common to both ordinary return (from above), benign
 	 * errors after we'd set up the trusted frame (.Lswitch_stack_too_small),
@@ -644,6 +710,17 @@
 	 * elsewhere.
 	 */
 	/*
+	 * As just before the call, we are preemptive and in the switcher.  If we
+	 * are signaled via MCAUSE_THREAD_INTERRUPT at this point, we will come
+	 * back here (with a0 holding -ECOMPARTMENTFAIL and a1 holding 0).  This
+	 * block is _idempotent_ until the update of mtdc's
+	 * TrustedStack::frameoffset, so until then we will effectively just
+	 * clobber the return values.  After that, though, we'd forcibly unwind out
+	 * of the caller.
+	 *
+	 * TODO: https://github.com/CHERIoT-Platform/cheriot-rtos/issues/372
+	 */
+	/*
 	 * The return sentry given to the callee as part of that cjalr could be
 	 * captured by the callee or passed between compartments arbitrarily for
 	 * later use.  That is, in some sense, we cannot assume that any use of this
@@ -670,6 +747,7 @@
 	 */
 
 	cspecialr          ctp, mtdc
+	// Atlas update: tp: pointer to TrustedStack
 
 	clear_hazard_slots ctp, ct2
 
@@ -694,7 +772,12 @@
 	 */
 	bgeu               t0, t2, .Lcommon_defer_irqs_and_thread_exit
 	cincoffset         ct1, ctp, t2
-	// Atlas update: t1: pointer to the TrustedStackFrame to bring on core
+	/*
+	 * Atlas update:
+	 *  t0: dead (again)
+	 *  t1: pointer to the TrustedStackFrame to bring on core
+	 *  t2: the TrustedStack::frameoffset associated with t1
+	 */
 
 	/*
 	 * Restore the untrusted stack pointer from the trusted stack.  This points
@@ -744,7 +827,18 @@
 #endif
 
 	// Zero all registers not holding state intended for caller; see atlas below
-//.Lswitch_callee_dead_zeros:
+.Lswitch_callee_dead_zeros:
+	/*
+	 * FROM: above
+	 * FROM: .Lswitch_trusted_stack_exhausted
+	 * LIVE IN: mtdc, ra, sp, gp, s0, s1, a0, a1
+	 *
+	 * Atlas:
+	 *  mtdc: pointer to this thread's TrustedStack
+	 *  a0, a1: return value(s)
+	 *  ra, sp, gp, s0, s1: caller state
+	 *  tp, t0, t1, t2, a2, a3, a4, a5: dead (to be zeroed here)
+	 */
 	zeroAllRegistersExcept ra, sp, gp, s0, s1, a0, a1
 .Lswitch_just_return:
 	/*
@@ -809,11 +903,10 @@
 	clc                cra, SPILL_SLOT_pcc(csp)
 	clc                cgp, SPILL_SLOT_cgp(csp)
 	cincoffset         csp, csp, SPILL_SLOT_SIZE
-	// Set the first return register (a0) and zero the other (a1) below
+	// Set the first return register (a0) and zero the other (a1)
 	li                 a0, -ENOTENOUGHTRUSTEDSTACK
-	// Zero everything else
-	zeroAllRegistersExcept ra, sp, gp, s0, s1, a0
-	cret
+	zeroOne            a1
+	j                  .Lswitch_callee_dead_zeros
 
 .size compartment_switcher_entry, . - compartment_switcher_entry
 
@@ -867,7 +960,7 @@
 	 * The guest sp/csp (x2/c2) is now in mtdc. Will be spilled later, but we
 	 * spill all the other 14 registers now.
 	 */
-	spillRegisters     cra, cgp, ctp, ct0, ct1, ct2, cs0, cs1, ca0, ca1, ca2, ca3, ca4, ca5
+	trustedSpillRegisters     cra, cgp, ctp, ct0, ct1, ct2, cs0, cs1, ca0, ca1, ca2, ca3, ca4, ca5
 
 	/*
 	 * The control flow of an exiting thread rejoins us (that is, running
@@ -918,6 +1011,7 @@
 #endif
 	csrr               t1, mcause
 	csw                t1, TrustedStack_offset_mcause(csp)
+	// Atlas update: t1: copy of mcause
 
 	/*
 	 * If we hit one of the exception conditions that we should let compartments
@@ -979,7 +1073,7 @@
 	// Call the scheduler.  This returns the new thread in ca0.
 	cjalr              cra
 
-.Lexception_scheduler_return:
+//.Lexception_scheduler_return:
 	/*
 	 * IFROM: above
 	 * IRQ ASSUME: deferred (reachable only by IRQ-deferring reverse sentry)
@@ -1007,10 +1101,19 @@
 	 * .Lcommon_context_install.
 	 */
 
-	// Switch onto the new thread's trusted stack, using gp as a scratch scalar
+	// Switch onto the new thread's trusted stack
 	LoadCapPCC         csp, .Lsealing_key_trusted_stacks
 	cunseal            csp, ca0, csp
 	// Atlas update: sp: unsealed target thread trusted stack pointer
+	/*
+	 * LOCAL SEAL: if the scheduler has shed GL(obal) of the reference it gave
+	 * us in a0, then sp will also lack GL(obal) after unsealing.  This
+	 * reference is not stored in memory (in the switcher, anyway), just mtdc.
+	 * However, when this reference is extracted and sealed for the next
+	 * context switch (in .Lexception_scheduler_call), the result will lack
+	 * GL(obal), which will likely prove challenging for the scheduler.  That
+	 * is, this is an elaborate way for the scheduler to crash itself.
+	 */
 
 	clw                t0, TrustedStack_offset_mcause(csp)
 	// Atlas update: t0: stored mcause for the target thread
@@ -1085,7 +1188,7 @@
 	 * sp/csp (x2/c2) will be loaded last and will overwrite the trusted stack
 	 * pointer with the thread's stack pointer.
 	 */
-	reloadRegisters cra, cgp, ctp, ct0, ct1, ct2, cs0, cs1, ca0, ca1, ca2, ca3, ca4, ca5, csp
+	trustedReloadRegisters cra, cgp, ctp, ct0, ct1, ct2, cs0, cs1, ca0, ca1, ca2, ca3, ca4, ca5, csp
 	mret
 
 /**
@@ -1199,6 +1302,14 @@
 	 * value (base is a displacement from the address).
 	 */
 	cgettag            t1, ct0
+
+	/*
+	 * A value of 0xffff indicates no error handler.  Both of our conditional
+	 * paths want this value, but we can load it once, now.
+	 */
+	li                 s1, 0xffff
+	// Atlas update: s1: 0xffff
+
 	/*
 	 * If there isn't enough space on the stack, see if there's a stackless
 	 * handler.
@@ -1224,7 +1335,6 @@
 	 * A value of 0xffff indicates no error handler.  If we found one, use it,
 	 * otherwise fall through and try to find a stackless handler.
 	 */
-	li                 s1, 0xffff
 	// LIVE OUT: sp, tp, t0, t1, s0, a0
 	bne                s0, s1, .Lhandle_error_found
 
@@ -1233,11 +1343,12 @@
 	 * FROM: above
 	 * FROM: .Lhandle_error_stack_oob
 	 * IRQ REQUIRE: deferred (TrustedStack spill frame is precious)
-	 * LIVE IN: sp, tp, t0
+	 * LIVE IN: sp, tp, s1, t0
 	 * Atlas:
 	 *  sp: pointer to TrustedStack
 	 *  tp: pointer to current TrustedStackFrame
 	 *  t0: interrupted thread's stack pointer
+	 *  s1: 0xffff
 	 */
 
 	clc                ct1, TrustedStackFrame_offset_calleeExportTable(ctp)
@@ -1254,7 +1365,6 @@
 	 * error handler for this compartment, having already tried any stackful
 	 * handler.
 	 */
-	li                 s1, 0xffff
 	// LIVE OUT: mtdc
 	beq                s0, s1, .Lcommon_force_unwind
 
@@ -1652,6 +1762,15 @@
 	 */
 	csrw               mcause, MCAUSE_THREAD_EXIT
 	/*
+	 * mtval may have been updated by the action of other threads in the system
+	 * and holds the last value latched during an exception.  From the
+	 * scheduler's perspective, thread exits are a kind of exception, and
+	 * exceptions get to see mtval.  Write a constant value to mtval to act more
+	 * like an architectural fault and to close a small information leak to the
+	 * scheduler's event handler.
+	 */
+	csrw               mtval, MCAUSE_THREAD_EXIT
+	/*
 	 * The thread exit code expects the TrustedStack pointer to be in csp and
 	 * the thread's stack pointer to be in mtdc.  After thread exit, we don't
 	 * need the stack pointer so just put zero there.
@@ -1669,10 +1788,11 @@
 	/*
 	 * FROM: .Lhandle_error_switcher_pcc
 	 * IRQ REQUIRE: deferred (TrustedStack spill frame is precious)
-	 * LIVE IN: mtdc
+	 * LIVE IN: mtdc, t1
 	 *
 	 * Atlas:
 	 *  mtdc:  pointer to TrustedStack
+	 *  t1: A copy of mepcc, the faulting program counter
 	 */
 	auipcc             ctp, %cheriot_compartment_hi(.Lswitch_entry_first_spill)
 	cincoffset         ctp, ctp, %cheriot_compartment_lo_i(.Lhandle_error_in_switcher)
@@ -1726,7 +1846,7 @@
 	 * alias for cspecialrw with a zero source, which means "don't write".  So,
 	 * put nullptr in a register with non-zero index, and then put that in mtcc.
 	 */
-	cmove              csp, cnull
+	zeroOne            sp
 	cspecialw          mtcc, csp
 	// Take a trap and wedge the machine on that null MTCC
 	clc                csp, 0(csp)
@@ -1759,10 +1879,14 @@
 	.type __Z23trusted_stack_has_spacei,@function
 __Z23trusted_stack_has_spacei:
 	/*
-	 * LIVE IN: mtdc, a0
+	 * FROM: malice
+	 * IRQ ASSUME: deferred
+	 * LIVE IN: mtdc, callee-save, ra, a0
 	 *
 	 * Atlas:
 	 *  mtdc: pointer to TrustedStack (or nullptr if from buggy scheduler)
+	 *  ra: return pointer (guaranteed because this symbol is reachable only
+	 *      through an interrupt-disabling forward-arc sentry)
 	 *  a0: requested number of trusted stack frames
 	 */
 	li                 a2, TrustedStackFrame_size
@@ -1790,15 +1914,20 @@
 	// LIVE OUT: mtdc, a0
 	cret
 
+// Reveal the stack pointer given to this compartment invocation
 	.section .text, "ax", @progbits
 	.p2align 2
 	.type __Z22switcher_recover_stackv,@function
 __Z22switcher_recover_stackv:
 	/*
-	 * LIVE IN: mtdc
+	 * FROM: malice
+	 * IRQ ASSUME: deferred
+	 * LIVE IN: mtdc, callee-save, ra
 	 *
 	 * Atlas:
 	 *  mtdc: pointer to TrustedStack (or nullptr if buggy scheduler)
+	 *  ra: return pointer (guaranteed because this symbol is reachable only
+	 *      through an interrupt-disabling forward-arc sentry)
 	 */
 	/*
 	 * Load the trusted stack pointer into a register that we will clobber after
@@ -1819,6 +1948,7 @@
 	 * on entry, and can be returned directly.
 	 */
 	li                 a2, TrustedStack_offset_frames
+	// Atlas update: a2: dead but exposed: TrustedStack_offset_frames
 	beq                a1, a2, 0f
 
 	/*
@@ -1832,6 +1962,11 @@
 	sub                a1, a1, a2
 	csetaddr           ca0, ca0, a2
 	csetboundsexact    ca0, ca0, a1
+	/*
+	 * Atlas update:
+	 *  a1: dead but exposed: the length of the stack
+	 *  a2: dead but exposed: base address of the stack
+	 */
 0:
 	// LIVE OUT: mtdc, a0
 	cret
@@ -1840,14 +1975,33 @@
 	.p2align 2
 	.type __Z30trusted_stack_interrupt_threadPv,@function
 __Z25switcher_interrupt_threadPv:
-	// Load the unsealing key into a register that we will clobber two
-	// instructions later.
+	/*
+	 * FROM: malice
+	 * IRQ ASSUME: deferred
+	 * LIVE IN: mtdc, callee-save, ra, a0
+	 *
+	 * Atlas:
+	 *   mtdc: pointer to TrustedStack (or nullptr if buggy scheduler)
+	 *   a0: sealed pointer to target thread TrustedStack
+	 *   ra: return pointer (guaranteed because this symbol is reachable only
+	 *       through an interrupt-disabling forward-arc sentry)
+	 */
+	/*
+	 * Because this function involves looking across two threads' states, it
+	 * needs to run with preemption prohibited, and that means IRQs deferred.
+	 */
+
+	// Load the unsealing key
 	LoadCapPCC         ca1, .Lsealing_key_trusted_stacks
 	/*
-	 * The target capability is in ca0.  Unseal, check tag and load the entry
-	 * point offset.
+	 * The target capability is in ca0.  Unseal, clobbering our authority;
+	 * check tag; and load the entry point offset.
 	 */
 	cunseal            ca1, ca0, ca1
+	// Atlas update: a1: unsealed pointer to target thread TrustedStack
+	/*
+	 * LOCAL SEAL: Nothing herein depends on a1 being GL(obal).
+	 */
 	cgettag            a0, ca1
 	// a0 (return register) now contains the tag.  We return false on failure
 	// so can just branch to the place where we zero non-return registers from
@@ -1858,12 +2012,14 @@
 	cspecialr          ca2, mtdc
 	li                 a0, 0
 	beq                a2, a1, .Lswitcher_interrupt_thread_return
+	// Atlas update: a2: unsealed pointer to current thread TrustedStack
 
-	// ca1 now contains the unsealed capability for the target thread.  We
-	// allow the target thread to be interrupted if (and only if) the caller is
-	// in the same compartment as the interrupted thread.  We will determine
-	// this by checking if the base of the two export table entries from the
-	// top of the trusted stack frames match.
+	/*
+	 * We allow the target thread to be interrupted if (and only if) the caller
+	 * is in the same compartment as the interrupted thread.  We will determine
+	 * this by checking if the base of the two export table entries from the
+	 * top of the trusted stack frames match.
+	 */
 
 // Helper macro that loads the export table from the register containing the
 // trusted stack.  The two arguments must be different registers.
@@ -1886,10 +2042,13 @@
 
 	// If the two export table entries differ, return.
 	bne                a2, a3, .Lswitcher_interrupt_thread_return
-	// After this point, we no longer care about the values in a0, a2, and a3.
+	// Atlas update: a1, a2, a3: dead (to be zeroed)
 
-	// Mark the thread as interrupted.
-	// Store a magic value in mcause
+	/*
+	 * Mark the thread as interrupted.  Store a magic value in mcause.  This
+	 * value will not be overwritten by a trap before the scheduler sees the
+	 * target thread, since we are on core and it isn't.
+	 */
 	li                 a2, MCAUSE_THREAD_INTERRUPT
 	csw                a2, TrustedStack_offset_mcause(ca1)
 	// Return success
@@ -1898,67 +2057,130 @@
 	zeroRegisters      a1, a2, a3
 	cret
 
+// Get a sealed pointer to the current thread's TrustedStack
 	.section .text, "ax", @progbits
 	.p2align 2
 	.type __Z23switcher_current_threadv,@function
 __Z23switcher_current_threadv:
+	/*
+	 * FROM: malice
+	 * IRQ ASSUME: deferred
+	 * LIVE IN: mtdc, callee-save, ra
+	 *
+	 * Atlas:
+	 *   mtdc: pointer to TrustedStack (or nullptr if buggy scheduler)
+	 *   ra: return pointer (guaranteed because this symbol is reachable only
+	 *       through an interrupt-disabling forward-arc sentry)
+	 */
+
 	LoadCapPCC         ca0, .Lsealing_key_trusted_stacks
+	// Atlas update: a0: sealing authority for trusted stacks
 	cspecialr          ca1, mtdc
+	// Atlas update: a1: copy of mtdc
 	cseal              ca0, ca1, ca0
 	li                 a1, 0
+	/*
+	 * Atlas update:
+	 *   a0: sealed copy of mtdc, this thread's TrustedStack
+	 *   a1: zero
+	 */
 	cret
 
+// Get a pointer to this thread's hazard pointers array
 	.section .text, "ax", @progbits
 	.p2align 2
 	.type __Z28switcher_thread_hazard_slotsv,@function
 __Z28switcher_thread_hazard_slotsv:
-	// Load the trusted stack pointer into a register that we will clobber in
-	// two instructions.
+	/*
+	 * FROM: malice
+	 * IRQ ASSUME: deferred
+	 * LIVE IN: mtdc, callee-save, ra
+	 *
+	 * Atlas:
+	 *   mtdc: pointer to TrustedStack (or nullptr if buggy scheduler)
+	 *   ra: return pointer (guaranteed because this symbol is reachable only
+	 *       through an interrupt-disabling forward-arc sentry)
+	 */
+
 	cspecialr          ca0, mtdc
+
+	// If this traps (from null mtdc, say), we'll forcibly unwind.
 	clc                ca0, TrustedStack_offset_hazardPointers(ca0)
+	// Atlas update: a0: pointer to hazard pointers
+
 	cret
 
+// Get the current thread's integer ID
 	.section .text, "ax", @progbits
 	.p2align 2
 	.type __Z13thread_id_getv,@function
 __Z13thread_id_getv:
-	// Load the trusted stack pointer into a register that we will clobber in
-	// the next instruction when we load the thread ID.
+	/*
+	 * FROM: malice
+	 * IRQ ASSUME: deferred
+	 * LIVE IN: mtdc, callee-save, ra
+	 *
+	 * Atlas:
+	 *   mtdc: pointer to TrustedStack (or nullptr if buggy scheduler)
+	 *   ra: return pointer (guaranteed because this symbol is reachable only
+	 *       through an interrupt-disabling forward-arc sentry)
+	 */
+
 	cspecialr          ca0, mtdc
+	/*
+	 * If this is a null pointer, don't try to dereference it and report that
+	 * we are thread 0.  This permits the debug code to work even from things
+	 * that are not real threads.
+	 */
 	cgettag            a1, ca0
-	// If this is a null pointer, don't try to dereference it and report that
-	// we are thread 0.  This permits the debug code to work even from things
-	// that are not real threads.
+	// Atlas update: a1: tag of a0/mtdc
 	beqz               a1, 0f
 	clh                a0, TrustedStack_offset_threadID(ca0)
+	// Atlas update: a0: integer ID of current thread
 0:
 	cret
 
 
+// Return the stack high-water mark
 	.section .text, "ax", @progbits
 	.p2align 2
 	.type __Z25stack_lowest_used_addressv,@function
 __Z25stack_lowest_used_addressv:
-	// Read the stack high-water mark into the return register.
 	csrr               a0, CSR_MSHWM
 	cret
 
+// Reset the count of error handler invocations in this compartment invocation
 	.section .text, "ax", @progbits
 	.p2align 2
 	.type __Z39switcher_handler_invocation_count_resetv,@function
 __Z39switcher_handler_invocation_count_resetv:
-	// Trusted stack pointer in ca1
+	/*
+	 * FROM: malice
+	 * IRQ ASSUME: deferred
+	 * LIVE IN: mtdc, callee-save, ra
+	 *
+	 * Atlas:
+	 *   mtdc: pointer to TrustedStack (or nullptr if buggy scheduler)
+	 *   ra: return pointer (guaranteed because this symbol is reachable only
+	 *       through an interrupt-disabling forward-arc sentry)
+	 */
+
 	cspecialr          ca1, mtdc
-	// Offset of the current trusted stack frame to a1
+	// Atlas update: a1: copy of mtdc
 	clhu               a0, TrustedStack_offset_frameoffset(ca1)
 	addi               a0, a0, -TrustedStackFrame_size
-	// Current trusted stack frame to ca1, a0 is dead
+	// Atlas update: a0: offset of the current trusted stack frame
 	cincoffset         ca1, ca1, a0
-	// Current invocation count (for return) in a0
+	/*
+	 * Atlas update:
+	 *  a0: dead
+	 *  a1: pointer to current TrustedStack::frame
+	 */
 	clh                a0, TrustedStackFrame_offset_errorHandlerCount(ca1)
+	// Atlas update: a0: current invocation count (for return)
 	// Reset invocation count
 	csh                zero, TrustedStackFrame_offset_errorHandlerCount(ca1)
-	// Zero trusted stack frame pointer register
+	// Atlas update: a1: dead (to be zeroed)
 	li                 a1, 0
 	cret
 
@@ -1987,7 +2209,10 @@
 .endm
 
 // Switcher entry point must be first.
-// We mangle the switcher export as if it were a compartment call.
+/*
+ * We mangle the switcher export as if it were a compartment call, but see
+ * loader/boot.cc's special handling of this entry.
+ */
 export __Z26compartment_switcher_entryz, __export_switcher
 export __Z23trusted_stack_has_spacei
 export __Z22switcher_recover_stackv
diff --git a/sdk/core/switcher/export-table-assembly.h b/sdk/core/switcher/export-table-assembly.h
index 5581f78..74fb128 100644
--- a/sdk/core/switcher/export-table-assembly.h
+++ b/sdk/core/switcher/export-table-assembly.h
@@ -11,3 +11,7 @@
 EXPORT_ASSEMBLY_OFFSET(ExportTable, cgp, 8)
 EXPORT_ASSEMBLY_OFFSET(ExportTable, errorHandler, 16)
 EXPORT_ASSEMBLY_OFFSET(ExportTable, errorHandlerStackless, 18)
+
+EXPORT_ASSEMBLY_EXPRESSION(ExportEntryInterruptStatusSwitcherMask,
+                           ExportEntry::InterruptStatusSwitcherMask,
+                           0x10)
diff --git a/sdk/include/cheri.hh b/sdk/include/cheri.hh
index 4663e17..0307cf7 100644
--- a/sdk/include/cheri.hh
+++ b/sdk/include/cheri.hh
@@ -813,6 +813,20 @@
 		}
 
 		/**
+		 * Remove some permissions from this capability.
+		 *
+		 * Because this function computes the permission mask by clearing bits
+		 * in the PermissionSet::omnipotent() all-ones mask, rather than from
+		 * the set of permissions currently held by this Capability, it is safe
+		 * to use to clear Global permission on a sealed capability.
+		 */
+		template<std::same_as<Permission>... Permissions>
+		void without_permissions(Permissions... drop)
+		{
+			permissions() &= PermissionSet::omnipotent().without(drop...);
+		}
+
+		/**
 		 * Pointer subtraction.
 		 */
 		Capability operator-(ptrdiff_t diff)
diff --git a/sdk/include/platform/generic-riscv/platform-simulation_exit.hh b/sdk/include/platform/generic-riscv/platform-simulation_exit.hh
new file mode 100644
index 0000000..6cbfe06
--- /dev/null
+++ b/sdk/include/platform/generic-riscv/platform-simulation_exit.hh
@@ -0,0 +1,31 @@
+// Copyright Microsoft and CHERIoT Contributors.
+// SPDX-License-Identifier: MIT
+
+#pragma once
+
+#ifdef SIMULATION
+#	include <stdint.h>
+#	ifdef RISCV_HTIF
+/**
+ * This is a special MMIO register. Writing an LSB of 1 terminates
+ * simulation. The upper 31 bits can pass extra metadata. We use all 0s
+ * to indicates success.
+ *
+ * This symbol doesn't need to be exported. The simulator is clever
+ * enough to find it even if it's local.
+ *
+ * HTIF is more general than our use here, so it's possible that someone else
+ * wants to use it as well, so we mark our symbol as weak.
+ */
+volatile uint32_t tohost[2] __attribute__((weak));
+#	endif
+
+static void platform_simulation_exit(uint32_t code)
+{
+#	ifdef RISCV_HTIF
+	// If this is using the standard RISC-V to-host mechanism, this will exit.
+	tohost[0] = 0x1 | (code << 1);
+	tohost[1] = 0;
+#	endif
+}
+#endif
diff --git a/sdk/include/platform/ibex/platform-simulation_exit.hh b/sdk/include/platform/ibex/platform-simulation_exit.hh
new file mode 100644
index 0000000..7d5d362
--- /dev/null
+++ b/sdk/include/platform/ibex/platform-simulation_exit.hh
@@ -0,0 +1,18 @@
+// Copyright Microsoft and CHERIoT Contributors.
+// SPDX-License-Identifier: MIT
+
+#pragma once
+
+#ifdef SIMULATION
+#	include <stdint.h>
+
+static void platform_simulation_exit(uint32_t code)
+{
+#	ifdef IBEX_SAFE
+	// If we didn't exit with to-host, try writing a non-ASCII character to the
+	// UART.  This is how we exit the CHERIoT Ibex simulator for the SAFE
+	// platform.
+	MMIO_CAPABILITY(Uart, uart)->blocking_write(0x80 + code);
+#	endif
+}
+#endif
diff --git a/sdk/include/platform/sunburst/platform-pwm.hh b/sdk/include/platform/sunburst/platform-pwm.hh
index 60f1704..727af3b 100644
--- a/sdk/include/platform/sunburst/platform-pwm.hh
+++ b/sdk/include/platform/sunburst/platform-pwm.hh
@@ -1,37 +1,20 @@
 #pragma once
 #include <debug.hh>
 #include <stdint.h>
+#include <utils.hh>
 
-/**
- * A driver for Sonata's Pulse-Width Modulation (PWM).
- *
- * Documentation source can be found at:
- * https://github.com/lowRISC/sonata-system/blob/97a525c48f7bf051b999d0178dba04859819bc5e/doc/ip/pwm.md
- *
- * Rendered documentation is served from:
- * https://lowrisc.github.io/sonata-system/doc/ip/pwm.html
- */
-struct SonataPulseWidthModulation
+namespace SonataPulseWidthModulation
 {
 	/**
-	 * Flag to set when debugging the driver for UART log messages.
+	 * A driver for Sonata's Pulse-Width Modulation (PWM).
+	 *
+	 * Documentation source can be found at:
+	 * https://github.com/lowRISC/sonata-system/blob/97a525c48f7bf051b999d0178dba04859819bc5e/doc/ip/pwm.md
+	 *
+	 * Rendered documentation is served from:
+	 * https://lowrisc.github.io/sonata-system/doc/ip/pwm.html
 	 */
-	static constexpr bool DebugDriver = false;
-
-	/**
-	 * Helper for conditional debug logs and assertions.
-	 */
-	using Debug = ConditionalDebug<DebugDriver, "PWM">;
-
-	/**
-	 * The number of pulse-width modulated outputs that are available.
-	 */
-	static constexpr size_t OutputCount = 1;
-
-	/**
-	 * The pulse-width modulation outputs available on Sonata.
-	 */
-	struct OutputRegisters
+	struct Output : private utils::NoCopyNoMove
 	{
 		/**
 		 * The duty cycle of the wave, represented as a width counter. That
@@ -46,23 +29,45 @@
 		 * as only an 8 bit counter is being used.
 		 */
 		uint32_t period;
-	} outputs[OutputCount];
 
-	/*
-	 * Sets the output of a specified pulse-width modulated output.
-	 *
-	 * The first argument is the index of the output. The second argument is
-	 * the period (length) of the output wave represented as a counter of
-	 * system clock cycles. The third argument is the number of clock cycles
-	 * for which a high pulse is sent within that period.
-	 *
-	 * So for example `output_set(0, 200, 31)` should set a 15.5% output.
-	 */
-	void output_set(uint32_t index, uint8_t period, uint8_t dutyCycle) volatile
+		/*
+		 * Sets the output of a specified pulse-width modulated output.
+		 *
+		 * @param period The length of the output wave represented as a counter
+		 * of system clock cycles.
+		 * @param dutyCycle The number of clock cycles for which a high pulse is
+		 * sent within that period.
+		 *
+		 * So for example `output_set(0, 200, 31)` should set a 15.5% output.
+		 * For a constant high output (100% duty cycle), set the dutyCycle >
+		 * period.
+		 */
+		void output_set(uint8_t period, uint8_t dutyCycle) volatile
+		{
+			this->period    = period;
+			this->dutyCycle = dutyCycle;
+		}
+	};
+
+	/// A convenience structure that can map onto multiple PWM outputs.
+	template<size_t NumberOfPwms = 6>
+	struct Array
 	{
-		Debug::Assert(index < OutputCount, "Specified PWM is out of range");
-		Debug::Assert(dutyCycle <= period, "Duty cycle cannot exceed 100%");
-		outputs[index].period    = period;
-		outputs[index].dutyCycle = dutyCycle;
-	}
-};
+		Output output[NumberOfPwms];
+
+		template<size_t Index>
+		volatile Output *get() volatile
+		{
+			static_assert(Index < NumberOfPwms, "PWM index out of bounds");
+			return output + Index;
+		}
+	};
+
+	/**
+	 * There are six general purpose PWM outputs are general purpose that can be
+	 * pinmuxed to different outputs.
+	 */
+	using General = Array<6>;
+	/// There is one dedicated PWM for the LCD backlight.
+	using LcdBacklight = Output;
+} // namespace SonataPulseWidthModulation
diff --git a/sdk/include/queue.h b/sdk/include/queue.h
index 68743da..1ce1901 100644
--- a/sdk/include/queue.h
+++ b/sdk/include/queue.h
@@ -102,11 +102,11 @@
  * and makes them fail to acquire the lock, before deallocating the underlying
  * allocation.
  *
- * This must be called on an unrestricted queue handle (*not* one returned by
- * `queue_make_receive_handle` or `queue_make_send_handle`).
+ * Returns 0 on success. This can fail only if deallocation would fail and will,
+ * in these cases, return the same error codes as `heap_free`.
  *
- * Returns 0 on success. On failure, returns `-EPERM` if the queue handle is
- * restricted (see comment above).
+ * This function will check the heap capability first and so will avoid
+ * upgrading the locks if freeing the queue would fail.
  */
 int __cheri_libcall queue_destroy(struct SObjStruct   *heapCapability,
                                   struct MessageQueue *handle);
diff --git a/sdk/include/string.h b/sdk/include/string.h
index 965a02b..2dd75f1 100644
--- a/sdk/include/string.h
+++ b/sdk/include/string.h
@@ -6,21 +6,27 @@
 #include <stddef.h>
 #include <stdint.h>
 
-int __cheri_libcall   memcmp(const void *str1, const void *str2, size_t count);
-void *__cheri_libcall memcpy(void *dest, const void *src, size_t n);
-void *__cheri_libcall memset(void *, int, size_t);
-void *__cheri_libcall memmove(void *dest, const void *src, size_t n);
-void *__cheri_libcall memchr(const void *, int, size_t);
-void *__cheri_libcall memrchr(const void *, int, size_t);
-size_t __cheri_libcall      strlen(const char *str);
-int __cheri_libcall         strncmp(const char *s1, const char *s2, size_t n);
-char *__cheri_libcall       strncpy(char *dest, const char *src, size_t n);
-int __cheri_libcall         strcmp(const char *s1, const char *s2);
-char *__cheri_libcall       strnstr(const char *haystack,
-                                    const char *needle,
-                                    size_t      haystackLength);
-char *__cheri_libcall       strchr(const char *s, int c);
-size_t __cheri_libcall      strlcpy(char *dest, const char *src, size_t n);
+int __cheri_libcall    memcmp(const void *str1,
+                              const void *str2,
+                              size_t      count) __asm__("memcmp");
+void *__cheri_libcall  memcpy(void       *dest,
+                              const void *src,
+                              size_t      n) __asm__("memcpy");
+void *__cheri_libcall  memset(void *, int, size_t) __asm__("memset");
+void *__cheri_libcall  memmove(void       *dest,
+                               const void *src,
+                               size_t      n) __asm__("memmove");
+void *__cheri_libcall  memchr(const void *, int, size_t);
+void *__cheri_libcall  memrchr(const void *, int, size_t);
+size_t __cheri_libcall strlen(const char *str);
+int __cheri_libcall    strncmp(const char *s1, const char *s2, size_t n);
+char *__cheri_libcall  strncpy(char *dest, const char *src, size_t n);
+int __cheri_libcall    strcmp(const char *s1, const char *s2);
+char *__cheri_libcall  strnstr(const char *haystack,
+                               const char *needle,
+                               size_t      haystackLength);
+char *__cheri_libcall  strchr(const char *s, int c);
+size_t __cheri_libcall strlcpy(char *dest, const char *src, size_t n);
 
 /**
  * Explicit bzero is a memset variant that the compiler is not permitted to
diff --git a/sdk/lib/freestanding/compat.S b/sdk/lib/freestanding/compat.S
new file mode 100644
index 0000000..b6b90c7
--- /dev/null
+++ b/sdk/lib/freestanding/compat.S
@@ -0,0 +1,31 @@
+// Copyright CHERIoT Contributors.
+// SPDX-License-Identifier: MIT
+
+/**
+ * This file contains compatibility aliases for exporting the freestanding
+ * library functions as both mangled and unmangled symbols.
+ */
+
+/**
+ * Given a function named `function_name`, export it as a library function
+ * named `export_function_name`.
+ */
+.macro EXPORT_COMPATIBILITY_ALIAS export_function_name, function_name, flags
+	.section .compartment_exports,"aR",@progbits
+	.type    __library_export_libcalls_\export_function_name\(),@object
+	.global  __library_export_libcalls_\export_function_name\()
+    .p2align 2
+  __library_export_libcalls_\export_function_name\():
+	.half \function_name - __compartment_pcc_start
+	// Stack usage: Ignored for library exports
+	.byte 0
+	// Flags, only interrupt state is used for library exports, 0 is inherited
+	.byte \flags
+	.size __library_export_libcalls_\export_function_name, 40
+	.previous
+.endm
+
+EXPORT_COMPATIBILITY_ALIAS _Z6memcmpPKvS0_j, memcmp, 3
+EXPORT_COMPATIBILITY_ALIAS _Z6memcpyPvPKvj, memcpy, 3
+EXPORT_COMPATIBILITY_ALIAS _Z6memsetPvij, memset, 2
+EXPORT_COMPATIBILITY_ALIAS _Z7memmovePvPKvj, memmove, 3
diff --git a/sdk/lib/freestanding/memcmp.c b/sdk/lib/freestanding/memcmp.c
index 8f3eef9..9a3a518 100644
--- a/sdk/lib/freestanding/memcmp.c
+++ b/sdk/lib/freestanding/memcmp.c
@@ -34,11 +34,12 @@
 
 #include <cdefs.h>
 #include <stddef.h>
+#include <string.h>
 
 /*
  * Compare memory regions.
  */
-int __cheri_libcall
+int
 memcmp(const void *s1, const void *s2, size_t n)
 {
 	if (n != 0) {
diff --git a/sdk/lib/freestanding/memcpy.c b/sdk/lib/freestanding/memcpy.c
index 5b7c791..80e880a 100644
--- a/sdk/lib/freestanding/memcpy.c
+++ b/sdk/lib/freestanding/memcpy.c
@@ -45,6 +45,7 @@
 
 #include <cdefs.h>
 #include <stddef.h>
+#include <string.h>
 
 typedef void *word;
 
@@ -54,7 +55,7 @@
 
 #define wmask (wsize - 1)
 
-void *__cheri_libcall memcpy(void *dst0, const void *src0, size_t length)
+void *memcpy(void *dst0, const void *src0, size_t length)
 {
 	char *      dst = dst0;
 	const char *src = src0;
@@ -119,7 +120,7 @@
 	return (dst0);
 }
 
-void *__cheri_libcall memmove(void *dst0, const void *src0, size_t length)
+void *memmove(void *dst0, const void *src0, size_t length)
 {
 	return memcpy(dst0, src0, length);
 }
diff --git a/sdk/lib/freestanding/memset.c b/sdk/lib/freestanding/memset.c
index c9e4c0a..8945d5c 100644
--- a/sdk/lib/freestanding/memset.c
+++ b/sdk/lib/freestanding/memset.c
@@ -34,11 +34,12 @@
 
 #include <cdefs.h>
 #include <stddef.h>
+#include <string.h>
 
 #define wsize sizeof(unsigned int)
 #define wmask (wsize - 1)
 
-void *__cheri_libcall memset(void *dst0, int c0, size_t length)
+void *memset(void *dst0, int c0, size_t length)
 {
 	size_t         t;
 	unsigned int   c;
diff --git a/sdk/lib/freestanding/xmake.lua b/sdk/lib/freestanding/xmake.lua
index 62f10fb..6daf6c5 100644
--- a/sdk/lib/freestanding/xmake.lua
+++ b/sdk/lib/freestanding/xmake.lua
@@ -1,2 +1,2 @@
 library("freestanding")
-  add_files("memcmp.c", "memcpy.c", "memset.c")
+  add_files("memcmp.c", "memcpy.c", "memset.c", "compat.S")
diff --git a/sdk/xmake.lua b/sdk/xmake.lua
index 0f26d6e..07a37c5 100644
--- a/sdk/xmake.lua
+++ b/sdk/xmake.lua
@@ -51,6 +51,17 @@
 stackCheckOption("allocator")
 stackCheckOption("scheduler")
 
+function testCheckOption(name)
+	option("testing-" .. name)
+		set_default(false)
+		set_description("Enable testing feature " .. name .. ". Do not enable this in builds that don't produce a UART log!")
+		set_showmenu(true)
+		set_category("Debugging")
+	option_end()
+end
+
+testCheckOption("model-output")
+
 -- Force -Oz irrespective of build config.  At -O0, we blow out our stack and
 -- require much stronger alignment.
 set_optimize("Oz")
@@ -284,7 +295,18 @@
 		local directory = path.directory(firmware)
 		firmware = path.filename(firmware)
 		local run = function(simulator)
-			os.execv(simulator, { firmware }, { curdir = directory })
+			local simargs = { firmware }
+			if get_config("testing-model-output") then
+				modeldir = path.join(scriptdir,
+				                     "..",
+				                     "scripts",
+				                     "model_output",
+				                     path.basename(target:values("board")),
+				                     "examples")
+				local modelout = path.join(modeldir, firmware .. ".txt")
+				simargs[#simargs+1] = modelout
+			end
+			os.execv(simulator, simargs, { curdir = directory })
 		end
 		-- Try executing the simulator from the sdk directory, if it's there.
 		local tools_directory = config.get("sdk")
diff --git a/tests/misc-test.cc b/tests/misc-test.cc
index dc09d77..e39b1e5 100644
--- a/tests/misc-test.cc
+++ b/tests/misc-test.cc
@@ -10,210 +10,274 @@
 
 using namespace CHERI;
 
-/**
- * Test timeouts.
- *
- * This test checks the following:
- *
- * - A timeout of zero would not block.
- * - `elapse` saturates values, i.e., a `remaining` value of zero will still be
- *   zero after a call to `elapse`, and an `elapsed` value of `UINT32_MAX`
- *   would still be `UINT32_MAX` after a call to `elapse`.
- * - An unlimited timeout is really unlimited, i.e., a call to `elapse` does
- *   not modify its `remaining` value, which blocks.
- */
-void check_timeouts()
+namespace
 {
-	debug_log("Test timeouts.");
 
-	// Create a zero timeout.
-	Timeout t{0};
-	// Ensure that a zero timeout does not block.
-	TEST(!t.may_block(), "A zero timeout should not block.");
-
-	// Create a zero timer with maximum elapsed time.
-	t = Timeout{UINT32_MAX /* elapsed */, 0 /* remaining */};
-	// Ensure that a call to `elapse` saturates both `elapsed` and
-	// `remaining`.
-	t.elapse(42);
-	TEST(t.remaining == 0,
-	     "`elapse` does not saturate the `remaining` value of a zero timer.");
-	TEST(t.elapsed == UINT32_MAX,
-	     "`elapse` does not saturate the `elapsed` value of a zero timer.");
-
-	// Create an unlimited timeout.
-	t = Timeout{UnlimitedTimeout /* remaining */};
-	// Ensure that a call to `elapse` does not modify the `remaining` value
-	// of the unlimited timeout.
-	t.elapse(42);
-	TEST(t.remaining == UnlimitedTimeout,
-	     "`elapse` alters the remaining value of an unlimited timeout.");
-	// Ensure that an unlimited timeout blocks.
-	TEST(t.may_block(), "An unlimited timeout should block.");
-}
-
-/**
- * Test memchr.
- *
- * This test checks the following:
- *
- * - memchr finds the first occurrence of the character when it is present
- *   (test for different values, particularly the first and the last one).
- * - memchr returns NULL when the string does not contain the character (test
- *   for non-NULL terminated string).
- * - memchr does not stop at \0 characters.
- * - memchr returns NULL for 0-size pointers.
- */
-void check_memchr()
-{
-	debug_log("Test memchr.");
-
-	char string[] = {'C', 'H', 'E', 'R', 'R', 'I', 'E', 'S'};
-
-	TEST(memchr(string, 'C', sizeof(string)) == &string[0],
-	     "memchr must return the first occurence of the character.");
-	TEST(memchr(string, 'R', sizeof(string)) == &string[3],
-	     "memchr must return the first occurence of the character.");
-	TEST(memchr(string, 'S', sizeof(string)) == &string[7],
-	     "memchr must return the first occurence of the character.");
-	TEST(memchr(string, 'X', sizeof(string)) == NULL,
-	     "memchr must return NULL when a character is not present.");
-
-	char stringWithNull[] = {'Y', 'E', 'S', '\0', 'N', 'O', '\0'};
-
-	TEST(memchr(stringWithNull, 'N', sizeof(stringWithNull)) ==
-	       &stringWithNull[4],
-	     "memchr must not stop at NULL characters.");
-
-	TEST(memchr(stringWithNull, 'N', 0) == NULL,
-	     "memchr must return NULL for zero-size pointers.");
-}
-
-/**
- * Test memrchr.
- *
- * This test checks the following:
- *
- * - memrchr finds the first occurrence of the character when it is present
- *   (test for different values, particularly the first and the last one).
- * - memrchr returns NULL when the string does not contain the character (test
- *   for non-NULL terminated string).
- * - memrchr does not stop at \0 characters.
- * - memrchr returns NULL for 0-size pointers.
- */
-void check_memrchr()
-{
-	debug_log("Test memrchr.");
-
-	char string[] = {'C', 'H', 'E', 'R', 'R', 'I', 'O', 'T'};
-
-	TEST(memchr(string, 'C', sizeof(string)) == &string[0],
-	     "memrchr must return the first occurence of the character.");
-	TEST(memrchr(string, 'R', sizeof(string)) == &string[4],
-	     "memrchr must return the first occurence of the character.");
-	TEST(memrchr(string, 'T', sizeof(string)) == &string[7],
-	     "memrchr must return the first occurence of the character.");
-	TEST(memrchr(string, 'X', sizeof(string)) == NULL,
-	     "memrchr must return NULL when a character is not present.");
-
-	char stringWithNull[] = {'F', 'U', '\0', 'B', 'A', 'R', '\0'};
-
-	TEST(memrchr(stringWithNull, 'F', sizeof(stringWithNull)) ==
-	       &stringWithNull[0],
-	     "memrchr must not stop at NULL characters.");
-
-	TEST(memrchr(stringWithNull, 'Y', 0) == NULL,
-	     "memrchr must return NULL for zero-size pointers.");
-}
-
-/**
- * Test pointer utilities.
- *
- * Not comprehensive, would benefit from being expanded at some point.
- */
-void check_pointer_utilities()
-{
-	debug_log("Test pointer utilities.");
-
-	int                              integer        = 42;
-	int                             *integerPointer = &integer;
-	ds::pointer::proxy::Pointer<int> pointer{integerPointer};
-
-	TEST((pointer == integerPointer) && (*pointer == 42),
-	     "The pointer proxy does not return the value of its proxy.");
-
-	int                              anotherInteger        = -100;
-	int                             *anotherIntegerPointer = &anotherInteger;
-	ds::pointer::proxy::Pointer<int> anotherPointer{anotherIntegerPointer};
-
-	pointer = anotherPointer;
-
-	TEST((pointer == anotherIntegerPointer) && (*pointer == -100),
-	     "The pointer proxy `=` operator does not correctly set the pointer.");
-}
-
-void check_shared_object(const char      *name,
-                         Capability<void> object,
-                         size_t           size,
-                         PermissionSet    permissions)
-{
-	debug_log("Checking shared object {}.", object);
-	TEST(object.length() == size,
-	     "Object {} is {} bytes, expected {}",
-	     name,
-	     object.length(),
-	     size);
-	TEST(object.permissions() == permissions,
-	     "Object {} has permissions {}, expected {}",
-	     name,
-	     PermissionSet{object.permissions()},
-	     permissions);
-}
-
-// This test is somewhat intimately familiar with parameters of CHERIoT's
-// capability encoding and so might need revision if that changes.
-void check_capability_set_inexact_at_most()
-{
-	void *p = malloc(3128);
-
-	debug_log("Test Capability::BoundsProxy::set_inexact_at_most with {}", p);
-
-	// Too many bits for mantissa, regardless of base alignment
+	/**
+	 * Test timeouts.
+	 *
+	 * This test checks the following:
+	 *
+	 * - A timeout of zero would not block.
+	 * - `elapse` saturates values, i.e., a `remaining` value of zero will still
+	 * be zero after a call to `elapse`, and an `elapsed` value of `UINT32_MAX`
+	 *   would still be `UINT32_MAX` after a call to `elapse`.
+	 * - An unlimited timeout is really unlimited, i.e., a call to `elapse` does
+	 *   not modify its `remaining` value, which blocks.
+	 */
+	void check_timeouts()
 	{
-		Capability<void> q      = {p};
-		size_t           reqlen = 2047;
-		q.bounds().set_inexact_at_most(reqlen);
-		debug_log("Requesting 2047 gives {}: {}", q.length(), q);
-		TEST(q.is_valid(), "set_inexact_at_most untagged");
-		TEST(q.length() < 2047, "set_inexact_at_most failed to truncate");
-		TEST(q.base() == q.address(), "set_inexact_at_most nonzero offset");
+		debug_log("Test timeouts.");
+
+		// Create a zero timeout.
+		Timeout t{0};
+		// Ensure that a zero timeout does not block.
+		TEST(!t.may_block(), "A zero timeout should not block.");
+
+		// Create a zero timer with maximum elapsed time.
+		t = Timeout{UINT32_MAX /* elapsed */, 0 /* remaining */};
+		// Ensure that a call to `elapse` saturates both `elapsed` and
+		// `remaining`.
+		t.elapse(42);
+		TEST(
+		  t.remaining == 0,
+		  "`elapse` does not saturate the `remaining` value of a zero timer.");
+		TEST(t.elapsed == UINT32_MAX,
+		     "`elapse` does not saturate the `elapsed` value of a zero timer.");
+
+		// Create an unlimited timeout.
+		t = Timeout{UnlimitedTimeout /* remaining */};
+		// Ensure that a call to `elapse` does not modify the `remaining` value
+		// of the unlimited timeout.
+		t.elapse(42);
+		TEST(t.remaining == UnlimitedTimeout,
+		     "`elapse` alters the remaining value of an unlimited timeout.");
+		// Ensure that an unlimited timeout blocks.
+		TEST(t.may_block(), "An unlimited timeout should block.");
 	}
 
-	// Fits in mantissa, but not reachable from misaligned base
+	/**
+	 * Test memchr.
+	 *
+	 * This test checks the following:
+	 *
+	 * - memchr finds the first occurrence of the character when it is present
+	 *   (test for different values, particularly the first and the last one).
+	 * - memchr returns NULL when the string does not contain the character
+	 * (test for non-NULL terminated string).
+	 * - memchr does not stop at \0 characters.
+	 * - memchr returns NULL for 0-size pointers.
+	 */
+	void check_memchr()
 	{
-		Capability<void> q = {p};
-		q.address() += 2;
-		size_t reqlen = 1024;
-		q.bounds().set_inexact_at_most(reqlen);
-		debug_log("Requesting 1024 at align 2 gives {}: {}", q.length(), q);
-		TEST(q.is_valid(), "set_inexact_at_most untagged");
-		TEST(q.length() < 1024, "set_inexact_at_most failed to truncate");
-		TEST(q.base() == q.address(), "set_inexact_at_most nonzero offset");
+		debug_log("Test memchr.");
+
+		char string[] = {'C', 'H', 'E', 'R', 'R', 'I', 'E', 'S'};
+
+		TEST(memchr(string, 'C', sizeof(string)) == &string[0],
+		     "memchr must return the first occurence of the character.");
+		TEST(memchr(string, 'R', sizeof(string)) == &string[3],
+		     "memchr must return the first occurence of the character.");
+		TEST(memchr(string, 'S', sizeof(string)) == &string[7],
+		     "memchr must return the first occurence of the character.");
+		TEST(memchr(string, 'X', sizeof(string)) == NULL,
+		     "memchr must return NULL when a character is not present.");
+
+		char stringWithNull[] = {'Y', 'E', 'S', '\0', 'N', 'O', '\0'};
+
+		TEST(memchr(stringWithNull, 'N', sizeof(stringWithNull)) ==
+		       &stringWithNull[4],
+		     "memchr must not stop at NULL characters.");
+
+		TEST(memchr(stringWithNull, 'N', 0) == NULL,
+		     "memchr must return NULL for zero-size pointers.");
 	}
 
-	// Fits in mantissa and reachable from misaligned base
+	/**
+	 * Test memrchr.
+	 *
+	 * This test checks the following:
+	 *
+	 * - memrchr finds the first occurrence of the character when it is present
+	 *   (test for different values, particularly the first and the last one).
+	 * - memrchr returns NULL when the string does not contain the character
+	 * (test for non-NULL terminated string).
+	 * - memrchr does not stop at \0 characters.
+	 * - memrchr returns NULL for 0-size pointers.
+	 */
+	void check_memrchr()
 	{
-		Capability<void> q = {p};
-		q.address() += 1;
-		size_t reqlen = 511;
-		q.bounds().set_inexact_at_most(reqlen);
-		debug_log("Requesting 511 at align 1 gives {}: {}", q.length(), q);
-		TEST(q.is_valid(), "set_inexact_at_most untagged");
-		TEST(q.length() == 511, "set_inexact_at_most truncated unnecessarily");
-		TEST(q.base() == q.address(), "set_inexact_at_most nonzero offset");
+		debug_log("Test memrchr.");
+
+		char string[] = {'C', 'H', 'E', 'R', 'R', 'I', 'O', 'T'};
+
+		TEST(memchr(string, 'C', sizeof(string)) == &string[0],
+		     "memrchr must return the first occurence of the character.");
+		TEST(memrchr(string, 'R', sizeof(string)) == &string[4],
+		     "memrchr must return the first occurence of the character.");
+		TEST(memrchr(string, 'T', sizeof(string)) == &string[7],
+		     "memrchr must return the first occurence of the character.");
+		TEST(memrchr(string, 'X', sizeof(string)) == NULL,
+		     "memrchr must return NULL when a character is not present.");
+
+		char stringWithNull[] = {'F', 'U', '\0', 'B', 'A', 'R', '\0'};
+
+		TEST(memrchr(stringWithNull, 'F', sizeof(stringWithNull)) ==
+		       &stringWithNull[0],
+		     "memrchr must not stop at NULL characters.");
+
+		TEST(memrchr(stringWithNull, 'Y', 0) == NULL,
+		     "memrchr must return NULL for zero-size pointers.");
 	}
 
-	free(p);
+	/**
+	 * Test pointer utilities.
+	 *
+	 * Not comprehensive, would benefit from being expanded at some point.
+	 */
+	void check_pointer_utilities()
+	{
+		debug_log("Test pointer utilities.");
+
+		int                              integer        = 42;
+		int                             *integerPointer = &integer;
+		ds::pointer::proxy::Pointer<int> pointer{integerPointer};
+
+		TEST((pointer == integerPointer) && (*pointer == 42),
+		     "The pointer proxy does not return the value of its proxy.");
+
+		int  anotherInteger        = -100;
+		int *anotherIntegerPointer = &anotherInteger;
+		ds::pointer::proxy::Pointer<int> anotherPointer{anotherIntegerPointer};
+
+		pointer = anotherPointer;
+
+		TEST(
+		  (pointer == anotherIntegerPointer) && (*pointer == -100),
+		  "The pointer proxy `=` operator does not correctly set the pointer.");
+	}
+
+	void check_shared_object(const char      *name,
+	                         Capability<void> object,
+	                         size_t           size,
+	                         PermissionSet    permissions)
+	{
+		debug_log("Checking shared object {}.", object);
+		TEST(object.length() == size,
+		     "Object {} is {} bytes, expected {}",
+		     name,
+		     object.length(),
+		     size);
+		TEST(object.permissions() == permissions,
+		     "Object {} has permissions {}, expected {}",
+		     name,
+		     PermissionSet{object.permissions()},
+		     permissions);
+	}
+
+	// This test is somewhat intimately familiar with parameters of CHERIoT's
+	// capability encoding and so might need revision if that changes.
+	void check_capability_set_inexact_at_most()
+	{
+		void *p = malloc(3128);
+
+		debug_log("Test Capability::BoundsProxy::set_inexact_at_most with {}",
+		          p);
+
+		// Too many bits for mantissa, regardless of base alignment
+		{
+			Capability<void> q      = {p};
+			size_t           reqlen = 2047;
+			q.bounds().set_inexact_at_most(reqlen);
+			debug_log("Requesting 2047 gives {}: {}", q.length(), q);
+			TEST(q.is_valid(), "set_inexact_at_most untagged");
+			TEST(q.length() < 2047, "set_inexact_at_most failed to truncate");
+			TEST(q.base() == q.address(), "set_inexact_at_most nonzero offset");
+		}
+
+		// Fits in mantissa, but not reachable from misaligned base
+		{
+			Capability<void> q = {p};
+			q.address() += 2;
+			size_t reqlen = 1024;
+			q.bounds().set_inexact_at_most(reqlen);
+			debug_log("Requesting 1024 at align 2 gives {}: {}", q.length(), q);
+			TEST(q.is_valid(), "set_inexact_at_most untagged");
+			TEST(q.length() < 1024, "set_inexact_at_most failed to truncate");
+			TEST(q.base() == q.address(), "set_inexact_at_most nonzero offset");
+		}
+
+		// Fits in mantissa and reachable from misaligned base
+		{
+			Capability<void> q = {p};
+			q.address() += 1;
+			size_t reqlen = 511;
+			q.bounds().set_inexact_at_most(reqlen);
+			debug_log("Requesting 511 at align 1 gives {}: {}", q.length(), q);
+			TEST(q.is_valid(), "set_inexact_at_most untagged");
+			TEST(q.length() == 511,
+			     "set_inexact_at_most truncated unnecessarily");
+			TEST(q.base() == q.address(), "set_inexact_at_most nonzero offset");
+		}
+
+		free(p);
+	}
+
+	/**
+	 * This is a regression test for #368.  There are many different ways for
+	 * the compiler to generate a memcmp call and this manages to trigger one of
+	 * the ones that wasn't being mangled the same way as others.  The run-time
+	 * behaviour of this test is irrelevant, we should get a linker failure if
+	 * the freestanding library and the compiler disagree on function names.
+	 */
+	void check_odd_memcmp()
+	{
+		std::string first  = "first";
+		std::string second = "second";
+		TEST((first == second) == false,
+		     "This test should never fail but exists to make sure that a "
+		     "comparison result is used");
+	}
+} // namespace
+
+void check_sealed_scoping()
+{
+	Capability<void> o{switcher_current_thread()};
+	TEST(o.is_valid() && (o.type() == CheriSealTypeSealedTrustedStacks),
+	     "Shared object cap not as expected: {}",
+	     o);
+
+	// Take the address of the o cap, requiring that it go out to memory.
+	Capability<Capability<void>> oP{&o};
+
+	/*
+	 * Load a copy of our sealed o cap through an authority that lacks
+	 * LoadGlobal permission.  The result should be identical to the original
+	 * but without global permission.
+	 */
+	Capability<Capability<void>> oPNoLoadGlobal = oP;
+	oPNoLoadGlobal.without_permissions(Permission::LoadGlobal);
+	const Capability<void> OLocal1 = *oPNoLoadGlobal;
+
+	TEST(OLocal1.is_valid(),
+	     "Loading global sealed cap through non-LoadGlobal invalid");
+	TEST_EQUAL(OLocal1.type(),
+	           o.type(),
+	           "Loading global sealed cap through non-LoadGlobal bad type");
+	TEST_EQUAL(OLocal1.permissions(),
+	           o.permissions().without(Permission::Global),
+	           "Loading global sealed cap through non-LoadGlobal bad perms");
+
+	/*
+	 * Use CAndPerm to shed Global from our o cap.
+	 * Spell this a little oddly to make sure we get CAndPerm with a mask of
+	 * all 1s but Global.  Using oLocal2.permissions().without() would do a
+	 * cgetperm and then candperm.
+	 */
+	Capability<void> oLocal2 = o;
+	oLocal2.without_permissions(Permission::Global);
+
+	TEST_EQUAL(oLocal2, OLocal1, "CAndPerm ~GL gone wrong");
 }
 
 int test_misc()
@@ -223,6 +287,8 @@
 	check_memrchr();
 	check_pointer_utilities();
 	check_capability_set_inexact_at_most();
+	check_sealed_scoping();
+
 	debug_log("Testing shared objects.");
 	check_shared_object("exampleK",
 	                    SHARED_OBJECT(void, exampleK),
@@ -247,5 +313,6 @@
 	                      void, test_word, true, false, false, false),
 	                    4,
 	                    {Permission::Global, Permission::Load});
+	check_odd_memcmp();
 	return 0;
 }
diff --git a/tests/multiwaiter-test.cc b/tests/multiwaiter-test.cc
index d9d99e9..b6b77dd 100644
--- a/tests/multiwaiter-test.cc
+++ b/tests/multiwaiter-test.cc
@@ -126,6 +126,7 @@
 	     "Queue reports ready to receive but should be empty.");
 	TEST(events[1].value == 1, "Futex reports no wake");
 
-	multiwaiter_delete(MALLOC_CAPABILITY, mw);
+	TEST_EQUAL(
+	  multiwaiter_delete(MALLOC_CAPABILITY, mw), 0, "Failed to clean up");
 	return 0;
 }