diff --git a/docs/runtime/03_consensus_2.md b/docs/runtime/03_consensus_2.md index 33509ae5adb683b2d35dbaa38bb7aa112757a59b..372b75601bf60763288636c557cdef7057558a59 100644 --- a/docs/runtime/03_consensus_2.md +++ b/docs/runtime/03_consensus_2.md @@ -136,7 +136,7 @@ And so the rule for joining a synchronous region was changed. Now it is simply: The example above hints at a second problem (figured out a long time ago by our unix overlords): there is no way within PDL code to say that we can perform a variety of behaviours triggered by the arrival of messages. For our `database` component above, we see that it can have multiple requesters connected to it, but there is no way to indicate that we can have valid behaviour for any one of them. So we introduce the `select` statement. It is a statement with a set of arms. Each arm has a guard, where we indicate which ports need to have incoming messages, and a block of code, that is executed when all of the indicated ports actually have received a message. -The select statement may only appear within async block. The arm's guard is formulated in terms of an expression or a variable declaration (that may contain `get` calls, but not `put` calls). The corresponding block of code is executed when all of the `get` calls in the guard have a message ready for them. In case multiple arm guards are satisfied then a random arms is chosen by the runtime for execution. +The select statement may only appear within a sync block. The arm's guard is formulated in terms of an expression or a variable declaration (that may contain `get` calls, but not `put` calls). The corresponding block of code is executed when all of the `get` calls in the guard have a message ready for them. In case multiple arm guards are satisfied then a random arms is chosen by the runtime for execution. So the select statement takes the form: @@ -164,6 +164,7 @@ while (still_waiting_for_a_message) { break; } + block_until_there_is_a_new_message(); } ``` @@ -177,4 +178,4 @@ Because the current consensus algorithm is a scaled down version of the previous Once a component has reached the end of the sync block it will submit its local solution (i.e. the port mapping) for validation by the consensus algorithm. If all components in the synchronous region have submitted a local solution, whose port mappings are pairwise consistent with one another, then we've found a global solution. With this global solution the components in the synchronous region are ordered to continue the execution of their PDL code. -As a small side-note: with speculative execution the consensus algorithm amounted to finding, for each component, a complete trace whose interactions are consistent with all of its peers. Without speculative execution we have the multi-party equivalent to an `Ack` message in the TCP protocol. (Yes, a lot of details of the TCP protocol are left out, but) in TCP both parties perform a best-effort attempt to ensure that a sent message has arrived at the receiver by the receiver `Ack`nowledging that the message has been received. In this cases the consensus algorithm performs this function: it ensures that the sent messages have all arrived at their peer. \ No newline at end of file +As a small side-note: with speculative execution the consensus algorithm amounted to finding, for each component, a complete trace whose interactions are consistent with all of its peers. Without speculative execution we have the multi-party equivalent to an `Ack` message in the TCP protocol. (Yes, this statement skips over a *lot* of details of the TCP protocol, but) in TCP both parties perform a best-effort attempt to ensure that a sent message has arrived at the receiver by the receiver `Ack`nowledging that the message has been received. In this cases the consensus algorithm performs this function: it ensures that the sent messages have all arrived at their peers in a single multi-party interaction. \ No newline at end of file