Add protocol subtyping for read-only operations

[cacay]

Consider the following program:

val limit: int@Replication(hosts = {alice, bob}) = 10;
for (var i: int = 0; i < limit; i += 1) {
    output i to alice;
}

This program gets compiled as follows:

val limit: int@Replication(hosts = {alice, bob}) = 10;
var i: int@Local(host = alice) = 0;
loop {
    let $tmp@Local(host = alice) = i;
    let $tmp_1@Replication(hosts = {alice, bob}) = limit;
    let $tmp_2@Replication(hosts = {alice, bob}) = ($tmp < $tmp_1);
    if ($tmp_2) {
        let $tmp_3@Local(host = alice) = i;
        output $tmp_3 to alice;
        i += 1;
    } else {
        break;
    }
}

Note that $tmp_1 is placed at Replication(alice, bob) since limit is placed there. Viaduct currently requires all method calls (queries and updates) to an object to happen on the protocol that stores that object. This has an unfortunate side effect: it looks like both alice and bob must be involved in the loop. This is a performance problem since bob uselessly has to follow the control flow. Worse, if the guard is invisible to bob (e.g., imagine i is labelled as {A}), then this program will fail to compile.

Our current solution to this problem is the notion of "mandatory participating hosts" which I do not understand. It looks pretty hacky, and the logic is spread across the entire protocol selection pipeline which makes the concept pretty mysterious.

I'd like to propose a more uniform solution: use-site subtyping for protocols. Protocols are allowed to declare sub-protocols that they can act like. We then allow executing read-only operations only (e.g., queries) at a subprotocol. For example, Replication(alice, bob, chuck) would declare

Local(alice), Local(bob),  Local(chuck), Replication(alice, bob), Replication(bob, chuck), Replication(alice, chuck)

and Commitment(sender=alice, receivers=H) would declare

Local(alice)

as subprotocols. The above program can now read limit at Local(alice) and it's clear from the compiled program (and not just some weird internal state the compiler maintains) that bob is not involved in the loop.

[rolph-recto]

The implementation definitely needs refactoring, but at bottom the "mandatory participating hosts" thing is quite similar to what you're proposing:

1. For a given simple statement and protocol, the protocol composer returns the set of hosts that must participate in the statement's execution. Basically every host in the protocol must participate except for reads at Replication, Commitment, ZKP.
2. To determine if a host that optionally participates in the execution of a statement actually participates, ProtocolAnalysis computes a use analysis to see if the host will ever need the value in the future. In your example, if you are updating a replicated variable instead of a local variable inside of the loop, then Bob needs to enter the loop, and ProtocolAnalysis determines that Bob does need to participate in executing tmp_1.

You are essentially proposing to replace 1. But all the complexity is really in 2. In your example, how would you calculate the protocol of tmp_1 above to be Local(alice)?

I do like the idea that queries don't have to have the same protocol as the object being queried; as you said, how the read of tmp_1 is made more clear in the compiled program. However, it might make the runtime system more complicated. Right now there is a clear connection between the protocol of a temporary and what backend will execute it. But in your proposal, a read of a committed value at the commitment creator can be in the Local protocol; how will the code generator or interpreter know that the query actually has to be done at the Commitment backend?

[cacay]

Doesn't the backend have to do something special with the current setup anyway? Or be written in a way that makes this all magically work? E.g., tmp_1 is stored on Replication(alice, bob), but the assignment is only executed on alice. So the backend better not expect an equivocation check message from bob. The current implementation doesn't, but the programmer of the backend had to keep mandatoryParticipatingHosts in mind. I don't think the proposal adds any complication that wasn't already there. It just makes it more explicit, which I would argue is a good thing.

[rolph-recto]

The backend interpreter keeps track of the set of participating hosts for each statement and will only call out a protocol backend for a host if the host is participating.

Within the protocol backends themselves, this is not a problem since everything is done through communication events. So for example if there is a read at a variable in Replication(alice,bob) but only Alice is participating then there will be no communication event involving Bob.

Again, I'm not opposed to the idea, but there are some questions that need to be answered:

• How do you know which "subprotocol" gets used for a query?
• When you interpret / generate code for a query, how do we calculate which protocol backend contains the variable being queried?