Tutorial: part4 ppcall from VMM to less prioritized Wordle_server

[Vincer239]

Hi, thank you for the nice work :) I just did the tutorial and wondered during part4. I have copy/pasted your wordle.system code into my config and found out that the PPC from VVM toWordle_Server still worked even though it violated the priority callee-caller setup. VMM ist at prio 101 and Wordle_server at 25 and it works like a charm.

A protected procedure call is only possible if the callee has strictly higher priority than the caller. This means that if A has a priority of 1 and B has a priority of 254, A can invoke B's protected procedure, but B cannot invoke A's protected procedure. (Tutorial description and documentation)

<!-- Create a VMM protection domain -->
    <protection_domain name="vmm" priority="101">
        <program_image path="vmm.elf" />
        <!-- [unchanged from tutorial code] -->
        <!-- possibly mistake in the template: id in VM missing; vcpu id unnecessary -->
        <virtual_machine name="linux" id="0" priority="100">
            <!-- [unchanged from tutorial code] -->
        </virtual_machine>
        <!-- [unchanged from tutorial code] -->
    </protection_domain>

    <protection_domain name="wordle_server" pp="true" priority="25">
        <program_image path="wordle_server.elf" />
    </protection_domain>

    <!-- vmm -> wordle server -->
    <channel>
        <!-- The VMM code expects the channel ID to be 1. -->
        <end pd="vmm" id="1" />
        <end pd="wordle_server" id="2" />
    </channel>

[Ivan-Velickovic]

Thanks for posting the issue.

Yes, you're right. While it does violate the rules of Microkit, there is no actual check right now stopping users from doing a PPC to a lower priority PD. We should obviously fix this.

[Ivan-Velickovic]

possibly mistake in the template: id in VM missing; vcpu id unnecessary

The current template is correct for Microkit 1.3.0. The Microkit tutorial was recently changed to use 1.3.0.

The tutorial used to provide a 'development' version of Microkit with some missing features such as virtualisation support, this is no longer the case and a mainline release of Microkit is used.

It should be easy to switch over to 1.3.0, you can find the release here: https://github.com/seL4/microkit/releases/tag/1.3.0.

[wucke13]

While it does violate the rules of Microkit, there is no actual check right now stopping users from doing a PPC to a lower priority PD. We should obviously fix this.

I quickly glanced at implementing this in the microkit tool in the parse() function. However, since both notification and pp rely on channel, flagging this while parsing the configuration would forbid all configurations in which two pd that both offer a pp to directly interact in any way or form (while sending notifications between two pd that are pp == true should be fine). Was it considered to use two distinct kinds of channels for notification/pp (at least during configuration), to allow this static config analysis without impeding valid uses?

The actual implementation can of course stay like it is (both using seL4 signals internally).

[gernotheiser]

That's an interesting idea worth considering, but then it's a relatively simple post-processing step. Note that our verified CapDL export does this as a side-effect, so it might be best to put this into production use.

[Ivan-Velickovic]

I think to fix this we will most likely have to introduce a breaking change to the SDF by removing the pp attribute on protection domains and make channels themselves declare whether they are for notifications, PPC, or both.

This would also enable single-directional channels, right now all of them are bi-directional.

[gernotheiser]

I can see that this is needed and useful. As long as it doesn't stop us having bi-directional channels with uni-directional PPC