One of the biggest challenges that blockchain faces is the one of throughput. When new projects are being evaluated people often compare how many transactions per second it can run and how does it compare to Visa ( according to some sources it may vary from 1700 TPS to 4400 TPS ). It is value that none of the currently operating decentralized blockchains can achieve. One of the fundamental design choices that new projects may make is to build a DAG (directed acyclic graph) rather than linear chain (as it is done in Bitcoin or Ethereum). The idea behind building a DAG is that validators may build a blockchain "in parallel" (imagine multiple threads that originate from the same place, run in parallel but join at some point in the future to form a single thread again). One of the fundamental issues with this design is conflict resolution. What to do when there are multiple transactions that want to modify the same account? We can't apply changes from all of them blindly. This may lead to overdraws (or double spends). This problem is not trivial and there are potentially multiple ways to solve it. This document presents how we address this in the CasperLabs platform.
Let's consider the execution of transactions included in a single block. So we have a and a collection of transactions:
As part of the validation of block , any validator receiving this block has to execute all transactions so to calculate the global state after applying this block. In principle, all these transactions could be executed sequentially, which is the easiest approach and does not bring any problems. Unfortunately, it is also the slowest one.
Given the multi-core architecture of contemporary computers one is interested in exploiting all possibilities where things can be executed concurrently. In the case of transaction execution, we anticipate that vast majority of transactions are "independent" from each other, so their execution could be parallelized.
The approach we apply in execution engine is as follows:
We expect that blocks are marked as SEQ or PAR by their creator.
If a block is marked as SEQ, we execute all transactions sequentially.
If a block is marked as PAR, we assume these transactions are mutually independent, so we can execute them in parallel and then "merge" the resulting global state to reflect the final global state.
However along the parallel execution, some precautions must be taken to discover any possible violation of mutual independence of transactions rule. In such case we signal to the consensus layer that the badly marked block was found, so its creator may be punished for violation of the protocol.
In this chapter we formalize the intuitive concept of "mutual independent transactions". We explain how such a concept can be defined and we sketch the proof of its correctness.
Let GS denote the set of global states. So an element is just a fixed state of the memory of our "blockchain computer" (which implementation-wise corresponds to a map from keys to values, as was explained here):
A transaction t is an execution of a program that reads the global state and possibly changes it. So it may be represented as a function:
Caution: Hidden here are assumptions about what features a smart contract programmer can access inside a body of a smart contract. No non-deterministic function is available. In other words, the execution of a transaction is completely determined by the global state it is applied to and parameters of the contract.
Further, it is not true that we are interested in every possible functions . Really, we are only interested in computable functions, so functions implementable as Turing Machine programs, where the only extra feature is the access to our global state. Hence such programs are sequential by nature and every access to global state can be traced.
Formally, by we understand the following set:
Consider two transactions and a fixed global state . To express that and are mutually independent in the context of gs, we just want to say that it does not matter in which order we apply them to gs, because the final result is going to be the same anyway.
Formally, we say that transactions and are commutative in the context of global state ,
Obviously, this definition can easily be extended to a finite set of transactions: we say that a set is commutative in the context of global state iff for all permutations :
For a given set of transactions, unfortunately, checking their coherence is rather non-trivial and the cost of such checking may easily outweigh any gain in performance achieved by parallel execution of transactions. So, we are only interested in performing these checks if they are both possible and efficient.
A pretty straightforward check algorithm can be established by storing a trace of all accesses to the global state done by a transaction, and then checking for a possible conflict by comparing traces.
For tracing the execution of transactions, we extend the read-write model with one additional case. Let's look for example at the addition operation:
Adding is commutative, but in the context of mutating global state, we want to see adding as a function of one variable. For example:
If we consider the sequence of transactions that want to access the storage:
then it is easy to notice, that we can shuffle consecutive readers and consecutive adders, but not writers. Also swapping a reader with a writer (or reader and adder) is going to be a problem.
The "adding" case can be actually generalized. We can change the order of any operations that come from a commutative Monoid (like integers with adding, integers with multiplication or hash maps with merging). We can generalize this even further, saying that apart from Read and Write operations, any commutative family of functions can be used, as long as we can easily recognize (while tracing) to which commutative family of functions given operation belongs.
Distinguished families of such commutative functions operating on Values are pre-selected and include most typical operations that we want to recognize as commutative:
storing key-value pair in a map
removing a key from a map
adding element to a set
removing elements from a set
Such a collection of selected commutative families of functions that are supported by the execution engine we will denote here as , or CF. So, using previously established notation for adding, we can recognize two example elements in that cover the integer addition and adding element of type to :
We define a of a transaction to be an ordered sequence of capturing subsequent accesses to the global state made by the program executing the transaction, once applied to a given :
Here, every is a pair: where
An example trace of execution could look like this:
We reduce such trace in two steps:
Grouping operations by key
Merging operations in every group, according to the following merging table:
Members of a commutative family commute with other members of the same family
Finally, the reduced execution trace of a transaction t can be represented as a function:
For a pair of transactions , , and their traces , we introduce the following way of checking if reduced traces commute:
where function is defined using following rules:
Theorem: If two transactions and have commuting reduced traces they commute. Formally:
Caution: the inverse theorem is not true, which can be observed in the following example.
Example: Transactions commute but their reduced traces don't.
Contract:val a = read(42)write(43, 1)
When reading above example contracts it's easy to see that transactions should be able to run in parallel (each of them modified different key). This is thanks to the fact that although transaction 1 reads from key 42 (which transaction 2 modifies) but it ignores its value. Unfortunately, we are not able to detect this by just pure analysis of execution traces and the reduced traces commutativity test will signal a potential conflict.
Lemma: Intuitively, only operations influence how the program executing the transaction operates. For two global states if the same transaction applied to created a different execution trace than when applied to then at some point of the trace there must be a operation where .
Assume that . We are going to prove:
This is to say that transaction is not affected by and so it operates following exactly the same storage access flow in both cases.
Let's assume the contrary is true:
Using lemma, this would mean that at some point of the trace there must be a operation where . Which is to say that some key k was modified by and the same key k is being read by . This, however, contradicts our assumption that and commute.
End of the proof.