TensorIR is a compiler abstraction for optimizing programs with tensor computation primitives in TVM. Imagine a DNN task as a graph, where each node represents a tensor computation. TensorIR explains how each node/tensor computation primitive in the graph is carried out. This post explains my attempt to implement 2D convolution using TensorIR. It is derived from the Machine Learning Compilation course offered by Tianqi Chen.

Implement 2D Convolution

2D convolution is a common operation in image processing. The image below captures how 2D convolution operates. I won’t go into details here. But you can find plenty information online regarding convolution.

First, we initialize both the input matrix and the weight matrix:

# batch, input_channel_dim, image_height, image_width, output_channel_dim, kernel_width & height
N, CI, H, W, CO, K = 1, 1, 8, 8, 2, 3
# output_height, output_width, assuming kernel has stride=1 and padding=0
OUT_H, OUT_W = H - K + 1, W - K + 1
data = np.arange(N*CI*H*W).reshape(N, CI, H, W)
weight = np.arange(CO*CI*K*K).reshape(CO, CI, K, K)

We can validate the results using torch.nn.functional.conv2d() from PyTorch.

One thing Tianqi recommended for starters is to write the implementation first in numpy, and then translate the numpy implementation to TensorIR. I started my implementation directly from TensorIR, before totally getting confused. So here’s how I approach the problem.

First, and perhaps most importantly, you should figure out the accessing pattern of the output matrix, and gradually fill up the compute rules for each element in the output matrix. So, we know the output matrix has a shape of (N, CO, OUT_H, OUT_w) (which corresponds to batch, number of output channels, output height, and output width). The numpy loop will look like:

for b in np.arange(0, N):
 for co in np.arange(0, CO):
 for h in np.arange(0, OUT_H):
 for w in np.arange(0, OUT_W):
 Y[b, co, h, w] = 0

Here, we access element in the output matrix one by one and initialize each element to be 0. Next, we will try to figure out how to compute each element. We know each element in the output matrix is just the sum of element-wise multiplication of both the 2D convolutional kernel (1 by 3 by 3) and the corresponding area in the input matrix (1 by 3 by 3):

for b in np.arange(0, N):
 for co in np.arange(0, CO):
 for h in np.arange(0, OUT_H):
 for w in np.arange(0, OUT_W):
 # init to 0
 Y[b, co, h, w] = 0
 # 2d conv kernel
 for ci in np.arange(0, CI):
 for kh in np.arange(0, K):
 for kw in np.arange(0, K):
 # reduction
 Y[b, co, h, w] += A[b, ci, h+kh, w+kw] * W[co, ci, kh, kw]

We can verify the function has the same output as torch.nn.functional.conv2d() from PyTorch.

The next part is to translate the numpy code into TensorIR. I won’t go into every the details of every single line here, but you can find all explanations from this note.

The nested loop can be encapsulated using T.grid() like this:

@tvm.script.ir_module
class MyConv:
 @T.prim_func
 def conv2d(data: T.Buffer[(N, CI, H, W), "int64"],
 weight: T.Buffer[(CO, CI, K, K), "int64"],
 result: T.Buffer[(N, CO, OUT_H, OUT_W), "int64"]):
 T.func_attr({"global_symbol": "conv2d", "tir.noalias": True})
 # loop through each elem in the output matrix
 for b, o, h, w in T.grid(N, CO, OUT_H, OUT_W):
 # kernel access pattern
 for kc, kh, kw in T.grid(CI, K, K):

Next, we define the block (a basic unit of computation in TensorIR). A block contains a set of block axes (vi, vj, vk) and computations defined around them. Here, we define the property about each block axes:

class MyConv:
 @T.prim_func
 def conv2d(data: T.Buffer[(N, CI, H, W), "int64"],
 weight: T.Buffer[(CO, CI, K, K), "int64"],
 result: T.Buffer[(N, CO, OUT_H, OUT_W), "int64"]):
 T.func_attr({"global_symbol": "conv2d", "tir.noalias": True})
 # impl
 for b, o, h, w in T.grid(N, CO, OUT_H, OUT_W):
 for kc, kh, kw in T.grid(CI, K, K):
 with T.block("A"):
 vb = T.axis.spatial(N, b)
 vc_o = T.axis.spatial(CO, o)
 vh = T.axis.spatial(OUT_H, h)
 vw = T.axis.spatial(OUT_W, w)
 vc_i = T.axis.reduce(CI, kc)
 vw_h = T.axis.reduce(K, kh)
 vw_w = T.axis.reduce(K, kw)

The outer loop all receives T.axis.spatial(), because we access each element in the output matrix element by element (spatially), without doing anything else. On the other hand, we see parameters in the innter loop receives T.axis.reduce(). Remember, each element in the output matrix is just the sum of element-wise multiplication of both the 2D convolutional kernel (1 by 3 by 3) and the corresponding area in the input matrix (1 by 3 by 3). Therefore, after the element-wise multiplication finishes, we need perform a reduction operation over all three axes. More concretely, we will sum up all elements in the row(K), column(K), and channel(CI): (1, 3, 3) -> (1)

@tvm.script.ir_module
class MyConv:
 @T.prim_func
 def conv2d(data: T.Buffer[(N, CI, H, W), "int64"],
 weight: T.Buffer[(CO, CI, K, K), "int64"],
 result: T.Buffer[(N, CO, OUT_H, OUT_W), "int64"]):
 T.func_attr({"global_symbol": "conv2d", "tir.noalias": True})
 # impl
 for b, o, h, w in T.grid(N, CO, OUT_H, OUT_W):
 for kc, kh, kw in T.grid(CI, K, K):
 with T.block("A"):
 vb = T.axis.spatial(N, b)
 vc_o = T.axis.spatial(CO, o)
 vh = T.axis.spatial(OUT_H, h)
 vw = T.axis.spatial(OUT_W, w)
 vc_i = T.axis.reduce(CI, kc)
 vw_h = T.axis.reduce(K, kh)
 vw_w = T.axis.reduce(K, kw)

 with T.init():
 result[vb, vc_o, vh, vw] = T.int64(0)
 # compute rule
 result[vb, vc_o, vh, vw] += data[vb, vc_i, vh+vw_h, vw+vw_w] * weight[vc_o, vc_i, vw_h, vw_w]

Recently, I was revisiting materials in Deep Learning. I need tools that generate diagrams easily. Drawing the graphs from scratch and upload them individually to the image hosting platform is a daunting process. This is when Mermaid comes into rescue. Now I can generate diagrams directly using Markdown. Here’s how to do it inside a Hugo site.

I use the etch theme, but this process should apply to all sites using Hugo. First, we create a new file /layouts/shortcodes/mermaid.html. We fill up mermaid.html with:

<script src="https://cdn.jsdelivr.net/npm/mermaid/dist/mermaid.min.js"></script>
<script>
 let isDark = window.matchMedia('(prefers-color-scheme: dark)').matches;
 let mermaidTheme = (isDark) ? 'dark' : 'default';
 let mermaidConfig = {
 theme: mermaidTheme,
 logLevel: 'fatal',
 securityLevel: 'strict',
 startOnLoad: true,
 arrowMarkerAbsolute: false,

 er: {
 diagramPadding: 20,
 layoutDirection: 'TB',
 minEntityWidth: 100,
 minEntityHeight: 75,
 entityPadding: 15,
 stroke: 'gray',
 fill: 'honeydew',
 fontSize: 12,
 useMaxWidth: true,
 },
 flowchart: {
 diagramPadding: 8,
 htmlLabels: true,
 curve: 'basis',
 },
 sequence: {
 diagramMarginX: 50,
 diagramMarginY: 10,
 actorMargin: 50,
 width: 150,
 height: 65,
 boxMargin: 10,
 boxTextMargin: 5,
 noteMargin: 10,
 messageMargin: 35,
 messageAlign: 'center',
 mirrorActors: true,
 bottomMarginAdj: 1,
 useMaxWidth: true,
 rightAngles: false,
 showSequenceNumbers: false,
 },
 gantt: {
 titleTopMargin: 25,
 barHeight: 20,
 barGap: 4,
 topPadding: 50,
 leftPadding: 75,
 gridLineStartPadding: 35,
 fontSize: 11,
 fontFamily: '"Open-Sans", "sans-serif"',
 numberSectionStyles: 4,
 axisFormat: '%Y-%m-%d',
 topAxis: false,
 },
 };
 mermaid.initialize(mermaidConfig);
</script>

This setup allows us to change Mermaid-generated diagrams’ theme based on the website’s current (light/dark) theme. This configuration is borrowed from the Setup.md from mermaid-js (except the theme part). You can find more information there about configuring mermaid.

You can also do this in /partials, but it will slow down the loading time because the mermaid js file is always loaded, regardless whether you are actually using mermaid.

Next, we add the follow lines to the file /layouts/shortcodes/mermaid.html:

<center>
<div class="mermaid">
 {{.Inner}}
</div>
</center>

Feel free to remove the <center> tag if you want to customize the diagram’s layout. And… we are done!

Here is an example sequenceDiagram. You should see that this diagram will adjust its theme accordingly based on light/dark mode. We use the example code from mermaid doc (just uncomment mermaid in the shortcode {{/*< mermaid >*/}}):

{{/*< mermaid >*/}}
sequenceDiagram
 participant Alice
 participant Bob
 Alice->>John: Hello John, how are you?
 loop Healthcheck
 John->>John: Fight against hypochondria
 end
 Note right of John: Rational thoughts <br/>prevail!
 John-->>Alice: Great!
 John->>Bob: How about you?
 Bob-->>John: Jolly good!
{{/*< /mermaid >*/}}

This diagram will adjust its theme based on light/dark theme. You can find more features from the Mermaid website.

Let’s say we want to classify an input text \(y\) and give it a label \(x\). Formally, we want to find:

\[ \textrm{argmax} P(x | y) \]

By Bayes’ rule this is the same as

\[ \textrm{argmax} \frac{P(y|x)P(y)}{P(x)} \]

Suppose we have five documents as training data and one document as the input as testing data. Our objective is to give a label to the test sentence.

Let’s define the probability of class as (\(N\) is the total number of classes)

\[ p(x) = \frac{count(x)}{N} \]

and the probability of a word appearing given a class label (total number of vocabs)

\[ p(w_i|x) = \frac{count(w_i,x) + 1}{count(x) + |V|} \]

The conditional probabilities for \(p(w_i|y)\) is

Now, we want to find out which language label should we assign the sentence “Chinese Chinese Chinese Tokyo Japan”. This is the same as asking which labels (\(x\))) should we pick so that \(P(W|x)P(x)\) yields the greatest value. Mathematically, we want to find out where the gradient of the function \(P(W|x)P(x)\) is flat.

If we label the sentence as j (Japanese), we have \(P(j | d_5) \propto \frac{1}{4}\cdot (\frac{2}{9}^3)\cdot \frac{2}{9}\cdot \frac{2}{9} \approx 0.0001\). If we calculate \(P(c|d_5)\), we get 0.0003, which generates the largest value for \(P(x | y)\).

This is a guide on setting up Megatron-LM with FastMoE. Megatron is a transformer developed by the Applied Deep Learning Research team at NVIDIA. FastMoE enables PyTorch support for the Mixture of Experts (MoE) models. We use the FastMoE layer to replace the MLP layers in the transformer language model.

Prerequisites

Docker

We recommend using one of NGC’s recent PyTorch containers. The Megatron-LM repo uses pytorch:20.12-py3. We pull the image with:

docker pull nvcr.io/nvidia/pytorch:20.12-py3

Note: it’s possible to use the official PyTorch image. However, there are a few dependencies missing, which requires manual installation. Also, PyTorch with versions greater than 1.8 seems to have problem during forward passing so we don’t use the official PyTorch image here.

After the image is pulled successfully, we want to start a container. The NGC site contains instructions on how to start a docker image. We use the following script:

docker run --gpus all -it --rm --ipc=host -v /home/edwardhu/:/home/edwardhu/ --name pytorch-moe <image_id>

Note: we might encounter problems before starting up the docker container. Make sure we set the GPG and remote repo for the nvidia-docker2 package on the host and install required packages:

distribution=$(. /etc/os-release;echo $ID$VERSION_ID) \
 && curl -s -L https://nvidia.github.io/nvidia-docker/gpgkey | sudo apt-key add - \
 && curl -s -L https://nvidia.github.io/nvidia-docker/$distribution/nvidia-docker.list | sudo tee /etc/apt/sources.list.d/nvidia-docker.list
sudo apt-get update
sudo apt-get install -y nvidia-docker2
sudo systemctl restart docker

Set up FastMoE

After we spin up the container, we clone the fastmoe repo and enter project. There is a setup.py file in the root of the project. Then we execute:

USE_NCCL=1 python setup.py install

to install FastMoE. For some reason, there is a compilation error saying that broadcastUniqueNCCLID(&ncclID)’s definition can not be found. We see there is a condition check right above the error function:

#if defined(TORCH_VERSION_MAJOR) && (TORCH_VERSION_MAJOR > 1 || \
 (TORCH_VERSION_MAJOR == 1 && TORCH_VERSION_MINOR >= 8))

For some reason, the check failed despite the container has PyTorch version 1.8.0a0+1606899. According to the author, the if macro was to deal with PyTorch’s API variance between v1.7.x and v1.8.x. For now, we simply comment out the if check and force the broadcastUniqueNCCLID(&ncclID, c10d::OpType::SEND, "fastmoe_nccl_comm", rank); to be used instead of the broadcastUniqueNCCLID(&ncclID) function:

//#if defined(TORCH_VERSION_MAJOR) && (TORCH_VERSION_MAJOR > 1 || \
// (TORCH_VERSION_MAJOR == 1 && TORCH_VERSION_MINOR >= 8))
 broadcastUniqueNCCLID(&ncclID,
 c10d::OpType::SEND,
 "fastmoe_nccl_comm",
 rank);
//#else
 //broadcastUniqueNCCLID(&ncclID);
//#endif
 ncclComm_t comm;
 NCCL_SAFE_CALL(ncclCommInitRank(&comm, getSize(), ncclID, rank));
 return comm;
 }
};

Finally, we need to download vocab file for later use since the Megatron repo doesn’t have one. Here, we use the vocab file from the SDNet repo. Feel free to use something else.

Megatron-LM Setup

After we set up FastMoE, we clone the Megatron-LM repo into the container. The FastMoE’s example guide on Megatron uses Megatron v2.2 release, so we need to choose the v2.2 tag in the Megatron repo.

Next, we follow the FastMoE’s guide on Megatron and apply the clip-grad-v2.2.path and fmoefy-v2.2.patch accordingly. Instructions on how to apply patches in Linux is easy to find, for example, here is one.

RACE Dataset

After setting up Megatron-LM, we download the RACE dataset for fine-tuning downstream tasks (RACE is used with BERT evaluation, the Megatron’s repo also has several other examples using GPT, here we stick to BERT). The Megatron repo also provides instructions on how to acquire these datasets for evaluation. For now, we just want to get the fine-tuning process up and running, without caring so much about the accuracy. Therefore, we don’t need to pre-train the BERT model just yet. After the dataset finished downloading, we simply need to decompress it.

Summury

The most important line to change a model to FastMoE style is through:

# Initialize FastMoE
 if args.fmoefy:
 from fmoe.megatron import patch_forward_step, patch_model_provider

 forward_step_func = patch_forward_step(forward_step_func)
 model_provider = patch_model_provider(model_provider)

More information can be found in the fmoefy patch file.

Dynamic Tensor Rematerialization (DTR) treats GPU memory as a large cache, where tensors can be evicted to save memory, and recomputed if needed later.

DTR’s eviction policy relies on the heuristic \(h\). The heuristic assigns a value \(h(t)\) to each resident tensor \(t\), approximating the cost of evicting the tensor. DTR evicts the tensor with the lowest cost based on the value of \(h\). \(h\) can factor in arbitrary metadata.

During every operator call in PyTorch, DTR intercepts the call and performs the following tasks:

In short, whenever we perform an operation, we first recursively re-calculate all the non-resident tensors the current operation depends on, while evicting tensors we don’t need until there are enough GPU space left. To decide which tensors to evict, DTR uses the tensor with the lowest value \(h\):

The heuristic \(h\) evicts tensors based on three properties: staleness, size, and compute cost. It evicts tensors that are: least recently used, takes large GPU memory space, and easy to recompute. \(H _{DTR}\) is computed as:

\[ h _{DTR}(s, m, c) (t) := \frac{c(t)}{m(t) \cdot s(t)’} \]

Recomputing an evicted tensor \(t\) may result in recomputing many more tensors that \(t\) recursively depends on. Thus, the paper proposes an improved heuristic to take the recursive recomputations into account (with more maintenance cost). These tensors are called evicted neighborhood \(e ^{*} (t)\).

\[ h_ {DTR-improved}(s, m, c) (t) := \frac{c(t) + \sum _{u \in e ^{*} (t)} c(u)}{m(t) \cdot s(t)’} \]

This heuristic captures the recomputation costs for all tensors that \(t\) recursively depend on.

Today marks the third month of my PhD life. Things finally start to become a little bit clearer. I finally have some potentially concrete ideas to work on.

Finding a research topic was the most difficult part. For several months, I was wondering around like a headless chicken, reading papers after papers: serverless, ML inference, compiler, pathlet routing, RDMA, you name it. The feeling of not having a topic was suffocating.

Talking to other people, especially people not from my own research areas, is extremely beneficial. In fact, I was able to narrow down what I want to work on after discussions with a friend of mine who was working on NLP, an area complete outside of networking. Chatting with lab mates and collaborators are also extremely helpful. They usually would ask questions I would never have thought of, and save me from spending countless hours exploring cluelessly.

To me, current system research feels like application-driven. Many research projects are designed to address a very specific challenge faced in the application level. Thus, it is very likely to find an interesting system problem in a non-system conference like KDD or even ICLR.

No systems can provide fault-free guarantees, including distributed systems. However, failures in distributed systems are independent. It means only a subset of processes fail at once. We can exploit this feature and provide some degree of fault tolerance. The problem is, fault tolerance makes everything else much more difficult.

The most common fault models is the fail-stop. It means a process completely “bricks”. When a process fail-stops, no messages can emerge from this process any more. We also don’t know if this process will ever restart. In addition, we must account for all possible states of the faulty process, including unsent messages in the process’s queue. On the other hand, it’s important to point out a process that takes a long time to respond is indistinguishable from a fail-stop. The intuition is such processes and the faulty ones may take an unknown amount of time before message emerge.

We use an example here to illustrate how and why a system fails to provide fault-tolerance. We take a system that replicates data by broadcasting operations using logical timestamps. This system uses Lamport clock to update local clocks (our previous post on Lamport Distributed Mutual Exclusion explains how Lamport clock works). In short, we overwrite the value stored in a replica if an incoming message has later timestamp \(ts\).

This system is not fault-tolerant. Imagine when one replica receives a write (marked by red incoming “write”) request and then tries to write the value to other replicas. This replica then fail-stops right after it writes to one replica and never writes to the other replica. In this case, not all replicas see the writes, thus violating consistency.

The solution to this problem is quite simple: reliable atomic broadcast. Under atomic broadcast, all writes are all-or-nothing. It eliminates the possibility for a process to fail-stop amid broadcasting.

Now let’s take the above example and update it with additional requirements. Instead of overwriting existing values, we append writes to an array and want to ensure every replica has the same array eventually. The major difference is that replicas needs to wait for acks with higher timestamps before it can append to its array.

This system is also not fault-tolerant. If one replica fail-stops, others will wait forever on a write, because every replicas relies on acks with higher timestamps before committing the append.

Thus, we want to extend the atomic broadcast so that updates become ordered. Under ordered atomic broadcast, writes are all-or-nothing and everyone agrees on the order of updates. If we assume the system to be fully asynchronous, ordered atomic broadcasts are not possible: (1) we can’t guarantee termination under asynchrony; (2) we could lose order. Thus, we rely on the synchronous approach.

Under the synchronous assumption, we can safely say a process fails after waiting for time \(t _{fail}\), where \(t _{fail} = 3 t _{msg} + 2 t _{turn}\). Here, \(t _{msg}\) is the message transfer latency, and \(t _{turn}\) is the max time to respond to a message.

To see why \(t _{fail}\) is calculated this way, we use the following example to explain the process:

Imagine process \(p\) sends a message to \(q\) and waits for an ack from \(q\). Before \(q\) is able respond with the ack, it somehow crashes. The max time taken for \(p\) to see an aco from \(q\) would be two message transfer time plus the execution time by \(q\), which is \(2t _{msg} + t _{turn}\). We add \(t\) to indicate the elapsed time when \(p\) sends the request.

Now imagine \(q\) is able to broadcast a request right before it fails. Later, another process is able to forward this request back to \(p\). Then \(p\) needs to wait for three message transfer time plus two message processing time before it can assume that it will no longer receive message from \(q\).

Under the synchronous assumption, ordered reliable atomic broadcast works as follows:

• When a client send a request to process \(p\), the process records logical time \(r _l(p,p)\) and physical time \(r _{t}(p,p)\). Then it broadcast the request.
• When process \(p\) receives a message \(m\), and if message \(m\) contains previously unseen timestamp \(t_m\), then we record the logical time we see message \(m\) at \(p\), denoted as \(r_l(p, p_m)\) as well as the physical time \(r _t(p, p_m)\). Then we broadcast the request. Finally, we send an ack back to the originator \(p_m\) without updated timestamp.
• When process \(p\) receives a message \(m\), \(p\) updates \(t _l(p, p_m)\). It means we update \(p\)’s notion of the latest timestamp of another process who just acked.
• Process \(p\) sets another process \(q\) as “failed” (denoted by \(f(p, q)\)) if \(t _l(p, q) \leq r _l(p, p’) < +\infty\) and \(t _t < r _t(p, p’) + t _{fail}\). In short, it means if we broadcast message and don’t receive any response after time \(t _{fail}\), and our last recorded logical time of process \(q\) is before our broadcast, then we know process \(q\) must have failed.
• Then we perform updates when for all \(q \neq p\), \(r _l(p,p) < r _l (p, q)\) (meaning everyone else’s request time is later than mine) and \(t _l(p,q) > r _l(p,p) \lor f(p, q)\). Intuitively, it means we only perform updates when we receive message from other processes after our broadcast, and when we think other processes’ timestamps are after us, or when they have all failed.

In a distributed system, eventual consistency provides a weak guarantee that data updates will be reflected in all nodes eventually. However, the downside of eventual consistency is that clients could potentially observe awkward intermediate states. For example, appending numbers to a client may result in states like [10], [10,13], [10,12,13].

Therefore, we need stronger consistency guarantees, which is easier to reason about. These consistency models provide various degree of consistency guarantees. However, it’s not always feasible to provide the strongest consistency guarantee. Usually, one needs to trade off consistency for availability and partition resilience (CAP theorem). Many contents here are attributed to Prof. Ken McMillan.

Global Consistency

The most primitive notion of consistency is global consistency. It means we have some history of events that is totally ordered.

It is (globally) consistency if it respects the intended sequential semantics of the events.

– Kenneth McMillan

Take read/write as an example, we have a sequence of write operations to the same memory location \(12\) at various timestamps, and we want to read values from the this location:

\[ \texttt{write}(0, 12, 2) \rightarrow \texttt{write}(1, 12, 3) \rightarrow \texttt{read}(2, 12, 3) \]

If we have global consistency, every read at a given memory location \(x\) will yield the most recently written value to \(x\).

In reality, it’s impossible to implement a global clock in a distributed system. Therefore, no node can observe the entire history of ordered events, making global consistency hard to implement.

Linearizability

In essence, linearizability is an approximation of global consistency. The difference is linearizability is based on logical time, as opposed to physical time used in global consistency. It means we don’t care in what order the event occur physically. We just want the ordering of events to be consistent to what we know about time, and what we know about time is based on causality.

Linearizability has two assumptions:

• Clients don’t have shared clock, but are able to send messages to each other. In other words, we want to create an illusion of global consistency by causality.
• If an event \(e_1\) ends before another event \(e_2\) begins in physical time, then \(e_1\) happens-before \(e_2\). We define the happen before relationship as \(hb(e_1, e_2)\). In simpler terms, is it possible for us to assume a causal connection between two events?

Take the following scenario as an example. We can say \(hb(e_1, e_2)\) holds because we can establish a causality relation between these two events. We are able to assume \(P_1\) sent a message \(m_1\) to \(P_2\), which caused the execution of \(e_2\).

Here is another example. Here, we can not establish a causal connection between \(e_1\) and \(e_2\) because we can not assume \(m_1\) caused the execution of \(e_2\)

To say a set of events, denoted as \(E\), is linearizable, the following conditions must be met:

• There exists a total order \(<_{lin}\) over events \(E\) s.t.
  • \((E,\ <_{lin})\) is globally consistent.
  • \(hb(e_1, e_2) \rightarrow e_1 <_{lin} e_2\)

In other words, a set of event \(E\) is linearizable if it respects the happen-before relationship, and is totally ordered.

Let’s look at one example. Suppose we have two processes \(P_1\) and \(P_2\). \(P_1\) writes 1 to location 0, and later reads from 0 and gets 1. \(P_2\) writes 2 to location 0 before \(P_1\) finishes its write.

These events are linearizable. We can order these three events as:

\[ \texttt{write}(1, 0, 2) \rightarrow \texttt{write}(0, 0, 1) \rightarrow \texttt{read}(0, 0, 1) \]

We know \(\texttt{write}(0, 0, 1)\) happens before \(\texttt{read}(0, 0, 1)\). The read gets the most recently written (not physical time, but causality) value, satisfying global consistency. Therefore, these events are linearizable.

Here is another example showing events that are not linearizable.

No matter how you order these four events, there will always be a contradiction. For example, \(rd(0,0,1)\) happens after \(wr(1,0,2)\) and \(wr(0,0,1)\). In order to satisfy global consistency requirement (reading the most recently written value), we must order these three events as

\[ wr(1,0,2) \rightarrow wr(0,0,1)\rightarrow rd(0,0,1)\rightarrow\ ? \]

However, \(wr(0,0,1)\) happens before \(rd(1,0,2)\), so \(rd(1,0,2)\) must be put after \(wr(0,0,1)\), but that way the most recently written value would be 1 and it would be impossible to read value 2, thus violating global consistency.

Commit Points

A different and perhaps easier way of thinking linearizability is using commit points. We say a set of events \(E\) is linearizable if every event can be assigned a physical commit time \(t_e\) such that:

• \(t_e\) occurs during the execution of an event \(e\).
• \((E,\lt _{lin})\) is globally consistent, where \(e < _{lin}\ d\) iff \(t_e < t_d\)

The following picture presents a scenario where we set three commit points on three write/read operations.

We know these events are linearizable because the three commit points we picked respects the \(\lt_{\textrm{lin}}\) relationship. The commit point \(wr(0,0,1)\) is set after the commit point for \(wr(1,0,2)\) and we know \(wr(1,0,2)< _{lin}wr(0,0,1)\).

Sequential Consistency

We can relax the requirement of linearizability even more, which leads us to sequential consistency. Sequential consistency (Lamport) is based on slightly different assumptions compared to linearizability:

• Assume clients don’t send messages to each other
• \(hb _{sc}(e_1, e_2)\) only holds if \(e _1\) executed before \(e _2\) in the same process.

These assumptions indicates each process doesn’t know the relative order of operations happening on other processes. Thus, we don’t have happen-before arc between processes.

Take the following example:

We know these events meets sequential consistency by the following order. The reason is that we can’t say \(hb_{sc}(wr(0,0,1), wr(1, 0, 2))\) must hold. This example would not be linearizable because \(wr(0,0,1)\) happens before \(wr(1,0,2)\).

\[ wr(1, 0, 2) \rightarrow wr(0,0,1) \rightarrow rd(0,0,1) \]

Take another example that is not sequentially consistent:

For \(rd(0,0,2)\) to be true, it must be that \(hb_{sc}(wr(0,0,1), wr(1,0,2))\) holds; for \(rd(1,0,1)\) to be true, iut must be that \(hb_{sc}(wr(1,0,2), wr(0,0,1))\) holds. Now we have a circle of ordering constraint, thus reaching a contradiction.

Causal Consistency

Causal consistency is an even weaker consistency model compared to sequential consistency. However, unlike all the consistency models we discussed before, causal consistency only applies to read/write operations. In causal consistency model, we define a causal order on those read/write operations such that read operations must see writes in order that respects causality.

Precisely, we define a reads-from map, denoted as \(RF\). \(RF\) of a read event \(e\) is going to produce the write operation that gave me the read value (there will be ambiguity if there are two writes writing the same value). For example, \(RF(rd(1,0,2))\) will produce the value \(2\), which is equal to the value written by a write operation \(wr(0,0,2)\). Putting \(RF\) in formal terms:

\[ RF(rd(p,a,v)) = wr(p’,a’,v’) \rightarrow a=a’ \land v = v' \]

In addition, \(hb_{RF}\) is the least transitive relation such that:

• \(hb_{SC}(e, e’) \rightarrow hb_{RF}(e,e’)\)
• \(RF(e’) = e \rightarrow hb_{RF}(e,e’)\). It means whoever gave me the value must happen before me, which represents a notion of causality.

We say a set of events \(E\) is causally consistent if there exists a \(RF\) map for \(E\) such that:

• For all reads \(e\in E\), there is no write \(e’ \in E\) such that \(hb_{RF}(RF(e),e’)\) and \(hb_{RF}(e’,e)\) have the same address.

In layman’s term, it says that if a write operation \(e\) causes us to read a value \(x\), it can’t be that there is another write operation \(e’\) that happens after \(e\) and writes some value to the same address. Because if there is such a write operation, then \(RF\) will produce write operation \(e’\) instead of \(e\).

Take a previous example here:

These events are causally consistent because \(RF(rd(0,0,1)) = wr(0,0,1)\) and \(RF(rd(1,0,2)) = wr(1,0,2)\). Thus \(hb_{RF}(wr(0,0,1), rd(0,0,1))\) and \(hb _{RF}(wr(1,0,2), rd(1,0,2))\). We also know we can’t say \(hb _{SC}(wr(0,0,1), wr(1,0,2))\) because sequential consistency assumes no communication between processes. Therefore, \(hb _{RF}(wr(0,0,1), wr(1,0,2))\) doesn’t hold, and we can safely say these events are causally consistent.

Let’s look at another example:

This is because \(RF(rd(2,0,3)) = wr(0,0,3)\). However, there is a write operation \(wr(0,0,1)\) happening after \(wr(0,0,3)\) that write 1 to location 0. Therefore, it can’t be that \(wr(0,0,3)\) causes \(rd(2,0,3)\) because \(wr(0,0,1)\) interferes and creates a contradiction. The easiest way to detect whether a set of events is causally consistent is to see if there is a circle of dependencies.

S3 Strong Consistency

A consistency model widely used in production systems is the S3 consistency used in Amazon S3 storage service. The S3 consistency models holds:

• if \(hb(w_1, w_2)\) and \(hb(w_2, r)\), then \(RF(r) \neq w_1\)
• Two reads must agree on the order of writes that happen before both reads.

Here is an example that is causally consistent, but not S3 consistent:

The reason is \(rd(1,0,2)\) sees write options as \(wr(0,0,1) \rightarrow wr(1,0,2)\) and \(rd(0,0,1)\) sees \(wr(1,0,2)\rightarrow wr(0,0,1)\).

However, with slight adjustment to the example, we have S3 consistency.

The reason is because \(hb(wr(1,0,2),rd(0,0,2)\) doesn’t hold. So even if \(rd(1,0,2)\) sees write options as \(wr(0,0,1) \rightarrow wr(1,0,2)\) and \(rd(0,0,1)\) sees \(wr(1,0,2)\rightarrow wr(0,0,1)\), only \(wr(0,0,1)\) happens before both reads, thus they would agree on the ordering of writes.

Summary

The consistency models discussed are only a tip of the iceberg. In fact, different storage service providers usually provide different consistency models. This may result in vendor lock-in because applications designed for one storage system may fall apart when deployed to another due to varying consistency implications.

Normally, having consistent event ordering in a distributed system is hard because we have no common clock. Since we don’t have a common clock to measure with, we rely on logical properties of time in the absence of clock. Here we use causality replation between events.

In essence, Causality indicates a clock \(C\) is map from events to time satisfying: \(e\rightarrow e’\) implies \(C(e) < C(e’)\)

We can synthesize a clock by a simple protocol, usually referred as scalar clock or Lamport clock:

• Each process \(p\) has a local clock \(C(p)\).
• A message send by a process is stampled with the its corresponding local clock.
• On receiving \(M\), set the process’s local clock to be \(max(C(p), C(M)) + 1\).

This will give us a consistent total order of events in a distributed system.

Let’s take Lamport distributed mutual exclusion (DME) as an example. We use scalar clock to agree on the order of access to critical sections. Each process broadcasts a request with its local clock time. Receiver stores the request time and responds with its update local time (\(max(C(p), C(M)) + 1\)).

A process can only enter critical section given the condition \(W\) is met: \(W \equiv \forall q \neq p,\ t(p,q) > r(p,p) \land r(p,p) < r(p,q)\). \(t(p, q)\) represents the latest time received by \(p\) from \(q\). \(r(p, q)\) is the request time received by \(p\) from \(q\) or \(+\infty\). Intuitively, it says if a process’s request time is smaller than all repsonses time and the process’s request time is smaller than all the other request time, then this process is the first one to send out the request and thus should enter critical section.

The reason why this protocol works is illustrated below:

When \(p_1\) sends a request at timestamp 2 and gets a repsonse with timestamp 3, we know \(p_1\) has the greatest clock value and \(p_0\) will update its own clock based on the timestamp sent from \(p_1\). Now \(p_1\) sees the response message from \(p_0\) with timestamp 3, it knows any request from \(p_0\) must have already been received, because the network channel is ordered and any request sent by \(p_0\) already arrived before the response with timestamp 3.

To see Lamport DME in action, we use Ivy to specify the protocol. The source file is borrowed from Ken’s presentation. The code is annotated and self-explanatory:

#lang ivy1.8

# This is an implememtation of Lamport's distributed mutual excluson
# (DME) algorithm.

include order
include network

# We start the module with a 'global' section. This contaions the
# declarations of any resources that are used in common by all
# processes. These usually include:
#
# - Data types
# - Services, such as network services
# - Immutable global parameters, such as netwrok addresses
#
# We can't have mutable global variables, since processes, being
# distributed, don't have shared memory.
#

global {

 # Our first global data type is the type of host identifiers. We
 # will have one process for each value of this type. Host
 # identifiers take on integer values from `0` to `node_max`.
 # We create the host identifier type by instantiating the
 # `host_iterable` module. It has a parameter `max` that gives the
 # maximum value of the type (and is supplied at run time).

 instance host_id : iterable

 # Since we have three kinds of messages in our protocol, we define
 # an enumerated type for the message kind with three symbolic
 # values.

 type msg_kind = {request_kind,reply_kind,release_kind}

 # In addition, we use a sequence type to represent timestamps. The
 # `unbounded_sequence` template in the `order` library gives a
 # discrete totally ordered type with a least value `0` and a
 # `next` operator.

 instance timestamp : unbounded_sequence

 # Our messages are stucts with three fields: the message kind and the
 # host identifier of the sender and a timestamp. We order messages
 # according to the timestamp. This ordering is useful in the proof
 # of correctness.

 class msg_t = {
 field kind : msg_kind
 field sender_id : host_id
 field ts : timestamp
 # definition (M1:msg_t < M2:msg_t) = ts(M1) < ts(M2)
 }

 # A useful enumerated type to describe node state:

 type state_t = {idle,waiting,critical}

 # Finally we instantiate a network service via which our processes
 # will communicate. Here, `transport.net` is a template defined in the
 # `network` library that we included above. The template takes one
 # parameter, which is the type of messages to be sent. Our instance
 # of this template is an object called `net`.

 instance net : tcp.net(msg_t)
}


# After the global section, we introduce some distribtued processes.
# A process with parameters has one instance for each value of the
# parameters. In this case we have one parameter of type `host_id`
# which means there is one process in the system for each value of
# `host_id` in the range `0..host_id.max`. The parameter is named `self`.
# This means that the process can refer to its own host identifier by
# the name `self`.

process node(self:host_id) = {

 # A process usually begins by declaring an *interface*. This
 # consists of a set of *actions* that are either calls in from the
 # environment (exports) or calls out to the environment (imports).

 # Our action is an export `request`, which our client uses to
 # request to enter the critical section. It takes no parameters.

 export action request

 # Our second action is an import `grant`. This is a callback to
 # the client indicating that is is safe to enter the critical
 # section.

 import action grant

 # Our third action is an export `release`. This is called by the
 # client when exiting the critical section, indicating it is safe to
 # another process to enter.

 export action release



 common {
 specification {

 var client_state(H:host_id) : state_t

 after init {
 client_state(H) := idle;
 }

 before request(self:host_id) {
 require client_state(self) = idle;
 client_state(self) := waiting;
 }

 before grant(self:host_id) {
 require client_state(self) = waiting;
 require client_state(X) ~= critical;
 client_state(self) := critical;
 }

 before release(self:host_id) {
 require client_state(self) = critical;
 client_state(self) := idle;
 }

 }
 }

 implementation {

 # Next we declare per-process objects. Each process needs a socket
 # on network `net` in order to communicate. We declare the socket
 # here. The socket `sock` is an instance of the template `socket`
 # declared by the network service `net`.

 instance sock : net.socket

 # We also declare some local (per-process) types and variables.

 var state : state_t

 # We also keep track of the current timestamp

 var ts : timestamp

 # Each process maintains a 'request queue', which a map from host_ids to
 # the timestamp of the current request from that host, or `0` if none.

 var request_ts(X:host_id) : timestamp

 # This map records the highest timestamp of a reply received from
 # each host.

 var reply_ts(X:host_id) : timestamp

 # Having declared our variables, we initialize them. Code in an
 # `after init` section runs on initialization of the process. You
 # aren't allowed to do much here, just assign values to local
 # variables.

 after init {
 state := idle;
 ts := 0;
 request_ts(X) := 0;
 reply_ts(X) := 0;
 }

 # Now we come to the implementation code. Here we implement our
 # exported actions, if any, and also any callback actions from the
 # services we use (i.e., actions that these services import from
 # us).

 # We start with the `request` action. This builds a request message,
 # appends it to the request queue, and broadcasts it. The action `broadcast` is
 # a local action (i.e., a subroutine) and is defined later.

 implement request {
 ts := ts.next;
 var outgoing : msg_t;
 outgoing.kind := request_kind;
 outgoing.sender_id := self;
 outgoing.ts := ts;
 broadcast(outgoing);
 request_ts(self) := ts;
 state := waiting;
 # BUG: should check waiting condition here, if host_id.max = 0
 }

 # Next we implement the callback `recv` from our network socket,
 # indicating we have an incoming message. This is called
 # `sock.recv`. It gives us as input parameters the network address
 # of the sending socket (not useful here) and the incoming
 # message.


 implement sock.recv(src:tcp.endpoint,incoming:msg_t) {

 # debug "recv" with self = self, src = src, msg = incoming;

 # First, we update out timestamp to reflect the incoming
 # message.

 ts := timestamp.max2(incoming.ts,ts).next;

 # We partly construct an outgoing message

 var outgoing : msg_t;
 outgoing.sender_id := self;
 outgoing.ts := ts;

 # What we do here depends on the kind of message.

 # When we receive a `request` message, we put it on our request queue,
 # and return a reply message to the sender.

 if incoming.kind = request_kind {
 outgoing.kind := reply_kind;
 request_ts(incoming.sender_id) := incoming.ts;
 unicast(outgoing,incoming.sender_id);
 }

 # When we receive a `release` message, the sender's request
 # must be at the head of our queue. We dequeue it.

 else if incoming.kind = release_kind {
 request_ts(incoming.sender_id) := 0;

 }

 # On a reply, we update the highest timestamp received from
 # this sender. Because of in-order devlivery, the timestamps
 # are received in increasing order, so the incoming one must
 # be the greatest so far.

 else if incoming.kind = reply_kind {
 reply_ts(incoming.sender_id) := incoming.ts;
 }

 # Having proceesed the incoming message, we might now be able
 # to enter our critical section. We do this if:
 #
 # - We are in the waiting state
 # - Our request message has the least timestamp in lexicographic order
 # - Every host has sent a reply later than our request

 # debug "waiting" with self = self, rq = request_ts(X), ts = reply_ts(X);

 if state = waiting
 & forall X. X ~= self ->
 (request_ts(X) = 0 | lexord(request_ts(self),self,request_ts(X),X))
 & reply_ts(X) > request_ts(self)
 {
 state := critical;
 grant;
 }
 }

 implement release {
 ts := ts.next;
 request_ts(self) := 0;
 var outgoing : msg_t;
 outgoing.sender_id := self;
 outgoing.ts := ts;
 outgoing.kind := release_kind;
 broadcast(outgoing);
 state := idle;
 }

 # At the end, we have definitions of internal (non-interface)
 # actions (in other words, subroutines) and functions (i.e., pure
 # functions).

 # This function takes two timestamp-host_id pairs and determines
 # whether (X1,Y1) < (X2,Y2) in lexicogrpahic order.

 function lexord(X1:timestamp,Y1:host_id,X2:timestamp,Y2:host_id) =
 X1 < X2 | X1 = X2 & Y1 < Y2


 # The action `unicast` sends a message to just one process.
 # To actually send a mesage to a socket, we call the `send` action
 # of our socket, giving it the receiving socket's network address
 # and the message to be sent. Notice we can get the network
 # address of process with identifier `idx` with the expression
 # `node(idx).sock.id`. This might seem odd, as we asre asking for
 # the local state of an object in another process. This is allowed
 # because the network addresses of the sockets are immutable
 # parameters that are determined at initialization and are
 # provided to all processes.

 action unicast(outgoing:msg_t, dst_id : host_id) = {
 # debug "send" with dst = dst_id, msg = outgoing;
 sock.send(node(dst_id).sock.id,outgoing);
 }

 # Action `broadcast` sends a message to all processes with
 # identifiers not equal to `self`. We use a 'for' loop to
 # iterate over the type `host_id`. The 'for' construct defines
 # two variables:
 #
 # - `it` is an 'iterator' of type `host.iter`
 # - `dst_id` is the value of the type the iterator refers to
 #
 # The reason we do it this way is the the finite subrange type
 # `host_id` has no value the is 'past the end' of the type, so
 # you can't write a traditional 'for' loop over this type. The
 # iterator type, however, does have a value corresponding to
 # 'past the end'.

 action broadcast(outgoing:msg_t) = {
 for it,dst_id in host_id.iter {
 # do not send to self!
 if dst_id ~= self {
 unicast(outgoing, dst_id);
 }
 }
 }
 }
}

# To compile and run with 3 nodes:
#
# $ ivyc lamport_mutex.ivy
# $ ivy_launch host_id.max=3
#
# To test:
#
# $ ivyc target=test lamport_mutex.ivy
# $ ivy_launch host_id.max=3
#
# Bounded model checking:
#
# TODO: As usual, we need the assumption that all endpoint id's are
# distinct.

axiom node(X).sock.id = node(Y).sock.id -> X = Y

# This says to try bounded model checking up to 20 steps (but Ivy
# won't actually get that far). The second parameter say to unroll the
# loops three times. This means that BMC ignores all executions in
# which a loop is executed more than three times. We need this because of
# the loop in `node.broadcast`

attribute method = bmc[20][3]

# Try adding a bug and see if you can find it with testing and bmc. Change
# this definition above:
#
# function lexord(X1:timestamp,Y1:host_id,X2:timestamp,Y2:host_id) =
# X1 < X2 | X1 = X2 & Y1 < Y2
#
# to this:
#
# function lexord(X1:timestamp,Y1:host_id,X2:timestamp,Y2:host_id) =
# X1 <= X2 | X1 = X2 & Y1 < Y2
#
# This mistake could allow two nodes with requests with the same timestamp
# to enter the CS at the same time. Here's a counter-example produced
# by BMC (it takes a while!):
#
# > node.request(1)
# > node.request(0)
# > node.sock.recv(0,{tcp.endpoint.addr:...,tcp.endpoint.port:...},{msg_t.kind:request,msg_t.sender_id:1,msg_t.ts:1})
# > node.sock.recv(1,{tcp.endpoint.addr:...,tcp.endpoint.port:...},{msg_t.kind:request,msg_t.sender_id:0,msg_t.ts:1})
# > node.sock.recv(1,{tcp.endpoint.addr:...,tcp.endpoint.port:...},{msg_t.kind:reply,msg_t.sender_id:0,msg_t.ts:2})
# < node.enter_cs(1)
# > node.sock.recv(0,{tcp.endpoint.addr:...,tcp.endpoint.port:...},{msg_t.kind:reply,msg_t.sender_id:1,msg_t.ts:2})
# < node.enter_cs(0)
# lamport_mutex_save.ivy: line 137: error: assertion failed

Before we jump into writing specifications in a distributed setting, we first define what a specification is. I take the definition from the magnificent Ken McMillan: a specification is a statement.

A statement describes an abstract view of a program. The view itself is often at an interface, which hides or abstracts internal states. A specification is stated in terms of two elements:

• Assumption: properties of the environment the system relies on
• Guarantee: properties that most hold if the assumption(s) is met

The way we write specifications is through an abstract program that observes or monitors all program events. This abstract program is able to remember the execution history of program being monitored, and decides, at any given moment, whether an action is allowable according to the specification.

One way to implement this abstract monitor program is to use guarded command form:

• Let \(A\) be a set of program actions
• An event \(e(x_1,\ …,\ x_n)\) is an action \(e\in A\) with parameter values \(x_1,\ …,\ x_n\) of the right types for \(e\).
• Let \(S\) be a set of states and \(s_0 \in S\) be the initial state.
• Guarded command set \(G\) is specified as:

\[e(V):\ \gamma (S,V) \rightarrow {S := \tau(S, V)}\]

It means if a guarded command \(\gamma\) determines a given event \(e\) satisfies certain specifications with parameter \(V\) under state \(S\), then we accept the code and then deterministically update the state with a function \(\tau\).

The observation \(E\) of system is going to be a finite sequence of events, which corresponds to the system behavior, denoted as \(e_0(V_0)…e_{n-1}(V_{n-1})\). A run of \(E\) is a state sequence \(s_0\ …s_n\) such that for \(i\in 0\ … n- 1\), \(\gamma(s_i, V_i)\) is true and \(s_{i+1} = \tau(s_i, v_i)\). Observation \(E\) is accepted by the specification iff it has a run. We can test whether an observation is accepted by just executing the guarded commands. In layman’s term, if all guarded commands accepts the their corresponding event at a given time, then the sequence events must satisfy our specification and should be accepted.

Now let’s replicated file as an example. Out first informal attempt to the specification for “append” operation would be:

• Assumption: network is ordered and non-duplicating
• Guarantee: if no further append requests, eventually replicas are equal

However, the problem with this specification is that this is a liveness property, meaning that we can’t practically test such property by observing a finite sequence of events. Therefore, we resort to a different safety specification we can test:

• If all sent messages are delivered, the two replicas are identical.

Now we convert liveness to safety by explicitly defining the moment hen the eventuality should hold.

Liveness property means a good thing eventually happens. A liveness property can be refuted by finite execution. Safety property means a bad thing never happens. A safety property can always be refuted by a finite execution.

To see how replicated file specification plays in action, we use the example given in Prof. McMillan’s presentation. The code is written in Ivy and is pretty self-explanatory. In this demo we only have two processes.

To install Ivy, simply execute virtualenv ivyenv && source ivyenv/bin/activate && pip install ms-ivy. This is tested on Ubuntu 18.04 LTS and may vary slight on other distros.

#lang ivy1.8

include numbers
include collections
include network

global {
 alias byte = uint[8]
 instance file : vector(byte)
 type pid = {0..1}
 instance net : tcp.net(byte)
}

process host(self:pid) = {
 export action append(val:byte)
 import action show(content:file)
 instance sock : net.socket
 var contents : file

 after init{
 contents := file.empty;
 }

 implement append {
 contents := contents.append(val);
 sock.send(host(1-self).sock.id, val);
 show(contents);
 }

 implement sock.recv(src:tcp.endpoint, val:byte) {
 contents := contents.append(val);
 show(contents);
 }
}

Then we form our specification based on the guarantee that if all sent messages are delivered, the two replicas are identical. The specification is equivalent to the guarded command we’ve talked about earlier.

specification {
 var msg_count : nat

 after init {
 msg_count := 0;
 }

 after host.sock.send(self:pid, dst:tcp.endpoint, val:byte) {
 msg_count := msg_count + 1;
 }

 after host.sock.recv(self:pid, src:tcp.endpoint, val:byte) {
 msg_count := msg_count - 1;
 ensure msg_count = 0 -> host(0).contents.eq(host(1).contents);
 }
}

We wrote the above code into a file named append.ivy and we generate the testing code using ivyc target=test append.ivy. Then we run the code using ivy_launch append.ivy.

Interestingly, the program yields an error message:

`ivy_shell`; ./append "[[0,{addr:0x7f000001,port:49124}],[1,{addr:0x7f000001,port:49125}]]"
> host.append(1,251)
< host.show(1,[251])
< host.show(0,[251])
> host.append(1,46)
< host.show(1,[251,46])
> host.append(0,183)
< host.show(0,[251,183])
< host.show(0,[251,183,46])
< host.show(1,[251,46,183])
assertion_failed("append.ivy: line 49")
append.ivy: line 49: error: assertion failed

What happens is the program generates tests that randomizes message arrival times and we can see a delivered message may arrive after its target sends another message, therefore creating corrupted file contents.

Notice that here we are actually running on real network to find counter examples, the downside is the test may be arbitrary long depending on the randomized testing cases. Instead, we will use bounded model checking (BMC) to test if the specification is correct. This way we can reply purely on the logic of our specification instead of running on the real network. The Ivy checker uses Z3 Theorem Prover.

BMC construct a boolean formula that is satisfiable if and only if the underlying state transition system can realize a finite sequence of state transitions that reaches certain states of interest.

To tell Ivy using bounded model checking, we add the following lines to append.ivy:

axiom host(0).sock.id ~= host(1).sock.id

attribute method=bmc[10]

Executing ivy_check detailed=false append.ivy, we see an error message:

> host.append(1,80)
< host.show(1,[80])
> host.append(0,64)
< host.show(0,[64])
> host.sock.recv(0,{tcp.endpoint.addr:...,tcp.endpoint.port:...},80)
< host.show(0,[64,80])
> host.sock.recv(1,{tcp.endpoint.addr:...,tcp.endpoint.port:...},64)
< host.show(1,[80,64])
append.ivy: line 49: error: assertion failed

Sometimes BMC can help us find the error faster because it is systematically checking all possible actions. However, increasing the number of steps for the BMC can result in the exploration space growing exponentially, so we are going to use some combination of BMC and randomized test cases.