18 Causality

Precedes relation on composite operations

Definition: Let M₁,M₂ be composite operations. We write M₁ → M₂ if

O₁ ∈ Ψ(M₁), O₂ ∈ Ψ(M₂) ⇒ O₁ → O₂

Definition: Let M₁,M₂ be composite operations. We write M₁ || M₂ if

O₁ ∈ Ψ(M₁), O₂ ∈ Ψ(M₂) ⇒ O₁ || O₂

Note that it is possible to have ¬(M₁ → M₂) ∧ ¬(M₂ → M₁) ∧ ¬(M₁ || M₂)

Causality with regard to the primitive operators

Consider two sites using the conventional approach of history buffers that are linear lists of operations that only grow as operations are appended at the ends of the lists.

Site S₁ HB = [a₁ a₂ a₃ a₄]

Site S₂ HB = [a₁ a₂ b₁ a₃ b₂]

S₂ is about to send b₁ and b₂. The operations that causally precede b₁ are { a₁,a₂ }, whereas the operations that causally precede b₂ are { a₁,a₂,a₃,b₁ }

In the conventional approach S₂ will send b₁ with a different execution context than b₂. The result is that the dual IT performed on S₁ must always involve concurrent operations.

However in the new proposed approach, S₂ will send an RFactor of its HB that contains both b₁ and b₂, and it is impossible for S₁ to know that a₃ precedes b₂ but not b₁. Our approach actually assumes that it is nevertheless possible for S₁ to merge this RFactor directly into its HB and ignore the fact that it can't actually tell for sure which of its operations are concurrent with the remote operation.

It is important to note that when we factorise the S₂ HB into Lf = { a₁ a₂ a₃ } and Rf = { b₁ b₂ } it is not the case that all atomic operations in Lf causally precede the atomic operations in Rf. Nevertheless such a factorisation is meaningful - because there is no operation in Rf that precedes an operation in Lf - which is exactly what is meant by a causally valid vector time.

The conventional approach can be seen as necessarily recording much more information about causality. The proposal suggests that this is not necessary - even to the extent of avoiding the need to implement a solution in terms of an inclusion transform that assumes that the operations are concurrent.

TODO: The subsequent treatment of assignment contains errors because of exactly this issue. It turns out that the proposal doesn't actually lead to uniqueness of a merge because of this very problem.