Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Minor fixes to manual #83

Merged
merged 2 commits into from
Nov 20, 2023
Merged
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
6 changes: 3 additions & 3 deletions docs/manual.md
Original file line number Diff line number Diff line change
Expand Up @@ -121,7 +121,7 @@ The isolation provided by the virtual address space is enforced by the underlyin
The virtual address space for a PD has mappings for the PD's *program image* along with any memory regions that the PD can access.
The program image is an ELF file containing the code and data which implements the isolated component.

The platform supports a maximum of 63 protection domains.
Microkit supports a maximum of 63 protection domains.

### Entry points

Expand Down Expand Up @@ -228,8 +228,8 @@ The control returns to the caller when the `protected` entry point returns.

The caller is blocked until the callee returns.
Protected procedures must execute in bounded time.
It is intended that future version of the platform will enforce this condition through static analysis.
In the present version the callee must trust the callee to conform.
It is intended that a future version of Microkit will enforce this condition through static analysis.
In the present version the caller must trust the callee to conform.

In general, PPs are provided by services for use by clients that trust the protection domain to provide that service.

Expand Down