Allow specifying notify or ppcalls on a per-channel, not per-protection domain basis #217
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
midnightveil
force-pushed
the
channel-extensions
branch
2 times, most recently
from
8a5a239 to
6e639d1
Compare
|
The first two commits look good, I'll review the main commit once the PR is ready for review. |
midnightveil
force-pushed
the
channel-extensions
branch
2 times, most recently
from
cc4c48c to
af11b68
Compare
midnightveil
commented
Sep 4, 2024
midnightveil
force-pushed
the
channel-extensions
branch
from
b50dd28 to
0f55270
Compare
midnightveil
force-pushed
the
channel-extensions
branch
5 times, most recently
from
c4d897e to
73e8f47
Compare
Ivan-Velickovic
force-pushed
the
channel-extensions
branch
5 times, most recently
from
6952a46 to
73e8f47
Compare
Turns a runtime invariant into a compile-time invariant. Signed-off-by: julia <[email protected]>
Previously this resulted in a panic with Option::unwrap() on a None Signed-off-by: julia <[email protected]>
midnightveil
force-pushed
the
channel-extensions
branch
from
73e8f47 to
7ba61c6
Compare
Ivan-Velickovic
force-pushed
the
channel-extensions
branch
from
7ba61c6 to
bac4efb
Compare
Previously, this was done on a per-protection domain basis, which meant that protection domains were given more rights than was strictly necessary. This also allows for authors to remove rights for sending notifications on either end of the channel, and so allows for having unidirectional notification channels. This removes the previous `pp="true"` attribute on PDs (the one you would PPC *into*), replacing it with `pp="true/false" and `notify="true/false"` on each channel end. So the following: ``` <protection_domain name="sender" [...] /> <protection_domain name="receiver" pp="true" [...] /> <channel> <end id="0" pd="sender" /> <end id="0" pd="receiver" /> </channel> ``` Becomes instead: ``` <protection_domain name="sender" [...] /> <protection_domain name="receiver" [...] /> <channel> <end id="0" pd="sender" pp="true" /> <end id="0" pd="receiver" /> </channel> ``` Signed-off-by: julia <[email protected]>
As per the Microkit manual, > A protected call is only possible if the callee has strictly higher > priority than the caller. Due to the change to specify `pp="true"` in the SDF in the previous commit, we can now verify that the priority invariant holds true, instead of it being possible to create a system with this behaviour. Signed-off-by: julia <[email protected]> Signed-off-by: Ivan-Velickovic <[email protected]>
Ivan-Velickovic
force-pushed
the
channel-extensions
branch
from
bac4efb to
1459dbc
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Also fixes #168, as this allows us enough precision to check priorities.
Can specify
pp="true"ornotify="false"(or vice-versa, for the defaults):ToDo: