Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions sel4-core.md
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ to build *any* seL4-based system. These include systems built on the
seL4 Core Platform, but also other classes of systems, such as dynamic
systems, minimal systems based on directly supporting run-times for
languages like Rust or Erlang. As such it should not impose policy
that restricts the design space enabled by se4.
that restricts the design space enabled by seL4.

This policy freedom applies to both run-time and build-time.

Expand All @@ -47,7 +47,7 @@ kernel

#. All the supported boards must support all configurations.

#. The release must include a way test test the functionality and performance of the components.
#. The release must include a way to test the functionality and performance of the components.

#. All the individual tests and benchmarks must be clearly documented as to their purpose.

Expand Down
6 changes: 3 additions & 3 deletions sel4-platform.md
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ best system for a particular use case, requiring extensive seL4 experience
from developers.

The seL4 Core Platform addresses this challenge by constraining the
system architecture and to one that provides enough features and power
system architecture to one that provides enough features and power
for this usage class, enabling a much simpler set of developer-visible
abstractions.

Expand Down Expand Up @@ -304,7 +304,7 @@ semaphore).
Memory regions may be attached to a communication channel.
It is possible for multiple memory regions to be attached to a communication channel.

Attached memory regions provided a way for the PD utilizing the communication channel to refer to a specific memory location.
Attached memory regions provide a way for the PD utilizing the communication channel to refer to a specific memory location.
A **memory reference** is an efficient encoding that identifies a specific offset within an attached memory region.

Normally an attached memory region will be mapped into both protection domains, however it is likely that the memory region will be mapped at different virtual address in each PD.
Expand Down Expand Up @@ -396,7 +396,7 @@ PPC arguments are passed by-value (i.e. copied) and are limited to 16 machine wo
> The PPC payload should be considered as analogous to function arguments in the C language; similar limitations exist in the C ABIs (Application Binary Interfaces) of various platforms.

The seL4 Core Platform provides the server with the (non-forgeable)
identify of the client PD. The server may use this to associate state with the client (e.g. for long-running operations) and enforce
identity of the client PD. The server may use this to associate state with the client (e.g. for long-running operations) and enforce
access control.

**Note**
Expand Down