fix merge conflicts

Signed-off-by: Birgit Brecknell <[email protected]>
seL4 · Jul 21, 2024 · e98f540 · e98f540
2 parents 22bfaba + ce32484
commit e98f540
Show file tree

Hide file tree

Showing 18 changed files with 199 additions and 35 deletions.
diff --git a/tutorials/camkes-vm-crossvm/camkes-vm-crossvm.md b/tutorials/camkes-vm-crossvm/camkes-vm-crossvm.md
@@ -1,7 +1,7 @@
 <!--
-  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
-Copyright 2024, seL4 Project a Series of LF Projects, LLC.
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
   SPDX-License-Identifier: BSD-2-Clause
 -->

diff --git a/tutorials/camkes-vm-linux/camkes-vm-linux.md b/tutorials/camkes-vm-linux/camkes-vm-linux.md
@@ -1,7 +1,7 @@
 <!--
-  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
-Copyright 2024, seL4 Project a Series of LF Projects, LLC.
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
   SPDX-License-Identifier: BSD-2-Clause
 -->
@@ -448,7 +448,7 @@ GetDefaultLinuxMinor(linux_minor)
 GetDefaultLinuxMd5(linux_md5)
 # Download and Configure our Linux sources
 DownloadLinux(${linux_major} ${linux_minor} ${linux_md5} vm_linux_extract_dir download_vm_linux)
-set(linux_config "${CAMKES_VM_LINUX_DIR}/linux_configs/${linux_major}.${linux_minor}/32/config")
+set(linux_config "${CAMKES_VM_LINUX_DIR}/linux_configs/${linux_major}.${linux_minor}/32/config.backup-singlecore")
 set(linux_symvers "${CAMKES_VM_LINUX_DIR}/linux_configs/${linux_major}.${linux_minor}/32/Module.symvers")
 ConfigureLinux(${vm_linux_extract_dir} ${linux_config} ${linux_symvers} configure_vm_linux
     DEPENDS download_vm_linux
@@ -539,7 +539,7 @@ In the function `main_continued` register \`poke_handler\`:
 vm_reg_new_vmcall_handler(&vm, poke_handler, 4); // <--- added
 
 /* Now go run the event loop */
-vmm_run(&vm);
+vm_run(&vm);
 ```
 
 Rebuild the project and try out the hypercall + module:

diff --git a/tutorials/capabilities/capabilities.md b/tutorials/capabilities/capabilities.md
@@ -1,5 +1,5 @@
 <!--
-  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
   Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
@@ -8,13 +8,17 @@
 
 /*? declare_task_ordering(['cnode-start', 'cnode-size', 'cnode-copy', 'cnode-delete', 'cnode-invoke']) ?*/
 
-# Capabilitieshelloo
+# Capabilities
 
 You will learn:
 1. The jargon CNode, CSpace, CSlot.
 2. How to invoke a capability.
 3. How to delete and copy CSlots.
 
+You will learn:
+1. The jargon CNode, CSpace, CSlot.
+2. How to invoke a capability.
+3. How to delete and copy CSlots.
 
 ## Initialising
 
@@ -249,6 +253,14 @@ The third line stating the number of slots in the CSpace, is incorrect, and your
 
 </details>
 
+<details markdown='1'>
+<summary style="display:list-item"><em>Quick solution</em></summary>
+
+```c
+    size_t initial_cnode_object_size_bytes = initial_cnode_object_size * (1u << seL4_SlotBits);
+```
+</details>
+
 ### Copy a capability between CSlots
 
 After the output showing the number of bytes in the CSpace, you will see an error:
@@ -389,7 +401,6 @@ [email protected]:56 Failed to suspend current thread
 <details markdown='1'>
 <summary style="display:list-item"><em>Quick solution</em></summary>
 
-
 ```c
 /*-- filter TaskContent("cnode-invoke", TaskContentType.COMPLETED, subtask='invoke', completion='Suspending current thread') -*/
     printf("Suspending current thread\n");

diff --git a/tutorials/dynamic-1/dynamic-1.md b/tutorials/dynamic-1/dynamic-1.md
@@ -1,7 +1,7 @@
 <!--
-  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
-Copyright 2024, seL4 Project a Series of LF Projects, LLC.
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
   SPDX-License-Identifier: BSD-2-Clause
 -->

diff --git a/tutorials/dynamic-2/dynamic-2.md b/tutorials/dynamic-2/dynamic-2.md
@@ -1,5 +1,5 @@
 <!--
-  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
 Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 

diff --git a/tutorials/dynamic-3/dynamic-3.md b/tutorials/dynamic-3/dynamic-3.md
@@ -1,7 +1,7 @@
 <!--
-  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
-Copyright 2024, seL4 Project a Series of LF Projects, LLC.
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
   SPDX-License-Identifier: BSD-2-Clause
 -->

diff --git a/tutorials/dynamic-4/dynamic-4.md b/tutorials/dynamic-4/dynamic-4.md
@@ -1,7 +1,7 @@
 <!--
-  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
-Copyright 2024, seL4 Project a Series of LF Projects, LLC.
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
   SPDX-License-Identifier: BSD-2-Clause
 -->

diff --git a/tutorials/fault-handlers/fault-handlers.md b/tutorials/fault-handlers/fault-handlers.md
@@ -1,5 +1,5 @@
 <!--
-  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
   Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 

diff --git a/tutorials/hello-camkes-0/hello-camkes-0.md b/tutorials/hello-camkes-0/hello-camkes-0.md
@@ -1,7 +1,7 @@
 <!--
-  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
-Copyright 2024, seL4 Project a Series of LF Projects, LLC.
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
   SPDX-License-Identifier: BSD-2-Clause
 -->

diff --git a/tutorials/hello-camkes-1/hello-camkes-1.md b/tutorials/hello-camkes-1/hello-camkes-1.md
@@ -1,7 +1,7 @@
 <!--
-  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
-Copyright 2024, seL4 Project a Series of LF Projects, LLC.
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
   SPDX-License-Identifier: BSD-2-Clause
 -->

diff --git a/tutorials/hello-camkes-2/hello-camkes-2.md b/tutorials/hello-camkes-2/hello-camkes-2.md
@@ -1,7 +1,7 @@
 <!--
-  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
-Copyright 2024, seL4 Project a Series of LF Projects, LLC.
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
   SPDX-License-Identifier: BSD-2-Clause
 -->

diff --git a/tutorials/interrupts/interrupts.md b/tutorials/interrupts/interrupts.md
@@ -1,5 +1,5 @@
 <!--
-  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
   Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 

diff --git a/tutorials/ipc/ipc.md b/tutorials/ipc/ipc.md
@@ -1,5 +1,5 @@
 <!--
-  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
   Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
@@ -298,7 +298,6 @@ does not respond, or wait for new messages from this point.
              printf("\n");
 /*-- endfilter -*/
 ```
-
 </details>
 
 At this point, you should see a single word output to the console in a loop.
@@ -334,6 +333,18 @@ This is because the server does not reply to the client, and continues to spin i
 ```
 </details>
 
+<details markdown='1'>
+<summary style="display:list-item"><em>Quick solution</em></summary>
+
+```c
+    info = seL4_ReplyRecv(endpoint, info, &sender);
+    for (int i = 0; i < seL4_MessageInfo_get_length(info); i++) {
+        printf("%c", (char) seL4_GetMR(i));
+    }
+    printf("\n");
+```
+</details>
+
 Now the output should be something like this:
 
 ```
@@ -377,6 +388,35 @@ capability for each sender. You can use `free_slot` to store the reply capabilit
 </details>
 
 
+<details markdown='1'>
+<summary style="display:list-item"><em>Quick solution</em></summary>
+
+```c
+    } else {
+
+        for (int i = 0; i < seL4_MessageInfo_get_length(info); i++) {
+                 printf("%c", (char) seL4_GetMR(i));
+             }
+             printf("\n");
+
+              error = seL4_CNode_SaveCaller(cnode, free_slot, seL4_WordBits);
+              assert(error == 0);
+              info = seL4_Recv(endpoint, &sender);
+              for (int i = 0; i < seL4_MessageInfo_get_length(info); i++) {
+                 printf("%c", (char) seL4_GetMR(i));
+              }
+              printf("\n");
+              seL4_Send(free_slot, seL4_MessageInfo_new(0, 0, 0, 0));
+
+             info = seL4_ReplyRecv(endpoint, info, &sender);
+        }
+    }
+
+```
+
+</details>
+
+
 Depending on your approach, successful output should look something like this:
 ```
 Client 2: received badged endpoint

diff --git a/tutorials/mapping/mapping.md b/tutorials/mapping/mapping.md
@@ -1,5 +1,5 @@
 <!--
-  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
   Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
@@ -160,6 +160,16 @@ the number of bits in the virtual address that could not be resolved due to miss
 ```
 </details>
 
+<details markdown='1'>
+<summary style="display:list-item"><em>Quick solution</em></summary>
+
+```c
+    // TODO map a page directory object
+    error = seL4_X86_PageDirectory_Map(pd,seL4_CapInitThreadVSpace, TEST_VADDR, seL4_X86_Default_VMAttributes);
+    assert(error == seL4_NoError);
+```
+</details>
+
 On success, you should see the following:
 ```
 Missing intermediate paging structure at level 21
@@ -192,6 +202,16 @@ Note that in the above output, the number of failed bits has changed from `30` t
 
 </details>
 
+<details markdown='1'>
+<summary style="display:list-item"><em>Quick solution</em></summary>
+
+```c
+    // map a page table object
+    error = seL4_X86_PageTable_Map(pt, seL4_CapInitThreadVSpace, TEST_VADDR, seL4_X86_Default_VMAttributes);
+    assert(error == seL4_NoError);
+```
+</details>
+
 On success, you should see the following:
 ```
 Read x: 0
@@ -238,6 +258,16 @@ that the fault occured on (address).
 
 </details>
 
+<details markdown='1'>
+<summary style="display:list-item"><em>Quick solution</em></summary>
+
+```c
+    // remap the page
+    error = seL4_X86_Page_Map(frame, seL4_CapInitThreadVSpace, TEST_VADDR, seL4_ReadWrite, seL4_X86_Default_VMAttributes);
+    assert(error == seL4_NoError);
+```
+</details>
+
 ### Unmapping pages
 
 Pages can be unmapped by either using `Unmap` invocations on the page or any intermediate paging structure, or deleting

diff --git a/tutorials/mcs/mcs.md b/tutorials/mcs/mcs.md
@@ -1,5 +1,5 @@
 <!--
-  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
   Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
@@ -21,8 +21,6 @@ Learn:
 3. The jargon *passive server*. 
 4. How to spawn round-robin and periodic threads.
 
-
-
 ## Initialising
 
 Then initialise the tutorial:
@@ -219,6 +217,16 @@ Yield
 </details>
 
 
+<details markdown='1'>
+<summary style="display:list-item"><em>Quick solution</em></summary>
+
+```c
+    error = seL4_SchedControl_Configure(sched_control, sched_context, 0.9 * US_IN_S, 1 * US_IN_S, 0, 0);
+    ZF_LOGF_IF(error != seL4_NoError, "Failed to configure schedcontext");
+```
+</details>
+
+
 By completing this task successfully, the output will not change, but the rate that the output is
 printed will slow: each subsequent line should be output once the period has elapsed. You should now
 be able to see the loop where the `mcs.c` process and `spinner.c` process alternate, until the `mcs.c`
@@ -321,6 +329,15 @@ Your next task is to use a different process, `sender` to experiment with sporad
     ZF_LOGF_IF(error != seL4_NoError, "Failed to bind schedcontext");
 /*-- endfilter -*/
 ```
+<details markdown='1'>
+<summary style="display:list-item"><em>Quick solution</em></summary>
+
+```c
+    error = seL4_SchedContext_Bind(sched_context, sender_tcb);
+    ZF_LOGF_IF(error != seL4_NoError, "Failed to bind schedcontext");
+```
+
+</details>
 
 </details>
 
@@ -392,6 +409,15 @@ not have a scheduling context, and needs one to initialise.
     ZF_LOGF_IF(error != seL4_NoError, "Failed to bind sched_context to server_tcb");
 /*-- endfilter -*/
 ```
+<details markdown='1'>
+<summary style="display:list-item"><em>Quick solution</em></summary>
+
+```c
+    error = seL4_SchedContext_Bind(sched_context, server_tcb);
+    ZF_LOGF_IF(error != seL4_NoError, "Failed to bind sched_context to server_tcb");
+```
+
+</details>
 
 </details>
 
@@ -512,6 +538,15 @@ The code then binds the scheduling context back to `spinner_tcb`, which starts y
     ZF_LOGF_IF(error != seL4_NoError, "Failed to set timeout fault endpoint for spinner");
 /*-- endfilter -*/
 ```
+<details markdown='1'>
+<summary style="display:list-item"><em>Quick solution</em></summary>
+
+```c
+    error = seL4_TCB_SetTimeoutEndpoint(spinner_tcb, endpoint);
+    ZF_LOGF_IF(error, "Failed to bind sched_context to spinner_tcb");
+```
+
+</details>
 
 </details>
 

diff --git a/tutorials/notifications/notifications.md b/tutorials/notifications/notifications.md
@@ -1,5 +1,5 @@
 <!--
-  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
+  Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
   Copyright 2024, seL4 Project a Series of LF Projects, LLC.