<?xml version="1.0" encoding="UTF-8"?>
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom" xmlns:dc="http://purl.org/dc/elements/1.1/">
  <channel>
    <title>DEV Community: Sergey Fedorov</title>
    <description>The latest articles on DEV Community by Sergey Fedorov (@sergefdrv).</description>
    <link>https://dev.to/sergefdrv</link>
    <image>
      <url>https://media2.dev.to/dynamic/image/width=90,height=90,fit=cover,gravity=auto,format=auto/https:%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Fuser%2Fprofile_image%2F1116763%2F4c5f574e-de9b-4b68-b9ce-ccef6e253bee.jpg</url>
      <title>DEV Community: Sergey Fedorov</title>
      <link>https://dev.to/sergefdrv</link>
    </image>
    <atom:link rel="self" type="application/rss+xml" href="https://dev.to/feed/sergefdrv"/>
    <language>en</language>
    <item>
      <title>A Sketch of Reversible Deterministic Concurrency for Distributed Protocols</title>
      <dc:creator>Sergey Fedorov</dc:creator>
      <pubDate>Fri, 30 May 2025 17:51:15 +0000</pubDate>
      <link>https://dev.to/replica-io/a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols-6k8</link>
      <guid>https://dev.to/replica-io/a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols-6k8</guid>
      <description>&lt;p&gt;This post presents preliminary results of elaborating the idea that was &lt;a href="https://github.com/orgs/replica-io/discussions/49#discussioncomment-12436415" rel="noopener noreferrer"&gt;introduced on project's GitHub&lt;/a&gt; and which can be referred to as &lt;em&gt;reversible deterministic concurrency&lt;/em&gt;. We try to make those ideas a little more concrete and apply them to modelling some well-known distributed protocols.&lt;/p&gt;

&lt;p&gt;The original post can be found &lt;a href="https://replica-io.dev/blog/2025/05/30/a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols" rel="noopener noreferrer"&gt;here&lt;/a&gt;.&lt;/p&gt;

&lt;p&gt;Designing, verifying, correctly implementing and later improving core mechanisms of complex distributed, decentralized systems, such as Byzantine fault tolerant consensus, is notoriously difficult and error-prone. One of the biggest challenges here is dealing with the inherently concurrent nature of distributed systems. So there is an underlying problem of structuring the inherently concurrent logic of distributed protocols that we don’t really know how to solve in a simple, flexible, and reliable way. Embarrassingly often, we approach this rather awkwardly and unsurprisingly end up with awfully complicated, obscure, and fragile code.&lt;/p&gt;

&lt;p&gt;&lt;a href="https://github.com/replica-io/replica-io/issues/47" rel="noopener noreferrer"&gt;Considering what modelling approach to initially adopt in the Replica_IO framework&lt;/a&gt;, an approach that would allow &lt;em&gt;both specifying and implementing&lt;/em&gt; complex distributed protocols in a &lt;em&gt;natural&lt;/em&gt; way, I decided to challenge the status quo and try to rethink the conventional approaches to modeling distributed systems and the ways of expressing distributed protocols. So came up the idea of reversible deterministic concurrency. The idea was inspired by a number of &lt;a href="https://github.com/replica-io/replica-io/issues/7" rel="noopener noreferrer"&gt;explored models of computation and programming models&lt;/a&gt;, as well as some principles from information theory, modern physics, reversible and quantum computing, such as conservation of information.&lt;/p&gt;

&lt;p&gt;The long-term goal is to develop this idea further into an approach for &lt;em&gt;specifying&lt;/em&gt; core mechanisms of concurrent, distributed systems, &lt;em&gt;implementing&lt;/em&gt; them in Rust code, as well as &lt;em&gt;verifying&lt;/em&gt; their correctness. The approach will be used as the foundation for the Replica_IO framework. Following this approach, it should be safe and easy to express concurrency and communication within the framework in a structured and composable way.&lt;/p&gt;

&lt;p&gt;In order to get some intuition about the idea, we'll begin by discussing some basic principles behind it. Then we'll try modelling some well-known distributed protocols following those principles, namely the Bracha's reliable broadcast and the Tendermint consensus protocols.&lt;/p&gt;

&lt;p&gt;Please bear in mind that this write-up is an early sketch and that many details of the approach presented here, including terminology, will likely undergo significant changes in the future.&lt;/p&gt;

&lt;h2&gt;
  
  
  Approach
&lt;/h2&gt;

&lt;p&gt;We conceptually think of concurrent systems as consisting of &lt;em&gt;deterministic&lt;/em&gt; components that can be connected with each other and interact &lt;em&gt;concurrently&lt;/em&gt;. The only means of interaction with the components are through their &lt;em&gt;inputs&lt;/em&gt; and &lt;em&gt;outputs&lt;/em&gt;. Each input and output can convey a certain type of data, and they are typed accordingly. Inputs and outputs matching in type can be connected &lt;em&gt;pairwise&lt;/em&gt;, so that data can flow through the connection. Connecting inputs and outputs of different components enables data flow between those components.&lt;/p&gt;

&lt;h3&gt;
  
  
  Base and composite components, extrinsic inputs and outputs
&lt;/h3&gt;

&lt;p&gt;Components can be &lt;em&gt;composite&lt;/em&gt;, i.e. consist of lower-level sub-components connected together. The remaining unconnected inputs and outputs become the inputs and outputs of the composite component. The process of decomposition bottoms out at &lt;em&gt;base components&lt;/em&gt; that are considered primitive and not decomposed further. Apart from base components, there can be &lt;em&gt;extrinsic inputs and outputs&lt;/em&gt; for exchanging information with the environment. The extrinsic inputs and outputs can represent interfaces for interacting with entities that are considered external to the modeled system, or they can be &lt;em&gt;sources&lt;/em&gt; of auxiliary data items and &lt;em&gt;sinks&lt;/em&gt; to dispose of excessive data.&lt;/p&gt;

&lt;h3&gt;
  
  
  Input-output pairs, interaction lines, and two kinds of interaction
&lt;/h3&gt;

&lt;p&gt;Inputs and outputs can only appear in complementary pairs. This applies to inputs and outputs of base components, and therefore of composite components, as well as to extrinsic inputs and outputs. Moreover, in a complete system, every input must be connected to exactly one output matching in type. So the input-output pairs connected one to another form a kind of chains or &lt;em&gt;interaction lines&lt;/em&gt;. Data items flowing along different interaction lines can interact with each other by redistributing the information contained within those data items when they arrive at the same base component. So there are &lt;em&gt;two kinds of interaction&lt;/em&gt; within the system: passing data items from one component to another along interaction lines and exchange of information between data items on different interaction lines within base components.&lt;/p&gt;

&lt;h3&gt;
  
  
  Determinism and reversibility
&lt;/h3&gt;

&lt;p&gt;All components are conceptually &lt;em&gt;deterministic&lt;/em&gt;: provided all the component's assumptions hold true, the output values must be completely determined by the input values and nothing else. Although the availability of output values can depend both on the availability of the input values and on the input values themselves, neither the output values nor their availability may per se depend on the relative order in which the input values become available. (It is worth noting here that this determinism is only conceptual: later we'll see how some input values may be left unspecified and, in normal operation, get chosen on spot, possibly depending on the availability and values of other inputs.) Moreover, the components must also be &lt;em&gt;reversible&lt;/em&gt;, so that the original input values can always be recovered from the resulting output values.&lt;/p&gt;

&lt;p&gt;One can view the determinism and reversibility requirements as a consequence of making all information flow within the system explicit. If all information that is used to determine the output values is contained in the input values then the inputs uniquely determine the outputs and the computation is deterministic. Similarly, if the output values collectively contain all the information that was contained in the original input values then the inputs can be recovered from the outputs and the computation is reversible. Determinism and reversibility are dual to each other: if a computation carried out in one direction is reversible then the same computation carried out in the opposite direction is deterministic.&lt;/p&gt;

&lt;p&gt;Requiring that components are conceptually deterministic we make non-determinism explicit, structurally evident rather than emergent or accidental, while treating concurrency implicitly as emerging naturally from data availability and the system’s structure rather than from control flow. This should improve modularity and facilitate &lt;em&gt;compositional reasoning&lt;/em&gt;. Together with the reversibility requirement this ensures that there is no hidden data flow, enables backward reasoning, backtracking mechanisms, &lt;em&gt;reverse debugging&lt;/em&gt; and would facilitate &lt;em&gt;management of resources&lt;/em&gt;, such as memory.&lt;/p&gt;

&lt;h3&gt;
  
  
  Simple components
&lt;/h3&gt;

&lt;h4&gt;
  
  
  Sum
&lt;/h4&gt;

&lt;p&gt;We can represent components graphically. For example, the following figure depicts a component that simply adds one integer value to another:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fxd0l5hgn0yw885gqtibt.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fxd0l5hgn0yw885gqtibt.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;The component is represented by a rectangle divided into horizontal sections, one section for each input-output pair, i.e. interaction line. The component is labeled above by its name, &lt;code&gt;Sum&lt;/code&gt;; its interaction lines are labeled as &lt;code&gt;x: Int&lt;/code&gt; and &lt;code&gt;y: Int&lt;/code&gt; , where &lt;code&gt;x&lt;/code&gt; and &lt;code&gt;y&lt;/code&gt; denote the names of the interaction lines and &lt;code&gt;Int&lt;/code&gt; is the type of data items conveyed by them. The inputs are on the left side of the component whereas the outputs are on the right side. The component takes two integers as input values, denoted as &lt;code&gt;a&lt;/code&gt; and &lt;code&gt;b&lt;/code&gt;, along lines &lt;code&gt;x&lt;/code&gt; and &lt;code&gt;y&lt;/code&gt; and returns two integers as output values; the first input value goes through unchanged, whereas the second one becomes the sum of the two input values. The first input is required to determine both outputs, and the second input is required to determine the second output. Since this component has just two interaction lines, one of which leaves the value unchanged, we can alternatively depict it as follows:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2F8v91wzj6g77o62ppjgut.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2F8v91wzj6g77o62ppjgut.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;It is easy to see that this component is deterministic, i.e. the output values are completely determined by the input values, no matter in which order the inputs become available. It is also not hard to see that this component is reversible, i.e. the original input values can always be recovered from the resulting output values. We can depict the inverse of the component as follows:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fq8nd6igzvhaymion6n2x.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fq8nd6igzvhaymion6n2x.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;h4&gt;
  
  
  Generalized controlled swap
&lt;/h4&gt;

&lt;p&gt;Let's consider another example. The following component represents a kind of generalized controlled swap operation&lt;sup id="fnref1"&gt;1&lt;/sup&gt;:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fhz459vjx4dnmnxi9jb4u.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fhz459vjx4dnmnxi9jb4u.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;or depicted alternatively:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fjtz7nmhvegq5s3jsce1q.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fjtz7nmhvegq5s3jsce1q.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;It has three interaction lines: one control line, &lt;code&gt;c&lt;/code&gt;, and two target lines, &lt;code&gt;t1&lt;/code&gt; and &lt;code&gt;t2&lt;/code&gt;. The value of the control line goes through unchanged, but it determines the output values of the target lines: If the control value is true then the values of the target lines get swapped, otherwise they simply go through unchanged. The controlled swap component is an inverse of itself.&lt;/p&gt;

&lt;h3&gt;
  
  
  Concurrency of interaction lines
&lt;/h3&gt;

&lt;p&gt;Interaction lines are highly &lt;em&gt;concurrent&lt;/em&gt;: an output value becomes available as soon as it can be obtained from the input values that are available for the interaction. For example, in the &lt;code&gt;CSwap&lt;/code&gt; component, once the value on the control line is available, each of the target outputs remains dependent only on one of the target inputs and becomes available as soon as that input value is available, concurrently and independently of each other.&lt;/p&gt;

&lt;h3&gt;
  
  
  Demand-driven nature of interactions
&lt;/h3&gt;

&lt;p&gt;Interactions are &lt;em&gt;demand-driven&lt;/em&gt;: certain extrinsic inputs and some inputs of base components may demand a value from the connected output, and this demand propagates further along the inputs required to determine the demanded output value until it eventually reaches available values and triggers the interactions required to satisfy the demand. Sinks are never demanding, but they will consume the value when it becomes available.&lt;/p&gt;

&lt;h3&gt;
  
  
  Unspecified values
&lt;/h3&gt;

&lt;p&gt;Certain inputs of base components may be connected to special sources of &lt;em&gt;unspecified&lt;/em&gt; values. Those unspecified values are not real; they are just placeholders that stand for concrete values. During normal operation, the component will choose appropriate concrete values for such unspecified values and act as if they were guessed correctly and provided by the environment. When debugging the system or during verification, the sources of unspecified values can be forced to provide specific values; in that case, the component has no choice but to take the forced value as is. One can think of an unspecified value as a "superposition" of all possible values of the corresponding type that will "collapse" to a concrete value when going through the base component.&lt;/p&gt;

&lt;h4&gt;
  
  
  The &lt;code&gt;Def&lt;/code&gt; component
&lt;/h4&gt;

&lt;p&gt;The following component is meant to be used with such sources of unspecified values:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fq4e7pqpr1q9t30fxr3k3.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fq4e7pqpr1q9t30fxr3k3.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;Both interaction lines of this component conceptually go through unchanged; however, if the value of the second input is unspecified, as denoted in the picture by the special source labeled with &lt;code&gt;?&lt;/code&gt;, then the component chooses it to be equal to the value of the first input. This is effectively a way to copy the value of the first input in normal operation, but the second line can be forced to an arbitrary value, e.g. to model a Byzantine failure during verification. To avoid cluttering, we will often abbreviate the &lt;code&gt;Def&lt;/code&gt; component in diagrams as follows:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fog3eokuder89vcrze1lc.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fog3eokuder89vcrze1lc.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;h4&gt;
  
  
  &lt;code&gt;CSwap&lt;/code&gt; with unspecified control
&lt;/h4&gt;

&lt;p&gt;The control line of the controlled swap component can also be left unspecified, e.g. as follows:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2F7o6ur711qczuw10t85ie.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2F7o6ur711qczuw10t85ie.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;or in an abbreviated form:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fc4xmzxy6m3jc3t7gp0kk.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fc4xmzxy6m3jc3t7gp0kk.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;In the diagram above, the control line is connected to a source of unspecified values, and the second target output is connected to a sink (which is never demanding). When there is a demand for the first target output value, &lt;code&gt;w&lt;/code&gt;, both of the target inputs will be demanded, and the demand for &lt;code&gt;w&lt;/code&gt; will be satisfied by taking either &lt;code&gt;u&lt;/code&gt; or &lt;code&gt;v&lt;/code&gt;, whichever becomes available earlier, and the value of the control line will be chosen accordingly. If both target inputs are available when the target output is demanded then the value of the control line is chosen to be false, i.e. the component is biased towards passing the values of target lines through without swapping them.&lt;/p&gt;

&lt;h3&gt;
  
  
  Synchronization
&lt;/h3&gt;

&lt;p&gt;In some cases, we need to make sure that a certain value only becomes available if some other value also becomes available, without changing the values themselves. This can be achieved with the following synchronization primitive:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fcezokiyvfexcf1uu9un2.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fcezokiyvfexcf1uu9un2.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;Values &lt;code&gt;u&lt;/code&gt; and &lt;code&gt;v&lt;/code&gt; go through the bar unchanged, but only once they both become available. Thus values &lt;code&gt;u&lt;/code&gt; and &lt;code&gt;v&lt;/code&gt; on the right side mean something more than those on the left side: a value becoming available on any line on the right side implies the existence and availability of some value on the other line as well.&lt;/p&gt;

&lt;h3&gt;
  
  
  Signals
&lt;/h3&gt;

&lt;p&gt;For similar reasons, it may also be useful to have a kind of &lt;em&gt;signalling&lt;/em&gt; interaction lines of unit type, which convey data items that can take only a single possible value. Such signal values themselves have no meaning other than their existence, i.e. availability. Signalling lines work naturally with synchronization bars:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Frfgv2xobxfrmjcko1kfh.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Frfgv2xobxfrmjcko1kfh.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;or in an abbreviated form:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2F7ooid6jmipp3ljadnzza.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2F7ooid6jmipp3ljadnzza.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;In the diagram above, values &lt;code&gt;u&lt;/code&gt; and &lt;code&gt;v&lt;/code&gt; go through unchanged, but &lt;code&gt;v&lt;/code&gt; becomes available on the right side only when &lt;code&gt;u&lt;/code&gt; becomes available. However, because there are separate synchronization bars and an additional signal line, the availability of &lt;code&gt;v&lt;/code&gt; has no effect on the availability of &lt;code&gt;u&lt;/code&gt;.&lt;/p&gt;

&lt;h3&gt;
  
  
  Delays and timers
&lt;/h3&gt;

&lt;p&gt;In order to represent time-dependent behavior of the system, we introduce the &lt;em&gt;delay&lt;/em&gt; component:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Frugfukjykexpg7nqtgm1.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Frugfukjykexpg7nqtgm1.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;or alternatively:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fyqj29zfmpfu3gczzr8uy.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fyqj29zfmpfu3gczzr8uy.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;Values &lt;code&gt;d&lt;/code&gt; and &lt;code&gt;v&lt;/code&gt; go through the delay component unchanged, but, in normal operation, value &lt;code&gt;v&lt;/code&gt; becomes available on the second output with a delay of at least time duration &lt;code&gt;d&lt;/code&gt;.&lt;/p&gt;

&lt;p&gt;Using the delay component, we can construct a timer component that passes an arbitrary value through the &lt;code&gt;trigger&lt;/code&gt; line, and then, after a given amount of time provided on the &lt;code&gt;duration&lt;/code&gt; line, lets a unit value to pass through the &lt;code&gt;signal&lt;/code&gt; line (which would normally be connected to a source of an immediately available unit value):&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fsu7a8v2jivgcumah8bhc.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fsu7a8v2jivgcumah8bhc.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;h3&gt;
  
  
  One-shot and composite lines
&lt;/h3&gt;

&lt;p&gt;Individual inputs and outputs, and therefore interaction lines composed thereof, are conceptually &lt;em&gt;one-shot&lt;/em&gt;, i.e. they can convey only a single data item. However, we can bundle multiple inputs/outputs together and thus construct &lt;em&gt;composite inputs/outputs and interaction lines&lt;/em&gt;. There is &lt;em&gt;no synchronization&lt;/em&gt; imposed by composing interaction lines together, i.e. each individual line remains &lt;em&gt;concurrent in composition&lt;/em&gt;.&lt;/p&gt;

&lt;p&gt;We can compose two interaction lines together and decompose them back by constructing and deconstructing a pair, graphically represented as follows:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fp8k9cti96acchtlk49a1.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fp8k9cti96acchtlk49a1.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;We can also uniformly bundle an arbitrary number of lines together as follows:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2F1zs7jw487yiwy4e3vbv6.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2F1zs7jw487yiwy4e3vbv6.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;In the diagram above, the source labeled with the bang symbol &lt;code&gt;!&lt;/code&gt; denotes an empty source. (With just two lines being multiplexed uniformly, the notation above appears the same as the one for constructing a pure pair; in such cases, the ambiguity will be resolved by the context.)&lt;/p&gt;

&lt;p&gt;Using this notation, we can also bundle a virtually indefinite number of lines together:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fojp1hhj1to1qtfeykyfk.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fojp1hhj1to1qtfeykyfk.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;Note that the line composition primitives are not components: there is neither interaction nor synchronization between individual interaction lines caused by the composition; this is just notational convenience for dealing with multiple interaction lines.&lt;/p&gt;

&lt;h3&gt;
  
  
  Transposition
&lt;/h3&gt;

&lt;p&gt;It may be useful to rearrange the elements within a composition. We can transpose the last two levels of a composition as follows:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fwp579193zh37a63s1vxb.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fwp579193zh37a63s1vxb.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;The transposer connects line xi,j from composite line x&lt;sup&gt;mn&lt;/sup&gt; on the left to line yj,i of composite line y&lt;sup&gt;nm&lt;/sup&gt; on the right. For example, it will rearrange&lt;br&gt;
&lt;/p&gt;

&lt;div class="highlight js-code-highlight"&gt;
&lt;pre class="highlight plaintext"&gt;&lt;code&gt;[ [u, v, w], [x, y, z] ]
&lt;/code&gt;&lt;/pre&gt;

&lt;/div&gt;



&lt;p&gt;into&lt;br&gt;
&lt;/p&gt;

&lt;div class="highlight js-code-highlight"&gt;
&lt;pre class="highlight plaintext"&gt;&lt;code&gt;[ [u, x], [v, y], [w, z] ]
&lt;/code&gt;&lt;/pre&gt;

&lt;/div&gt;



&lt;h3&gt;
  
  
  The &lt;code&gt;Select&lt;/code&gt; component
&lt;/h3&gt;

&lt;p&gt;Using composite interaction lines we can define a component representing a choice from an arbitrary number of options:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2F75tln5hh1uzqrkmghozn.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2F75tln5hh1uzqrkmghozn.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;In the &lt;code&gt;Select&lt;/code&gt; component, the first input, &lt;code&gt;choice&lt;/code&gt;, determines the value of which element from the second, composite input, &lt;code&gt;options&lt;/code&gt;, should become available on the third output, &lt;code&gt;chosen&lt;/code&gt;. The &lt;code&gt;chosen&lt;/code&gt; input is supposed to be connected to a source of unspecified values. The &lt;code&gt;choice&lt;/code&gt; input can also be left unspecified; in that case, the component chooses it to select the element of &lt;code&gt;options&lt;/code&gt; that becomes available earlier.&lt;/p&gt;

&lt;h3&gt;
  
  
  Uncluttering diagrams
&lt;/h3&gt;

&lt;p&gt;To unclutter diagrams, we may depict several connections in one stroke and omit sources of unspecified values and sinks like this:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fafiw3ikxiro3bmsmd3l7.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fafiw3ikxiro3bmsmd3l7.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;h3&gt;
  
  
  Repetitive patterns
&lt;/h3&gt;

&lt;h4&gt;
  
  
  Replication box
&lt;/h4&gt;

&lt;p&gt;We would often need to connect one or many components in a repetitive pattern. To represent such patterns in a diagram, we can depict a single instance of the repeating part of the diagram enclosed in a &lt;em&gt;replication box&lt;/em&gt;:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fplqzq32ximvwnulvcoz9.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fplqzq32ximvwnulvcoz9.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;In the diagram above, component &lt;code&gt;G&lt;/code&gt; enclosed in a replication box is virtually repeated for each element of the composite lines entering and exiting the replication box.&lt;/p&gt;

&lt;h4&gt;
  
  
  Recursive loops
&lt;/h4&gt;

&lt;p&gt;We can use the replication box to represent recursive patterns of connections as follows:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2F9u7j15d288gtbf5ldnid.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2F9u7j15d288gtbf5ldnid.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;h3&gt;
  
  
  Domains and projections
&lt;/h3&gt;

&lt;p&gt;Each interaction line belongs to a certain &lt;em&gt;domain&lt;/em&gt;, which characterizes its location. For example, we can define a separate domain for each node of a distributed system. Interaction lines cannot cross domain boundaries, but &lt;em&gt;some components may span multiple domains&lt;/em&gt; and thus enable &lt;em&gt;cross-domain interaction&lt;/em&gt;.&lt;/p&gt;

&lt;p&gt;We can then derive a &lt;em&gt;projection&lt;/em&gt; of a system model onto a subset of its domains. Connections with base components that span the projection boundary will be represented as extrinsic inputs and outputs. So we can project a model of the whole distributed system separately onto each node and derive the local logic of individual nodes. The base components that represent means of communication between nodes, which are necessarily cross-domain, will be replaced by extrinsic inputs and outputs standing for gateways to the networking layer.&lt;/p&gt;

&lt;h3&gt;
  
  
  Assume-guarantee reasoning and modelling of faults
&lt;/h3&gt;

&lt;p&gt;The behavior of individual components could be specified in terms of the assumptions about their inputs and the guarantees about their outputs. This would enable &lt;em&gt;assume-guarantee reasoning&lt;/em&gt; about correctness of the system and &lt;em&gt;compositional verification&lt;/em&gt;. In the context of distributed systems, benign node faults can be modeled by suppressing some extrinsic sources belonging to the corresponding domains, whereas Byzantine faults can be modeled by forcing some of the extrinsic sources with arbitrary values ("garbage in — garbage out").&lt;/p&gt;

&lt;h3&gt;
  
  
  Confining interaction lines
&lt;/h3&gt;

&lt;p&gt;The total number of interaction lines in complex components can quickly become too large. Therefore, components should only expose a subset of input-output pairs that is enough to guarantee determinism and reversibility under the component's assumptions, &lt;em&gt;confining&lt;/em&gt; the remaining interaction lines by connecting them to sources and sinks inside the component. For example, in distributed protocols, the exact set of votes forming a valid quorum for certain decisions of the protocol logic often does not affect the outcomes, given the assumptions about the maximal fraction of faulty nodes hold true; so the corresponding interaction lines can be confined within a component representing the protocol.&lt;/p&gt;

&lt;h2&gt;
  
  
  Modelling Distributed Protocols
&lt;/h2&gt;

&lt;h3&gt;
  
  
  Bracha's Reliable Broadcast
&lt;/h3&gt;

&lt;p&gt;Now we'll try to apply the approach to modelling a relatively simple distributed protocol, namely Bracha's broadcast&lt;sup id="fnref2"&gt;2&lt;/sup&gt;. Bracha's broadcast is a foundational distributed protocol implementing a Byzantine fault-tolerant reliable broadcast mechanism in the asynchronous model. The protocol allows one party to broadcast a message such that all correct parties eventually deliver the message and agree on the delivered message, given that less than a third of the parties may be corrupt. The protocol adopts the asynchronous model, i.e. it makes no timing assumptions but requires that every message sent by a correct process is eventually received.&lt;/p&gt;

&lt;p&gt;For the sake of simplicity, we will model a one-shot version of the protocol that only allows broadcasting a single value from a designated sender party. The protocol can be expressed in traditional event-oriented pseudo-code as follows:&lt;br&gt;
&lt;/p&gt;

&lt;div class="highlight js-code-highlight"&gt;
&lt;pre class="highlight plaintext"&gt;&lt;code&gt;upon broadcast(m): // only sender
    send message &amp;lt;SEND, m&amp;gt; to all

upon receiving a message &amp;lt;SEND, m&amp;gt; from the sender:
    send message &amp;lt;ECHO, m&amp;gt; to all

upon receiving n-f messages &amp;lt;ECHO, m&amp;gt; and not having sent a READY message:
    send message &amp;lt;READY, m&amp;gt; to all

upon receiving f+1 messages &amp;lt;READY, m&amp;gt; and not having sent a READY message:
    send message &amp;lt;READY, m&amp;gt; to all

upon receiving n-f messages &amp;lt;READY, m&amp;gt;:
    deliver(m)
&lt;/code&gt;&lt;/pre&gt;

&lt;/div&gt;



&lt;h4&gt;
  
  
  Peer-to-peer links
&lt;/h4&gt;

&lt;p&gt;We will start by modelling communication between individual nodes in the system. Each party in the protocol is represented by a node, and each node is modeled as a separate domain. For the nodes to communicate, those domains need to be able to interact through some kind of cross-domain component. So we define the following component for that purpose:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fjaqfkaq40yyo7rmm27po.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fjaqfkaq40yyo7rmm27po.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;The &lt;code&gt;Link&lt;/code&gt; component allows sending an authenticated value from one node to another. If the &lt;code&gt;rcv&lt;/code&gt; input is left unspecified, as supposed, the component chooses the value from the &lt;code&gt;snd&lt;/code&gt; input as the value of the &lt;code&gt;rcv&lt;/code&gt; output.  The &lt;code&gt;snd&lt;/code&gt; line belongs to the message sender's domain, whereas the &lt;code&gt;rcv&lt;/code&gt; line belongs to the destination node's domain. If we treat &lt;code&gt;Link&lt;/code&gt; as a composite component, we can model it as shown on the right side of the diagram above, where the internal interaction line in the middle belongs to a separate domain and represents the communication medium.&lt;/p&gt;

&lt;h4&gt;
  
  
  Weak broadcast
&lt;/h4&gt;

&lt;p&gt;Although the underlying communication mechanism is point-to-point message exchange, if we look closer, the basic communication pattern used in the reliable broadcast protocol is sending the same message to all nodes. Let's refer to this pattern as weak broadcast and represent it as the following component:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2F12e2kin231layslwv6de.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2F12e2kin231layslwv6de.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;The &lt;code&gt;bc&lt;/code&gt; line belongs to the sending node's domain, whereas the elements of the composite &lt;code&gt;dlvr&lt;/code&gt; line belong to the corresponding receiving nodes' domains. We can model a corrupt sender committing the failure of message equivocation (sending different messages to some receivers) by forcing some of the sources in its domain with arbitrary values. The component is mainly composed of &lt;code&gt;Link&lt;/code&gt; and &lt;code&gt;Def&lt;/code&gt; components replicated for each receiving node. The &lt;code&gt;Def&lt;/code&gt; components are meant to create an individual copy of the &lt;code&gt;bc&lt;/code&gt; value for each instance of &lt;code&gt;Link&lt;/code&gt;. Note the recursive pattern, used together with the replication box, that forms a kind of forward loop in order to thread the value from the &lt;code&gt;bc&lt;/code&gt; input through the replicated components.&lt;/p&gt;

&lt;h4&gt;
  
  
  Quorums
&lt;/h4&gt;

&lt;p&gt;Another kind of component that we will need is for collecting quorums of values received from peer nodes:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fqw6fcpmczwz6y7t4xfpy.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fqw6fcpmczwz6y7t4xfpy.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;The &lt;code&gt;WeakQuroum&lt;/code&gt; and &lt;code&gt;StrongQuorum&lt;/code&gt; components are identical except the number of votes required to reach the quorum: &lt;code&gt;f+1&lt;/code&gt; and &lt;code&gt;n-f&lt;/code&gt;, respectively. &lt;code&gt;WeakQuorum&lt;/code&gt; ensures that there is at least one vote from a correct node, whereas &lt;code&gt;StrongQuorum&lt;/code&gt; ensures that any two of such quorums must intersect in at least one correct node. Moreover, &lt;code&gt;StrongQuorum&lt;/code&gt; ensures that any of its quorums contains at least as many votes from correct nodes as the total number of votes required by &lt;code&gt;WeakQuorum&lt;/code&gt;. The &lt;code&gt;votes&lt;/code&gt; line represents the values received from peer nodes, whereas the &lt;code&gt;value&lt;/code&gt; line represents the value supported by a sufficient quorum of votes. If the &lt;code&gt;value&lt;/code&gt; input is left unspecified then the component will choose the value corresponding to the earliest quorum of votes becoming available; if the &lt;code&gt;value&lt;/code&gt; input is forced then the component will make the complementary output available only once a quorum becomes available on the &lt;code&gt;votes&lt;/code&gt; input.&lt;/p&gt;

&lt;h4&gt;
  
  
  Overall protocol model
&lt;/h4&gt;

&lt;p&gt;Now we can model the Bracha's reliable broadcast protocol as a cross-domain component with an interface identical to &lt;code&gt;WB&lt;/code&gt; but providing the guarantees of reliable broadcast:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2F2c1y5uucijpczkg57u6n.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2F2c1y5uucijpczkg57u6n.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;In this diagram, we omit sources of unspecified values and sinks. We also omit types, but indicate the dimentionality of composite lines. We label the instances of the  &lt;code&gt;WB&lt;/code&gt; component with names: &lt;code&gt;send&lt;/code&gt;, &lt;code&gt;echo&lt;/code&gt;, and &lt;code&gt;ready&lt;/code&gt;, indicating the kind of protocol message being communicated through those components.&lt;/p&gt;

&lt;p&gt;The &lt;code&gt;send&lt;/code&gt; component is used to send a value from the designated sender node to all nodes, whereas the &lt;code&gt;echo&lt;/code&gt; and &lt;code&gt;ready&lt;/code&gt; components are replicated for each node and represent all-to-all communication. Note that the composite &lt;code&gt;dlvr&lt;/code&gt; outputs of the &lt;code&gt;WB&lt;/code&gt; components replicated for each node sending &lt;code&gt;ECHO&lt;/code&gt; and &lt;code&gt;READY&lt;/code&gt; messages go through transposers outside of replication boxes. Remember that individual lines of the &lt;code&gt;dlvr&lt;/code&gt; output belong to the corresponding receiving nodes' domains, but we need to connect the &lt;code&gt;votes&lt;/code&gt; inputs of the quorum components so that they all belong to the same node's domain. The trasnposers rearrange the composite lines to achieve that.&lt;/p&gt;

&lt;p&gt;The &lt;code&gt;Select&lt;/code&gt; component, replicated for each node, represents a choice between two alternative causes for sending a &lt;code&gt;READY&lt;/code&gt; message: either upon receiving a strong quorum of &lt;code&gt;ECHO&lt;/code&gt; messages or upon receiving a weak quorum of &lt;code&gt;READY&lt;/code&gt; message from other nodes.&lt;/p&gt;

&lt;h4&gt;
  
  
  Consistent broadcast and modularized protocol model
&lt;/h4&gt;

&lt;p&gt;We should recognize that a part of this reliable broadcast protocol actually represents a consistent broadcast protocol. Consistent broadcast guarantees that receivers agree on the delivered values, but it does not guarantee that all correct receivers eventually deliver the value even if some correct receivers deliver. We can represent this sub-protocol as a cross-domain component:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Focsyq8mfp0rr4s8u9m0y.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Focsyq8mfp0rr4s8u9m0y.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;and then restructure the reliable broadcast protocol as follows:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2F9nvxjr63e2c1hz5vd90y.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2F9nvxjr63e2c1hz5vd90y.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;h3&gt;
  
  
  Tendermint Consensus
&lt;/h3&gt;

&lt;p&gt;Now we'll try to apply the approach to a more complicated protocol and sketch a model of the Tendermint consensus protocol&lt;sup id="fnref3"&gt;3&lt;/sup&gt;. Tendermint is a Byzantine fault-tolerant sequence consensus protocol (a.k.a. total order broadcast or atomic broadcast), which allows nodes to agree on a single growing sequence of values where values can be proposed by different nodes. The protocol adopts the partially synchronous model, i.e. it assumes that eventually all messages are delivered within certain time bound, although there might be periods of asynchrony in the system. The timing assumptions complicate modelling by adding more non-determinism and appear in the protocol in a form of timeouts.&lt;/p&gt;

&lt;h4&gt;
  
  
  Gossip communication
&lt;/h4&gt;

&lt;p&gt;The Tendermint protocol relies upon a gossip-based mechanism for communication between nodes: a node can broadcast a message through the gossip mechanism and it will be delivered at all correct nodes. Moreover, if a correct node delivers a message from the gossip mechanism then the same message is guaranteed to be delivered at all other correct nodes. We will model this communication mechanism as the following cross-domain component:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fiolul6pxh3ei9sa2nf89.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fiolul6pxh3ei9sa2nf89.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;The &lt;code&gt;bc&lt;/code&gt; line belongs to the sending node and represents the set of values broadcast through this instance of the gossip mechanism; each element of the &lt;code&gt;dlvr&lt;/code&gt; line belongs to the corresponding receiving node and represents the set of values delivered from that instance of the gossip mechanism.&lt;/p&gt;

&lt;p&gt;Individual elements in the &lt;code&gt;Set&lt;/code&gt; type are concurrent and can become available independently of each other. We can think of the &lt;code&gt;Set&amp;lt;T&amp;gt;&lt;/code&gt; type as a composition of single-bit lines, each representing the presence or absence of a particular value of &lt;code&gt;T&lt;/code&gt; in the set.&lt;/p&gt;

&lt;p&gt;If the &lt;code&gt;bc&lt;/code&gt; line belongs to a correct node then the same set of values becomes available on all elements of the &lt;code&gt;dlvr&lt;/code&gt; output that belong to correct nodes as the set of values on the &lt;code&gt;bc&lt;/code&gt; input. Moreover, if any value becomes available on one element of &lt;code&gt;dlvr&lt;/code&gt; of a correct node then the same value also becomes available on all correct nodes' elements of &lt;code&gt;dlvr&lt;/code&gt;.&lt;/p&gt;

&lt;p&gt;Correct nodes in the Tendermint protocol only ever broadcast a single value through each instance of the &lt;code&gt;Gossip&lt;/code&gt; component; however, Byzantine nodes may broadcast multiple values and all correct nodes would eventually deliver all of those values from that instance of the &lt;code&gt;Gossip&lt;/code&gt; component.&lt;/p&gt;

&lt;h4&gt;
  
  
  Overall protocol model
&lt;/h4&gt;

&lt;p&gt;Nodes in the Tendermint protocol decide on a single value at each &lt;em&gt;height&lt;/em&gt; in the growing sequence of values. At each height, the protocol may need one or multiple &lt;em&gt;rounds&lt;/em&gt; in order to reach agreement between nodes and determine the decision value to &lt;em&gt;commit&lt;/em&gt; at that height. Each round consists of the &lt;em&gt;proposal&lt;/em&gt;, &lt;em&gt;prevote&lt;/em&gt;, and &lt;em&gt;precommit&lt;/em&gt; stages. So we can model the overall protocol as the following cross-domain component:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fovqh9lqqikhey19gby8b.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fovqh9lqqikhey19gby8b.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;Here, again, we omit sources of unspecified values and sinks, omit most of the types, but indicate the dimentionality of composite lines with superscript indeces.&lt;/p&gt;

&lt;p&gt;The &lt;code&gt;Tendermint&lt;/code&gt; component represents the overall protocol. Its composite &lt;code&gt;value&lt;/code&gt; input represents the values that would be proposed by each node (index &lt;code&gt;n&lt;/code&gt;) in each round (index &lt;code&gt;r&lt;/code&gt;) at each height (index &lt;code&gt;h&lt;/code&gt;); the &lt;code&gt;proposer&lt;/code&gt; input represent the designated proposer for each round at each height; the &lt;code&gt;decision&lt;/code&gt; output represents the decision value by each node at each height. Finally, the composite &lt;code&gt;aux&lt;/code&gt; line represents the auxiliary lines added for each height in order to satisfy the determinism and reversibility requirements.&lt;/p&gt;

&lt;p&gt;The &lt;code&gt;Height&lt;/code&gt; component represents the protocol logic for each height. Its interaction lines are mostly identical to those of the &lt;code&gt;Tendermint&lt;/code&gt; component, without the last level of composition, except that the auxiliary line is represented more explicitly. Namely, the &lt;code&gt;aux&lt;/code&gt; line of &lt;code&gt;Tendermint&lt;/code&gt; is composed of the following lines of &lt;code&gt;Height&lt;/code&gt;: &lt;code&gt;decisionRound&lt;/code&gt; representing the round number in which each nodes commits the decision value, &lt;code&gt;timeouts&lt;/code&gt; and &lt;code&gt;aborts&lt;/code&gt; representing timeouts and aborts happened at each node in each round.&lt;/p&gt;

&lt;h4&gt;
  
  
  &lt;code&gt;Height&lt;/code&gt; component
&lt;/h4&gt;

&lt;p&gt;We model the &lt;code&gt;Height&lt;/code&gt; component as follows:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fe4bvzvqga4wpz2hn1q9h.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fe4bvzvqga4wpz2hn1q9h.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;The &lt;code&gt;Round&lt;/code&gt; component represents a single instance of the repetitive part of the protocol that includes the proposal, prevote, and precommit stages, in which a designated proposer broadcasts a proposal proposing a decision value to all nodes who can then broadcast prevote and precommit votes for the proposed value. At each node, instead of voting for the proposal, the prevote and precommit stages may timeout, in which case the node broadcasts a special &lt;code&gt;nil&lt;/code&gt; vote, or abort, in which case the node does not broadcast any vote in that stage of the round; the propose stage can also abort. As we'll see later, the rounds and stages are coordinated by the signals from the &lt;code&gt;pmSignals&lt;/code&gt; input. Those signals are required for the round stages to broadcast a proposal or vote, to timeout, or to abort. The actual timeout and abort decisions are represented by the &lt;code&gt;timeouts&lt;/code&gt; and &lt;code&gt;aborts&lt;/code&gt; lines.&lt;/p&gt;

&lt;p&gt;The Tendermint protocol defines certain conditions that a proposal must satisfy in order to be voted for. Those conditions depend on the outcomes of the previous round, so there is a forward loop, represented by the &lt;code&gt;loopFwd&lt;/code&gt; line, that connects successive instances of the replicated &lt;code&gt;Round&lt;/code&gt; component and conveys the required values from the previous to the next round.&lt;/p&gt;

&lt;p&gt;The &lt;code&gt;Commit&lt;/code&gt; component represents the decision logic of the protocol that is replicated for each node. Given the proposal and precommit votes from each round, it determines the single decision by selecting the value proposed in one of the rounds, the decision round, for which there exists a strong quorum of matching precommit votes.&lt;/p&gt;

&lt;p&gt;The &lt;code&gt;Pacemaker&lt;/code&gt; component coordinates the rounds and stages of the protocol by making the corresponding signals available according to the required dynamics of the protocol. We'll see those signals connected to the corresponding components in the next diagram.&lt;/p&gt;

&lt;h4&gt;
  
  
  &lt;code&gt;Round&lt;/code&gt; component
&lt;/h4&gt;

&lt;p&gt;We model the &lt;code&gt;Round&lt;/code&gt; component as follows:&lt;/p&gt;

&lt;p&gt;&lt;a href="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fmmtxyrke6xpe2c0iskek.png" class="article-body-image-wrapper"&gt;&lt;img src="https://media2.dev.to/dynamic/image/width=800%2Cheight=%2Cfit=scale-down%2Cgravity=auto%2Cformat=auto/https%3A%2F%2Fdev-to-uploads.s3.amazonaws.com%2Fuploads%2Farticles%2Fmmtxyrke6xpe2c0iskek.png"&gt;&lt;/a&gt;&lt;/p&gt;

&lt;p&gt;The &lt;code&gt;Propose&lt;/code&gt;, &lt;code&gt;Prevote&lt;/code&gt;, and &lt;code&gt;Precommit&lt;/code&gt; components represent the stages of the protocol logic and determine the values of the corresponding messages to broadcast through the gossip mechanism. &lt;code&gt;Prevote&lt;/code&gt; and &lt;code&gt;Precommit&lt;/code&gt; are replicated so that there are individual instances for each node. Note that there are separate instances of the &lt;code&gt;Gossip&lt;/code&gt; component for each node and stage, except for the proposal that is broadcast only by the designated proposer node, and those instances are replicated in the overall protocol component for each round and height. This way, there is no need to include the message tag, height and round numbers in the values that are broadcast through the &lt;code&gt;Gossip&lt;/code&gt; component instances. The composite lines representing all-to-all communication go through transposers outside of the replication boxes in order to rearrange their components appropriately.&lt;/p&gt;

&lt;p&gt;The &lt;code&gt;validVR&lt;/code&gt; and &lt;code&gt;lockedVR&lt;/code&gt; are composite lines representing &lt;code&gt;(validValue, validRound)&lt;/code&gt; and &lt;code&gt;(lockedValue, lockedRound)&lt;/code&gt;, respectively, with the values corresponding to the variables of the same name from the protocol pseudo-code as it is described in the original paper&lt;sup id="fnref3"&gt;3&lt;/sup&gt;. Basically, &lt;code&gt;validVR&lt;/code&gt; is used to determine whether the proposer should propose a new value or re-propose a value proposed in one of the previous rounds, &lt;code&gt;lockedVR&lt;/code&gt; determines which proposals are safe to cast a prevote for. As we can see from the diagram, the values in those lines are updated in the &lt;code&gt;Precommit&lt;/code&gt; component. The &lt;code&gt;prevoteQVals&lt;/code&gt; line is a composite line each element of which corresponds to the prevote, if any, supported by a strong quorum in the previous rounds. Note how the &lt;code&gt;prevoteQVals&lt;/code&gt; and &lt;code&gt;round&lt;/code&gt; lines are updated for each node in a replication box: the composite &lt;code&gt;prevoteQVals&lt;/code&gt; line is extended with an additional line connected to the corresponding output of the &lt;code&gt;Precommit&lt;/code&gt; component, whereas &lt;code&gt;round&lt;/code&gt; is simply incremented by the component labeled with &lt;code&gt;+1&lt;/code&gt;.&lt;/p&gt;

&lt;p&gt;We will not decompose the components further since the main point was to make a sketch of how we can model the overall structure of the Tendermint protocol, namely the heights, rounds, stages, the interconnection between them, and represent the dynamics of the protocol.&lt;/p&gt;

&lt;h2&gt;
  
  
  Conclusion
&lt;/h2&gt;

&lt;p&gt;We explored a possible way of applying the ideas of reversible deterministic concurrency to modelling distributed protocols. We tried to make the vague ideas a little more concrete and give a better intuition of how an approach based on those ideas may look like by considering some guiding principles, spelling out some details, introducing some primitives and patterns, expressing this in a graphical notation. We considered modelling distributed systems as a whole and then deriving local projections for individual nodes. We also considered how we can model node failures, both benign and Byzantine. Finally, we saw how some concrete, well-known distributed protocols may look like when modeled following this approach.&lt;/p&gt;

&lt;p&gt;We also anticipated some potential benefits of the approach, such as modularity, composability, compositional reasoning and verification, absence of hidden data flows, enhanced debugging and verification methods, resource management, representing a distributed system as a whole and then deriving the logic and implementation for its local nodes.&lt;/p&gt;

&lt;p&gt;This is just the beginning of developing those ideas into a practical solution. We'll need to see what this approach means for different aspects of designing and implementing distributed protocols. We'll need to invent some kind of textual notation and develop a clear, consistent concept codifying the core principles. We'll need to find a way of implementing those ideas in real code and examine its expressivity and limitations, better understand the benefits and drawbacks. In other words, we need to find a good way of turning this into a solid foundation for our framework.&lt;/p&gt;

&lt;p&gt;If you like the project and find it valuable, please &lt;a href="https://github.com/sponsors/replica-io" rel="noopener noreferrer"&gt;support&lt;/a&gt; its further development! 🙏&lt;br&gt;
&lt;a href="https://github.com/sponsors/replica-io" class="crayons-btn crayons-btn--primary" rel="noopener noreferrer"&gt;❤️ Replica_IO&lt;/a&gt;
&lt;/p&gt;

&lt;p&gt;If you have any thought you would like to share or any question regarding this post, please add a comment &lt;a href="https://github.com/orgs/replica-io/discussions/80" rel="noopener noreferrer"&gt;here&lt;/a&gt;. You are also welcome to &lt;a href="https://github.com/orgs/replica-io/discussions/new" rel="noopener noreferrer"&gt;start a new discussion&lt;/a&gt; or chime in to &lt;a href="https://discord.replica-io.dev/" rel="noopener noreferrer"&gt;our Discord&lt;/a&gt; server.&lt;/p&gt;




&lt;ol&gt;

&lt;li id="fn1"&gt;
&lt;p&gt;Controlled swap of individual bits is known as &lt;a href="https://en.wikipedia.org/wiki/Fredkin_gate" rel="noopener noreferrer"&gt;Fredkin gate&lt;/a&gt; in &lt;a href="https://en.wikipedia.org/wiki/Reversible_computing" rel="noopener noreferrer"&gt;reversible&lt;/a&gt; and &lt;a href="https://en.wikipedia.org/wiki/Quantum_computing" rel="noopener noreferrer"&gt;quantum&lt;/a&gt; computing; here we generalize it to operate on target values of arbitrary type. ↩&lt;/p&gt;
&lt;/li&gt;

&lt;li id="fn2"&gt;
&lt;p&gt;To learn about Bracha's broadcast in detail, please refer to the &lt;a href="https://ecommons.cornell.edu/bitstream/handle/1813/6430/84-590.pdf" rel="noopener noreferrer"&gt;original paper&lt;/a&gt;, where it was introduced as a key building block of an asynchronous consensus protocol. The following post may also be helpful: &lt;a href="https://decentralizedthoughts.github.io/2020-09-19-living-with-asynchrony-brachas-reliable-broadcast/" rel="noopener noreferrer"&gt;Living with Asynchrony: Bracha's Reliable Broadcast&lt;/a&gt;, as well as &lt;a href="https://dcl.epfl.ch/site/_media/education/sdc_byzconsensus.pdf" rel="noopener noreferrer"&gt;these lecture notes&lt;/a&gt;. ↩&lt;/p&gt;
&lt;/li&gt;

&lt;li id="fn3"&gt;
&lt;p&gt;For a more precise and detailed description of the Tendermint protocol please refer to the &lt;a href="https://arxiv.org/pdf/1807.04938" rel="noopener noreferrer"&gt;original paper&lt;/a&gt;. ↩&lt;/p&gt;
&lt;/li&gt;

&lt;/ol&gt;

</description>
      <category>distributedsystems</category>
      <category>decentralizedcomputing</category>
      <category>faulttolerance</category>
      <category>replication</category>
    </item>
    <item>
      <title>On Frameworks for Implementing Distributed Protocols</title>
      <dc:creator>Sergey Fedorov</dc:creator>
      <pubDate>Thu, 29 Aug 2024 15:33:10 +0000</pubDate>
      <link>https://dev.to/replica-io/on-frameworks-for-implementing-distributed-protocols-37a0</link>
      <guid>https://dev.to/replica-io/on-frameworks-for-implementing-distributed-protocols-37a0</guid>
      <description>&lt;p&gt;This post concludes the second phase of the &lt;a href="https://github.com/replica-io/replica-io/issues/7" rel="noopener noreferrer"&gt;state-of-the-art exploration&lt;/a&gt; in the scope of milestone &lt;a href="https://github.com/replica-io/replica-io/milestone/1" rel="noopener noreferrer"&gt;M0.1&lt;/a&gt; of the Replica_IO project, namely exploration of existing frameworks for implementing distributed protocols. It shares the main conclusions drawn from exploring 7 different frameworks.&lt;/p&gt;

&lt;p&gt;The original post can be found &lt;a href="https://replica-io.dev/blog/2024/08/27/on-frameworks-for-implementing-distributed-protocols" rel="noopener noreferrer"&gt;here&lt;/a&gt;.&lt;/p&gt;

&lt;p&gt;A companion video is available on YouTube:&lt;br&gt;
&lt;iframe width="710" height="399" src="https://www.youtube.com/embed/oRQG6EBzVe4"&gt;
&lt;/iframe&gt;
&lt;/p&gt;

&lt;h2&gt;
  
  
  Exploring Distributed Protocol Frameworks
&lt;/h2&gt;

&lt;p&gt;Trying to make a real breakthrough, such as what the Replica_IO project aims at, it is important to learn from prior attempts to deal with the problem. Having explored how real-world code bases typically implement the core distributed protocols like consensus and having summarized the findings in &lt;a href="https://replica-io.dev/blog/2024/03/04/on-implementation-of-distributed-prtocols" rel="noopener noreferrer"&gt;the previous post&lt;/a&gt;, I continued the exploration by surveying existing attempts to find a better approach to the problem, i.e. different frameworks for implementing distributed protocols.&lt;/p&gt;

&lt;p&gt;I looked at the documentation and examples provided by each of the frameworks, as well as into their implementation, in order to figure out how they model and structure distributed systems, what kind of notation is used to specify and implement distributed protocols in those frameworks, what is their approach to communication, concurrency, and composition of protocol components, and what they offer for ensuring the correctness of protocols and their implementations.&lt;/p&gt;

&lt;p&gt;After having explored each of the frameworks, I summarized and shared some of my findings. You can find those overviews on &lt;a href="https://github.com/replica-io/replica-io/wiki/State-of-the-art-exploration" rel="noopener noreferrer"&gt;this wiki page&lt;/a&gt;.&lt;/p&gt;

&lt;p&gt;Here is the full list of 7 frameworks, based on different programming languages, that I explored&lt;sup id="fnref1"&gt;1&lt;/sup&gt;:&lt;/p&gt;

&lt;ul&gt;
&lt;li&gt;
&lt;a href="https://github.com/consensus-shipyard/mir" rel="noopener noreferrer"&gt;Mir&lt;/a&gt; — a framework for implementing, debugging, and analyzing distributed protocols (based on Go);&lt;/li&gt;
&lt;li&gt;
&lt;a href="https://github.com/SecureSolutionsLab/Atlas" rel="noopener noreferrer"&gt;Atlas&lt;/a&gt; — a modular framework for building distributed mechanisms focused on configurability and performance (based on Rust);&lt;/li&gt;
&lt;li&gt;
&lt;a href="https://github.com/pfouto/babel-core" rel="noopener noreferrer"&gt;Babel&lt;/a&gt; — a generic framework for implementing and executing distributed protocols (based on Java);&lt;/li&gt;
&lt;li&gt;
&lt;a href="https://distal.github.io/" rel="noopener noreferrer"&gt;DiStaL&lt;/a&gt; — a framework for implementing and executing distributed protocols (based on Scala);&lt;/li&gt;
&lt;li&gt;
&lt;a href="https://github.com/dzufferey/psync" rel="noopener noreferrer"&gt;PSync&lt;/a&gt; — a framework for implementing and verifying fault-tolerant distributed protocols (based on Scala);&lt;/li&gt;
&lt;li&gt;
&lt;a href="https://github.com/DistributedComponents/disel" rel="noopener noreferrer"&gt;Disel&lt;/a&gt; — a framework for implementation and compositional machine-assisted verification of distributed systems and their clients (based on Coq);&lt;/li&gt;
&lt;li&gt;
&lt;a href="https://github.com/uwplse/verdi" rel="noopener noreferrer"&gt;Verdi&lt;/a&gt; — a framework for implementing and formally verifying distributed systems (based on Coq).&lt;/li&gt;
&lt;/ul&gt;

&lt;p&gt;In the subsequent sections, I will share some of the observations and conclusions I made while exploring those frameworks. I decided to structure the discussion around the following aspects:&lt;/p&gt;

&lt;ul&gt;
&lt;li&gt;
&lt;em&gt;model&lt;/em&gt;: how distributed systems and their components are modeled;&lt;/li&gt;
&lt;li&gt;
&lt;em&gt;structure&lt;/em&gt;: how distributed protocol components are structured and composed together;&lt;/li&gt;
&lt;li&gt;
&lt;em&gt;notation&lt;/em&gt;: what kind of notation is used to specify and implement distributed protocols;&lt;/li&gt;
&lt;li&gt;
&lt;em&gt;operation&lt;/em&gt;: how distributed protocol components are executed and interact with each other;&lt;/li&gt;
&lt;li&gt;
&lt;em&gt;verification&lt;/em&gt;: how distributed protocols and their implementations are verified for correctness.&lt;/li&gt;
&lt;/ul&gt;

&lt;p&gt;But before we go into details, I would like to note that most of those frameworks were purely academic efforts and almost all of them seem to be abandoned now; unfortunately, they didn't seem to have found practical use. Nevertheless, it was good to learn from them. Let's now dive in.&lt;/p&gt;

&lt;h2&gt;
  
  
  Model
&lt;/h2&gt;

&lt;p&gt;The way that systems and their components are modeled has a profound effect on the structure and shape of their specifications and implementation, on the operational aspects and verification for correctness. We can consider different levels of abstraction when modeling distributed systems: the high-level model of the system as a whole, the model of individual nodes within the system, as well as individual protocols and components within the nodes. Let's take a look at how the explored frameworks model distributed systems and their components.&lt;/p&gt;

&lt;p&gt;The common approach is to model distributed systems at high level as &lt;a href="https://en.wikipedia.org/wiki/Transition_system" rel="noopener noreferrer"&gt;state transition systems&lt;/a&gt; where the global system state changes upon external and internal events, such as client requests, messages exchanged within the system, and timeouts. In this model, the global system state includes the states of all individual nodes and their components, as well as the environment state. The environment state usually includes the state of the network the nodes communicate through, in particular the messages in transit. Transitioning from one state to another happens according to a global &lt;em&gt;transition function&lt;/em&gt; triggered by events. The transition function receives the current state of the system together with the triggering event and returns the new system state.&lt;/p&gt;

&lt;p&gt;The explored frameworks follow the &lt;a href="https://en.wikipedia.org/wiki/Message_passing" rel="noopener noreferrer"&gt;message-passing&lt;/a&gt; approach, where the states of individual nodes and protocol components are disjoint, i.e. different parts do not share pieces of state. Interaction between nodes happens through the network by sending and receiving messages. Sending and receiving of messages are modeled as events modifying the global system state by updating the set of messages in transit in the network state and, in case of message receiving, the state of the target component in the destination node. For example, in Disel, the system state includes a "message soup" for each protocol, which models the current state and the history of the network. In Disel's abstract model, messages are never removed from the message soup, instead they are marked either as active or consumed.&lt;/p&gt;

&lt;p&gt;Nodes and network failures are modeled as special events, e.g. dropping or duplicating messages in the network, disabling normal event handling in faulty nodes or (partially) resetting their state. Some of the frameworks only consider crash faults, leaving &lt;a href="https://en.wikipedia.org/wiki/Byzantine_fault" rel="noopener noreferrer"&gt;Byzantine faults&lt;/a&gt; for the future work. The system models in most of the frameworks do not seem to include timing assumption, so they can be considered asynchronous. In contrast, PSync employs the Heard-Of model based on communication-closed rounds, which provides an illusion of simple synchronous communication on top of the partial synchrony of the actual underlying network. In this model, protocol execution proceeds in explicit rounds, alternating communication with protocol state transition based on the set of messages received during the round. Network and node faults in this model are unified, and the network assumptions are specified in terms of the heard-of sets.&lt;/p&gt;

&lt;p&gt;Communication between nodes is predominantly modeled as fire-and-forget message delivery, where messages can be reordered or dropped by the network abstraction. Though, in Verdi, protocols are first modeled with an idealistic, reliable network semantics, which can then be translated into weaker fault models using verified system transformers. Babel allows modeling protocols in stronger communication models using communication channel abstractions, which represent communication mechanisms with different properties and guarantees.&lt;/p&gt;

&lt;p&gt;Individual components within nodes are commonly modeled as sequential, event-driven state machines interacting with each other via reliable message passing. The message passing normally follows the one-to-one one-way or request-response patterns; however, some of the frameworks also support one-to-many notifications between components. Some frameworks (e.g., Verdi) explicitly distinguish between the events that are external to the distributed protocol, like client requests, and internal events, like exchanging messages between protocol components and nodes within the distributed system.&lt;/p&gt;

&lt;p&gt;To overcome the limitations of strict state separation between protocol components in the abstract model, Disel allows coupling protocols via inter-protocol behavioral dependencies, called send-hooks, which allow restricted logical access to other protocol's state. Disel doesn't seem to strictly follow the message-passing model for protocol components within the same node, supporting generic composition of protocol components. Disel also provides mechanisms to establish stronger properties of protocols and their combinations by strengthening them with additional inductive invariants.&lt;/p&gt;

&lt;p&gt;As we can see, although there are some interesting variations and extensions, the underlying system model in the explored frameworks is largely the same, namely the one of a state transition system composed of components, which are sequential, event-driven state machines with disjoint state, interacting via message passing. This is remarkably similar to how distributed protocols are usually implemented in real-world code bases, which do not use any framework, as I described in &lt;a href="https://replica-io.dev/blog/2024/03/04/on-implementation-of-distributed-prtocols" rel="noopener noreferrer"&gt;the previous post&lt;/a&gt;. This approach tends to shift the focus more to the operational rather than functional and logical aspects of the system. There I also pointed out, when discussing how protocol implementations attempt to &lt;a href="https://replica-io.dev/blog/2024/03/04/on-implementation-of-distributed-prtocols#evading-concurrency" rel="noopener noreferrer"&gt;evade concurrency&lt;/a&gt;, that this approach may complicate the implementation and cause fragmentation of the protocol logic. Perhaps, adopting the same kind of the underlying model is one of the reasons why the explored frameworks do not seem to have made a real breakthrough in designing and implementing distributed protocols.&lt;/p&gt;

&lt;h2&gt;
  
  
  Structure
&lt;/h2&gt;

&lt;p&gt;In all of the explored frameworks, protocol implementations rely on some kind of runtime or shim provided by the framework, hiding low-level concerns from implementation of the protocol logic. In most of the frameworks, the runtime is responsible for coordinating the execution of protocol components and interaction between them; some of the frameworks also provide there dedicated interfaces for communication over the network and setting timers. Protocol components normally need to be registered within the runtime before they can function within the system. &lt;/p&gt;

&lt;p&gt;In most cases, protocol components within the same node can interact by simply sending some kind of internal messages to each other, without establishing any explicit connection. In contrast, components in Atlas require explicit orchestration of the interaction with the rest of the system. Disel instead supports composition of components expressed as effectful functional programs; it also allows loosely coupling protocol components via inter-protocol behavioral dependencies, called send-hooks, at the formal specification level.&lt;/p&gt;

&lt;p&gt;Since the runtime in Mir is only responsible for coordinating the execution of protocol components and interaction between them, there are special components that provide functionality for sending and receiving messages over the network, as well as for setting local timers and for cryptographic operations. Mir explicitly distinguishes between passive components, which can only produce events synchronously, as a result of processing input events provided by the runtime, and active components, which can asynchronously produce new events on their own.&lt;/p&gt;

&lt;p&gt;There are frameworks that provide means for enhancing protocol components with additional properties. Disel provides a protocol combinator &lt;code&gt;ProtocolWithIndInv&lt;/code&gt;, which allows elaborating a protocol by strengthening it with additional inductive invariants. Verdi provides verified system transformers, which allow transforming protocols specified, implemented, and verified in an idealistic, reliable network semantics into an equivalent implementation, preserving the transformed system properties under a weaker fault model. PSync provides a class, which can be used to wrap protocol round instances to support updating progress conditions and synchronizing rounds in a Byzantine setting.&lt;/p&gt;

&lt;p&gt;There are two main approaches to structure interaction of distributed protocols with the rest of the application. Some frameworks provide a mechanism for interacting with protocol components by sending and receiving messages, same as protocol components interact with each other. Other frameworks allow defining dedicated interfaces for that purpose, featuring callable methods or special IO events. In some of the frameworks, protocol components are supplied with some kind of handles to trigger side effects, such as sending messages or setting up timers; in other frameworks, side effects only happen after returning the control back to the runtime, e.g. through the return value or using a monadic structure.&lt;/p&gt;

&lt;p&gt;Protocol components commonly consist of the component's state and protocol logic structured as handlers modifying the state or state transition functions, which are triggered by the runtime upon certain events or conditions. In Distal and Disel, the handlers/transitions can be augmented with guarding conditions that must hold in order to trigger the action.&lt;/p&gt;

&lt;p&gt;The round-based model in PSync imposes a particular structure of protocol components. Protocol components in PSync must specify a sequence of protocol rounds. Each round, in general, consists of methods to: initialize the round, send messages at the beginning of the round, process received messages, and finally update the internal state before transitioning into the next round.&lt;/p&gt;

&lt;p&gt;PSync and Disel explicitly separate the protocol specification from its implementation, whereby the specification is used to formally verify the implementation. Protocol specifications in PSync consist of protocol properties, as well as safety and liveness predicates (assumptions). In order to aid automated verification in PSync, the specification should also include round and/or phase invariants; round transition relations are automatically derived from the code, although this imposes certain limitations on the code. In Disel, high-level abstract protocol specifications are defined in terms of state-space coherence predicates and send/receive transitions.&lt;/p&gt;

&lt;p&gt;The configuration of protocol components within nodes and their internal structure can be more static or dynamic. For example, in Babel, protocol components and various components' callbacks are registered within the runtime dynamically. The configuration of top-level components in Mir is rather static, for it cannot be changed after initialization, but there is a special component, called factory module, that supports creating sub-components dynamically. Such flexibility at runtime can make formal verification particularly hard, so the frameworks focused on formal verification (PSync, Disel, and Verdi) tend to be rather static with respect to the configuration and internal structure of protocol components.&lt;/p&gt;

&lt;p&gt;Overall, the abstract model adopted by a framework, e.g. the model of a generic state transition system with message-passing or the Heard-Of model based on communication-closed rounds, largely determines how protocol specifications and implementations are structured within the framework. The framework's features like formal verification can add further restrictions, e.g. restricting runtime flexibility of the configuration and internal structure of protocol components.&lt;/p&gt;

&lt;h2&gt;
  
  
  Notation
&lt;/h2&gt;

&lt;p&gt;All of the explored frameworks use the general-purpose programming language they are based on as the primary means for expressing protocol implementations. To enhance ergonomics and expressiveness, most of the frameworks introduce some notational extensions, e.g. elements of an embedded domain-specific language (eDSL).&lt;/p&gt;

&lt;p&gt;Using a regular general-purpose programming language as the basis allows tapping directly into the comprehensive features of the language, such as the type system, polymorphism, inheritance, and metaprogramming. On the other hand, implementing protocol components in regular code can produce some undesirable effects such as nondeterminism, e.g. when iterating over built-in unordered data structures, which is problematic for reproducible simulation-based testing. For that reason, Mir provides some utility functions that should be used in place of usual idiomatic code to avoid that kind of nondeterminism. Rich expressiveness of general-purpose languages can also make automatic verification difficult, e.g. PSync is quite limited in what kind of Scala constructs it supports in automatic derivation of transition relations from the code.&lt;/p&gt;

&lt;p&gt;In most cases, the notational extensions introduced by the frameworks serve to make the code more declarative and concise. One target of such enhancements is providing a convenient and clear way of expressing the typical event-oriented pseudo-code notation with &lt;code&gt;upon&lt;/code&gt; statements. For example, the protocol logic in Distal is implemented by defining rules and the corresponding actions, whereby the rules are expressed in a declarative style resembling typical pseudo-code found in the literature and specify event predicates, such as the message type and matching conditions, as well as the means to specify composite events, which are triggered by collections of messages.&lt;/p&gt;

&lt;p&gt;Another area of applying notational enhancements is for expressing certain actions performed by the protocol logic and overcoming the limitations of the host language. For example, Distal provides a special notation for sending messages, discarding received messages, as well as for scheduling actions to be executed in future. Disel extends Coq's specification language Gallina with effectful commands (actions), such as sending and receiving messages, reading from local state, monadic sequential composition, and general recursion. For message sending and receiving actions, Disel provides transition wrappers, which lift low-level operations on the networking layer to the level of well-typed program primitives corresponding to the protocol specification. Similarly, Verdi provides a monad for expressing the actions of sending messages, emitting output event, and manipulating the current state, as well as convenience notation for various monadic bindings.&lt;/p&gt;

&lt;p&gt;Finally, expressing protocol properties, assumptions, and invariants, as well as the related annotations in the protocol implementation can also benefit from notational enhancements. PSync, for instance, defines a DSL for expressing properties, predicates and invariants, in which one of the main primitives is the notion of domain, representing a set of values of certain type with universal and existential quantification defined for it, as well as set comprehension. Disel features a special notation for representing the higher-order Hoare types of program fragments.&lt;/p&gt;

&lt;p&gt;Many elements of a DSL can be implemented using common programming language techniques like polymorphism, inheritance, composition, higher-order functions, and the type system features. This way, Distal implements most of its DSL as ordinary methods and convenience aliases. However, this approach has certain limitations, and such techniques as metaprogramming (macros) or code generation are often required. For instance, in Distal, the key element of the DSL is implemented as a macro; in PSync, automatic derivation of transition relations from the code is also implemented as a macro. Code generation in Mir reduces the amount of hand-written boilerplate code by processing Protobuf definitions annotated with special extensions. Disel and Verdi take advantage of Coq's syntax extension features.&lt;/p&gt;

&lt;p&gt;Clear and convenient notation for defining protocol specifications and their implementation is crucial for ergonomics and expressiveness. Building upon ordinary code, clever use of common programming language techniques, such as polymorphism, inheritance, composition, higher-order functions, and the type system features, should be the preferred approach for achieving notational expressiveness. Such techniques as metaprogramming and code generation can greatly help overcoming the limitations of that approach or further improving the notation, but they can make the framework more complicated and, therefore, should be employed judiciously.&lt;/p&gt;

&lt;h2&gt;
  
  
  Operation
&lt;/h2&gt;

&lt;p&gt;In terms of operation, the core part in most of the frameworks is some kind of runtime or engine that orchestrates the execution of protocol components and their interaction. For concurrent execution of protocol components, the runtimes mostly rely on conventional concurrency mechanisms used in the corresponding language's ecosystem, such as goroutines in Go and execution pools in Java and Scala. Atlas, notably, is based on native OS threads rather than an async Rust runtime like Tokio, presumably due to a performance overhead of the latter.&lt;/p&gt;

&lt;p&gt;There are two main approaches to implementing interaction based on message-passing between protocol components and with the networking layer: using a central event dispatching loop or through explicit channels established between components. Mir is a good example of the former approach, whereas Atlas follows the latter one. Since different protocol components normally operate asynchronously, there is often some kind of event queue or buffer placed between the components to accommodate for the asynchrony.&lt;/p&gt;

&lt;p&gt;This raises an issue of preventing unbounded growth of those queues. Mir addresses this problem by temporarily blocking the influx of external events from active modules when the amount of events buffered in internal queues exceeds certain thresholds. Atlas relies on flow control provided by bounded buffered channels for communication between components.&lt;/p&gt;

&lt;p&gt;In general, garbage collection issue is an important aspect of operation in distributed protocol implementations. Sometimes it can happen automatically, e.g. in PSync, received message sets are automatically discarded by the runtime upon transitioning into a new round. However, in some cases, it requires special care. For example, in Distal, protocol components should explicitly discard automatically buffered messages that become irrelevant for further execution of the protocol, in order to avoid unbounded growth of state and slowing down evaluation of rules. In Mir, there is an interesting pattern for performing garbage collection of internal component's state, whereby each disposable piece of state is assigned a numerical retention index, and the component removes the pieces of state whose retention index is below a specified value upon processing a dedicated garbage collection event emitted by another component.&lt;/p&gt;

&lt;p&gt;Communication between nodes in most of the frameworks is implemented in a simplistic manner, providing best-effort message delivery, following the fire-and-forget communication style. Babel is a notable exception, since it introduces a notion of communication channel abstraction, where different channel types can represent different communication mechanisms with different properties and guarantees, e.g. more reliable message delivery, multiplexing connections, and φ-accrual failure detection.&lt;/p&gt;

&lt;p&gt;So orchestrating the execution and coordinating interaction of protocol components often require some kind of runtime provided by the framework. The runtime should take care of asynchrony, garbage collection, communication, and coordination within the node, preventing unbounded growth of internal state and ensuring good performance.&lt;/p&gt;

&lt;h2&gt;
  
  
  Verification
&lt;/h2&gt;

&lt;p&gt;Not all of the explored frameworks are concerned with verifying correctness of protocols and their implementations. Verification is the primary area of focus for Disel and Verdi, as well as PSync. Verification is not a major concern in Mir, though it provides some mechanisms that can be considered as lightweight verification of protocol implementation correctness.&lt;/p&gt;

&lt;p&gt;Mir includes support for recording, inspecting, modifying, and replaying traces of events being passed by the node engine between the components, which can be very helpful for debugging, but also to perform correctness analysis. Mir also comes with a simple discrete-event simulation runtime that can be used for randomized reproducible testing with simulated time.&lt;/p&gt;

&lt;p&gt;Full-fledged formal verification of protocol specifications and implementation in Disel and Verdi relies on machine-assisted theorem proving, whereas PSync attempts to automate the process. Theorem proving, even if machine-assisted, is a very difficult, time consuming task and requires special expertise. Automated verification, on the other hand, is in general undecidable and can only be achieved with certain restrictions to the system model and the protocol implementation.&lt;/p&gt;

&lt;p&gt;Formal verification requires formal specification of the assumptions and the required properties. In Disel, protocol specifications are defined in terms of state-space coherence predicates and send/receive transitions. In Verdi, the correct behavior of the protocol is specified as a logical predicate over its possible traces of events. Formal specifications in PSync are expressed in terms of protocol properties, expressed in a fragment of a first-order temporal logic, as well as safety and liveness predicates (assumptions), expressed in terms of cardinalities of heard-of sets.&lt;/p&gt;

&lt;p&gt;In these frameworks, the method of formally proving the correctness is typically by induction, constructing inductive state invariants. Coming up with appropriate inductive invariants constitutes the greatest difficulty in the verification effort and requires special skills. &lt;/p&gt;

&lt;p&gt;In PSync, the simple round-based structure with lock-step semantics makes protocol implementation amenable to automated verification that can check safety and liveness properties. The verification, though, requires inductive invariants at the boundaries between rounds. However, the automated verification problem is decidable with certain constraints.&lt;/p&gt;

&lt;p&gt;The correctness of protocol implementation in Verdi is proved directly, whereas Disel employs a different approach. For implementing protocol specification, Disel provides a DSL, embedded shallowly into Coq, that extends Coq's specification language Gallina. Disel programs and their fragments are assigned types corresponding to the protocol specification in higher-order separation-style Hoare logic. For message sending and receiving actions, Disel provides transition wrappers, which lift low-level operations on the networking layer to the level of well-typed program primitives corresponding to the protocol specification. Well-typed programs are guaranteed to be &lt;em&gt;correct by construction&lt;/em&gt; w.r.t. the protocol specifications.&lt;/p&gt;

&lt;p&gt;In Verdi, once the protocol is specified, implemented, and verified in an idealistic reliable network semantics, it can be translated using &lt;em&gt;verified system transformers&lt;/em&gt; into an equivalent implementation, preserving the transformed system properties under a weaker fault model. &lt;/p&gt;

&lt;p&gt;in Disel, protocol specifications can be generic and parameterized. The generic protocol specifications with their proven invariants can be used in composition. Disel provides mechanisms to establish stronger properties of generic protocols and their combinations by elaborating the protocol, i.e. strengthening it with additional inductive invariants.&lt;/p&gt;

&lt;p&gt;Correctness is very important for the critical fault-tolerant protocols; therefore, the verification aspect deserves special attention. There are relatively easy-to-apply lightweight methods, such as randomized reproducible testing with discrete-event simulation, and there are sophisticated formal methods typically requiring special skills and expertise, such as machine-assisted theorem proving. However, some particularly structured system models may enable automated reasoning and make formal verification more practical, though at the cost of additional limitations.&lt;/p&gt;

&lt;h2&gt;
  
  
  Conclusions
&lt;/h2&gt;

&lt;p&gt;Having explored these 7 frameworks for implementing distributed protocols, I found most of them not sufficiently developed for practical use, though some of the ideas and techniques employed there were worth exploring. Being purely academic efforts, most of the frameworks seem to have been abandoned after exploring some ideas and publishing the results. As of time of this writing, Mir is perhaps the most mature, well documented, and up-to-date one among these frameworks.&lt;/p&gt;

&lt;p&gt;Focusing on some particular aspects of implementing distributed protocols, such as unifying and standardizing components, testing and debugging, notational convenience, or formal verification, while mostly neglecting the remaining aspects, may be appropriate for academic research, but this is certainly not sufficient for achieving practical adoption. Moreover, the programming languages that most of the frameworks are based on would make it hard to integrate the protocol implementations directly into larger code bases written in other languages, let alone that having to learn a less commonly used language like Scala or Coq is an additional obstacle for adoption. Please refer to the &lt;a href="https://replica-io.dev/blog/2024/03/04/on-implementation-of-distributed-prtocols" rel="noopener noreferrer"&gt;previous post&lt;/a&gt; about practical aspects of implementing distributed protocols.&lt;/p&gt;

&lt;p&gt;Most important, perhaps, is that all of the frameworks seem to basically adopt the same model of a state transition system and trying to mimic the event-oriented notation as found in typical pseudo-code with &lt;code&gt;upon&lt;/code&gt; statements in the literature on distributed protocols. This largely impacts how protocol implementations are expressed and structured in those frameworks.&lt;/p&gt;

&lt;p&gt;I believe, if we want to make a real breakthrough in &lt;em&gt;both designing and implementing&lt;/em&gt; distributed protocols, which is what the Replica_IO project is about, then we should first of all be innovative, challenging the status quo, and think holistically, taking into account all relevant aspects. Trying to rethink the conventional distributed system model and the way of expressing distributed protocols would be a good start.&lt;/p&gt;

&lt;h2&gt;
  
  
  Next Steps
&lt;/h2&gt;

&lt;p&gt;Having explored some distributed protocol implementations and frameworks for implementing distributed protocols, now it is a good time to clearly state the problems in designing and implementing distributed protocols to focus on for the rest of milestone &lt;a href="https://github.com/replica-io/replica-io/milestone/1" rel="noopener noreferrer"&gt;M0.1&lt;/a&gt; and start gathering ideas on how we could approach them. Apart from that, there are still some potentially related concepts, approaches, and techniques worth looking into as part of the initial state-of-the-art exploration. The exploration tasks are tracked in the scope of &lt;a href="https://github.com/replica-io/replica-io/issues/7" rel="noopener noreferrer"&gt;this issue&lt;/a&gt; on GitHub.&lt;/p&gt;

&lt;p&gt;Once the initial exploratory stage is over, it will be time to come up with key ideas concerning core principles that will guide the process of designing and implementing generic components within the framework (milestone &lt;a href="https://github.com/replica-io/replica-io/milestone/1" rel="noopener noreferrer"&gt;M0.1&lt;/a&gt;). Then those ideas will be developed into clearly formulated concepts (milestone &lt;a href="https://github.com/replica-io/replica-io/milestone/2" rel="noopener noreferrer"&gt;M0.2&lt;/a&gt;), their feasibility will be verified with code (milestone &lt;a href="https://github.com/replica-io/replica-io/milestone/3" rel="noopener noreferrer"&gt;M0.3&lt;/a&gt;). After that, prototype, MVP, and production versions of the framework will be developed and released (milestones &lt;a href="https://github.com/replica-io/replica-io/milestone/4" rel="noopener noreferrer"&gt;M1&lt;/a&gt;, &lt;a href="https://github.com/replica-io/replica-io/milestone/5" rel="noopener noreferrer"&gt;M2&lt;/a&gt;, and &lt;a href="https://github.com/replica-io/replica-io/milestone/6" rel="noopener noreferrer"&gt;M3&lt;/a&gt;).&lt;/p&gt;

&lt;p&gt;It does not mean at all that exploration, ideation, and prototyping will not take place at later stages; the milestones simply define the framework's general level of maturity. The framework will continuously evolve and expand and at some point become a de facto standard for implementing critical fault-tolerant systems providing a growing collection of easy-to-use reliable and efficient distributed replication mechanisms.&lt;/p&gt;

&lt;p&gt;If you like the project and find it valuable, please &lt;a href="https://github.com/sponsors/replica-io" rel="noopener noreferrer"&gt;support&lt;/a&gt; its further development! 🙏&lt;br&gt;
&lt;a href="https://github.com/sponsors/replica-io" class="ltag_cta ltag_cta--branded" rel="noopener noreferrer"&gt;❤️ Replica_IO&lt;/a&gt;
&lt;/p&gt;

&lt;p&gt;If you have any thought you would like to share or any question regarding this post, please add a comment &lt;a href="https://github.com/orgs/replica-io/discussions/43" rel="noopener noreferrer"&gt;here&lt;/a&gt;. You are also welcome to &lt;a href="https://github.com/orgs/replica-io/discussions/new" rel="noopener noreferrer"&gt;start a new discussion&lt;/a&gt; or chime in to &lt;a href="https://discord.replica-io.dev/" rel="noopener noreferrer"&gt;our Discord&lt;/a&gt; server.&lt;/p&gt;




&lt;ol&gt;

&lt;li id="fn1"&gt;
&lt;p&gt;If you know of some other framework for implementing distributed protocols that I should have looked into, please let me know. ↩&lt;/p&gt;
&lt;/li&gt;

&lt;/ol&gt;

</description>
      <category>distributedsystems</category>
      <category>decentralizedcomputing</category>
      <category>faulttolerance</category>
      <category>replication</category>
    </item>
    <item>
      <title>On Implementation of Distributed Protocols</title>
      <dc:creator>Sergey Fedorov</dc:creator>
      <pubDate>Fri, 05 Apr 2024 11:10:27 +0000</pubDate>
      <link>https://dev.to/replica-io/on-implementation-of-distributed-protocols-266c</link>
      <guid>https://dev.to/replica-io/on-implementation-of-distributed-protocols-266c</guid>
      <description>&lt;p&gt;This post concludes the first phase of the &lt;a href="https://github.com/replica-io/replica-io/issues/7"&gt;state-of-the-art exploration&lt;/a&gt; in the scope of milestone &lt;a href="https://github.com/replica-io/replica-io/milestone/1"&gt;M0.1&lt;/a&gt; of the &lt;a href="https://replica-io.dev/"&gt;Replica_IO&lt;/a&gt; project, namely exploration of selected notable distributed protocol implementations. It shares the main conclusions drawn from exploring 14 different code bases and outlines the key areas of focus for the next steps developing the Replica_IO framework.&lt;/p&gt;

&lt;p&gt;&lt;em&gt;The original post can be found &lt;a href="https://replica-io.dev/blog/2024/03/04/on-implementation-of-distributed-prtocols"&gt;here&lt;/a&gt;.&lt;/em&gt;&lt;/p&gt;

&lt;p&gt;A companion video is available on YouTube: &lt;iframe width="710" height="399" src="https://www.youtube.com/embed/Q6wW8NqtpGw"&gt;
&lt;/iframe&gt;
&lt;/p&gt;

&lt;h2&gt;
  
  
  Exploring Distributed Protocol Implementations
&lt;/h2&gt;

&lt;p&gt;I believe that discovering neat, yet practical, solutions to complicated problems demands serious, deliberate preparation. Clearly, before being able to come up with such solutions, one first needs to acquire a deep understanding of the problem, identify the relevant aspects and requirements. It is also important to learn from prior attempts to deal with the problem. Otherwise, it would be naive to expect any significant advancement beyond the status quo.&lt;/p&gt;

&lt;p&gt;Since Replica_IO aims at making a breakthrough in designing and implementing distributed protocols, I decided to start exploring the state of the art by selecting and looking into a number of notable distributed protocol implementations. Although I already had experience implementing such protocols myself, nevertheless, I decided to dive in and see for myself how others had approached this challenge. I wanted to learn from those projects, better understand the typical requirements and difficulties coming up in real-world use cases, and, perhaps, discover some interesting techniques or ideas along the way, as well as to identify the key areas of focus for the next steps.&lt;/p&gt;

&lt;p&gt;So I onboarded myself into one code base after the other, as if I were to work on it. I was focused on the general structure of code, node-to-node communication mechanisms, the implementation details of the core protocols ensuring consistency between nodes, as well as mechanisms for monitoring and controlling execution of the protocol. I tried my best to understand &lt;em&gt;how&lt;/em&gt; those protocols are structured and implemented. After having explored each of the code bases, I summarized and shared some of my findings. You can find those overviews on &lt;a href="https://github.com/replica-io/replica-io/wiki/State-of-the-art-exploration"&gt;this wiki page&lt;/a&gt;.&lt;/p&gt;

&lt;p&gt;Here is the full list of the code bases, written in different programming languages, that I explored&lt;sup id="fnref1"&gt;1&lt;/sup&gt;:&lt;/p&gt;

&lt;ol&gt;
&lt;li&gt;
&lt;a href="https://github.com/tendermint/tendermint"&gt;Tendermint Core&lt;/a&gt; / &lt;a href="https://github.com/cometbft/cometbft"&gt;CometBFT&lt;/a&gt; — a state machine replication engine (written in Go);&lt;/li&gt;
&lt;li&gt;
&lt;a href="https://github.com/etcd-io/raft"&gt;etcd Raft&lt;/a&gt; — a library for maintaining replicated state machines (written in Go);&lt;/li&gt;
&lt;li&gt;
&lt;a href="https://github.com/aptos-labs/aptos-core/tree/aptos-cli-v1.0.13/consensus"&gt;AptosBFT&lt;/a&gt; — a consensus component supporting state machine replication in the Aptos blockchain (written in Rust);&lt;/li&gt;
&lt;li&gt;
&lt;a href="https://github.com/bft-smart/library"&gt;BFT-SMaRt&lt;/a&gt; — a library implementing BFT-SMaRt, a state machine replication system (written in Java);&lt;/li&gt;
&lt;li&gt;
&lt;a href="https://github.com/SmartBFT-Go/consensus"&gt;SmartBFT-Go&lt;/a&gt; — a library implementing state machine replication inspired by BFT-SMaRt (written in Go);&lt;/li&gt;
&lt;li&gt;
&lt;a href="https://github.com/paritytech/substrate"&gt;Substrate&lt;/a&gt; — a framework for building application-specific blockchains (written in Rust);&lt;/li&gt;
&lt;li&gt;
&lt;a href="https://github.com/sigp/lighthouse"&gt;Lighthouse&lt;/a&gt; — an Ethereum consensus client (written in Rust);&lt;/li&gt;
&lt;li&gt;
&lt;a href="https://github.com/algorand/go-algorand"&gt;Algorand&lt;/a&gt; — a blockchain based on the Algorand consensus protocol (written in Go);&lt;/li&gt;
&lt;li&gt;
&lt;a href="https://github.com/ava-labs/avalanchego"&gt;Avalanche&lt;/a&gt; — a blockchain platform based on the Avalanche consensus protocol (written in Go);&lt;/li&gt;
&lt;li&gt;
&lt;a href="https://github.com/dfinity/ic"&gt;Internet Computer blockchain&lt;/a&gt; (ICP) — a general-purpose blockchain system developed by the DFINITY Foundation (written in Rust);&lt;/li&gt;
&lt;li&gt;
&lt;a href="https://github.com/MystenLabs/sui"&gt;Sui&lt;/a&gt; — a smart contract platform based on Narwhal and Bullshark protocols (written in Rust);&lt;/li&gt;
&lt;li&gt;
&lt;a href="https://github.com/apache/zookeeper"&gt;Apache ZooKeeper&lt;/a&gt; — a distributed coordination, synchronization, and configuration service (written in Java);&lt;/li&gt;
&lt;li&gt;
&lt;a href="https://github.com/apache/kafka"&gt;Apache Kafka&lt;/a&gt; — a distributed event streaming platform implementing a variant of the Raft consensus protocol (written in Java, integrated with Scala);&lt;/li&gt;
&lt;li&gt;
&lt;a href="https://github.com/input-output-hk/cardano-node"&gt;Cardano&lt;/a&gt; — a blockchain platform based on the Ouroboros family of consensus protocols (written in Haskell).&lt;/li&gt;
&lt;/ol&gt;

&lt;p&gt;In the subsequent sections, I will share with you some of the observations and conclusions I made while exploring those code bases. I decided to structure the discussion around the following aspects of implementing distributed protocols:&lt;/p&gt;

&lt;ul&gt;
&lt;li&gt;
&lt;em&gt;complexity&lt;/em&gt;: what makes distributed protocols hard to reason about and implement;&lt;/li&gt;
&lt;li&gt;
&lt;em&gt;correctness&lt;/em&gt;: how to ensure that the implementation guarantees the requires properties;&lt;/li&gt;
&lt;li&gt;
&lt;em&gt;resource utilization&lt;/em&gt;: how to prevent ineffective expenditure of limited computing resources;&lt;/li&gt;
&lt;li&gt;
&lt;em&gt;maintainability&lt;/em&gt;: how to manage long-running distributed systems and diagnose issues;&lt;/li&gt;
&lt;li&gt;
&lt;em&gt;flexibility&lt;/em&gt;: how to achieve high adaptability, reusability, and evolvability of code.&lt;/li&gt;
&lt;/ul&gt;

&lt;h2&gt;
  
  
  Complexity
&lt;/h2&gt;

&lt;p&gt;Distributed, fault-tolerant protocols are notoriously hard to implement, and there are justifiable reasons for that. This is primarily because that kind of system consists of largely independent nodes communicating through potentially unstable, unreliable network; some of the nodes may fail in different ways. The protocol is required to tolerate, within a bound, such unfavorable conditions and keep working reliably. More than that, it is supposed to deliver decent performance using limited resources. All this adds a great deal of &lt;em&gt;inherent, essential complexity&lt;/em&gt;, which we simply cannot remove without weakening our requirements.&lt;/p&gt;

&lt;p&gt;However, when it comes to actually designing and implementing these protocols, there is also another kind of complexity: &lt;em&gt;incidental, non-essential complexity&lt;/em&gt;. This kind of complexity, though being closely related, does not strictly belong to the problem. We incidentally introduce it because we are not aware of or fail to recognize a simpler way of solving the problem at hand.&lt;/p&gt;

&lt;p&gt;Incidental complexity can start creeping in when trying to understand and interpret a protocol specification&lt;sup id="fnref2"&gt;2&lt;/sup&gt;, which is often too far from the realities of software engineering. Simply the way a protocol is specified can misguide the engineer trying to implement it and induce all sorts of difficulties. For example, pseudo-code in scientific papers is often defined in terms of global, unstructured variables and omits concurrency issues.&lt;/p&gt;

&lt;p&gt;Implementing a distributed protocol in one of the conventional programming languages, chances are that the implementation will simply employ some general techniques commonly used in that language's ecosystem. Such general techniques may be very powerful and universal, but freely using this unconstrained power and flexibility, we can easily end up with a code base that is very hard to understand and maintain. For example, dealing with concurrency and synchronization using low-level primitives in the implementation of high-level protocol logic clutters the code and multiplies the complexity.&lt;/p&gt;

&lt;p&gt;Haste is another great source of incidental complexity. There is always temptation to cut corners, especially when under time pressure. Imprudently copying approaches from elsewhere, adding temporary workarounds and ad hoc patches makes code entangled and poorly structured.&lt;/p&gt;

&lt;p&gt;Using advanced features and sophisticated techniques can also add unnecessary complexity. Though this is ambivalent because it can actually help to express the implementation more conveniently and simplify the reasoning about it, but only when the advanced machinery is hidden behind a simple, clear, and easy to use interface.&lt;/p&gt;

&lt;p&gt;It is pretty clear that introducing additional complexity is generally bad. But does it really matter? Couldn't we just implement the thing somehow, test it well, and simply tolerate the additional complexity? Well, surely, with rigorous testing, we can be sufficiently confident that our implementation is correct. However, in that case, making a small change, e.g. applying a simple fix to address a major issue discovered later can reportedly&lt;sup id="fnref3"&gt;3&lt;/sup&gt; take months of work. So it would be very hard to further improve, adapt, or reuse such implementation.&lt;/p&gt;

&lt;p&gt;We need a structured, yet flexible enough, approach guiding us away from incidental complexity if we wish to avoid wasted efforts and foster innovation in the field. Let's look into more details concerning complexity in implementation of distributed protocols.&lt;/p&gt;

&lt;h3&gt;
  
  
  Modularity
&lt;/h3&gt;

&lt;p&gt;We can deal with a complex problem, such as implementing a distributed protocol, by dividing it into smaller, simpler problems, solving them individually, and then combining the solutions to finally address the original problem. This is, basically, what modularity is about. In this process, it is crucial how we divide the problem, what kind of pieces we get, and how we combine them back together.&lt;/p&gt;

&lt;h4&gt;
  
  
  Granularity
&lt;/h4&gt;

&lt;p&gt;First of all, modularity comes in different levels of &lt;em&gt;granularity&lt;/em&gt;. Implementing a large component, such as a state machine replication engine, we can define its external dependencies, then split the component into several chunks of functionality and stop there. That is certainly better than having to deal with a complete monolith, but this level of modularity would still be too &lt;em&gt;coarse&lt;/em&gt;. Instead, we can continue decomposing the sub-components further until we end up with reasonably small and simple, yet non-trivial, components; this is &lt;em&gt;fine&lt;/em&gt; modularity.&lt;/p&gt;

&lt;p&gt;All of the explored code bases exhibit some level of modularity. It is quite common to separate concerns by delegating pieces of functionality to external components. This way, most of the code bases clearly separate implementation of the protocol logic from such functionality as communication between nodes, producing and verifying cryptographic signatures, persistent storage, executing transactions on the replicated state, etc. Most of the implementations also separate dispatching of events, such as inbound messages, from their handling; there is typically a component responsible for classifying events and a number of components responsible for handling specific event types. Quite often there are separate components implementing the protocol logic specific to different roles that a node can play, e.g. leader and follower, or modes of operation, e.g. synchronization and normal operation. It is also common to separate different logical stages of the protocol, e.g. creating a proposal, validating a proposal, finalizing the decision. Another common pattern is to have a separate class of component responsible for maintaining state for each of the remote peers the node communicates with.&lt;/p&gt;

&lt;p&gt;Some implementations go further and introduce smaller components, e.g. encapsulating the state of each individual proposal or representing the logic of counting votes and determining if there is a sufficient quorum. Nevertheless, there still remain components that are too complicated and hard to follow, so this modularity cannot be considered fine. To combat complexity, we need to learn how to achieve fine modularity.&lt;/p&gt;

&lt;h4&gt;
  
  
  Decomposition
&lt;/h4&gt;

&lt;p&gt;As one can cut bricks at different angles, so one can decompose components into sub-components in different ways. One way is to focus on the &lt;em&gt;operational&lt;/em&gt; aspects, i.e. on how the pieces of implementation are going to be executed. With this approach, components would be primarily organized around actual data and control flow. This has a profound effect on the structure of the implementation.&lt;/p&gt;

&lt;p&gt;Focusing on the operational aspects, protocol implementations will tend to be represented as stateful components, or as collections of stateful components, reacting to external events. This naturally induces applying the object-oriented approach to structuring the whole implementation, in which the protocol logic is mostly expressed as modifying pieces of component's state in response to &lt;em&gt;individual&lt;/em&gt; inbound events and optionally producing new outbound events.&lt;/p&gt;

&lt;p&gt;Although pieces of functionality tend to imply some state, individual events in a distributed system mostly happen as logical consequences of some other, causally related events in the scope of a larger &lt;em&gt;distributed&lt;/em&gt; process. Thus structuring the implementation around event handling might &lt;em&gt;not&lt;/em&gt; help to clearly express the overall protocol logic.&lt;/p&gt;

&lt;p&gt;The way we approach decomposition also greatly impacts such properties of code as &lt;a href="https://en.wikipedia.org/wiki/Coupling_(computer_programming)"&gt;&lt;em&gt;coupling&lt;/em&gt;&lt;/a&gt; and &lt;a href="https://en.wikipedia.org/wiki/Cohesion_(computer_science)"&gt;&lt;em&gt;cohesion&lt;/em&gt;&lt;/a&gt;, i.e. the degree of interdependence between different components and the strength of relationship between the elements inside components, respectively. Loose coupling and high cohesion are generally desirable.&lt;/p&gt;

&lt;p&gt;Failing to recognize the significance of implicit logical connections and properly express them often causes higher degree of coupling between components, i.e. entanglement. It is particularly important to distinguish essential and incidental complexity here. Sometimes complications, such as &lt;em&gt;circular dependencies&lt;/em&gt;, may occur naturally and represent essential features of the protocol logic, e.g. &lt;em&gt;recursiveness&lt;/em&gt;. For example, some internal events should often be treated, for the most part, the same way as equivalent external events. This can be achieved by looping those events back for handling in the protocol implementation.&lt;/p&gt;

&lt;p&gt;Organizing components in a more structured way helps to manage dependencies between them, e.g. they can be arranged in &lt;em&gt;layers&lt;/em&gt; or &lt;em&gt;hierarchically&lt;/em&gt;, chained together in &lt;em&gt;pipelines&lt;/em&gt;, etc. For example, in the Algorand implementation, the core logic of the consensus protocol is structured as a hierarchical state machine. The layered approach is well exemplified in the  &lt;a href="https://docs.rs/tower/0.4.12/tower/"&gt;&lt;code&gt;tower&lt;/code&gt;&lt;/a&gt; networking library, which is used by the Sui implementation. In the Apache ZooKeeper implementation, client requests are processed using a pipeline of request processing components chained together.&lt;/p&gt;

&lt;p&gt;The amount of mutable internal state maintained by components also matters. Making components more static can often help to simplify the implementation. For example, in the Sui implementation, most of the consensus-specific components are static in terms of consensus configuration, i.e. instead of supporting reconfiguration directly in those components, they are simply recreated upon reconfiguration.&lt;/p&gt;

&lt;p&gt;Many components require certain &lt;em&gt;context&lt;/em&gt; or &lt;em&gt;environment&lt;/em&gt;, i.e. they depend on some common piece of state or functionality like information about prior communication with the remote peer, access to persistent storage, diagnostic logging, etc. This is usually accomplished by capturing references to the environment inside the component or passing it explicitly. In functional programming, one can represent the environment with a &lt;a href="https://en.wikipedia.org/wiki/Monad_(functional_programming)"&gt;monadic&lt;/a&gt; interface. Some programming languages provide special features for that purpose, e.g. &lt;a href="https://docs.scala-lang.org/tour/implicit-parameters.html"&gt;contextual parameters in Scala&lt;/a&gt;. Interacting with the context from withing a component should be convenient but clearly constrained by the component's interface.&lt;/p&gt;

&lt;p&gt;We would like to possibly avoid &lt;em&gt;fragmentation&lt;/em&gt; of the core logic and facilitate &lt;em&gt;local reasoning&lt;/em&gt; so that it is easier to reason about correctness, especially when introducing changes, without being too much concerned about larger scopes. We need to shift the focus more onto the &lt;em&gt;functional&lt;/em&gt; and &lt;em&gt;logical&lt;/em&gt; aspects, i.e. what the pieces of implementation achieve and how they ensure the desired outcome, so that the protocol implementation better reflects causal dependencies and logical connections.&lt;/p&gt;

&lt;h4&gt;
  
  
  Composability
&lt;/h4&gt;

&lt;p&gt;Even a highly modular implementation is not necessarily highly &lt;a href="https://en.wikipedia.org/wiki/Composability"&gt;&lt;em&gt;composable&lt;/em&gt;&lt;/a&gt;, i.e. allowing to easily recombine and reuse its components. It is hard to reuse components that are not composable. Moreover, composability has huge transformative potential: unlocking true power of expressiveness and flexibility, we can push the limits and uncover a new dimension of possibilities for finding better solutions, whether to fix a flaw in an existing implementation or to design and implement something completely new.&lt;/p&gt;

&lt;p&gt;Composability primarily emerges from the properties of individual components and the way they can be combined together. It demands components that are not only loosely coupled, but &lt;em&gt;generic&lt;/em&gt; as well. It also requires &lt;em&gt;unified&lt;/em&gt; means of abstraction and combination that satisfy certain properties, such as &lt;a href="https://en.wikipedia.org/wiki/Closure_(mathematics)"&gt;closure&lt;/a&gt; and &lt;a href="https://en.wikipedia.org/wiki/Associative_property"&gt;associativity&lt;/a&gt;, while preserving principal properties of individual components in combination.&lt;/p&gt;

&lt;p&gt;All of the explored code bases were meant to implement only a specific protocol or a close family of protocols, except Substrate, which is supposed to support a wide range of protocols. Most of the implementations define abstract interfaces for major components, employing various forms of &lt;a href="https://en.wikipedia.org/wiki/Polymorphism_(computer_science)"&gt;polymorphism&lt;/a&gt;, and apply the &lt;a href="https://en.wikipedia.org/wiki/Dependency_inversion_principle"&gt;dependency inversion principle&lt;/a&gt;. This makes components replacable and can help to reduce coupling. Being able to replace a component allows using alternative implementations of the component, e.g. for unit testing. However, most of those dependency inversion interfaces seem to only make sense within a very specific, predefined structure of the whole implementation, i.e. they are mostly about decomposing rather than recomposing. Truly composable components, on the other hand, are those that can be put together in an open-ended range of new, surprising combinations.&lt;/p&gt;

&lt;p&gt;Though there are some examples of composability used in the explored code bases. The communication layer in the Sui implementation takes advantage of the layered design of  &lt;a href="https://github.com/MystenLabs/anemo"&gt;&lt;code&gt;anemo&lt;/code&gt;&lt;/a&gt;, a peer-to-peer networking library based on &lt;a href="https://docs.rs/tower/0.4.12/tower/"&gt;&lt;code&gt;tower&lt;/code&gt;&lt;/a&gt;: it processes RPC requests from other nodes through pipelines composed out of &lt;code&gt;tower&lt;/code&gt; middleware layers provided by the &lt;code&gt;anemo&lt;/code&gt; library. The state machine representing the core logic of the consensus protocol in the Algorand implementation consists of uniformly defined event handlers organized in a hierarchy of event routers dispatching events to the corresponding handler.&lt;/p&gt;

&lt;p&gt;&lt;a href="https://en.wikipedia.org/wiki/Asynchrony_(computer_programming)"&gt;Asynchrony&lt;/a&gt; and &lt;a href="https://en.wikipedia.org/wiki/Concurrency_(computer_science)"&gt;concurrency&lt;/a&gt; make achieving composability particularly challenging. Components implemented using usual concurrent programming techniques based on &lt;a href="https://en.wikipedia.org/wiki/Lock_(computer_science)"&gt;lock-based&lt;/a&gt; synchronization primitives fall short of composability: a simple combination of individually absolutely correct components may easily fail to ensure consistency or cause a deadlock. Ensuring correctness in this model often requires breaking abstractions and dealing with synchronization directly in an awkward and error-prone way. Alternative concurrent programming techniques, such as &lt;a href="https://en.wikipedia.org/wiki/Software_transactional_memory"&gt;software transactional memory&lt;/a&gt; (STM) used in the Cardano implementation, can help to overcome these issues without compromising on modularity and composability. More on asynchrony and concurrency in the next section.&lt;/p&gt;

&lt;p&gt;Functional programming places a significant emphasis on composability. One of its core principles is to break down programs into smaller, reusable functions, avoiding side effects, that can be easily combined to create more complex functionality. This encourages a more &lt;em&gt;declarative notation&lt;/em&gt;, which often results in code that is easier to reason about. The approaches and techniques employed in functional programming, such as &lt;a href="https://en.wikipedia.org/wiki/Immutable_object"&gt;immutability&lt;/a&gt;, &lt;a href="https://en.wikipedia.org/wiki/Lazy_evaluation"&gt;lazy evaluation&lt;/a&gt;, &lt;a href="https://en.wikipedia.org/wiki/Monad_(functional_programming)"&gt;monads&lt;/a&gt; and &lt;a href="https://en.wikipedia.org/wiki/Effect_system"&gt;effect systems&lt;/a&gt;, etc., are therefore a great source of ideas for enhancing composability.&lt;/p&gt;

&lt;p&gt;Composability is indispensable for &lt;em&gt;future-proof&lt;/em&gt; software solutions. Though this property doesn't necessarily emerge together with modularity; conversely, achieving it may be challenging, especially in the inherently concurrent context of distributed systems. Therefore, we should approach this proactively and deliberately design for composability.&lt;/p&gt;

&lt;h3&gt;
  
  
  Concurrency
&lt;/h3&gt;

&lt;p&gt;&lt;a href="https://en.wikipedia.org/wiki/Concurrent_computing"&gt;Concurrent programming&lt;/a&gt; is a way to structure code into multiple &lt;em&gt;threads of control&lt;/em&gt;—concurrent tasks—that can execute concurrently. Observable effects caused by individual tasks can interleave in concurrent execution. Understanding and reasoning about code in concurrent programming requires a more complex mental model compared to sequential programming. Perhaps, &lt;em&gt;nondeterminism&lt;/em&gt; is the main source of complexity in concurrent programming: concurrent programs can produce different results depending on the exact timing of external events and task execution.&lt;/p&gt;

&lt;p&gt;Concurrent programming is known to be error prone. Concurrent tasks accessing shared resources generally require some form of coordination. Depending on the available mechanisms for interaction and communication between concurrent tasks, there may be different methods of coordinating them and controlling concurrency, e.g. &lt;a href="https://en.wikipedia.org/wiki/Lock_(computer_science)"&gt;lock-based synchronization primitives&lt;/a&gt;, &lt;a href="https://en.wikipedia.org/wiki/Message_passing"&gt;message passing&lt;/a&gt;, and &lt;a href="https://en.wikipedia.org/wiki/Software_transactional_memory"&gt;software transactional memory&lt;/a&gt;. However, properly applying those methods in a nontrivial system often becomes complicated and requires great deal of care. When concurrent tasks happen to &lt;em&gt;interfere&lt;/em&gt; with each other in unanticipated ways, subtle issues, such as &lt;a href="https://en.wikipedia.org/wiki/Race_condition#In_software"&gt;race conditions&lt;/a&gt;, &lt;a href="https://en.wikipedia.org/wiki/Deadlock"&gt;deadlocks&lt;/a&gt;, and &lt;a href="https://en.wikipedia.org/wiki/Starvation_(computer_science)"&gt;resource starvation&lt;/a&gt;, may start manifesting themselves.&lt;/p&gt;

&lt;p&gt;Concurrent programs with mutable memory shared between threads can suffer from &lt;a href="https://en.wikipedia.org/wiki/Race_condition#Data_race"&gt;&lt;em&gt;data races&lt;/em&gt;&lt;/a&gt;. A data race is basically a situation where one thread accesses a memory location whereas another thread can simultaneously perform a conflicting write to that memory location. Preventing data races is not only important to avoid memory corruption; this can also significantly simplify the mental model.&lt;/p&gt;

&lt;p&gt;Normally, we can assume &lt;a href="https://en.wikipedia.org/wiki/Sequential_consistency"&gt;sequential consistency&lt;/a&gt; in concurrent programs that are free of data races. In essence, a sequentially consistent execution of a concurrent program must be equivalent to &lt;em&gt;some&lt;/em&gt; &lt;em&gt;sequential&lt;/em&gt; execution, respecting the order and semantics of operations specified in the program. So such executions are linear schedules, each representing a possible concurrent interleaving of the program. &lt;/p&gt;

&lt;p&gt;Execution schedules that only differ in the interleaving of operations local to threads of execution, i.e. operations not visible to other threads or externally, are effectively equivalent. Therefore, the number of possible distinct schedules depends on the number of &lt;em&gt;non-local&lt;/em&gt; operations in the execution, i.e. operations used to communicate between threads or cause externally visible effects, and it grows exponentially.&lt;/p&gt;

&lt;p&gt;Concurrent programming is an effective model of computation, but it is more complex and requires an appropriate approach in order to avoid subtle concurrency issues. Data face freedom is a particularly desired property since it simplifies the model providing sequential consistency. Under that model, reducing the number of non-local operations can greatly help to further simplify reasoning about the concurrent program.&lt;/p&gt;

&lt;h4&gt;
  
  
  Approaches to Concurrency
&lt;/h4&gt;

&lt;p&gt;Programming languages support different approaches to concurrency; they provide different features and different concurrency mechanisms in their runtimes and ecosystems. The explored code bases are written in the following languages: Java, Go, Rust, and Haskell. Let's have a look at how those code bases approach concurrency, depending on the choice of programming language.&lt;/p&gt;

&lt;p&gt;The code bases written in traditional mainstream languages like Java tend to achieve concurrency by explicitly spawning &lt;a href="https://en.wikipedia.org/wiki/Thread_(computing)#Kernel_threads"&gt;&lt;em&gt;OS threads&lt;/em&gt;&lt;/a&gt;, which communicate through &lt;em&gt;shared mutable memory&lt;/em&gt; and synchronize with &lt;a href="https://en.wikipedia.org/wiki/Lock_(computer_science)"&gt;&lt;em&gt;lock-based primitives&lt;/em&gt;&lt;/a&gt;. Those implementations are normally structured into objects exposing thread-safe methods to interact with them concurrently. This approach is well known and established in the industry; it is therefore &lt;em&gt;widely supported&lt;/em&gt; in the ecosystems built around those languages. Newer system programming languages like Rust usually provide support for this approach, as well.&lt;/p&gt;

&lt;p&gt;This low-level approach gives the programmer a &lt;em&gt;high level of control&lt;/em&gt; as it directly reflects how concurrency is actually achieved by the system. On the other hand, it requires a lot of care since properly using low-level synchronization primitives together is tricky and &lt;em&gt;error prone&lt;/em&gt;. Moreover, OS threads are relatively &lt;em&gt;expensive&lt;/em&gt;, and, therefore, building highly concurrent programs by frequently spawning short-living threads on demand is impractical. Instead, programs are often organized into a small number of long-running threads; though using thread pools can help to achieve more flexibility. Most importantly, as mentioned before, concurrent components synchronized with the lock-based primitives suffer from &lt;em&gt;poor composability&lt;/em&gt;.&lt;/p&gt;

&lt;p&gt;The Go language has built-in support for concurrency based on &lt;a href="https://en.wikipedia.org/wiki/Computer_multitasking#Preemptive_multitasking"&gt;preemptive multitasking&lt;/a&gt; with lightweight &lt;a href="https://en.wikipedia.org/wiki/Thread_(computing)#User_threads"&gt;user threads&lt;/a&gt; called &lt;em&gt;goroutines&lt;/em&gt;. It encourages &lt;em&gt;message-passing&lt;/em&gt; style of communication and synchronization between goroutines through blocking, optionally buffered FIFO &lt;em&gt;channels&lt;/em&gt;; though it also supports traditional lock-based synchronization. The built-in &lt;a href="https://go.dev/ref/spec#Select_statements"&gt;&lt;code&gt;select&lt;/code&gt; statement&lt;/a&gt; can be used to combine several channel operations in order to perform a single pseudo-randomly selected operation that is ready to proceed; unless there is a default case, the &lt;code&gt;select&lt;/code&gt; statement blocks until at least one of the operations can proceed. &lt;/p&gt;

&lt;p&gt;The &lt;code&gt;select&lt;/code&gt; statement in Go allows &lt;em&gt;composing&lt;/em&gt; multiple potentially blocking operations on channels into a single operation. For that reason, some of the explored code bases, e.g. SmartBFT-Go, occasionally use Go channels in place of traditional lock-based synchronization primitives in order to combine them with channel operations in a single &lt;code&gt;select&lt;/code&gt; statement. &lt;/p&gt;

&lt;p&gt;Go does not restrict access to &lt;em&gt;shared mutable data&lt;/em&gt; by concurrent goroutines, so &lt;em&gt;data races&lt;/em&gt; are still possible. Go provides quite &lt;em&gt;limited control&lt;/em&gt; over the runtime managing execution of goroutines, thus making fine-tuning and controlling concurrent execution difficult.&lt;/p&gt;

&lt;p&gt;The Rust language emphasizes safety without sacrificing performance. Thanks to the &lt;a href="https://doc.rust-lang.org/book/ch04-00-understanding-ownership.html"&gt;ownership model&lt;/a&gt; and strong type system, it can effectively ensure at compile time that the code is &lt;em&gt;free of data races&lt;/em&gt;. Being a system programming language, Rust supports concurrent programming with OS threads and shared memory, which are useful to optimize performance and for implementing other styles of concurrency, such as message passing. Rust's ownership and type system features prevent accidental sharing of mutable state between threads. &lt;/p&gt;

&lt;p&gt;The explored code bases written in Rust primarily rely on the &lt;a href="https://en.wikipedia.org/wiki/Asynchrony_(computer_programming)"&gt;asynchronous&lt;/a&gt; programming features of Rust to achieve concurrency. Async Rust can be seen as a form of &lt;a href="https://en.wikipedia.org/wiki/Cooperative_multitasking"&gt;cooperative multitasking&lt;/a&gt; where asynchronous, non-blocking computations are represented with the &lt;a href="https://docs.rs/futures/latest/futures/future/trait.Future.html"&gt;&lt;code&gt;Future&lt;/code&gt;&lt;/a&gt; trait (interface). Rust futures are &lt;em&gt;passive&lt;/em&gt;, i.e. they have to be actively driven by &lt;em&gt;polling&lt;/em&gt; in order to make progress. &lt;/p&gt;

&lt;p&gt;Ultimately, asynchronous code in Rust requires some &lt;em&gt;executor&lt;/em&gt; function that can drive a future by polling it to completion. There is an open-ended &lt;em&gt;choice of async runtimes&lt;/em&gt; in the Rust ecosystem, which provide executors. &lt;a href="https://tokio.rs/"&gt;Tokio&lt;/a&gt; is one of the most widely used runtimes in the Rust ecosystem; all of the explored code bases written in Rust are based on it. One can create &lt;em&gt;specialized runtimes&lt;/em&gt;, e.g. Sui has a simulator that provides an drop-in replacement for Tokio and supports deterministic, randomized execution.&lt;/p&gt;

&lt;p&gt;The &lt;a href="https://en.wikipedia.org/wiki/Async/await"&gt;async/await syntax&lt;/a&gt; in Rust helps writing asynchronous fragments of code very close to normal, synchronous code. The &lt;code&gt;async&lt;/code&gt; keyword introduces an &lt;em&gt;async context&lt;/em&gt; by constructing a future from the corresponding piece of code; the &lt;code&gt;await&lt;/code&gt; expression can be used within an async context to poll another future and yield control if that future is not yet ready to produce a value. &lt;/p&gt;

&lt;p&gt;Apart from using the async/await syntax, Rust futures can be &lt;em&gt;composed&lt;/em&gt; together using various combinators provided by the &lt;a href="https://docs.rs/futures/latest/futures/"&gt;&lt;code&gt;futures&lt;/code&gt;&lt;/a&gt;, &lt;a href="https://docs.rs/tokio/latest/tokio/"&gt;&lt;code&gt;tokio&lt;/code&gt;&lt;/a&gt;, and other crates. In particular, the &lt;code&gt;select&lt;/code&gt; macro allows polling multiple futures simultaneously until one of them completes, similar to the &lt;code&gt;select&lt;/code&gt; statement in Go; the &lt;code&gt;join&lt;/code&gt; macro polls multiple futures to completion. There are also asynchronous channels for asynchronously producing a sequence of values and streams for communication between asynchronous tasks. &lt;/p&gt;

&lt;p&gt;Asynchronous Rust is evolving rapidly; thus, it may still lack maturity, has limited documentation and less-established best practices. Many developers find programming in asynchronous Rust quite challenging and sometimes counter-intuitive, e.g. when dealing with cancellation, long-running or blocking operations, and due to the passive nature of futures. Although Rust prevents some concurrency problems like data races, concurrent code is still vulnerable to different types of concurrency bugs (e.g., deadlocks, logic errors, etc.) and requires deep understanding and careful design.&lt;/p&gt;

&lt;p&gt;Finally, concurrency in Haskell is based on lightweight &lt;a href="https://en.wikipedia.org/wiki/Thread_(computing)#User_threads"&gt;user threads&lt;/a&gt;. Haskell allows throwing asynchronous exceptions from one thread to another. Handling asynchronous exceptions safely requires great care in &lt;a href="https://en.wikipedia.org/wiki/Critical_section"&gt;critical sections&lt;/a&gt;, i.e. when manipulating shared resources. Since Haskell is a &lt;a href="https://en.wikipedia.org/wiki/Purely_functional_programming"&gt;purely functional&lt;/a&gt; programming language, it does not explicitly support shared mutable memory for communication between threads. One of the mechanisms for normal communication between Haskell threads is &lt;a href="https://hackage.haskell.org/package/base-4.19.0.0/docs/Control-Concurrent-MVar.html"&gt;&lt;code&gt;MVar&lt;/code&gt;&lt;/a&gt;, a synchronizing variable, which can act as a synchronized container for shared state or as a one-place channel. Concurrent Haskell &lt;em&gt;prevents data races&lt;/em&gt;, but using &lt;code&gt;MVar&lt;/code&gt;s is susceptible to other concurrency bugs, such as race conditions, deadlocks, etc.&lt;/p&gt;

&lt;p&gt;Another mechanism for concurrent communication widely used in the Haskell ecosystem is &lt;a href="https://en.wikipedia.org/wiki/Software_transactional_memory"&gt;Software Transactional Memory&lt;/a&gt; (STM). STM is an &lt;a href="https://en.wikipedia.org/wiki/Optimistic_concurrency_control"&gt;optimistic concurrency&lt;/a&gt; mechanism that allows transactions over shared mutable variables (transactional variables or &lt;a href="https://hackage.haskell.org/package/stm-2.5.2.1/docs/Control-Concurrent-STM-TVar.html"&gt;&lt;code&gt;TVar&lt;/code&gt;&lt;/a&gt;s) to be &lt;em&gt;safely composed&lt;/em&gt; and &lt;a href="https://hackage.haskell.org/package/stm-2.5.2.1/docs/Control-Monad-STM.html#v:atomically"&gt;atomically executed&lt;/a&gt;, without exposing the implementation details. STM transactions can &lt;a href="https://hackage.haskell.org/package/stm-2.5.2.1/docs/Control-Monad-STM.html#v:retry"&gt;block&lt;/a&gt; on an &lt;em&gt;arbitrary&lt;/em&gt; condition; alternative STM transactions can be composed together using the &lt;a href="https://hackage.haskell.org/package/stm-2.5.2.1/docs/Control-Monad-STM.html#v:orElse"&gt;&lt;code&gt;orElse&lt;/code&gt;&lt;/a&gt; combinator. The Haskell type system ensure that STM transactions cannot have undesired side effects and thus are safe to roll back and retry. &lt;/p&gt;

&lt;p&gt;Building various custom concurrency abstractions and combinators with STM is relatively easy and safe, thanks to &lt;em&gt;high composability&lt;/em&gt;. For instance, in Cardano, concurrent components expose STM transactions for retrieving relevant pieces of their mutable current state; the components then interact by combining and atomically executing such STM queries from other components and atomically updating the corresponding pieces of their own mutable state.&lt;sup id="fnref4"&gt;4&lt;/sup&gt;&lt;/p&gt;

&lt;p&gt;However, STM has some limitations and caveats. First of all, &lt;em&gt;composable&lt;/em&gt; &lt;em&gt;multi-way&lt;/em&gt; communication between threads cannot be expressed in STM. That is because STM transactions cannot produce a visible side effect while being blocked. This is closely related to another limitation: STM does not provide &lt;em&gt;fairness&lt;/em&gt; for threads waiting in a blocked STM transaction. In contrast, &lt;code&gt;MVar&lt;/code&gt;s guarantee fair scheduling of threads blocked on the same &lt;code&gt;MVar&lt;/code&gt;. STM also incurs some overhead in terms of memory and performance costs, which depends on the size of transactions. Though sometimes it can actually help building more efficient mechanisms. Long-running STM transactions can suffer from starvation, i.e. being repeatedly rolled-back and retried. Finally, Haskell, similar to Go, provides quite limited control over its runtime.&lt;/p&gt;

&lt;p&gt;To summarize, the traditional mainstream approach to concurrency based on explicit, low-level synchronization primitives and communication directly through shared mutable memory is well known and established, but it is tricky, error prone, and suffers from poor composability. Restricting concurrent access to shared memory, e.g. with the ownership model as in Rust or immutability as in Haskell, can help preventing data races. Communication and synchronization through message passing primitives like channels and using combinators like select can improve composability. Spawning short-lived OS threads may be too expensive; thread pools and lightweight user thread runtimes can help to achieve more flexibility. Though relying on a concurrency runtime is an additional dependency that is not always replacable or adjustable. Another approach to concurrency with good flexibility and composability is asynchronous programming with cooperative multitasking and async/await syntax, as exemplified by Rust. Software transactional memory is a highly composable and flexible approach to concurrency, though it has some restrictions, additional overhead and does not guarantee fairness.&lt;/p&gt;

&lt;h4&gt;
  
  
  Evading Concurrency
&lt;/h4&gt;

&lt;p&gt;Given all the challenges with concurrent programming, why not trying to avoid concurrency as much as possible? Some of the explored code bases go quite far this route and implement almost all of the core protocol logic as a &lt;em&gt;completely sequential state machine&lt;/em&gt;, perhaps only offloading long-running operations (e.g., computationally intensive cryptography) to dedicated concurrent execution pools. Let's consider consequences of this approach.&lt;/p&gt;

&lt;p&gt;First of all, distributed systems are &lt;em&gt;inherently concurrent&lt;/em&gt; because they, by definition, consist of multiple nodes running largely independently. Thus, each node needs to handle events (e.g., messages received over the network or expired timeouts) originating from different sources &lt;em&gt;asynchronously&lt;/em&gt;, i.e. independent of its main program flow and handling of events from other sources. Moreover, the protocol logic must also reflect the concurrent nature of the system.&lt;/p&gt;

&lt;p&gt;So some parts of the protocol are fundamentally sequential, e.g. delivering totally ordered transactions, whereas some parts are fundamentally concurrent, e.g. handling of messages received over the network from different peer nodes. Some parts &lt;em&gt;may&lt;/em&gt; be concurrent, but don't have to, e.g. validation of the subsequent messages while finishing processing of the current one.&lt;/p&gt;

&lt;p&gt;Attempting to implement an essentially concurrent part of the protocol in a sequential manner, i.e. without using concurrent programming techniques, necessarily requires explicitly maintaining and switching contexts. Not only this adds some amount of boilerplate code and makes it entangled, more importantly, this causes &lt;em&gt;fragmentation&lt;/em&gt; of the core protocol logic because such an artificially sequential component still has to multiplex handling of asynchronous events. Therefore, what in concurrent programming could have been naturally expressed as a blocking operation becomes an abrupt return of control, breaking out of the sequential component.&lt;/p&gt;

&lt;p&gt;There is another problem with multiplexed handling of asynchronous events in sequential code, namely controlling the flow of events from concurrent sources. Consider a situation where a sequential component is given an event to handle that it cannot yet fully process because, in order to make a decision on how to react to the event, it first needs to handle some other events, e.g. it has to complete the current round of the protocol before participating in a new one. Since the sequential component cannot block waiting and has to return the control back, there are basically two options: dropping the event or putting it aside into some kind of buffer. In the first case, the event source cannot assume that all events it emits will be reliably handled and has to take this into account in its logic, e.g. emit an equivalent event under some conditions later. In the second case, there should be some way to enforce a reasonable bound on the amount of buffered pending events without compromising the protocol properties, e.g. emitting further events only after having received an acknowledgement from the destination. This can add a lot more complexity to the protocol implementation.&lt;/p&gt;

&lt;p&gt;So concurrency cannot be easily evaded in distributed systems. Attempting to avoid using concurrent programming techniques complicates the implementation and causes fragmentation of the protocol logic in code. On the other hand, when done appropriately, designing for concurrency and using concurrent programming techniques can actually be advantageous. It boils down to recognizing inherently concurrent and sequential parts of the protocol and finding appropriate ways to express this distinction in code. Those parts of the protocol that are neither inherently concurrent nor sequential may nevertheless benefit from being implemented as concurrent: Designing for concurrency can guide towards better decoupling of components while concurrent execution can help to achieve higher responsiveness and performance.&lt;/p&gt;

&lt;h3&gt;
  
  
  Nondeterminism
&lt;/h3&gt;

&lt;p&gt;As mentioned in the previous section, distributed systems are inherently concurrent and therefore nondeterministic. If we think of nondeterminism in terms of events happening in the system then it can manifest itself as unpredictable events or their order. For example, requests from external agents (clients, users, etc.), values produced by a random-number generator, or node failures are not known in advance; the same set of messages may arrive at different nodes in different order due to unpredictable delays in communication; timeouts may happen due to unexpectedly long delays. Inner workings of nodes can introduce additional, implementation-specific nondeterminism, e.g. unspecified order of iteration over unordered collections, scheduling of concurrent tasks, etc. To some extend, the purpose of distributed protocols can be seen as confining nondeterminism within certain constraints in order to maintain the required invariants.&lt;/p&gt;

&lt;p&gt;Nondeterministic steps in protocol execution introduce alternative state transitions, thus expanding the &lt;a href="https://en.wikipedia.org/wiki/State_space_(computer_science)"&gt;&lt;em&gt;state space&lt;/em&gt;&lt;/a&gt;. This complicates reasoning about distributed protocols, as well as implementing and verifying them, because it often requires considering a large number of possible executions. Nondeterministic execution also makes &lt;em&gt;reproducing&lt;/em&gt; problems and debugging particularly challenging. Therefore, it is desirable to control nondeterminism or attempt to eliminate it.&lt;/p&gt;

&lt;p&gt;Some of the explored code bases constrain nondeterminism by implementing parts of the protocol as &lt;em&gt;deterministic&lt;/em&gt; state machines. Inherently nondeterministic aspects, such as time, randomness, and asynchronous operations, are abstracted out of those state machines. Randomness, as well as current time, can be supplied to the state machine through abstract interfaces provided as dependencies. Alternatively, the current timestamp can be supplied to the state machine at each step explicitly in the input. Time can also be represented in terms of an abstract logical clock maintained by the state machine, which is then advanced with special tick events periodically supplied to the state machine. Asynchronous operations can be requested by the state machine by emitting special output events; the result is then supplied back as special input events. This approach is very close to evading concurrency discussed before and therefore is associated with the same kind of disadvantages.&lt;/p&gt;

&lt;p&gt;In Haskell, as a strictly typed purely functional programming language, ordinary functions are deterministic (&lt;a href="https://en.wikipedia.org/wiki/Referential_transparency"&gt;referentially transparent&lt;/a&gt;) in the mathematical sense: given the same input, they must produce the same result. Nondeterministic computations are expressed using the &lt;a href="https://en.wikipedia.org/wiki/Monad_(functional_programming)"&gt;monadic&lt;/a&gt; interface. Only IO actions, when executed in the &lt;a href="https://hackage.haskell.org/package/base-4.19.0.0/docs/GHC-IO.html#t:IO"&gt;IO monad&lt;/a&gt;, can cause side effects and produce nondeterministic results. This is enforced by the type system. Cardano takes advantage of this by making most of its code polymorphic in the main IO-like monad. This allows fully controlling nondeterminism by choosing the main monad implementation.&lt;/p&gt;

&lt;p&gt;Being able to control nondeterminism is particularly useful for testing and debugging. This allows creating &lt;em&gt;reproducible&lt;/em&gt; test environments, as well as &lt;a href="https://en.wikipedia.org/wiki/Discrete-event_simulation"&gt;discrete-event simulation&lt;/a&gt; for faster-than-real-time simulation of time delays. For example, Cardano uses a simulation environment for the IO monad that closely follows core Haskell packages; Sui has a simulator based on &lt;a href="https://github.com/madsim-rs/madsim"&gt;&lt;code&gt;madsim&lt;/code&gt;&lt;/a&gt; that provides an API-compatible replacement for the &lt;a href="https://tokio.rs/"&gt;Tokio&lt;/a&gt; runtime and intercepts various POSIX API calls in order to enforce determinism. Both allow running the same code in production as in the simulator for testing.&lt;/p&gt;

&lt;p&gt;Nondeterminism is an important aspect of distributed systems, so it should be clearly expressed in the implementation. Type system features can help with that. Confining nondeterminism within &lt;em&gt;natural&lt;/em&gt; boundaries of components can reduce complexity and simplify reasoning about the protocol implementation. Simulated execution of unmodified code with controlled nondeterminism is a very effective technique in testing and debugging.&lt;/p&gt;

&lt;h3&gt;
  
  
  Communication
&lt;/h3&gt;

&lt;p&gt;Communication is at the core of distributed systems where individual nodes need to coordinate in order to act as a coherent system. Nodes in a distributed system interact with each other by exchanging &lt;em&gt;peer-to-peer&lt;/em&gt; (P2P) messages. The communication happens over an &lt;em&gt;unreliable&lt;/em&gt; network medium that only provides &lt;em&gt;best-effort, unordered delivery&lt;/em&gt; of data packets, i.e. it may fail to deliver individual packets or deliver them out of order. Moreover, nodes can fail, and, in general, it may be impossible to determine precisely if a peer node has failed or its messages were simply dropped or delayed in the network. Nodes can also differ in processing power and experience different traffic load. Therefore, it is important to manage the rate of data transmission using &lt;a href="https://en.wikipedia.org/wiki/Flow_control_(data)"&gt;&lt;em&gt;flow control&lt;/em&gt;&lt;/a&gt; mechanisms, as well as to retransmit lost pieces of data. This can contribute significantly to the overall complexity of distributed protocols and their implementation.&lt;/p&gt;

&lt;h4&gt;
  
  
  Communication Layers
&lt;/h4&gt;

&lt;p&gt;Most of the explored implementations use SSL/TLS over TCP/IP as a transport layer for P2P communication. Establishing a TCP connection takes a few packet round trips over the network. Moreover, operating systems impose limits on the number of open TCP connections per process because they consume system resources. For those reasons, communication layers based on TCP establish long-lived connections with remote peers and try to keeps the number of open connections low. This often means that the transport-level connections have to be &lt;em&gt;multiplexed&lt;/em&gt; into multiple logical sub-streams.&lt;/p&gt;

&lt;p&gt;Substrate and Lighthouse use &lt;a href="https://libp2p.io/"&gt;&lt;code&gt;libp2p&lt;/code&gt;&lt;/a&gt; as a networking stack for communication between nodes. The &lt;code&gt;libp2p&lt;/code&gt;  framework is a versatile modular peer-to-peer networking stack. It provides a collections of abstractions, mechanisms, and protocols for facilitating communication in P2P systems. In particular, &lt;code&gt;libp2p&lt;/code&gt; supports multiple transport mechanisms (TCP, QUIC, WebSocket, WebTransport, etc.), encryption schemes (TLS and Noise), and stream multiplexing. Higher-level protocols in &lt;code&gt;libp2p&lt;/code&gt; are implemented on top of reliable, ordered, bidirectional binary streams, which are transparently encrypted and multiplexed by the framework.&lt;/p&gt;

&lt;p&gt;Communication layer in Sui is based on &lt;a href="https://github.com/MystenLabs/anemo"&gt;&lt;code&gt;anemo&lt;/code&gt;&lt;/a&gt;, a peer-to-peer networking library built on top of &lt;a href="https://en.wikipedia.org/wiki/QUIC"&gt;QUIC&lt;/a&gt;. QUIC is a modern higher-level network transport protocol layered over UDP. It has built-in support for encryption and multiplexing. Similar to TCP connections, QUIC streams are reliable, ordered, bidirectional, providing flow control (backpressure), but they are cheap and almost instantaneous to open once an initial connection is established. The &lt;code&gt;anemo&lt;/code&gt; library takes advantage of the efficient stream-multiplexing capability of QUIC; &lt;code&gt;libp2p&lt;/code&gt; also uses the built-in capabilities of QUIC when it is used as a transport mechanism.&lt;/p&gt;

&lt;p&gt;So there may be several levels of communication abstractions. There are low-level transport protocols like UDP or TCP, medium-level ones like QUIC, and comprehensive high-level networking stacks like &lt;code&gt;libp2p&lt;/code&gt;. Higher-level mechanisms can be built on top of lower-level layers. Sometimes, it makes sense to fuse several layers, e.g. QUIC efficiently embeds security into the transport layer. In order to simplify implementation of higher-level layers, it is desirable to take advantage of those properties that are already guaranteed by lower-level layers, e.g. reliable, ordered delivery and flow control provided by commonly used transport layers such as TCP and QUIC.&lt;/p&gt;

&lt;h4&gt;
  
  
  Styles of Communication
&lt;/h4&gt;

&lt;p&gt;There are different ways to organize communication between nodes. The most common styles of communication in the explored code bases are &lt;em&gt;request-response&lt;/em&gt; and &lt;em&gt;fire-and-forget&lt;/em&gt; message delivery. The &lt;em&gt;request-response&lt;/em&gt; style follows the remote procedure call (RPC) pattern: the initiator node sends a message to the remote node, and the latter is expected to respond back. In the fire-and-forget style, the initiator node unidirectionally sends messages to the remote node without waiting for a response. Another style of communication, which is also often used in the explored implementations, is &lt;em&gt;gossiping&lt;/em&gt;, where nodes publish and disseminate pieces of information among themselves in an indirect and random manner. Cardano uses a &lt;em&gt;session-based&lt;/em&gt; style of communication, where peers establish continuous bidirectional communication channels and exchange messages according to some stateful communication protocol.&lt;/p&gt;

&lt;p&gt;The &lt;em&gt;fire-and-forget&lt;/em&gt; message delivery is a very simple style of communication. It does not mandate any acknowledgement from the remote node, so it can only provide best-effort delivery guarantee. Messages that cannot be handled for any reason are often simply dropped, e.g. when a message queue is full. Usually, there is also no guarantee about ordering of messages. Higher-level code needs to take care of such things as flow control, retransmission of lost messages, as well as determining and maintaining the context to handle messages in. On the other hand, this style can be expressed with a non-blocking interface. That allows sending a message to a group of remote nodes at once, which is a simple form of best-effort multi-/broadcasting. Some implementations provide a blocking or asynchronous variant of the interface giving more control over data flow within the local node. For example, in Substrate, the sender should wait until it acquires a free slot in the outgoing message buffer; the slot reservation is then consumed to enqueue a message.&lt;/p&gt;

&lt;p&gt;The &lt;em&gt;request-response&lt;/em&gt; style is a simple type of session-based communication: sending a request initiates a new session, which normally terminates with reception of the corresponding response. Sessions can terminate abnormally, e.g. upon a timeout. The request-response style demands blocking or asynchronous interface on the sender side since it should wait for and handle the eventual response or error. This provides a context for response messages linking them to the corresponding requests. However, the communication layer treats each individual session independently. More complex patterns of interaction have to be split into a number of one-shot request-response sessions. Multiple sessions may be initiated concurrently, and the communication layer needs to keep track of those one-shot sessions starting, running, and finishing concurrently.&lt;/p&gt;

&lt;p&gt;The &lt;em&gt;session-based&lt;/em&gt; style of communication is connection-oriented and supports &lt;em&gt;stateful&lt;/em&gt; interaction between nodes. Communication sessions are established between individual nodes and represent reliable, ordered, bidirectional message streams. This provides a context for the messages being exchanged between nodes and implies blocking or asynchronous interface. Thanks to reliable and ordered delivery, the context establishes causal relationship between individual messages. Relying on those assumptions can greatly simplify the protocol implementation while taking advantage of the guarantees commonly provided by stream-based transport layers. This style of communication is quite generic and can express many different patterns of interaction. Combined with built-in flow control (backpressure), it is particularly suited for implementing &lt;em&gt;consumer-driven&lt;/em&gt; communication. On the other hand, session-based communication cannot directly express multi-/broadcasting primitives and can induce additional latency in certain patterns of interaction. Though higher-level communication mechanisms built on top of session-based communication can implement multi-/broadcasting, whereas using &lt;a href="https://en.wikipedia.org/wiki/Protocol_pipelining"&gt;pipelining&lt;/a&gt; techniques can help to hide latency and achieve good performance.&lt;/p&gt;

&lt;p&gt;The &lt;em&gt;gossip-style&lt;/em&gt; communication designates probabilistic broadcasting in a relay network of nodes. It resembles the best-effort broadcasting in the fire-and-forget message delivery style. The key difference is that data in the gossip-style communication can propagate from one node to another in multiple hops rather than being received directly from the source node. This makes it suitable for sparsely connected networks. Therefore, gossip communication can scale well in large networks. It can provide, with high probability, eventual delivery of bounded amount of data under normal network conditions. This style of communication implies a publish-subscribe interface. Similar to the fire-and-forget message delivery, the interface is largely stateless and can be non-blocking. Under the hood, it is often implemented using the advertise-request-response pattern of communication: nodes advertise available pieces of data to their neighbors and exchange with them the missing parts following the request-response pattern. Efficient gossip implementations require adaptive network topology and advanced data dissemination techniques, which can make them fairly complicated.&lt;/p&gt;

&lt;p&gt;An interesting example of using the gossip-style communication is artifact pools in the Internet Computer blockchain. Artifact pools in ICP are structured collections of artifacts, generic pieces of data produced by the local replica or received from other nodes. The gossip layer is responsible for synchronizing artifact pools between nodes. Nodes communicate with each other through the artifact pools by adding/removing/moving artifacts to/from/between pool sections. Higher-level code is responsible for artifact validation; it also determines retention and prioritization policies.&lt;/p&gt;

&lt;p&gt;It is easy to notice that some styles of communication can be implemented in terms of others. So the request-response style is a reduced from of the session-based communication, which is more generic and expressive. Both can be implemented relying on the fire-and-forget delivery and using some message retransmission and acknowledgement protocol. Or conversely, the fire-and-forget message delivery can be implemented on top of a reliable session-based communication using bounded lossy message queues. Similarly, gossip mechanisms can be implemented using any of the other styles of communication; though the implementations may differ in complexity.&lt;/p&gt;

&lt;p&gt;Different styles of communication have different properties that can significantly influence the shape of code built around them. Some of them are strictly more expressive than others, but do not necessarily reduce to an equivalent, because less expressive mechanisms may have more efficient implementations. In order to avoid accidental complexity when implementing distributed protocols, it is important to have a range of communication mechanisms with aligned interfaces and clearly defined properties.&lt;/p&gt;

&lt;h4&gt;
  
  
  Internal Communication
&lt;/h4&gt;

&lt;p&gt;Apart from interaction between nodes, there is also communication between concurrent tasks within the same node. This internal communication shares some similarity with communication between nodes. The main difference is in the communication medium: while different nodes communicate through unreliable and slow network, internal communication happens through fast and reliable shared memory. Some programming models and techniques make the similarity particularly prominent, e.g. the &lt;a href="https://en.wikipedia.org/wiki/Actor_model"&gt;actor model&lt;/a&gt;, &lt;a href="https://en.wikipedia.org/wiki/Communicating_sequential_processes"&gt;communicating sequential processes&lt;/a&gt; (CSP), &lt;a href="https://en.wikipedia.org/wiki/Remote_procedure_call"&gt;remote procedure calls&lt;/a&gt; (RPC), etc.&lt;/p&gt;

&lt;p&gt;Any piece of shared memory can act as a communication channel between internal components. Such a channel can be established by simply sharing a reference to the corresponding piece of memory. Internal messages do not need translation into/from a binary representation; they can be simply shared by reference. The request-response style of communication can be implemented as simple invocation of blocking or asynchronous procedures (functions); invoking non-blocking procedures (functions) without a return value corresponds to the fire-and-forget message delivery style. Obviously, such procedures need to be safe for concurrent invocation. &lt;/p&gt;

&lt;p&gt;The session-based communication style can be implemented for internal communication using the constructs commonly known as &lt;a href="https://en.wikipedia.org/wiki/Channel_(programming)"&gt;&lt;em&gt;channels&lt;/em&gt;&lt;/a&gt; (e.g. &lt;a href="https://go.dev/ref/spec#Channel_types"&gt;channels&lt;/a&gt; in Go, &lt;a href="https://docs.rs/tokio/latest/tokio/sync/index.html#message-passing"&gt;Tokio channels&lt;/a&gt; in Rust) or concurrent &lt;em&gt;queues&lt;/em&gt; (e.g. &lt;a href="https://docs.oracle.com/javase/8/docs/api/java/util/concurrent/LinkedBlockingQueue.html"&gt;&lt;code&gt;LinkedBlockingQueue&lt;/code&gt;&lt;/a&gt; and other concurrent &lt;a href="https://docs.oracle.com/javase/8/docs/api/java/util/Queue.html"&gt;queues&lt;/a&gt; in Java). Those constructs belong to fundamental mechanisms of &lt;em&gt;communication and coordination&lt;/em&gt; between concurrent components. Channels can be &lt;em&gt;buffered&lt;/em&gt; or &lt;em&gt;unbuffered&lt;/em&gt; (i.e. not buffered). Buffered channels and queues can hold items being sent through them without blocking the sender. In contrast, sending to or receiving from an unbuffered channel acts as a rendezvous point: it synchronizes the sender and the receiver at the point of communication.&lt;/p&gt;

&lt;p&gt;Buffered channels and queues that can hold more than a singe item may return items to a receiver in different order. FIFO is the most commonly used ordering policy, in which items are returned in the same order as they were inserted. LIFO is another option, in which the most recently inserted item is the one that is returned first. One can think of many other options such as priority queues etc. The preferred ordering policy would depend on the purpose of communication.&lt;/p&gt;

&lt;p&gt;Buffered channels and queues can be &lt;em&gt;bounded&lt;/em&gt; or &lt;em&gt;unbounded&lt;/em&gt;. The bounded version imposes a hard limit on the amount of items that they can hold. Unbounded channels and queues usually provide a simple &lt;em&gt;non-blocking&lt;/em&gt; interface for inserting new items. However, they require some additional mechanism to prevent accumulating indefinite amount of items, e.g. blocking ingress of external events when internal buffers grow above certain threshold or relying on time-based assumptions such as throttling the data flow or imposing expiration time on the items. Such mechanisms can make reasoning about the protocol implementation more complicated.&lt;/p&gt;

&lt;p&gt;Bounded channels and queues usually provide blocking or asynchronous interface. They can also support non-blocking insertion of new items, but then they must discard some items when there is no more capacity left. There may be different eviction policies. The simplest one is to discard the item being inserted. Otherwise, the new item is inserted, but some of the buffered items must be discarded, e.g. the least recently inserted one. Similarly to the ordering policy, there may be many other options, and the choice depends on the purpose of communication.&lt;/p&gt;

&lt;p&gt;It is also worth mentioning buffered channels with a single-item buffer. They can be convenient for communicating a single item from one concurrent component to another, e.g. sending a response message back to the requester. The &lt;a href="https://docs.rs/tokio/latest/tokio/sync/oneshot/index.html"&gt;&lt;code&gt;oneshot&lt;/code&gt;&lt;/a&gt; channel in Tokio is a good example of such channel type. &lt;a href="https://docs.oracle.com/javase/8/docs/api/java/util/concurrent/CompletableFuture.html"&gt;&lt;code&gt;CompletableFuture&lt;/code&gt;&lt;/a&gt; in Java can also be considered a kind of single-item buffered channel, as well as synchronizing variables &lt;a href="https://hackage.haskell.org/package/base-4.19.0.0/docs/Control-Concurrent-MVar.html"&gt;&lt;code&gt;MVar&lt;/code&gt;&lt;/a&gt; and &lt;a href="https://hackage.haskell.org/package/stm-2.5.2.1/docs/Control-Concurrent-STM-TMVar.html"&gt;&lt;code&gt;TMVar&lt;/code&gt;&lt;/a&gt; in Haskell. Another interesting example of a single-item buffered channel is the &lt;a href="https://docs.rs/tokio/latest/tokio/sync/watch/index.html"&gt;&lt;code&gt;watch&lt;/code&gt;&lt;/a&gt; channel in Tokio: it always keeps the last value sent to it. The &lt;code&gt;watch&lt;/code&gt; channel is useful for watching for changes to a value from multiple concurrent components. Transactional variables (&lt;a href="https://hackage.haskell.org/package/stm-2.5.3.0/docs/Control-Concurrent-STM-TVar.html"&gt;&lt;code&gt;TVar&lt;/code&gt;&lt;/a&gt;s) in Haskell are somewhat similar to watch channels since STM transactions can be suspended until one of the &lt;a href="https://hackage.haskell.org/package/stm-2.5.2.1/docs/Control-Concurrent-STM-TVar.html"&gt;&lt;code&gt;TVar&lt;/code&gt;&lt;/a&gt;s that it has read from has been updated.&lt;/p&gt;

&lt;p&gt;Channels and queues often serve as fundamental constructs to implement &lt;a href="https://en.wikipedia.org/wiki/Message_passing"&gt;message passing&lt;/a&gt; between concurrent components. They can be used to implement various styles of internal communication and higher-level components. For example, implementations of components for communication between nodes often use channels and queues as internal message buffers.&lt;/p&gt;

&lt;p&gt;The &lt;a href="https://en.wikipedia.org/wiki/Publish%E2%80%93subscribe_pattern"&gt;publish-subscribe&lt;/a&gt; design pattern resembles the gossip style of communication. It can be implemented for internal communication as an event bus or broadcast channel. Same as channels and queues, it can be buffered or unbuffered, bounded or unbounded. Unless messages can be dropped, unbuffered and bounded buffered implementations only support non-blocking publishing/broadcasting of messages if no subscriber blocks.&lt;/p&gt;

&lt;p&gt;Similar to communication between nodes, different mechanisms and styles of internal communication have different properties that can significantly influence the shape of code. Therefore, it is equally important to have a range of internal communication mechanisms with aligned interfaces and clearly defined properties. The similarity between mechanisms for internal communication and communication between nodes provides an interesting perspective and can help to come up with better abstractions for communication.&lt;/p&gt;

&lt;h3&gt;
  
  
  Resilience
&lt;/h3&gt;

&lt;p&gt;&lt;em&gt;Fault-tolerant&lt;/em&gt; distributed systems are meant to tolerate (within limits) faults of individual nodes due to crashes, network partitioning, malfunctioning, or even malicious behavior. Crash fault tolerant (CFT) systems, e.g. Apache Kafka and Apache Zookeeper, are relatively simple since they can only withstand node crashes and network partitioning. Byzantine fault tolerant (BFT) systems, e.g. public blockchains, are designed to withstand arbitrary (including malicious) behavior of a fraction of nodes and thus are significantly more complicated. There are two sides of the issue: preventing faulty or malicious nodes from compromising the whole system and recovering failed nodes to rejoin the system.&lt;/p&gt;

&lt;p&gt;Theoretically, fault-tolerant distributed protocols are designed so that they guarantee their safely and liveness properties despite the presence of faulty nodes in the system, provided that certain assumptions hold. In practice, those guarantees are only provided if the implementation ensures that the required assumptions actually hold. This is particularly challenging in BFT systems meant to operate in adversarial environments. Nodes in such systems can be subjects to various attacks, such as denial-of-service (DoS) attacks through resource exhaustion. &lt;em&gt;Fairness&lt;/em&gt; between peers is another concern since it may also impact resilience.&lt;/p&gt;

&lt;p&gt;To mitigate those risks, many implementations maintain &lt;em&gt;reputation&lt;/em&gt; metrics for remote peers and apply &lt;em&gt;rate-limiting&lt;/em&gt; or &lt;em&gt;throttling&lt;/em&gt; techniques. Peer reputation is based on the observable behavior of the peer, such as protocol violations, timeouts, and performance. Nodes normally disconnect from remote peers whose reputation drops below a certain threshold, as well as reject inbound connections from those peers. Conversely, peers with higher reputation may be preferred for communication in sparsely connected systems.&lt;/p&gt;

&lt;p&gt;In its threat-aware design approach, Cardano emphasizes &lt;em&gt;detecting protocol violations as early as possible&lt;/em&gt; in the operational cycle where the data is available but the least resources have been expended to process the received data&lt;sup id="fnref5"&gt;5&lt;/sup&gt;. For instance, block and transaction relaying is interleaved with validation to avoid circulating invalid data in the system. This approach works well with &lt;em&gt;stateful&lt;/em&gt; &lt;em&gt;consumer-driven&lt;/em&gt; communication between nodes: Inbound messages must be well-formed syntactically and semantically valid in the context of information previously received from the peer node.&lt;/p&gt;

&lt;p&gt;In order to allow failed nodes to efficiently restore and safely rejoin the system, some parts of the protocol state can be persisted in a stable storage. This is usually implemented as a &lt;a href="https://en.wikipedia.org/wiki/Write-ahead_logging"&gt;write-ahead log&lt;/a&gt; (WAL), an append-only stable storage used for crash recovery. Certain events are first recorded in the log before the corresponding actions are taken, e.g. before sending messages to other nodes. This allows the node to restore and continue participating in the protocol from where it stopped, without violating the protocol. Persistence mechanisms are also required to support recovery from a massive system crash, i.e. to provide the &lt;a href="https://en.wikipedia.org/wiki/Durability_(database_systems)"&gt;durability&lt;/a&gt; property.&lt;/p&gt;

&lt;p&gt;Early detection of protocol violations is advantageous, and the implementation structure should allow that. There should be a clear path for propagating information about detected protocol violations and other anomalies to adjust peer reputation metrics and take appropriate measures. Persistence mechanisms, such as write-ahead logging, are required for durability, as well as for safe and efficient node recovery.&lt;/p&gt;

&lt;h3&gt;
  
  
  Optimization
&lt;/h3&gt;

&lt;p&gt;Practical distributed systems require not only reliability but also efficiency. Simplistic designs and implementations unfortunately tend to exhibit poor performance, whereas we would like that our systems scale well and provide decent &lt;em&gt;throughput&lt;/em&gt; and &lt;em&gt;latency&lt;/em&gt;. Improving those characteristics demands optimization at protocol and implementation levels. Great effort has been put into optimizing distributed protocols during decades of active research. This gave rise to a range of elaborate protocols attempting to achieve ever higher performance. On the implementation level, there also exists a variety of technical means for increasing efficiency. Optimizations, however, often add more complexity and make protocols harder to reason about and implement.&lt;/p&gt;

&lt;p&gt;Protocol-level optimizations may involve using more complex communication patterns and topologies. Protocol phase &lt;em&gt;pipelining&lt;/em&gt;, i.e. participating with a single message in multiple protocol phases at once, and &lt;em&gt;speculative execution&lt;/em&gt; are common techniques to improve responsiveness. &lt;em&gt;Batching&lt;/em&gt;, as well as advanced cryptography such as &lt;a href="https://en.wikipedia.org/wiki/Threshold_cryptosystem"&gt;threshold signatures&lt;/a&gt;, helps to reduce communication overhead. State-of-the-art protocols are often based on &lt;em&gt;advanced data structures&lt;/em&gt;, such as &lt;a href="https://en.wikipedia.org/wiki/Directed_acyclic_graph"&gt;directed acyclic graphs&lt;/a&gt; (DAGs). At the implementation level, &lt;em&gt;on-demand execution&lt;/em&gt; and &lt;em&gt;caching&lt;/em&gt; are often used to avoid performing unnecessary or duplicate operations.&lt;/p&gt;

&lt;p&gt;Communication contributes significantly to the overall overhead in distributed systems and, therefore, is a clear target for optimization. Point-to-point &lt;a href="https://en.wikipedia.org/wiki/Protocol_pipelining"&gt;protocol &lt;em&gt;pipelining&lt;/em&gt;&lt;/a&gt;, i.e. continuous sending of requests without waiting for the corresponding responses, can greatly increase performance by hiding high network latency. Widely used transport protocols, such as TCP, tend to perform best under &lt;em&gt;steady data flow&lt;/em&gt;. Moreover, keeping multiple network connections consumes additional system resources. Therefore, implementations commonly &lt;em&gt;multiplex&lt;/em&gt; multiple logical communication streams through a single network connection. Minimizing &lt;a href="https://en.wikipedia.org/wiki/Head-of-line_blocking"&gt;&lt;em&gt;head-of-line blocking&lt;/em&gt;&lt;/a&gt; effects may require &lt;em&gt;flow control&lt;/em&gt; mechanisms at the level of individual logical streams; large pieces of data should be transmitted through a multiplexed connection &lt;em&gt;in chunks&lt;/em&gt;. Specific kinds of communication, e.g. state synchronization in blockchain systems, can benefit from dedicated, specialized communication mechanisms.&lt;/p&gt;

&lt;p&gt;Interaction between concurrent components and across levels of abstraction is also subject to fine-tuning and optimization. &lt;em&gt;Prioritization&lt;/em&gt; and flexible &lt;em&gt;policies&lt;/em&gt; can help to maximize performance. For example, the system may perform better when certain concurrent tasks or communication paths have higher priority. Internal communication, as well as communication between nodes, may be optimized through prioritization and retention policies applied to individual messages or kinds of messages. This sort of optimization requires deep understanding of the protocol and its  inner workings.&lt;/p&gt;

&lt;p&gt;Expensive low-level operations, such as spawning threads, blocking on locks, and copying data, can become a hidden cause of suboptimal performance. There are well-known techniques that can help to avoid unnecessary low-level overhead. For example, &lt;a href="https://en.wikipedia.org/wiki/Thread_pool"&gt;&lt;em&gt;execution pools&lt;/em&gt;&lt;/a&gt; avoid the overhead associated with creation and destruction of threads for executing short-lived concurrent tasks; &lt;a href="https://en.wikipedia.org/wiki/Non-blocking_algorithm"&gt;&lt;em&gt;non-blocking algorithms&lt;/em&gt;&lt;/a&gt; can improve performance by avoiding unnecessary suspension of thread execution; &lt;a href="https://en.wikipedia.org/wiki/Zero-copy"&gt;&lt;em&gt;zero-copy&lt;/em&gt;&lt;/a&gt; techniques focus on eliminating excessive copying of data.&lt;/p&gt;

&lt;p&gt;Improving performance characteristics of distributed systems may require nontrivial changes in the underlying protocols and their implementations. The structure of the code should be flexible enough to support such changes. Some optimizations can be confined within boundaries of abstract components, whereas some may require crossing the borders of modularity. &lt;em&gt;Flexible&lt;/em&gt; and &lt;em&gt;composable&lt;/em&gt; primitives and interfaces &lt;em&gt;designed for optimization&lt;/em&gt; would help to fully realize the potential of distributed systems in practice.&lt;/p&gt;

&lt;h2&gt;
  
  
  Correctness
&lt;/h2&gt;

&lt;p&gt;Correctness is absolutely essential for implementation of distributed fault-tolerant protocols since they are critical for ensuring reliability of the whole system. &lt;a href="https://en.wikipedia.org/wiki/Formal_verification"&gt;&lt;em&gt;Formal verification&lt;/em&gt;&lt;/a&gt; methods allow confirming protocol correctness in terms of desired properties. Applying those methods requires that the protocol is described precisely with a &lt;a href="https://en.wikipedia.org/wiki/Formal_specification"&gt;&lt;em&gt;formal specification&lt;/em&gt;&lt;/a&gt;. Though the way protocols are actually implemented in code tends to be significantly different from the notation used in protocol specifications. This discrepancy is clearly a potential source of errors. There are different methods that can help to acquire higher confidence in correctness of the protocol implementation.&lt;/p&gt;

&lt;p&gt;Testing is an established practice to examine correctness of software. Comprehensive testing of complex systems happens at different levels, and modularity of the code supports more effective testing by isolating functionalities, enabling independent unit testing, simplifying integration testing, and promoting code reuse. Some code bases include &lt;em&gt;dedicated interfaces&lt;/em&gt; and &lt;em&gt;hooks&lt;/em&gt; to facilitate testing; &lt;a href="https://man.freebsd.org/cgi/man.cgi?query=fail"&gt;&lt;em&gt;fail points&lt;/em&gt;&lt;/a&gt; is a technique that allows injecting errors and other behavior at runtime for testing purposes, which is used in Aptos and Sui. In Algorand, each component of the hierarchical state machine implementing the consensus protocol can perform &lt;em&gt;pre- and post-condition checks&lt;/em&gt; to validate if it conforms to its contract. Most code bases perform diagnostic &lt;em&gt;logging&lt;/em&gt; or &lt;em&gt;tracing&lt;/em&gt; that can also be useful for testing, e.g. to check invariants in property-based testing.&lt;/p&gt;

&lt;p&gt;&lt;em&gt;Deterministic &lt;a href="https://en.wikipedia.org/wiki/Discrete-event_simulation"&gt;discrete-event simulation&lt;/a&gt;&lt;/em&gt; is a powerful technique that can be used for performing &lt;em&gt;randomized&lt;/em&gt; but &lt;em&gt;reproducible&lt;/em&gt; testing. For example, Sui, Apache Kafka, and Cardano employ this technique. It works by running the code within a special runtime that supports deterministic, randomized execution of concurrent code, as well as faster-than-real-time simulation of time delays. This technique can be used to run an entire network in a single process, with &lt;em&gt;simulated network&lt;/em&gt; latency and packet loss. To ensure deterministic execution, the simulation approach usually requires that the code is generic over the sources of local time and randomness; it can also rely on code instrumentation techniques. The key advantage of this approach is that it allows running precisely the same code in the simulator for testing as in production.&lt;/p&gt;

&lt;p&gt;Certain correctness properties of code can be ensured statically, i.e. at compile time. Those checks rely on the programming language's type system. Software engineers can take advantage of &lt;em&gt;type safety&lt;/em&gt; features to implement components in a way that makes them &lt;em&gt;safe by construction&lt;/em&gt;. For example, Cardano uses the &lt;a href="https://github.com/input-output-hk/typed-protocols/tree/typed-protocols-0.1.0.5"&gt;&lt;code&gt;typed-protocols&lt;/code&gt;&lt;/a&gt; package, a generic framework for implementing application-level protocols, which is based on a simple form of &lt;a href="https://en.wikipedia.org/wiki/Session_type"&gt;session typing&lt;/a&gt;.&lt;sup id="fnref6"&gt;6&lt;/sup&gt; Within this framework, protocols are described as state machines encoded into Haskell types. The allowed transitions between states correspond to messages exchanged between the peers, so the protocol state determines which messages are allowed to be sent or must be accepted when received, at type level. This simplifies protocol implementation, allows early detection of protocol violations, and makes the protocols themselves deadlock-free by construction. More advanced type-level programming techniques may allow achieving impressive levels of type safety; however, such code may be significantly harder to implement, understand, and maintain.&lt;/p&gt;

&lt;p&gt;Ensuring correctness in distributed systems is a complex task. Protocols and their properties can be formally specified and verified. Expressing the protocol specification and its implementation using possibly similar notations could help to ensure equivalence between the two. Modular and generic structure of code, as well as using various testing support features within the code base, support more effective testing. Supporting deterministic discrete-event simulation is particularly powerful for reproducible randomized testing. Finally, type safety techniques like session types and typestates can eliminate certain kinds of programming errors at compile time.&lt;/p&gt;

&lt;h2&gt;
  
  
  Resource Utilization
&lt;/h2&gt;

&lt;p&gt;Real computing systems are fundamentally bounded in the amount of available resources. Computers operate with limited computational power, memory, storage, and network bandwidth. Operating systems impose further limits on such system resources as threads, open network connections, file handles, etc. Practical systems are required to prevent &lt;a href="https://en.wikipedia.org/wiki/Resource_leak"&gt;resource leaks&lt;/a&gt;, as well as to ensure fair and efficient utilization of available resources.&lt;/p&gt;

&lt;p&gt;Some resources, such as allocated memory, open file handles and network connections, spawned concurrent tasks and threads, may require explicit actions to release them properly when they are no longer needed. Failing to release resources promptly is known as a resource leak. It can cause &lt;a href="https://en.wikipedia.org/wiki/Resource_starvation"&gt;resource starvation&lt;/a&gt;, slowdowns, and instability in the system. Relying on explicit releasing of acquired resources is known to be error-prone. Automatically releasing resources based on &lt;em&gt;lifetimes&lt;/em&gt; and &lt;em&gt;lexical scopes&lt;/em&gt; is a more robust form of &lt;a href="https://en.wikipedia.org/wiki/Resource_management_(computing)"&gt;resource management&lt;/a&gt;. Sometimes the encompassing lexical scope's lifetime is longer than the resource's natural life cycle, e.g. when managing concurrent tasks, so that strict lexical scoping becomes inappropriate. In such cases, resources may be managed more explicitly within the scope, but with a fallback mechanism to track resources and ensure that any remaining resource gets released when leaving the scope.&lt;sup id="fnref7"&gt;7&lt;/sup&gt;&lt;/p&gt;

&lt;p&gt;Concurrency often makes resource management more challenging. First of all, concurrent tasks running in background is a kind of resource that needs to be released when no longer needed. Moreover, they can acquire other resources that should be released when the task is terminated, even in case of asynchronous cancellation. In simple cases, there is a limited number of long-running concurrent tasks, which are responsible for releasing the resources acquired by them, and their termination is synchronized with the main task; short-living jobs can run concurrently on execution pools that distribute those jobs among a number of long-running concurrent tasks. When more flexibility is desired, &lt;a href="https://en.wikipedia.org/wiki/Structured_concurrency"&gt;&lt;em&gt;structured concurrency&lt;/em&gt;&lt;/a&gt; can help managing concurrent code in a more organized and predictable manner by organizing concurrent tasks into a structured hierarchy with well-defined scopes and lifetimes.&lt;sup id="fnref8"&gt;8&lt;/sup&gt;&lt;/p&gt;

&lt;p&gt;Individual parts of a distributed system may operate at different pace. Moreover, for performance reasons, it is common to apply pipelining techniques when communicating with remote nodes, i.e. proceed without waiting for a response or acknowledgement form the remote node in order to hide network latency. Compensating for the delays and variability in throughput demands some kind of explicit or implicit buffering, e.g. buffered channels, send/receive queues, pending request trackers, out-of-context message buffers, etc. The amount of buffered state tends to grow under certain conditions, e.g. under heavy load or during network instability. Therefore, there should be some mechanisms to prevent &lt;em&gt;unbounded growth of state&lt;/em&gt; without compromising liveness. That can be such mechanisms as backpressure, rate limiting, item expiration and eviction policies, etc.&lt;/p&gt;

&lt;p&gt;In adversarial environments, potential DoS attacks through &lt;em&gt;resource exhaustion&lt;/em&gt; is a major threat. An adversary may attempt to exhaust node's resources, such as network bandwidth, memory and computational capacity. In order to effectively mitigate such attacks, they should be prohibitively expensive for the attacker relative to the amount of resource consumed from honest participants. &lt;em&gt;Early detection of protocol violations&lt;/em&gt; and &lt;em&gt;consumer-driven data flow&lt;/em&gt;, as employed in Cardano, can reduce the amount of resources expended by the nodes under attack. It may also be useful to tack resource expenditure caused by processing messages from remote peers, as done in Avalanche, and apply &lt;em&gt;fair throttling&lt;/em&gt; to communication channels.&lt;/p&gt;

&lt;p&gt;Proper resource management is indispensable in long-running systems. It can be particularly challenging combined with concurrency. Reliable resource management approaches, e.g. based on lifetimes and lexical scopes, as well as structured concurrency, should be, when applicable, preferred to relying on explicit hand-coded releasing of acquired resources. Potential growth of state due to buffering requires mechanisms for ensuring bounded memory usage. Resource exhaustion attacks should be anticipated in adversarial environments and mitigated by minimizing their impact on honest nodes.&lt;/p&gt;

&lt;h2&gt;
  
  
  Maintainability
&lt;/h2&gt;

&lt;p&gt;Maintenance of distributed systems is challenging. Those systems are usually long-running critical parts of infrastructure with high reliability requirements. They are complex systems consisting of multiple nodes, often operated independently by different entities. Publicly available deployments are also subject to malicious attacks. Thus effective maintenance of distributed systems demands comprehensive mechanisms and tools.&lt;/p&gt;

&lt;p&gt;First of all, deploying distributed systems may require specific &lt;em&gt;bootstrapping&lt;/em&gt; procedures in order to ensure a secure setup for the whole system. Different distributed protocols may have different requirements and rely on different assumptions for the &lt;em&gt;setup phase&lt;/em&gt;.&lt;sup id="fnref9"&gt;9&lt;/sup&gt; Protocol implementations should be clear about the requirements and assumptions for their setup phase. Long-running, highly available distributed systems should be capable of &lt;em&gt;upgrading&lt;/em&gt; individual nodes with newer versions of the protocol implementation without disrupting the whole system. This requires designing for &lt;em&gt;backward and forward compatibility&lt;/em&gt;. Similarly, failed nodes should be able to &lt;em&gt;recover&lt;/em&gt; and &lt;em&gt;rejoin&lt;/em&gt; the system safely and efficiently. Moreover, it is also desired that the system is able to safely recover from a massive crash, i.e. provide &lt;a href="https://en.wikipedia.org/wiki/Durability_(database_systems)"&gt;durability&lt;/a&gt;. Therefore, the protocols should be designed and implemented with a clear recovery procedure.&lt;/p&gt;

&lt;p&gt;Distributed system administrators need mechanisms and tools for monitoring individual nodes in order to analyze the system and promptly detect anomalies. Developers also need effective mechanisms for analyzing, diagnosing issues, and identifying bugs in protocol implementations. &lt;em&gt;Logging&lt;/em&gt;, &lt;em&gt;tracing&lt;/em&gt;, and collecting &lt;em&gt;metrics&lt;/em&gt; are common &lt;em&gt;observability&lt;/em&gt; techniques to allow monitoring and obtaining diagnostic information from the system; most of the explored code bases use these techniques. &lt;a href="https://opentelemetry.io/"&gt;OpenTelemetry&lt;/a&gt; and &lt;a href="https://prometheus.io/"&gt;Prometheus&lt;/a&gt; are popular open-source monitoring solutions, which are used in many of the explored code bases.&lt;/p&gt;

&lt;p&gt;Diagnostic logging typically refers to emitting and recording chronological &lt;em&gt;textual&lt;/em&gt; messages that capture important events happening during the execution of software. Messages in diagnostic logs are traditionally assigned a severity level that can be used to disable logging of messages below a certain severity level, e.g. debug messages. Log messages can support addition of structured data along with a formatted text message, e.g. key-value context fields. Logging can be organized hierarchically, reflecting the structure of components within the system. Messages in &lt;em&gt;hierarchical logging&lt;/em&gt; are usually automatically enriched with context from higher-level components. &lt;/p&gt;

&lt;p&gt;Tracing is somewhat similar to logging, but it is focused on capturing a detailed view of the flow of execution in the system. Tracing records are primarily &lt;em&gt;structured&lt;/em&gt; rather than textual and reflect &lt;em&gt;causal relationships&lt;/em&gt;. In particular, &lt;em&gt;distributed tracing&lt;/em&gt; is tracking of events caused by processing individual logical operations, such as user requests or transactions, across different components of a distributed system. A distributed trace is associated with a single logical operation and consists of spans linked with causal relationships where each span represents a particular activity within the operation. Spans normally contain structured data describing the corresponding activity and timing information.&lt;/p&gt;

&lt;p&gt;Metrics represent numeric measurements that describe the system's behavior over time. Metrics are typically collected and aggregated at regular intervals. They can include various types of information such as CPU and memory utilization, latency, error rates, throughput, queue lengths, etc. There are different kinds or metrics; the most widely used are counter, gauge, and histogram. A counter is a cumulative metric monotonically increasing over time; a gauge expresses the current value of some measurement; a histogram records sampled observations in a statistical representation.&lt;/p&gt;

&lt;p&gt;Observability is a &lt;a href="https://en.wikipedia.org/wiki/Cross-cutting_concern"&gt;cross-cutting concern&lt;/a&gt;. Most implementations define abstract interfaces for logging, tracing, and capturing metrics and require them as dependency across components; some use code instrumentation techniques. Cardano uses an interesting approach to implement observability features, called &lt;em&gt;contravariant tracing&lt;/em&gt;, in which domain-specific values are provided to domain-agnostic processors. The &lt;a href="https://en.wikipedia.org/wiki/Functor#Covariance_and_contravariance"&gt;contravariance&lt;/a&gt; property allows domain-agnostic tracers to be adapted and stand in where a domain-specific tracer is required. This discourages using textual encoding for diagnostic logging/tracing in favor of dedicated domain-specific event types. Contravariant tracing can also be used to collect metrics.&lt;/p&gt;

&lt;p&gt;Detailed logging and tracing can add significant overhead. When logging a large amount of diagnostic data is expensive, logging can be &lt;em&gt;sampled&lt;/em&gt;, producing only a subset of the total messages based on a predetermined sampling rate or criteria. The contravariant tracing incurs zero runtime cost if the program is compiled with tracing disabled; this is possible even when dealing with a tracer which ignores only certain types of events.&lt;/p&gt;

&lt;p&gt;Fault-tolerant distributed protocols should be designed and implemented with clear bootstrapping, upgrading, and recovery procedures. Note that upgradability relies on backward and forward compatibility of the implementation. It is also worth considering the durability feature, i.e. the ability to safely recover the system from a massive crash. There should be seamless support for usual observability and diagnostic mechanisms.&lt;/p&gt;

&lt;h2&gt;
  
  
  Flexibility
&lt;/h2&gt;

&lt;p&gt;Flexible software is able to adapt to changing requirements without having to undergo extensive restructuring. Flexibility is crucial for &lt;em&gt;adoption&lt;/em&gt;, &lt;em&gt;reuse&lt;/em&gt;, and &lt;em&gt;evolution&lt;/em&gt; of code. Each explicit or implicit &lt;em&gt;assumption&lt;/em&gt; or &lt;em&gt;requirement&lt;/em&gt; imposed on how the code can be used is an additional &lt;em&gt;constraint&lt;/em&gt; reducing flexibility. The explored code bases were primarily meant to implement particular protocols or serve specific purposes rather than to address fundamental needs for implementing distributed systems in general. This is a common approach to building software, but it tends to result in rather limited flexibility of the code.&lt;/p&gt;

&lt;p&gt;In general, highly &lt;em&gt;modular&lt;/em&gt; and &lt;em&gt;composable&lt;/em&gt; code is also more flexible. Clear &lt;a href="https://en.wikipedia.org/wiki/Separation_of_concerns"&gt;&lt;em&gt;separation of concerns&lt;/em&gt;&lt;/a&gt; through abstract interfaces and &lt;a href="https://en.wikipedia.org/wiki/Dependency_inversion_principle"&gt;dependency inversion&lt;/a&gt; contributes to flexibility by enabling interchangeable components, as well as facilitating easier code modifications and extensions. Flexibility can also be enhanced with &lt;em&gt;generic&lt;/em&gt; and &lt;em&gt;configurable&lt;/em&gt; components. &lt;a href="https://en.wikipedia.org/wiki/Generic_programming"&gt;&lt;em&gt;Generic programming&lt;/em&gt;&lt;/a&gt; techniques, such as &lt;a href="https://en.wikipedia.org/wiki/Parametric_polymorphism"&gt;parametric polymorphism&lt;/a&gt;, encourage the development of more generic and adaptable components that can be used in different contexts without modification.&lt;/p&gt;

&lt;p&gt;The ability to seamlessly integrate into larger systems is another aspect of flexibility required for adoption and reuse of protocol implementations. Since larger systems may opt for different programming languages and runtime environments, it is important to support interfacing with other languages and impose minimal runtime requirements. Rust is particularly suitable to implement robust software components for integrating into other languages and environments due to its rich language features, zero-cost abstractions, predictable performance, safe memory management without a garbage collector, and the ability to use custom concurrency runtimes.&lt;/p&gt;

&lt;p&gt;Designing for flexibility promotes adoption, reuse, and evolution of code. Following this approach should be a deliberate choice from the beginning. Avoiding strong constraints, assumptions, and requirements, aiming at modularity and composability with generic and configurable components make for greater flexibility.&lt;/p&gt;

&lt;h2&gt;
  
  
  Conclusions
&lt;/h2&gt;

&lt;p&gt;I learned a lot while exploring those 14 code bases. I have acquired a much deeper understanding of what is important for a practical distributed protocol implementation and what are the typical challenges there. I have seen different approaches in use and discovered some interesting ideas and techniques scattered around. Though I find the ways distributed protocols are implemented quite unsatisfactory. Even for an engineer experienced in implementing this kind of protocols, most of the the code bases were fairly hard to comprehend and follow. I can imagine how much effort it took and how painful was it to first make them work, as well as to improve them later.&lt;/p&gt;

&lt;h3&gt;
  
  
  Status Quo
&lt;/h3&gt;

&lt;p&gt;Most of the time, it was rather hard to follow the main protocol, its causal dependencies and logical connections in the code that was presumably structured focusing on the operational aspects, fragmented, entangled, and cluttered. Structuring the protocol implementation directly around simplistic communication mechanisms foregoing reliable and ordered delivery guarantees provided by the transport layers, expressing concurrency and synchronization explicitly in terms of low-level mechanisms based on shared mutable memory and lock-based primitives or attempting to evade concurrency in favor of sequential state machines, all seem to cause fragmentation of the protocol logic across the code base, shift the focus towards operational technicalities, and incur cluttering of the code with boilerplate and hand-coded flow control, context switching, resource management, etc. Invasive ad hoc optimizations, patches, and cross-cutting concerns also contribute to muddling the code. Often insufficient modularity, unclear structure, excessive coupling, and abundance of mutable state complicate the matter further. Using sophisticated techniques and lack of inline documentation present additional obstacles for understanding.&lt;/p&gt;

&lt;p&gt;It seems barely possible to fully convince oneself that the majority of the implementations actually correspond closely to the original protocol and guarantee the claimed properties under unfavorable conditions. The way the protocols are expressed in code does not appear anything like formal specification. The ever-present possibility of such subtle issues as race conditions, deadlocks, resource starvation, and, in some languages, data races manifesting themselves in such complicated code bases does not add more confidence. Unconstrained nondeterminism and abundance of non-local operations result in state space explosion, making rigorous test-based verification infeasible. Only a few of the implementations support reproducible testing with deterministic discrete-event simulation of unmodified code.&lt;/p&gt;

&lt;p&gt;It also seems unclear how many of the implementations would behave under certain high load conditions, e.g. under a denial-of-service attack. Protocol violations are not always optimally detected at early stages of processing incoming data; many implementations lack mechanisms for propagating information about detected anomalies towards lower communication layers in order to restrict communication with offending nodes. The majority of the implementations employ the push style of communication and forgo flow control mechanisms of transport layers, so individual remote nodes can potentially send arbitrary amounts of data that the receiving node has to deal with in time. Uncomfortably often there are unbounded buffers and queues with unclear mechanisms that could control growth of state. Unreliable explicit hand-coded resource management could cause resource leaks, including concurrent tasks dangling in background.&lt;/p&gt;

&lt;p&gt;In terms of observability, most of the protocol implementations rely on simple logging with context fields and collect various metrics. However, this may not provide enough details and context for effective debugging and analysis of the protocol execution.&lt;/p&gt;

&lt;p&gt;The explored code bases are quite specific to particular protocols, execution environments, and use cases. Modularity there is rather coarse and most of the components are not meant to be reused or recombined; tight coupling is also not rare. This harms adaptability and reusability of the code, making it inflexible.&lt;/p&gt;

&lt;h3&gt;
  
  
  We Can Do Better
&lt;/h3&gt;

&lt;p&gt;I think we can do much better. I think we should not waste our efforts reinventing the wheel over and over again and repeating mistakes. Builders better focus on implementing the functionality specific to their solutions without having to figure out how to approach implementing the tricky but critically important distributed protocols. There should be a framework that solves the problem of implementing distributed protocols once and for all, a framework reach with easy-to-use, reliable primitives and components that can be taken as is or mixed and matched as needed, a framework that guides towards robust and understandable code, a framework that supports analyzing, monitoring, testing, and debugging protocol implementations, a framework that is reasonably efficient and can be easily integrated into various environments.&lt;/p&gt;

&lt;p&gt;The framework should guide away from incidental, non-essential complexity and allow expressing protocol implementations in clear and understandable code. Protocol implementations should be structured primarily focusing on functional and logical aspects with clear separation of concerns, operational technicalities and sophisticated techniques possibly hidden behind simple and clearly defined abstractions. Fine modularity of reasonably small and simple components expressed in more declarative notation with reduced number of non-local operations should facilitate local reasoning. Components should have minimal internal state, as well as clearly defined requirements, properties, and external dependencies.&lt;/p&gt;

&lt;p&gt;Concurrency requires special attention since it is unavoidable, tricky, and can add a great deal of complexity, whereas designing for concurrency can be actually advantageous in terms of code structure and modularity. Working with concurrency should be possibly safe, easy, and efficient. Low-level concurrency mechanisms, such as OS threads, lock-based synchronization primitives, and shared mutable memory, should only be used for implementing the internals of higher-level, safer, and easier-to-use concurrency mechanisms, such as concurrency runtimes. Expressing concurrent parts of the protocol in code should feel as natural as expressing sequential ones. This can be achieved with syntactical means, abstractions, and a concurrency model that recognizes any causally independent operations as potentially concurrent.&lt;/p&gt;

&lt;p&gt;Since communication interfaces can greatly affect the structure of code built around them, we need a range of communication mechanisms with aligned interfaces and clearly defined properties. There should be different levels of abstractions for communication. Higher levels should take advantage of the properties already guaranteed by lower-level layers, such as reliable, ordered communication channels with flow control provided by commonly used transport layers. Expressing communication in stateful sessions can help to express causal relationship between individual messages and greatly simplify protocol implementations. Similarity between internal and external communication can suggest better abstractions.&lt;/p&gt;

&lt;p&gt;Flexibility is extremely important to make the framework applicable to an open-ended space of use cases. Therefore, we should by all means avoid strong constraints, assumptions, and requirements. The framework should support integration with different programming languages and runtime environments. Its components should be generic and configurable. It should also support backward and forward compatibility. Composability is critical for ensuring great adaptability, reusability, and evolvability. It requires unified means of abstraction and combination. Generic programming techniques, such as parametric polymorphism, can be used to make components generic; functional and asynchronous programming techniques can be great sources of ideas for enhancing composability, particularly with concurrency.&lt;/p&gt;

&lt;p&gt;Correctness of distributed protocol implementations should be verifiable, in terms of both safety and liveness properties. Formal verification methods are able to provide rigorous assurance about correctness of protocols and their implementations. However, since formal verification involves exhaustively analyzing all possible states of a system, it may become infeasible for large and complex components. Fine modularity, components amenable to local reasoning, as well as reducing the number of non-local and nondeterministic operations, can help making formal verification more tractable. In order to maintain equivalence between a formally verified protocol specification and its implementation in code, the implementation should be expressed possibly close to the formal specification, preferably using an identical notation. Type safely techniques, such as ownership, typestates, session types, linear and uniqueness types, can greatly help to ensure correctness of the code by making it virtually safe by construction in terms of certain properties. Hybrid approaches combining formal verification with other testing methods can be used to achieve decently high assurance about correctness where purely formal methods become infeasible. Deterministic discrete-event simulation of unmodified code is a particularly powerful technique to complement other verification methods with randomized, reproducible testing. Confining nondeterministic aspects behind abstract interfaces in code and being able to control nondeterminism during simulation is the key for enabling reproducible testing.&lt;/p&gt;

&lt;p&gt;Distributed protocols and their implementations should provide strong guarantees even under unfavorable conditions, especially those supposed to be deployed in adversarial environments. The framework should employ a reliable approach for resource management in concurrent code, e.g. based on lifetimes and lexical scopes, structured concurrency. There should be mechanisms for flow control preventing unlimited growth of state and ensuring bounded memory usage. The framework should emphasize threat-aware design. Potential impact of resource exhaustion (DoS) attacks should be minimized with early detection of protocol violations and propagating information about detected anomalies for maintaining peer reputation metrics and taking appropriate measures. For that reason, consumer-driven patterns of communication should be preferred. There should also be mechanisms for safe and efficient recovery of failed nodes from persistent storage. Supporting durability, i.e. safe recovery after a massive system crash, is also desirable.&lt;/p&gt;

&lt;p&gt;Protocols and their implementations should be clear about bootstrapping and recovery requirements and procedures. Upgradability requires backward and forward compatibility. There should be seamless support for usual observability and diagnostic mechanisms, such as logging, tracing, and collecting metrics. It may also be useful to provide mechanisms for tracking resource expenditure caused by processing incoming data. In place of simple logging with context fields, it seems advantageous supporting structured distributed tracing using domain-specific trace event types. This kind of tracing could also be suitable for collecting metrics. It is important to minimize incurred overhead when tracing is disabled. Code instrumentation can help to avoid cluttering code with tracing boilerplate.&lt;/p&gt;

&lt;p&gt;The framework should provide good performance and support various optimizations, such as speculative and on-demand execution, caching, flexible prioritization policies. To support protocol-level optimizations, the framework should allow expressing complex communication patterns. The communication layer should prevent such undesired effects as head-of-line blocking, optimize data flow and take advantage of the properties provided by the transport layers. Lightweight user threads and non-blocking algorithms allow achieving high concurrency without compromising efficiency. Zero-copy techniques can be used to eliminate unnecessary copying of data.&lt;/p&gt;

&lt;p&gt;So we need a structured, yet flexible enough, approach guiding away from incidental complexity towards understandability, fine modularity, and composability. The framework's components should be generic and configurable, allowing local reasoning about the implementation. Expressing concurrency and communication abstractions should be safe and easy, structured and composable. We should be serious about correctness and resilience against unfavorable conditions. The framework should also cater for maintenance needs, provide great observability and diagnostic mechanisms. It should deliver decent performance and allow for various optimizations.&lt;/p&gt;

&lt;h2&gt;
  
  
  Next Steps
&lt;/h2&gt;

&lt;p&gt;Having explored those implementations of distributed protocol, now it became more clear to me what is worth focusing on while developing the Replica_IO framework. I define the following key areas of focus:&lt;/p&gt;

&lt;ul&gt;
&lt;li&gt;
&lt;em&gt;simplicity&lt;/em&gt;: making protocol implementations well structured and understandable;&lt;/li&gt;
&lt;li&gt;
&lt;em&gt;flexibility&lt;/em&gt;: keeping the framework adaptable, widely applicable, and evolvable;&lt;/li&gt;
&lt;li&gt;
&lt;em&gt;reliability&lt;/em&gt;: ensuring that protocol correctness is verifiable and the implementation is resilient;&lt;/li&gt;
&lt;li&gt;
&lt;em&gt;efficiency&lt;/em&gt;: allowing for various optimizations and delivering good performance;&lt;/li&gt;
&lt;li&gt;
&lt;em&gt;maintainability&lt;/em&gt;: catering for maintenance needs and providing great diagnostic mechanisms.&lt;/li&gt;
&lt;/ul&gt;

&lt;p&gt;Achieving all of that at once is obviously not realistic. Therefore, the primary focus will be initially put on simplicity, flexibility, and reliability, but without neglecting the remaining aspects. Of particular interest are the matters of structure and notation supporting composability in concurrency and communication mechanisms, as well as controlling nondeterminism.&lt;/p&gt;

&lt;p&gt;Exploring distributed protocol implementations was the first phase of the initial state-of-the-art exploration. The next step is to select and examine some existing frameworks for developing distributed protocols in order to find out how they attempt to approach the problem and, perhaps, also discover some interesting techniques or ideas employed there. Then there are some potentially related concepts, approaches, and techniques worth looking into. The exploration tasks are tracked in the scope of &lt;a href="https://github.com/replica-io/replica-io/issues/7"&gt;this issue&lt;/a&gt; on GitHub.&lt;/p&gt;

&lt;p&gt;Once the initial exploratory stage is over, it will be time to come up with key ideas concerning core principles that will guide the process of designing and implementing generic components within the framework (milestone &lt;a href="https://github.com/replica-io/replica-io/milestone/1"&gt;M0.1&lt;/a&gt;). Then those ideas will be developed into clearly formulated concepts (milestone &lt;a href="https://github.com/replica-io/replica-io/milestone/2"&gt;M0.2&lt;/a&gt;), their feasibility will be verified with code (milestone &lt;a href="https://github.com/replica-io/replica-io/milestone/3"&gt;M0.3&lt;/a&gt;). After that, prototype, MVP, and production versions of the framework will be developed and released (milestones  &lt;a href="https://github.com/replica-io/replica-io/milestone/4"&gt;M1&lt;/a&gt;,  &lt;a href="https://github.com/replica-io/replica-io/milestone/5"&gt;M2&lt;/a&gt;, and  &lt;a href="https://github.com/replica-io/replica-io/milestone/6"&gt;M3&lt;/a&gt;).&lt;/p&gt;

&lt;p&gt;It does not mean at all that exploration, ideation, and prototyping will not take place at later stages; the milestones simply define the framework's general level of maturity. The framework will continuously evolve and expand and at some point become a de facto standard for implementing critical fault-tolerant systems providing a growing collection of easy-to-use reliable and efficient distributed replication mechanisms.&lt;/p&gt;

&lt;p&gt;If you like the project and find it valuable, please &lt;a href="https://github.com/sponsors/replica-io"&gt;support&lt;/a&gt; its further development! 🙏&lt;br&gt;
&lt;a href="https://github.com/sponsors/replica-io" class="ltag_cta ltag_cta--branded"&gt;❤️ Replica_IO&lt;/a&gt;
&lt;/p&gt;

&lt;p&gt;If you have any thought you would like to share or any question regarding this post, please add a comment &lt;a href="https://github.com/orgs/replica-io/discussions/35"&gt;here&lt;/a&gt;. You are also welcome to &lt;a href="https://github.com/orgs/replica-io/discussions/new/choose"&gt;start a new discussion&lt;/a&gt; or chime in to &lt;a href="https://discordapp.com/invite/CzPfN75URD"&gt;our Discord&lt;/a&gt; server.&lt;/p&gt;




&lt;ol&gt;

&lt;li id="fn1"&gt;
&lt;p&gt;If you know of some other implementation that I should have absolutely looked into for some reason, please let me know. ↩&lt;/p&gt;
&lt;/li&gt;

&lt;li id="fn2"&gt;
&lt;p&gt;Actually, incidental complexity can start creeping in even earlier, into the way we &lt;em&gt;think&lt;/em&gt; about distributed systems, but let's not go into this here. ↩&lt;/p&gt;
&lt;/li&gt;

&lt;li id="fn3"&gt;
&lt;p&gt;Zarko Milosevic, CTO at Informal Systems, &lt;a href="https://www.youtube.com/watch?v=c4BQ7v-CQfk&amp;amp;t=296s"&gt;tells&lt;/a&gt; in his invited talk at &lt;a href="https://research.protocol.ai/sites/consensusday23/"&gt;ConsensusDays 23&lt;/a&gt; how a small protocol change addressing a major issue resulted in months of implementation work on the Tendermint code base. ↩&lt;/p&gt;
&lt;/li&gt;

&lt;li id="fn4"&gt;
&lt;p&gt;In his talk "&lt;a href="https://www.youtube.com/watch?v=qlAKyivFxGQ"&gt;Using STM for Modular Concurrency&lt;/a&gt;", Duncan Coutts expands on the approach to concurrency employed by Cardano. ↩&lt;/p&gt;
&lt;/li&gt;

&lt;li id="fn5"&gt;
&lt;p&gt;More about the threat-aware design approach in &lt;a href="https://iohk.io/en/research/library/papers/introduction-to-the-design-of-the-data-diffusion-and-networking-for-cardano-shelley/"&gt;"Introduction to the design of the Data Diffusion and Networking for Cardano Shelley"&lt;/a&gt;. ↩&lt;/p&gt;
&lt;/li&gt;

&lt;li id="fn6"&gt;
&lt;p&gt;The &lt;code&gt;typed-protocols&lt;/code&gt; framework was presented in the talk "&lt;a href="https://skillsmatter.com/skillscasts/14633-45-minute-talk-by-duncan-coutts"&gt;Well-Typed Communication Protocols&lt;/a&gt;" by Duncan Coutts. ↩&lt;/p&gt;
&lt;/li&gt;

&lt;li id="fn7"&gt;
&lt;p&gt;&lt;a href="https://github.com/input-output-hk/ouroboros-consensus/blob/release-ouroboros-consensus-0.8.0.0/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Util/ResourceRegistry.hs#L80"&gt;&lt;code&gt;ResourceRegistry&lt;/code&gt;&lt;/a&gt; used in Cardano is an example of a fallback mechanism based on lexical scoping for preventing resource leaks. ↩&lt;/p&gt;
&lt;/li&gt;

&lt;li id="fn8"&gt;
&lt;p&gt;Nathaniel J. Smith elaborates on structured concurrency in great detail in his blog post &lt;a href="https://vorpus.org/blog/notes-on-structured-concurrency-or-go-statement-considered-harmful/"&gt;"Notes on structured concurrency, or: Go statement considered harmful"&lt;/a&gt;. ↩&lt;/p&gt;
&lt;/li&gt;

&lt;li id="fn9"&gt;
&lt;p&gt;&lt;a href="https://decentralizedthoughts.github.io/2019-07-19-setup-assumptions/"&gt;This post&lt;/a&gt; discusses the setup phase in distributed systems. ↩&lt;/p&gt;
&lt;/li&gt;

&lt;/ol&gt;

</description>
      <category>distributedsystems</category>
      <category>decentralizedcomputing</category>
      <category>faulttolerance</category>
      <category>replication</category>
    </item>
    <item>
      <title>The Story Behind Replica_IO</title>
      <dc:creator>Sergey Fedorov</dc:creator>
      <pubDate>Fri, 05 Apr 2024 10:49:45 +0000</pubDate>
      <link>https://dev.to/replica-io/the-story-behind-replicaio-3036</link>
      <guid>https://dev.to/replica-io/the-story-behind-replicaio-3036</guid>
      <description>&lt;p&gt;This post tells how the &lt;a href="https://replica-io.dev/"&gt;Replica_IO&lt;/a&gt; project originated and explains the&lt;br&gt;
motivation behind it.&lt;/p&gt;

&lt;p&gt;&lt;em&gt;The original post can be found &lt;a href="https://replica-io.dev/blog/2023/09/04/the-story-behind-replica_io"&gt;here&lt;/a&gt;.&lt;/em&gt;&lt;/p&gt;

&lt;h2&gt;
  
  
  My Background
&lt;/h2&gt;

&lt;p&gt;I'd like to start by tell you a bit about my professional background.&lt;br&gt;
I'm a research engineer with quite some experience in software&lt;br&gt;
engineering. I began working as a software engineer back in 2009.&lt;/p&gt;

&lt;p&gt;First 7 years, I was mostly focused on developing low-level system&lt;br&gt;
software: I worked with such things as Linux kernel, microcontrollers,&lt;br&gt;
hardware emulation, and trusted execution. Back then, I particularly&lt;br&gt;
enjoyed contributing to &lt;a href="http://qemu.org/"&gt;Qemu&lt;/a&gt;, a generic and&lt;br&gt;
open-source machine emulator and virtualizer. My contribution included&lt;br&gt;
enhancing emulation of the ARM platform and enabling multithreading&lt;br&gt;
support in the generic binary translation engine&lt;/p&gt;

&lt;p&gt;In 2016, I took a big leap and came into research and development in&lt;br&gt;
the areas of blockchain, distributed and decentralized systems. Soon&lt;br&gt;
enough, I became absolutely excited about this, and since then, I keep&lt;br&gt;
expanding my knowledge and experience in that area, in particular,&lt;br&gt;
designing and implementing distributed protocols. During that period,&lt;br&gt;
apart from proprietary stuff, I worked on the following open-source&lt;br&gt;
projects:&lt;/p&gt;

&lt;ul&gt;
&lt;li&gt;
&lt;a href="http://github.com/hyperledger-labs/minbft"&gt;MinBFT Hyperledger Lab&lt;/a&gt; — an implementation of the MinBFT
consensus protocol as a pluggable component. I was the main author,
contributor, and maintainer of the project.&lt;/li&gt;
&lt;li&gt;
&lt;a href="http://github.com/filecoin-project/mir"&gt;Mir&lt;/a&gt; — a framework for implementing, debugging, and analyzing
distributed protocols. My main contribution was implementation of
the checkpointing mechanism, protocol garbage collection, and
reproducible testing with simulated time.&lt;/li&gt;
&lt;li&gt;
&lt;a href="http://fil.space/#components"&gt;Interplanetary Consensus (IPC)&lt;/a&gt; — a framework to enable
on-demand horizontal scalability of the Filecoin blockchain. My
main contribution was redesign and implementation of the atomic
cross-chain transaction execution protocol in Rust.&lt;/li&gt;
&lt;/ul&gt;

&lt;h2&gt;
  
  
  Implementing Distributed Protocols
&lt;/h2&gt;

&lt;p&gt;So much was I excited about distributed systems, but, after a while, I&lt;br&gt;
started feeling like there's something fundamentally wrong in how we&lt;br&gt;
usually design and implement them.&lt;/p&gt;

&lt;p&gt;Distributed protocols are notoriously complex, and it took academia&lt;br&gt;
significant effort to develop a solid theoretical foundation for them.&lt;br&gt;
Due to inherent concurrency, the reasoning about distributed systems&lt;br&gt;
is quite tricky, and there are lots of pitfalls where one gets trapped&lt;br&gt;
pretty quickly, unless being extremely careful. Though, I find this&lt;br&gt;
really fascinating because I particularly love digging deep and&lt;br&gt;
thinking thoroughly.&lt;/p&gt;

&lt;p&gt;However, the way distributed protocols are conventionally described on&lt;br&gt;
paper makes it hardly possible to implement them correctly with&lt;br&gt;
confidence; it's simply too far from the realities of software&lt;br&gt;
engineering. Not only academic papers often neglect some details of&lt;br&gt;
practical importance but also the language and notation used there,&lt;br&gt;
they require nontrivial translation to the languages and patterns&lt;br&gt;
commonly used in programming. Add there typical issues that come up&lt;br&gt;
inevitably when programming concurrent systems, time pressure, and we&lt;br&gt;
end up with a great mess that one can hardly comprehend and maintain.&lt;/p&gt;

&lt;p&gt;Moreover, it seems like those engineers who get their hands dirty and&lt;br&gt;
implement distributed protocols for practical use tend to jump in and&lt;br&gt;
try applying whatever approach they were used to or that was implied&lt;br&gt;
by the surrounding system. Although one can certainly learn a lot from&lt;br&gt;
such experiments (and I'm doing that), it's generally waste of efforts&lt;br&gt;
when one simply needs to get the thing reliably working. More than&lt;br&gt;
that, since this kind of code is quite hard to get right, inevitable&lt;br&gt;
mistakes creep into such implementations and lurk there unnoticed.&lt;br&gt;
Even when some of those mistakes get revealed, individual projects are&lt;br&gt;
usually too busy and too specific to keep following and effectively&lt;br&gt;
learning from each other.&lt;/p&gt;

&lt;p&gt;Having implemented a couple of distributed protocols myself, I find&lt;br&gt;
this status quo deeply unsatisfactory, especially when it comes to&lt;br&gt;
distributed replication mechanisms such as consensus protocols. After&lt;br&gt;
all, they are supposed to ensure consistency and availability in such&lt;br&gt;
critical computing systems as distributed coordination services,&lt;br&gt;
distributed databases, and blockchain. There is an opinion that the&lt;br&gt;
main obstacle to wider adoption of distributed, decentralized systems,&lt;br&gt;
particularly those capable of tolerating arbitrary (Byzantine) faults,&lt;br&gt;
is their requirement for additional resources and reduced performance.&lt;br&gt;
While it's certainly true that high reliability doesn't come for free,&lt;br&gt;
I think the concerns regarding complexity do actually matter a lot in&lt;br&gt;
the end; it's simply hard to get it right.&lt;/p&gt;

&lt;p&gt;I think decentralized Byzantine-fault tolerant mechanisms should&lt;br&gt;
prevail in future computing systems and we can do a much better job&lt;br&gt;
working towards that. I believe such complex problems can have neat&lt;br&gt;
solutions, not only efficient, but also easy to use. Clearly,&lt;br&gt;
discovering and developing such solutions does take quite some effort.&lt;br&gt;
There must have been attempts to solve this problem, apparently not&lt;br&gt;
very successful. But since I like to think of myself as someone&lt;br&gt;
discovering smart solutions to hard problems, I'm not too scared; I'm&lt;br&gt;
stubborn enough 😄&lt;/p&gt;

&lt;h2&gt;
  
  
  Replica_IO
&lt;/h2&gt;

&lt;p&gt;So I was thinking about this for years, but never managed to find room&lt;br&gt;
for seriously working on it. Suddenly, in February 2023, I was&lt;br&gt;
affected by a lay-off in &lt;a href="https://protocol.ai/"&gt;Protocol Labs&lt;/a&gt; and had to&lt;br&gt;
leave; by that time, I had worked with the company as a long-term&lt;br&gt;
collaborator, a Research Engineer at the &lt;a href="https://research.protocol.ai/groups/consensuslab/"&gt;ConsensusLab&lt;/a&gt;&lt;br&gt;
group, for almost a year. After a while, I realized that this is&lt;br&gt;
actually a great chance to finally start working on what I was&lt;br&gt;
dreaming of.&lt;/p&gt;

&lt;p&gt;Initially, I thought I would just take a break and spend some time on&lt;br&gt;
a hobby project. I already had a name for it — Replica_IO, which had&lt;br&gt;
come to my mind a few months before, as I had been yet again thinking&lt;br&gt;
about communication between replicas in a distributed replication&lt;br&gt;
system. However, once I started asking myself about my real intention&lt;br&gt;
behind this, I realized that it's much bigger than just playing with a&lt;br&gt;
pet project: what I really want is to make a breakthrough in how&lt;br&gt;
distributed systems are designed and implemented!&lt;/p&gt;

&lt;p&gt;In March 2023, I decided to found the Replica_IO project and work on&lt;br&gt;
it full time as an independent research engineer. Since I believe in&lt;br&gt;
open source, open innovation and collaboration, I also wanted to make&lt;br&gt;
it radically open and started developing it entirely in the open from&lt;br&gt;
day one. I &lt;a href="https://github.com/replica-io/replica-io/issues/2"&gt;described&lt;/a&gt; the project's purpose, goals, and&lt;br&gt;
approach, &lt;a href="https://github.com/replica-io/replica-io/issues/3"&gt;created&lt;/a&gt; its logo, &lt;a href="https://github.com/replica-io/replica-io/issues/1"&gt;defined&lt;/a&gt; the initial&lt;br&gt;
roadmap, and started working on the &lt;a href="https://github.com/replica-io/replica-io/milestone/1"&gt;first milestone&lt;/a&gt;.&lt;/p&gt;

&lt;p&gt;At the time of this writing, I'm &lt;a href="https://github.com/replica-io/replica-io/issues/7"&gt;exploring&lt;/a&gt; some relevant&lt;br&gt;
state of the art, &lt;a href="https://github.com/replica-io/replica-io/wiki/State-of-the-art-exploration"&gt;summarizing&lt;/a&gt; the findings.&lt;br&gt;
Approaching this in a systematic way lets me dive deeper into the&lt;br&gt;
problem, form a more educated opinion, find some inspiration, and&lt;br&gt;
ultimately come up with effective ideas for achieving the project's&lt;br&gt;
key technical objectives.&lt;/p&gt;

&lt;p&gt;I understand how ambitious the goals of this project are and that it&lt;br&gt;
may take long time to get there, but I'm absolutely sure it is worth&lt;br&gt;
the effort. I'm surprised how much attention the project has already&lt;br&gt;
attracted and would like to see great experts from the relevant fields&lt;br&gt;
become involved and help to make it real. I also count on getting enough&lt;br&gt;
support for this initiative, and I'm grateful to those who have&lt;br&gt;
already been helping 🙏&lt;/p&gt;

&lt;p&gt;If you'd like to learn more about this project, please visit the&lt;br&gt;
&lt;a href="//replica-io.dev/about"&gt;About&lt;/a&gt; page and watch &lt;a href="https://youtu.be/oJlryr6bMCo"&gt;this talk&lt;/a&gt;.&lt;/p&gt;

</description>
      <category>decentralizedcomputing</category>
      <category>distributedsystems</category>
      <category>faulttolerance</category>
      <category>replication</category>
    </item>
  </channel>
</rss>
