this is my first post on this exchange.

I am looking for some help with defining a proof that a set of operations I have designed forms a commutative monoid.

(Disclaimer: I am not sure that I have phrased the question properly so I will be very grateful for restructuring it if necessary.)

I think it will be better if I illustrate what my problem looks like:

I assume that:

$\exists cm(t) \in CM$

means that there exists an instance of $commutative \space monoid$ for type $t$.


$k \in Keys$

$op \in \{NoOp, Add, Read, Write\}$

$tr \in \{Identity, Write(k, v), Add(k, v): \exists cm(v) \in CM\}: \forall k \in K$

Point of this description is to allow for easier detection of conflicts when more than one process wants to modify the value under some key. My mental model for this is close to optimistic concurrency control (or optimistic locking) married with CmRDT.

Every process $p$ operates on the "copy" of some state. When p wants to access value under key $k$ this fact is recorded in the form of $(Key, Op, Transform)$ tuple. (note: that $Add$ transformations are allowed only if there exists an instance of $commutative \space monoid$ for this type).

We define an instance of $commutative \space monoid$ for $Ops$:

$$\begin{array}{c|c|c|c|c} & \text{NoOp} & \text{Read} & \text{Add} & \text{Write} \\ \hline \text{NoOp} & \text{NoOp} & \text{Read} & \text{Add} & \text{Write} \\ \hline \text{Read} & - & \text{Read} & \text{Write} & \text{Write} \\ \hline \text{Add} & - & - & \text{Add} & \text{Write} \\ \hline \text{Write} & - & - & - & \text{Write} \\ \hline \end{array}$$

(matrix is symmetric so I omitted the lower left half). Note that $Read * Add$ becomes a $Write$. My reasoning behind it is that $Read$ may influence $Add$-ed value so it should not commute with anything else.

When $p$ executes an engine records operation it performs on every $k$ and uses rules defined above so that later it is easy to decide which operations conflict:

Two operations on key $k$ conflict if any of them is $Write$.

Now, what I want to prove? I want to prove myself and to my management that operations, defined by above algorithm as non-conflicting, will never lead to inconsistent state. Inconsistent state is defined as one in which order of executing transformations changes the final value.

I tried coming up with a description in $TLA^+$ and $F^*$ but I am not an expert in either of them. My level of understanding category theory (and math in general) is not superb either. Can you please help me coming up with proper definition of this?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.