A Sketch of Reversible Deterministic Concurrency for Distributed Protocols

[sergefdrv]

This discussion is for comments to the blog post "A Sketch of Reversible Deterministic Concurrency for Distributed Protocols".

[TomasMikula]

Nice write-up and graphical notation!

I lack some clarity around composite lines, though. On one hand, there are line composition primitives, which suggests that they are part of the formalism. On the other hand, you say they are just notational convenience, which I read as existing only at the meta level. Practically speaking, the question is whether the shape of a composite line is always statically known down to the primitive level, or whether it can be determined dynamically during execution. It then has implications for the replication box: can it be statically expanded (i.e. is also just a notational convenience), based on the static shape of the input line, or does it expand dynamically based on how the input line expands at runtime? If the intention is for it to be dynamic (which is what I suppose), then there's a bunch of things that are left unspecified in the write-up, such as:

• Can a line expand to any composite shape, or is there a way to constrain it (e.g. to (a, (b, (c, ...))) = [a, b, c, ...], but also other recursive shapes)?
• To build components taking in dynamically expanding input lines (e.g. a transposer), there needs to be a way to detect whether the line is ! (empty source) or it's a pair of lines, and continue correspondingly.
• Which line of the replication box determines the replication? Is it the input line and the output line is expanded accordingly? I saw some diagrams with multiple inputs to replication box. How does that behave?

Also, what does availability mean on a composite line? First input available? Some input available? All of the inputs available? Dynamic expansion completed (but element inputs not necessarily available yet)? First level of dynamic expansion completed? ...

[sergefdrv]

@TomasMikula, thanks for your feedback! Very good questions! Composite lines and component replication indeed require further elaboration. For now, I'll just share my current intuition for how it should probably work.

whether the shape of a composite line is always statically known down to the primitive level, or whether it can be determined dynamically during execution

I think we should start by assuming that the shape, i.e. the pattern of composition, is statically known, but how much it will actually expand, i.e. become available, is to be determined at run time. (The verification approach we'll end up employing in the framework should better check that such expansion doesn't go out of bounds.) In some cases, both the shape and length/depth can be statically known, e.g. [a, b, c] = (a, (b, (c, !))), but in general, the composition could be statically of indefinite length/depth, e.g. [a, b, ...] = (a, (b, ...)), but dynamically only expand within bounds.

Can a line expand to any composite shape, or is there a way to constrain it

I think we'll need to find a way of expressing types of composite lines so that we can define both recursive and non-recursive types. E.g., we might just want to bundle three lines of certain types together for convenience, or we may want to express a composite line that bundles a series of same-typed lines of indefinite length, like a list in functional programming.

components taking in dynamically expanding input lines (e.g. a transposer)

Transposer should probably be treated as a wiring primitive rather than component.

a way to detect whether the line is ! (empty source) or it's a pair of lines, and continue correspondingly

Empty source is not a special type of line or value, it can represent a source of any type that just never becomes available. Determining whether a continuation is a dead end that can be abandoned should be a matter of run time (or verification).

Which line of the replication box determines the replication?

All lines crossing the same replication box must agree on the dementionality of the outermost regular level of composition. Remember that we can always bundle multiple lines together. If there are multiple composite lines entering the same replication box, we can treat them as first bundled into a single composite line that is then transposed before entering the replication box and un-bundled right away inside the replication box; same for exiting lines, just in reverse.

what does availability mean on a composite line?

Perhaps the best way of thinking is that composite lines gradually become available as their elements (the individual lines they are composed of) become available. We can say that a composite line becomes fully available when all of its elements become available (this won't apply to recursively-typed compositions).

[TomasMikula]

I'm also not clear about the role of demand-drivenness. Was it essential for some other things to work?

[sergefdrv]

One of the reasons for introducing the notion of demand was for representing races using CSwap with unspecified control: If there were no difference between demanded and not demanded outputs then the values on target lines would just always go through and the control line would never be set true.

Apart from that, making computations demand-driven prevents them from starting too early, just based on inputs connected to sources of immediately available values, such as sources of constants or undefined values. This is especially important for replicated components. Moreover, once a component starts computation using available input values, it becomes responsible for keeping the data around until there is a demand for the corresponding output that will consume the data. Inputs may become available faster than the results are demanded. We need some kind of flow control and keep memory consumption bounded.

I also think that computation should be primarily demand-driven because if there's no demand for an output then computing it may just be waste of resources for no good. Though, the runtime may actually perform some computations speculatively as a kind of optimization.

[sergefdrv]

I gave a short talk on this at Protocol Berg in Berlin. The recording is available now: https://watch.protocol.berlin/65a90bf47932ebe436ba9351/watch?session=68555a2690bd41297b3fb6b2

Slides are available here: https://cfp.protocol.berlin/media/protocol-berg-v2/submissions/QHGJDW/resources/New_insights_into_distributed_and_concurre_oPQ5QNu.pdf