diff --git a/Tutorials/GettingStarted/overview.md b/Tutorials/GettingStarted/overview.md deleted file mode 100644 index 40aa091f8b..0000000000 --- a/Tutorials/GettingStarted/overview.md +++ /dev/null @@ -1,23 +0,0 @@ -We have developed a series of tutorials to introduce seL4 and -developing systems on seL4. - -The tutorials are split into a number of broad categories: - -- [About seL4](about-seL4) and [Getting started with the Microkit tutorial](microkit) introduce seL4 concepts. -- The [seL4 Kernel tutorials](../seL4Kernel/overview.md) are a deep dive into seL4 concepts. -- [MCS](../MCS/mcs-extensions) introduces seL4 MCS extensions. -- [Dynamic Libraries](../DynamicLibraries/initialisation.md) covers the libraries that have been developed for rapidly prototyping systems on seL4. -- [CAmkES](../CAmkES/hello-camkes.md) is a platform for building componentised systems for embedded platforms. -- [Microkit](https://trustworthy.systems/projects/microkit/tutorial/)is an operating system framework on top of seL4 provides a small set of simple abstractions that ease the design and implementation of statically structured systems on seL4. (Links to the same tutorial as in the [Getting Started](../GettingStarted/microkit) section.) -- [Rust](https://github.com/seL4/rust-sel4) provide crates for supporting the use of Rust in seL4 userspace. - -

Resources

-Additional resources to assist with learning: -- The [seL4 manual](https://sel4.systems/Info/Docs/seL4-manual-latest.pdf) -- [API references](../../projects/sel4/api-doc) -- The [How to](../Resources/how-to) page provides links to tutorial solutions as quick references for seL4 calls and methods. -- [FAQs](../../projects/sel4/frequently-asked-questions) -- [Debugging guide](../../projects/sel4-tutorials/debugging-guide) -- [Discourse forum](https://sel4.discourse.group/) -- [Developer mailing list](https://lists.sel4.systems/postorius/lists/devel.sel4.systems/) -- [Mattermost channel](https://mattermost.trustworthy.systems/sel4-external/channels/web-doc-revamp) diff --git a/Tutorials/Resources/how-to.md b/Tutorials/Resources/how-to.md index bbeb2badd5..9975779210 100644 --- a/Tutorials/Resources/how-to.md +++ b/Tutorials/Resources/how-to.md @@ -69,88 +69,92 @@ seL4Kernel/ipc#use-capability-transfer-to-send-the-badged-capability) - [Use passive servers](../MCS/mcs-extensionspassive-servers) - [Configure fault endpoints](../MCS/mcs-extensionsconfiguring-a-fault-endpoint-on-the-mcs-kernel) -## Dynamic libraries - - [Initiliasation & threading](../DynamicLibraries/initialisation) - - [Obtain BootInfo](../DynamicLibraries/initialisation#obtain-bootinfo) - - [Initialise simple](../DynamicLibraries/initialisation#initialise-simple) - - [Use simple to print BootInfo](../DynamicLibraries/initialisation#use-simple-to-print-bootinfo) - - [Initialise an allocator](../DynamicLibraries/initialisation#initialise-an-allocator) - - [Obtain a generic allocation interface (vka)](../DynamicLibraries/initialisation#obtain-a-generic-allocation-interface-vka) - - [Find the CSpace root cap](../DynamicLibraries/initialisation#find-the-cspace-root-cap) - - [Find the VSpace root cap](../DynamicLibraries/initialisation#find-the-vspace-root-cap) - - [Allocate a TCB Object](../DynamicLibraries/initialisation#allocate-a-tcb-object) - - [Configure the new TCB](../DynamicLibraries/initialisation#configure-the-new-tcb) - - [Name the new TCB](../DynamicLibraries/initialisation#name-the-new-tcb) - - [Set the instruction pointer](../DynamicLibraries/initialisation#set-the-instruction-pointer) - - [Write the registers](../DynamicLibraries/initialisation#write-the-registers) - - [Start the new thread](../DynamicLibraries/initialisation#start-the-new-thread) - - [IPC](../DynamicLibraries/ipc) - - [Allocate an IPC buffer](../DynamicLibraries/ipc#allocate-an-ipc-buffer) - - [Allocate a page table](../DynamicLibraries/ipc#allocate-a-page-table) - - [Map a page table](../DynamicLibraries/ipc#map-a-page-table) - - [Map a page](../DynamicLibraries/ipc#map-a-page) - - [Allocate an endpoint](../DynamicLibraries/ipc#allocate-an-endpoint) - - [Badge an endpoint](../DynamicLibraries/ipc#badge-an-endpoint) - - [Set a message register](../DynamicLibraries/ipc#message-registers) - - [Send and wait for a reply](../DynamicLibraries/ipc#ipc) - - [Receive a reply](../DynamicLibraries/ipc#receive-a-reply) - - [Receive an IPC](../DynamicLibraries/ipc#receive-an-ipc) - - [Validate a message](../DynamicLibraries/ipc#validate-the-message) - - [Write the message registers](../DynamicLibraries/ipc#write-the-message-registers) - - [Reply to a message](../DynamicLibraries/ipc#reply-to-a-message) -- [Processes & Elf loading](../DynamicLibraries/processes) - - [Create a VSpace object](../DynamicLibraries/processes#virtual-memory-management) - - [Configure a process](../DynamicLibraries/processes#configure-a-process) - - [Get a cspacepath](../DynamicLibraries/processes#get-a-cspacepath) - - [Badge a capability](../DynamicLibraries/processes#badge-a-capability) - - [Spawn a process](../DynamicLibraries/processes#spawn-a-process) - - [Receive a message](../DynamicLibraries/processes#receive-a-message) - - [Send a reply](../DynamicLibraries/processes#send-a-reply) - - [Initiate communications by using seL4_Call](../DynamicLibraries/processes#client-call) - - [Timer](../DynamicLibraries/timer) - - [Allocate a notification object](../DynamicLibraries/timer#allocate-a-notification-object) - - [Initialise a timer](../DynamicLibraries/timer#initialise-the-timer) - - [Use a timer](../DynamicLibraries/timer#use-the-timer) - - [Handle an interrupt](../DynamicLibraries/timer#handle-the-interrupt) - - [Destroy a timer](../DynamicLibraries/timer#destroy-the-timer) - - ## [CAmkES](../CAmkES/) - - [A basic CAmkES application](../CAmkES/camkes1) - - [Define instance in the composition section of the ADL](../CAmkES/camkes1#define-instance-in-the-composition-section-of-the-adl) - - [Add a connection](../CAmkES/camkes1#add-a-connection) - - [Define an interface](../CAmkES/camkes1#define-an-interface) - - [Implement a RPC function](../CAmkES/camkes1#implement-a-rpc-function) - - [Invoke a RPC function](../CAmkES/camkes1#invoke-a-rpc-function) - - [Events in CAmkES](../CAmkES/camkes2) - - [Specify an events interface](../CAmkES/camkes2#specify-an-events-interface) - - [Wait for data to become available](../CAmkES/camkes2#wait-for-data-to-become-available) - - [Signal that data is available](../CAmkES/camkes2#signal-that-data-is-available) - - [Register a callback handler](../CAmkES/camkes2#register-a-callback-handler) - - [Specify dataport interfaces](../CAmkES/camkes2#specify-an-events-interface) - - [Specify dataport connections](../CAmkES/camkes2#specify-dataport-connections) - - [Copy strings to an untyped dataport](../CAmkES/camkes2#copy-strings-to-an-untyped-dataport) - - [Read the reply data from a typed dataport](../CAmkES/camkes2#read-the-reply-data-from-a-typed-dataport) - - [Send data using dataports](../CAmkES/camkes2#send-data-using-dataports) - - [Read data from an untyped dataport](../CAmkES/camkes2#read-data-from-an-untyped-dataport) - - [Put data into a typed dataport](../CAmkES/camkes2#put-data-into-a-typed-dataport) - - [Read data from a typed dataport](../CAmkES/camkes2#read-data-from-a-typed-dataport) - - [Set component priorities](../CAmkES/camkes2#set-component-priorities) - - [Restrict access to dataports](../CAmkES/camkes2#restrict-access-to-dataports) - - [Test the read and write permissions on the dataport](../CAmkES/camkes2#test-the-read-and-write-permissions-on-the-dataport) - - [CAmkES Timer](../CAmkES/camkes) - - [Instantiate a Timer and Timerbase](../CAmkES/camkes3#task-1) - - [Connect a timer driver component](../CAmkES/camkes3#task-2) - - [Configure a timer hardware component instance](../CAmkES/camkes3#task-3) - - [Call into a supplied driver to handle the interrupt](../CAmkES/camkes3#task-4) - - [Stop a timer](../CAmkES/camkes3#task-5) - - [Acknowledge an interrupt](../CAmkES/camkes3#task-6) - - [Get a timer handler](../CAmkES/camkes3#task-7) - - [Start a timer](../CAmkES/camkes3#task-8) - - [Implement a RPC interface](../CAmkES/camkes3#task-9) - - [Set a timer interrupt](../CAmkES/camkes3#task-10) - - [Instantiate a TimerDTB component](../CAmkES/camkes3#task-1-1) - - [Connect interfaces using the seL4DTBHardware connector](../CAmkES/camkes3#task-2-1) - - [Configure the `TimerDTB` component](../CAmkES/camkes3#task-3-1) - - -(../CAmkES/camkes3 -(../CAmkES/camkes3 +## [Dynamic libraries](../DynamicLibraries/initialisation) +### [Initiliasation & threading](../DynamicLibraries/initialisation) + - [Obtain BootInfo](../DynamicLibraries/initialisation#obtain-bootinfo) + - [Initialise simple](../DynamicLibraries/initialisation#initialise-simple) + - [Use simple to print BootInfo](../DynamicLibraries/initialisation#use-simple-to-print-bootinfo) + - [Initialise an allocator](../DynamicLibraries/initialisation#initialise-an-allocator) + - [Obtain a generic allocation interface (vka)](../DynamicLibraries/initialisation#obtain-a-generic-allocation-interface-vka) + - [Find the CSpace root cap](../DynamicLibraries/initialisation#find-the-cspace-root-cap) + - [Find the VSpace root cap](../DynamicLibraries/initialisation#find-the-vspace-root-cap) + - [Allocate a TCB Object](../DynamicLibraries/initialisation#allocate-a-tcb-object) + - [Configure the new TCB](../DynamicLibraries/initialisation#configure-the-new-tcb) + - [Name the new TCB](../DynamicLibraries/initialisation#name-the-new-tcb) + - [Set the instruction pointer](../DynamicLibraries/initialisation#set-the-instruction-pointer) + - [Write the registers](../DynamicLibraries/initialisation#write-the-registers) + - [Start the new thread](../DynamicLibraries/initialisation#start-the-new-thread) + +### [IPC](../DynamicLibraries/ipc) + - [Allocate an IPC buffer](../DynamicLibraries/ipc#allocate-an-ipc-buffer) + - [Allocate a page table](../DynamicLibraries/ipc#allocate-a-page-table) + - [Map a page table](../DynamicLibraries/ipc#map-a-page-table) + - [Map a page](../DynamicLibraries/ipc#map-a-page) + - [Allocate an endpoint](../DynamicLibraries/ipc#allocate-an-endpoint) + - [Badge an endpoint](../DynamicLibraries/ipc#badge-an-endpoint) + - [Set a message register](../DynamicLibraries/ipc#message-registers) + - [Send and wait for a reply](../DynamicLibraries/ipc#ipc) + - [Receive a reply](../DynamicLibraries/ipc#receive-a-reply) + - [Receive an IPC](../DynamicLibraries/ipc#receive-an-ipc) + - [Validate a message](../DynamicLibraries/ipc#validate-the-message) + - [Write the message registers](../DynamicLibraries/ipc#write-the-message-registers) + - [Reply to a message](../DynamicLibraries/ipc#reply-to-a-message) + +### [Processes & Elf loading](../DynamicLibraries/processes) + - [Create a VSpace object](../DynamicLibraries/processes#virtual-memory-management) + - [Configure a process](../DynamicLibraries/processes#configure-a-process) + - [Get a cspacepath](../DynamicLibraries/processes#get-a-cspacepath) + - [Badge a capability](../DynamicLibraries/processes#badge-a-capability) + - [Spawn a process](../DynamicLibraries/processes#spawn-a-process) + - [Receive a message](../DynamicLibraries/processes#receive-a-message) + - [Send a reply](../DynamicLibraries/processes#send-a-reply) + - [Initiate communications by using seL4_Call](../DynamicLibraries/processes#client-call) + +### [Timer](../DynamicLibraries/timer) + - [Allocate a notification object](../DynamicLibraries/timer#allocate-a-notification-object) + - [Initialise a timer](../DynamicLibraries/timer#initialise-the-timer) + - [Use a timer](../DynamicLibraries/timer#use-the-timer) + - [Handle an interrupt](../DynamicLibraries/timer#handle-the-interrupt) + - [Destroy a timer](../DynamicLibraries/timer#destroy-the-timer) + +## [CAmkES](../CAmkES/) + +### [A basic CAmkES application](../CAmkES/camkes1) + - [Define instance in the composition section of the ADL](../CAmkES/camkes1#define-instance-in-the-composition-section-of-the-adl) + - [Add a connection](../CAmkES/camkes1#add-a-connection) + - [Define an interface](../CAmkES/camkes1#define-an-interface) + - [Implement a RPC function](../CAmkES/camkes1#implement-a-rpc-function) + - [Invoke a RPC function](../CAmkES/camkes1#invoke-a-rpc-function) + +### [Events in CAmkES](../CAmkES/camkes2) + - [Specify an events interface](../CAmkES/camkes2#specify-an-events-interface) + - [Wait for data to become available](../CAmkES/camkes2#wait-for-data-to-become-available) + - [Signal that data is available](../CAmkES/camkes2#signal-that-data-is-available) + - [Register a callback handler](../CAmkES/camkes2#register-a-callback-handler) + - [Specify dataport interfaces](../CAmkES/camkes2#specify-an-events-interface) + - [Specify dataport connections](../CAmkES/camkes2#specify-dataport-connections) + - [Copy strings to an untyped dataport](../CAmkES/camkes2#copy-strings-to-an-untyped-dataport) + - [Read the reply data from a typed dataport](../CAmkES/camkes2#read-the-reply-data-from-a-typed-dataport) + - [Send data using dataports](../CAmkES/camkes2#send-data-using-dataports) + - [Read data from an untyped dataport](../CAmkES/camkes2#read-data-from-an-untyped-dataport) + - [Put data into a typed dataport](../CAmkES/camkes2#put-data-into-a-typed-dataport) + - [Read data from a typed dataport](../CAmkES/camkes2#read-data-from-a-typed-dataport) + - [Set component priorities](../CAmkES/camkes2#set-component-priorities) + - [Restrict access to dataports](../CAmkES/camkes2#restrict-access-to-dataports) + - [Test the read and write permissions on the dataport](../CAmkES/camkes2#test-the-read-and-write-permissions-on-the-dataport) + +### [CAmkES Timer](../CAmkES/camkes) + - [Instantiate a Timer and Timerbase](../CAmkES/camkes3#task-1) + - [Connect a timer driver component](../CAmkES/camkes3#task-2) + - [Configure a timer hardware component instance](../CAmkES/camkes3#task-3) + - [Call into a supplied driver to handle the interrupt](../CAmkES/camkes3#task-4) + - [Stop a timer](../CAmkES/camkes3#task-5) + - [Acknowledge an interrupt](../CAmkES/camkes3#task-6) + - [Get a timer handler](../CAmkES/camkes3#task-7) + - [Start a timer](../CAmkES/camkes3#task-8) + - [Implement a RPC interface](../CAmkES/camkes3#task-9) + - [Set a timer interrupt](../CAmkES/camkes3#task-10) + - [Instantiate a TimerDTB component](../CAmkES/camkes3#task-1-1) + - [Connect interfaces using the seL4DTBHardware connector](../CAmkES/camkes3#task-2-1) + - [Configure the TimerDTB component](../CAmkES/camkes3#task-3-1) diff --git a/Tutorials/index.md b/Tutorials/index.md index c64a317ef7..b4acbc43e3 100644 --- a/Tutorials/index.md +++ b/Tutorials/index.md @@ -1,7 +1,31 @@ - -The redirect will only work once deployed. For testing click [here](/Tutorials/GettingStarted/overview.md) \ No newline at end of file +--- +toc: true +layout: project +SPDX-License-Identifier: CC-BY-SA-4.0 +SPDX-FileCopyrightText: 2024 seL4 Project a Series of LF Projects, LLC. +--- +# Tutorials about seL4 + +We have developed a series of tutorials to introduce seL4 and +developing systems on seL4. + +The tutorials are split into a number of broad categories: + +- [About seL4](about-seL4) and [Getting started with the Microkit tutorial](microkit) introduce seL4 concepts. +- The [seL4 Kernel tutorials](../seL4Kernel/overview.md) are a deep dive into seL4 concepts. +- [MCS](../MCS/mcs-extensions) introduces seL4 MCS extensions. +- [Dynamic Libraries](../DynamicLibraries/initialisation.md) covers the libraries that have been developed for rapidly prototyping systems on seL4. +- [CAmkES](../CAmkES/hello-camkes.md) is a platform for building componentised systems for embedded platforms. +- [Microkit](https://trustworthy.systems/projects/microkit/tutorial/)is an operating system framework on top of seL4 provides a small set of simple abstractions that ease the design and implementation of statically structured systems on seL4. (Links to the same tutorial as in the [Getting Started](../GettingStarted/microkit) section.) +- [Rust](https://github.com/seL4/rust-sel4) provide crates for supporting the use of Rust in seL4 userspace. + +

Resources

+Additional resources to assist with learning: +- The [seL4 manual](https://sel4.systems/Info/Docs/seL4-manual-latest.pdf) +- [API references](../../projects/sel4/api-doc) +- The [How to](../Resources/how-to) page provides links to tutorial solutions as quick references for seL4 calls and methods. +- [FAQs](../../projects/sel4/frequently-asked-questions) +- [Debugging guide](../../projects/sel4-tutorials/debugging-guide) +- [Discourse forum](https://sel4.discourse.group/) +- [Developer mailing list](https://lists.sel4.systems/postorius/lists/devel.sel4.systems/) +- [Mattermost channel](https://mattermost.trustworthy.systems/sel4-external/channels/web-doc-revamp) diff --git a/_includes/nav-sidebar.html b/_includes/nav-sidebar.html index df9b2fa5cf..f3942a2f87 100644 --- a/_includes/nav-sidebar.html +++ b/_includes/nav-sidebar.html @@ -55,55 +55,63 @@ {% endif %} {% if page_url[1] == "Tutorials" %} + {% if page_url[2] contains "" %} + {% assign url = "../" %} + {% endif %}