Practical Smart Contract Shardingwith Ownership and Commutativity Analysis
George Pîrlea∗

Amrit Kumar

Ilya Sergey

National University of Singapore
Singapore
gpirlea@comp.nus.edu.sg

Zilliqa Research
United Kingdom
amrit@zilliqa.com

Yale-NUS College
National University of Singapore
Singapore
ilya.sergey@yale-nus.edu.sg

Abstract

1 Introduction

Sharding is a popular way to achieve scalability in blockchain
protocols, increasing their throughput by partitioning the setof transaction validators into a number of smaller committees, splitting the workload. Existing approaches for blockchain sharding, however, do not scale well when concurrent
transactions alter the same replicated state componentÐa
common scenario in Ethereum-style smart contracts.
We propose a novel approach for efficiently sharding suchtransactions. It is based on a folklore idea: state-manipulating
atomic operations that commute can be processed in parallel,with their cumulative result defined deterministically, while
executing non-commuting operations requires one to own
the state they alter. We present CoSplitÐa static program
analysis tool that soundly infers ownership and commutativity summaries for smart contracts and translates those summaries to sharding signatures that are used by the blockchain
protocol to maximise parallelism. Our evaluation shows thatusing CoSplit introduces negligible overhead to the transaction validation cost, while the inferred signatures allow
the system to achieve a significant increase in transaction
processing throughput for real-world smart contracts.

The idea of Nakamoto consensus (aka blockchain) has been
instrumental for enabling decentralised digital currencies,
such as Bitcoin [48]. The applications of blockchains have further expanded with the wide-spread adoption of smart contracts [62]Ðself-enforcing, self-executing protocols governing an interaction between several mutually distrusting parties. The Ethereum blockchain has provided a versatile framework for defining smart contracts as blockchain-replicatedstateful objects identified by their account numbers [65].
The open and decentralised nature of Nakamoto consensus comes at the price of throughput scalability. At a highlevel, in order for a sequence of transactions (so-called block)to be agreed upon system-wide, the system’s participants(so-called miners) have to validate those transactions, witheach miner executing them individually [4]. As a result,
the throughput of blockchain systems such as Bitcoin andEthereum does not improve, and even slightly deteriorates,
as more participants join the system: Bitcoin currently processes up to 7 transactions per second, while Ethereum’s
throughput is around 18 transactions per second. Even worse,
popular smart contracts may cause high congestion, forcing
protocol participants to exclusively process transactions specific to those contracts. This phenomenon has been frequentin Ethereum: in the past, multiple ICOs (Initial Coin Offering, a form of a crowdfunding contract) and games, such
as CryptoKitties, have rendered the system useless for any
other purposes for noticeable periods of time [14].

CCS Concepts: · Computing methodologies → Distributed programming languages.
Keywords: Smart Contracts, Static Analysis, Parallelism
ACM Reference Format:
George Pîrlea, Amrit Kumar, and Ilya Sergey. 2021. Practical SmartContract Sharding with Ownership and Commutativity Analysis. In
Proceedings of the 42nd ACM SIGPLAN International Conference on
Programming Language Design and Implementation (PLDI ’21), June
20ś25, 2021, Virtual, Canada. ACM, New York, NY, USA, 15 pages.
https://doi.org/10.1145/3453483.3454112

Sharding in Blockchains. One of the most promising
approaches to increase blockchain throughput is to split theset of miners into a number of smaller committees, so they
can process incoming transactions in parallel, subsequently
achieving a global agreement via an additional consensus
mechanismÐan idea known as sharding. Sharding transaction executions, as well as sharding the replicated state,
has been an active research topic recently, both in industry [23, 30, 39, 51, 60, 64, 67] and academia [1, 17, 36, 45, 66].
Many of those works focus exclusively on sharding thesimplest kind of transactionsÐuser-to-user transfers of digitalfunds,Ðwhich are paramount in blockchain-based cryptocurrencies, while ignoring sharding of smart contracts [36, 45,
66, 67]. Existing proposals tackling smart contracts impose∗ Work partially conducted while employed at Zilliqa Research.

Permission to make digital or hard copies of part or all of this work forpersonal or classroom use is granted without fee provided that copies are
not made or distributed for profit or commercial advantage and that copies
bear this notice and the full citation on the first page. Copyrights for thirdparty components of this work must be honored. For all other uses, contact
the owner/author(s).
PLDI ’21, June 20ś25, 2021, Virtual, Canada© 2021 Copyright held by the owner/author(s).
ACM ISBN 978-1-4503-8391-2/21/06.
https://doi.org/10.1145/3453483.3454112

1327

PLDI ’21, June 20ś25, 2021, Virtual, Canada

George Pîrlea, Amrit Kumar, and Ilya Sergey

heavy restrictions on contract-manipulating transactions,for instance, requiring the accounts of both the contract andits user to be assigned the same shard, or processing all suchtransactions in a specialised shard [17, 30, 39]. Other solutions assume a complex cross-shard communication protocol
to reconcile possible conflicts [23, 30, 51, 60, 64], or adopt a
contract design very different from Ethereum [1].
To the best of our knowledge, none of these approaches
allows for parallel sharded executions involving the same
smart contract. That is, none solve the mentioned congestion
problem in Ethereum, caused by highly-popular contracts.
In this work, we describe a novel approach for significantly increasing the throughput of blockchains for smart
contract-manipulating transactions. To achieve this, insteadof treating contract implementations as łblack boxesž (as doall the works mentioned above), we design a solution basedon PL techniques, specifically, on static program analysis.

leverage commutativity in user-defined replicated computations (e.g., smart contracts) have been made to date.
In this work, we present CoSplitÐa static analysis toolthat soundly infers both ownership and commutativity information from source code of smart contracts and translates it
to sharding signatures. The signatures are used, upon the deployment of a contract, to define a sharding strategy for thecontract-manipulating transactions via the following rules:• All transactions touching parts of a contract’s state owned
by a shard S must be executed in this shard;• Transactions executed in different shards are guaranteed
to commute. Their cumulative result can be obtained bymeans of łjoiningž their respective contributions in a way
prescribed by the sharding signature.
These two rules allow the system to enjoy a notion of consistency for parallel transaction executions adopted fromworks on the semantics of concurrent revisions [7, 8, 43]:
1. Potentially conflicting contract-manipulating transactions
will be executed in some globally-agreed order.
2. Commuting transactions can be executed in parallel, as
their effect does not depend on their order.
As we will discuss in Sec. 2, popular Ethereum-style contracts
often allow for a łlogical splitž of their state into disjointly
owned components, which is much more fine-grained thanassigning an entire contract to a single shard. This split
makes it possible to process transactions affecting thosecontracts in parallel in different shards, thus providing apractical solution to scale up the network throughput.

Our Approach. Why can user-to-user money transfers
be sharded efficiently without complex inter-shard communication, and how can we generalise (perhaps, conservatively)
this logic to shard arbitrary smart contracts?
Consider a transaction tx 1 that manifests a transfer of 10
units of some digital currency from the user 𝐴 to 𝐵, anda transaction tx 2 that states that 𝐴 transfers 20 units to 𝐶.
In order to ensure that 𝐴 does not double-spend, both tx 1
and tx 2 have to be executed in the same shardÐthe one thatowns 𝐴’s account and keeps track of 𝐴’s balance. However,neither 𝐵 nor 𝐶 need to be owned by 𝐴’s shard: as long as
tx 1 and tx 2 are validated within 𝐴’s shard, the positive deltas
to 𝐵 and 𝐶’s accounts can be simply broadcast through the
network, so their balances are increased accordingly withno extra inter-shard interaction.

B

A: -10
B: +10tx1

A

A: -20
C: +20tx2

C

D: -15
C: +15tx3

Our Contributions. The contributions of this work are:• Identifying logical state ownership and operation commutativity as enabling mechanisms for sharding Ethereumstyle contracts, and demonstrating adequacy of those notions for real-world Ethereum-style contracts (Sec. 2).
• A compositional static analysis that infers ownership andcommutativity signatures for contracts written in Scilla [57]and translates them to shard allocation strategies (Sec. 3).
• An implementation of the analysis and of the algorithm forderiving sharding strategies in the tool called CoSplit andan end-to-end integration of CoSplit with a productiongrade sharded blockchain protocol [45, 67] (Sec. 4). The
archived software artefact is publicly available [53].
• Evaluation of parallelism enabled by CoSplit-inferredsignatures, demonstrating a consistent increase in systemthroughput with increasing the number of shards (Sec. 5).

D

Now consider a transaction tx 3 , in which 𝐷 transfers 15 units
to 𝐶. Notice that it does not matter in which order tx 1 andtx 3 are going to be processed, as they commute: either of
their relative orderings will increase 𝐶’s balance by 35.
The notions of state ownership and operation commutativity have been central in a number of works dedicated toreasoning about deterministic parallelism and proving correctness of concurrent programs [19, 20, 22, 34, 40, 44, 50].
In those works, the ownership discipline determines whatparts of the shared state need to be manipulated sequentiallyby the same thread, while commutativity allows certain actions to be executed in concurrent threads in parallel, with adeterministic result. The virtues of commutative operations
have also been studied in the systems community for scaling concurrent software [3, 13, 52, 55] and achieving fasterconsensus in replication protocols [11, 37, 42, 47]. However,to the best of our knowledge, no attempts to automatically

2 Motivation and Key Ideas
2.1

Contract Usage in Ethereum

To motivate the design of our approach for sharding, we
first present the trends for smart contract usage in Ethereum.
Since there are over 700 million Ethereum transactions todate, processing all the execution traces is too computationally expensive. Therefore, we selected a random sample of1328

ERC20 Transfer Single Calls
Other Single Calls

Transfer
Single Call
Multi-CallOthers

80
60
40
20
0
0

0.2

0.4

0.6

Block number

0.8

1
·107

0

0.2

0.4

0.6

Block number

0.8

1
·107

Figure 1. Left: Ethereum transaction breakdown per type;the percentage distribution is averaged over 100K block periods. Right: breakdown of single-call transactions.
16,611 blocks, containing 1.1M transactions. The sample wascollected in January 2020 and includes transactions up to
block 9.25M, representing 0.17% of the total number of transactions up to that point and giving our measurements a 1%
margin of error at a 99% confidence level.1 As the left plot in
Fig. 1 shows, ordinary user-to-user transfers are on a solid
downward trend. Moreover, single-contract transactions takeup to 55% of the recent blocks in our sample.
In this work we focus on sharding single-contract transactions. The right plot in Fig. 1 shows the dominance of a
specific type of such transactions that represent token transfers in a special kind of contractÐERC20 token contracts [24].
ERC20 and other similar standardised contracts pose a big
bottleneck to the network throughput: each of them requires
sequential processing of all transactions that affect it.

1 contract ERC20 {2mapping (address => uint256) balances;3
mapping (address => mapping (address => uint256)) allowances;
4/* Main public functions */5function transfer(recipient, amount) {6_transfer(_msgSender(), recipient, amount);
7
return true;
8}
9function approve(spender, amount) {10_approve(_msgSender(), spender, amount);
11
return true;
12}
13
function transferFrom(sender, recipient, amount) {14_transfer(sender, recipient, amount);
15_approve(sender, _msgSender(),
16
allowances[sender][_msgSender()] - amount);
17
return true;
18}
19/* Auxiliary internal functions */20function _transfer(sender, recipient, amount) {21
balances[sender] = balances[sender] - amount;
22
balances[recipient] = balances[recipient] + amount;
23}
24
function _approve(owner, spender, amount) {25
allowances[owner][spender] = amount;26} /* More functions */ }Figure 2. A fragment of an ERC20 contract in Solidity.
tx1
balances

100

PLDI ’21, June 20ś25, 2021, Virtual, Canada

allowances

Percentage of transactions per type

Practical Smart Contract Sharding with Ownership and Commutativity Analysis

2.2 Towards Sharding an ERC20 Contract
Fig. 2 shows a fragment of the implementation of an ERC20
token contract [24] in Ethereum’s high-level language Solidity [25]. The contract’s replicated state is represented by
two mutable fields: the mapping balances that contains data
about the amount of tokens owned by token holders; and themapping allowances that captures the amounts of tokens authorised for third-party transfers by their holders. The state
manipulations are done by transactions initiated by users(aka senders) calling one of the functions: transfer for transferring tokens, approve for granting the transfer rights for acertain amount of tokens to a third party, and transferFrom
for transferring tokens on behalf of the user identified as
sender. The subtractions in lines 16 and 21 will fail if theapproved spender (resp. the sender) does not have enoughallowance, thus preventing double-spends.
The design of the ERC20 contract provides ample opportunities for shard-based parallelism. Consider the leftpart of Fig. 3 that shows a fragment of the mutable ERC20
state: the balances field mapping account addresses 𝐴ś𝐸(top part of each box) to the respective token balances (bottom part of the box), and allowances, which is a mapping

tx3

tx1

tx2

tx3 tx2

B

A

C

B

A

C

balB

balA

balC

balB

balA

balC

A

D

E

A

D

E

allAD

allAE

allAD

allAE

tx4

Legend:tx4transfertransferFrom

approve

Figure 3. Two ways to identify footprints of four ERC20transactions: via full affected state (left) and via state affectedby non-commuting operations (right).

from addresses (e.g., 𝐴) to mappings of amounts allowed
to transfer by third parties (e.g., 𝐷 and 𝐸) on their behalf.
Now consider the following four single-contract transactions accessing that state concurrently by invoking functions
from Fig. 2: tx 1 = transfer𝐴 (𝐵, 𝑣 1 ); tx 2 = transfer𝐶 (𝐴, 𝑣 2 );tx 3 = transferFrom𝐷 (𝐴, 𝐶, 𝑣 3 ); tx 4 = approve𝐴 (𝐸, 𝑣 4 ). Here,a subscript denotes the transaction sender’s address (accessed via _msgSender() in Fig. 2), while 𝑣𝑖 stand for various
non-negative amounts, whose exact value is not important.
All those transactions alter the contract state; the left part of
Fig. 3 shows their corresponding footprints, i.e., componentsof the state that they interact with. It is easy to see that thefootprints of, e.g., tx 1 and tx 4 are disjoint, thus, their effects
on the contract’s state commute. Therefore, assuming thesystem provides an operation to join (i.e., merge) updates

1 The Ethereum dataset and analysis are part of the archived artefact [53].

1329PLDI ’21, June 20ś25, 2021, Virtual, Canada

George Pîrlea, Amrit Kumar, and Ilya Sergey

on the łlogically disjointž state components, it should bepossible to execute, e.g., tx 1 and tx 4 in different shards.

2.3

Commutativity and State Ownership

It is common to reason about operation commutativity interms of action traces [13]. That said, our way of thinking is
inspired by the logical abstractions used for compositionalverification of heap-manipulating programs [9, 10, 50].
In our setup, we are interested in parallelising executionsof a family of single-contract transactions over a state-space
Σ of a contract, collectively represented by a function F𝑥 :
Σ → Σ. Here, 𝑥 denotes a vector of user inputs, i.e., specifying
which contract’s function to call, as well as its inputs. Twotransactions identified by different user inputs 𝑥 1 and 𝑥 2
commute iff for any state 𝜎, F𝑥 1 (F𝑥 2 (𝜎)) = F𝑥 2 (F𝑥 1 (𝜎)).
In order to enable parallelism, our goal is to identify a commutative, associative, and partial operation ⊎ : Σ → Σ → Σ,such that for any 𝜎1 , 𝜎2 and 𝑥, if F𝑥 (𝜎1 ) is defined (i.e., 𝜎1
contains at least the footprint of F𝑥 ) and 𝜎1 ⊎ 𝜎2 is defined,
then F𝑥 (𝜎1 ⊎ 𝜎2 ) = F𝑥 (𝜎1 ) ⊎ 𝜎2 . This equality is referred
to as action locality in the program logics literature [10],and, when it holds, it enables compositional program analyses [21] and concurrency specifications [44].2 The virtue ofF𝑥 ’s locality for our purposes becomes apparent by observing the following chain of equalities for 𝜎 = 𝜎1 ⊎ 𝜎2 when𝜎1 and 𝜎2 are such that F𝑥 1 (𝜎1 ) and F𝑥 2 (𝜎2 ) are defined:

Sharding Strategy 1: Disjoint State Ownership. Let us
formulate the constraints for parallel execution of the transactions tx 1 śtx 4 from Fig. 3, out of the knowledge that someof them commute, thanks to their footprint disjointness. We
will denote by Owns(S, {f1, . . . , f𝑛 }) an ownership constraint,
meaning that the shard S logically owns the contract’s statecomponents (fields or map entries) f1, . . . , f𝑛 and, thus, only
this shard may alter the values of those components by sequentially processing all the corresponding transactions.
Now consider two shards, S1 and S2 and the following
set of ownership constraints, where bal and all denote thecorresponding fields balance and allowances:
Owns(S1, {bal[𝐴], bal[𝐵], bal[𝐶], all[𝐴] [𝐷]}),(1)
Owns(S2, {all[𝐴] [𝐸]})
Clearly, S1 and S2 own disjoint portions of the contract’s
state, thus, it will be safe to assign transactions to shards as
S1 ↦→ {tx 1, tx 2, tx 3 } and S2 ↦→ {tx 4 }, obtain the final result
deterministically by merging their non-conflicting changes.
This sharding strategy scales for more shards with designatedownership of the contract’s components and larger numberof transactions with logically disjoint footprints.

F𝑥 1 (F𝑥 2 (𝜎)) = F𝑥 1 (F𝑥 2 (𝜎1 ⊎ 𝜎2 )) = F𝑥 1 (𝜎1 ⊎ F𝑥 2 (𝜎2 ))Sharding Strategy 2: Commutativity of Addition. Even
though transaction tx 2 modifies the component bal[𝐴], it
does so in a commutative fashion and, thus, cannot affectthe outcome of any other of the listed transactions (ditto
for tx 1 and bal[𝐵]). With this observation, we can refine thetransaction footprints and the notion of ownership (Fig. 3,
right), allowing for a parallel execution with three shards:
Owns(S1, {bal[𝐴], all[𝐴] [𝐷]}),(2)
Owns(S2, {all[𝐴] [𝐸]}), Owns(S3, {bal[𝐶]})In the constraints above, S1 no longer has to own bal[𝐵]or bal[𝐶], while shard S3 now needs to own bal[𝐶]. In order to perform transactions allocated as S1 ↦→ {tx 1, tx 3 },S2 ↦→ {tx 4 }, S3 ↦→ {tx 2 }, obtaining the same result as in
the previous case, we need to redefine the state join operation. Specifically, instead of overwriting the values in entries
bal[𝐵] and bal[𝐴] upon łdisjoint mergingž as before, we willneed to add up the deltas to those components resulting fromtoken transfers in tx 1 and tx 3 , similarly to handling ordinarytransfers (Sec. 1).

= F𝑥 2 (𝜎2 ) ⊎ F𝑥 1 (𝜎1 ) = F𝑥 2 (𝜎2 ⊎ F𝑥 1 (𝜎1 ))= F𝑥 2 (F𝑥 1 (𝜎2 ⊎ 𝜎1 )) = F𝑥 2 (F𝑥 1 (𝜎))This reasoning demonstrates the desired commutativity,
and also provides a recipe for computing the final result ina divide-and-conquer fashion by taking it to be F𝑥 1 (𝜎1 ) ⊎F𝑥 2 (𝜎2 ); the order does not matter, as ⊎ is commutative andassociative. One can think of ⊎ as both the łlogical split andjoinž operations, while a footprint of a transaction executing
F𝑥 is the minimal part 𝜎 ′ of the contract state, which must
be owned by the shard executing it, so that F𝑥 (𝜎 ′) is defined.
Getting back to our motivating example of ERC20 sharding, Strategy 1 corresponds to ⊎ taken as a disjoint unionof the entry sets of the contract’s mapping fields (let’s callit OwnOverwrite). Strategy 2 corresponds to ⊎ defined asa non-disjoint union with an implicit split of integer values
in map entriesÐthis way in the case of concurrent updates,
the result can be obtained by summation of the per-shard
portions of those values (we will call it IntMerge).
2.4

The Main Idea. To summarise these observations: contracts such as ERC20, whose operations only manipulate asmall part of the state, allow for parallel conflict-free execution of their operations, if these operations commute. The
ownership constraints state which parts of a contract’s state ashard must have exclusive access to in order to execute its
operations without conflicts with other shards altering thesame contract concurrently. The join defines the way to deterministically reconcile outcomes of the parallel executions.

Pragmatic Considerations and Technical Setup

Ethereum is the most popular smart contract platform, and anumber of other blockchain ecosystems also use the Ethereum
Virtual Machine (EVM). While it would be desirable to implement our ideas directly in Ethereum, unfortunately, its
infrastructure is currently unsuitable for our purposes:
2 Readers familiar with state-of-the art program logics for concurrency canrecognise that we are looking for a suitable Partial Commutative Monoid(PCM) [10, 34, 44], which would enable framing of contract operations F𝑥 .

1330

Practical Smart Contract Sharding with Ownership and Commutativity Analysis(identifiers) i, f , 𝑐 ::= alpha-numeric string(types)t ::= int | string | unit | bool | map t t | t → t | . . .
(patterns)
pat ::= _ | i | constr 𝑐 pat(expressions) e ::= val v | var i | message (i ↦→ i) | constr 𝑐 t i |builtin blt i | let i = e1 in e2 | fun (i : t) ⇒ e |app i i 𝑗 | match i pat ⇒ e | tfun 𝛼 ⇒ e | inst i t(statements)
s ::= i1 ← i2 | i1 := i2 | i = e | i1 [i𝑘 ] := i2 | i1 ← i2 [i𝑘 ] |i1 ← exists i2 [i𝑘 ] | delete i1 [i𝑘 ] | i1 ← &i2 |match i pat ⇒ s | accept | send i | event i | throw

Figure 4. Scilla syntax.
• Protocol-level Support. At the time of writing, the available prototype of Ethereum 2.0 [64] does not support crossshard transactions or smart contracts.
• Language-level Support. EVM bytecode, Ethereum’s lowlevel language, is difficult to analyse soundly, due to thelack of modularity and structured control flow [65]. One
could engineer an analysis inferring ownership constraints
for Solidity [25], a high-level Ethereum language, by possibly decompiling EVM contracts [29]. However, a numberof Solidity’s features (e.g., inter-contract calls) and unpredictable performance of EVM decompilers make it a challenging target for an efficient sound static analysis [33].
Bringing Ethereum infrastructure to the state necessary to
deploy the described ideas would be an effort going wellbeyond the scope of this paper. Instead, we implemented ourapproach as a static analysis for Scilla [57]Ða strongly-typed
ML-style language for smart contracts. Scilla is supported
natively (via a definitional interpreter) by an industry-scale
blockchain [45, 67] that (a) provides rudimentary infrastructure for sharding, (b) is available open-source, and (c) iswidely used and contains dozens of contracts implemented
in Scilla by users and available for evaluating our approach.

1 transition Transfer(to: ByStr20, amount: Uint)2
get_from_bal ← balances[_sender];3match get_from_bal with
4
| Some bal ⇒5
can_do = uint_le amount bal;
6
match can_do with
7
| True ⇒8
new_from_bal = builtin sub bal amount;9balances[_sender] := new_from_bal;
10
get_to_bal ← balances[to];11
new_to_bal = (match get_to_bal with
12
| Some bal ⇒ builtin add bal amount13| None ⇒ amount);
14
balances[to] := new_to_bal
15| False ⇒ (* Report a transaction failure *)16
msg_to_recipient = {_tag : "Accepted"; _to : to; ...};
17
msg_to_sender = {_tag : "Success"; _to : _sender; ...};
18
send msg_to_recipient; send msg_to_sender

Figure 5. FungibleToken Transfer transition in Scilla.
its transitions as reactions to received messages from theusers or other contracts. While transitions in Scilla contracts
are similar to functions in Solidity, they provide stronger
encapsulation and atomicity guarantees, in particular, disallowing reentrancy. This model allows one to analyse eachcontract’s transitions in isolation from any other contract’scode, thus allowing for deriving their signatures staticallywithout over-approximating the effects of the external calls.
Fig. 4 describes the syntax for Scilla statements and expressions, and Fig. 5 shows the code for the Transfer transition ofa FungibleToken (i.e., ERC20) contract. The transition takes
one implicit argument, the address _sender of the transaction originator, and two explicit arguments, the address of
the recipient and the amount of tokens to be transferred.
It reads the balance of the sender (line 2), ensures that thesender has enough tokens to transfer (line 6), and updates
the sender (line 9) and recipient balances (line 14).
3.2

3 CoSplit Analysis in a Nutshell
3.1

PLDI ’21, June 20ś25, 2021, Virtual, Canada

Inferring Transition Summaries

CoSplit implements a compositional inter-procedural effectanalysis [49] inferring transition summaries (a set of effects),
which describe, in a symbolic form, (1) the state footprintof transitions and (2) the contributions of the initial valuesof contract fields, read during a transition’s execution, tothe final field values. A transition’s summary is the result of
the abstract interpretation [15, 16] of the transition’s code.
These summaries help answer queries such as (1) łDoes thetransition write to field f?ž and (2) łCan the transition’s effectto field f be represented as an addition of a constant to f’s
old value?ž. The two types of queries correspond to our two
sharding strategies (see the discussion in Sec. 2.2).
The state footprint describes the portion of a contract state
affected by a transition (and, respectively, by a transactionthat executes it), whereas the contribution types let us decideif writes that affect the same piece of state commute. We
explain the analysis in two stages, corresponding to the two
types of queries. The stages are intertwined in the implementation, but here we separate them to aid in presentation.

The Language

Scilla [57] is a minimalistic memory- and type-safe functional
language, similar to OCaml and Haskell for an account-based(i.e., Ethereum-style) smart contract model. Scilla provides
a very small set of state-manipulating primitives for altering contract state (i.e., reading from the blockchain stateand changing the values of contract fields). Its pure (i.e.,side effect-free) fragment corresponds to System F [27, 54]
without recursion (but with bounded iteration). All of thestandard library as well as user-defined contract-agnostic
computations are implemented in Scilla as pure functions.
This design choice removes the need for inter-contract calls
for the sake of code reuse and makes contract analysis scale,as pure functions need to be analysed only once.
Contracts in Scilla are encoded as communicating statetransition systems in the style of IO-automata [46]. That is,
all interaction between contracts is done by means of message
passing. A contract’s state changes as a result of executing

1331

PLDI ’21, June 20ś25, 2021, Virtual, Canada(effect)𝜀George Pîrlea, Amrit Kumar, and Ilya Sergey

MapUpdate::= Read(f) | Write(f, 𝜏) | Condition(𝜏) |AcceptFunds | SendMsg(𝜏) | ⊤Γ ⊢ e : 𝜏 Γ′ = Γ, i : 𝜏Γ; Σ ⊢ i = e ⇝ Γ′ ; Σ(contrib. type) 𝜏 ::= ⟨cs ↦→ (card, ops), p⟩ | EFun i 𝜏 | ⊤ | ⊥(contrib. src.) cs ::= Field f | Const c | Formal i | ⊤(cardinality) card ::= 0 | 1 | 𝜔(precision)𝑝 ::= Exact | Inexact(operation)
op ::= Builtin blt | Cond0 ⊔ 𝛼 = 𝛼1 ⊔ 1 = 1
𝛼 ⊔ 𝜔 = 𝜔Γ ; Σ ⊢ i1 [i𝑘 ] := i2 ⇝ Γ ; Σ, 𝜀𝑏=Write(i2 [i𝑘 ], _) ∉ Σ∧ CanSummarise i𝑘𝜏 , 𝜀 = if 𝑏 then ⟨Field i2 [ik ] ↦→ (1, ∅), Exact ⟩ , Read(i2 [i𝑘 ]) else ⊤, ⊤
Γ ; Σ ⊢ i1 ← i2 [i𝑘 ] ⇝ Γ, i1 : 𝜏 ; Σ, 𝜀Constr0 ⊗ 𝛼 = 0
1 ⊗ 1 = 1
𝛼 ⊗ 𝜔 = 𝜔Literal𝜏 = ⊕ Γ (𝑖)Γ ⊢ val 𝑙 : ⟨Const l ↦→ (1, ∅), Exact ⟩i = unique arg. identifierΓ′ = Γ, i : ⟨Formal i ↦→ (1, ∅), Exact ⟩Γ′ ⊢ e : 𝜏e 𝜏 = EFun i 𝜏eΓ ⊢ fun (i : t) ⇒ e : 𝜏𝜏 ′ = ⊕ Γ (arg)𝜏 = 𝜏 ′ with ops += bltΓ ⊢ builtin blt arg : 𝜏

Figure 6. Components of CoSplit abstract domain.

App

Let

State Footprints

ij = unique identifier for j -th arg.
Γ ⊢ f : 𝜏f ∀j, Γ ⊢ aj : 𝜏j
𝜏 = ⊕ (𝜏f [ij ] ⊗ 𝜏j )Γ′ = Γ, i : 𝜏1Γ ⊢ e1 : 𝜏1 Γ′ ⊢ e2 : 𝜏Γ ⊢ let i = e1 in e2 : 𝜏

Fig. 6 shows the CoSplit abstract domain. The first stage ofthe analysis computes an over-approximation of the state
footprints of contract transitions, expressed as a set of effects(denoted 𝜀). Effects describe how the transition interacts
with the blockchain state. For instance, the AcceptFunds
effect (contributed by the accept statement) changes boththe contract’s and the sender’s native token balances.3 Similarly, the SendMsg effect (contributed by send) might invoke transitions of other contracts or send native tokens.
Finally, the Read and Write effects describe which portionsof the contract’s own state may be accessed by the transition. For each transition, CoSplit iterates over every statement in the transition’s code and determines the static overapproximation of that statement’s effect. In some cases, thisover-approximation is the uninformative effect ⊤. Due to
Scilla’s design, the translation between statements and effects is direct. As an example, we show the analysis rules formap reads and writes, which can be found in the top box ofFig. 7. These rules are applied when analysing lines 2, 9, and
14 in Fig. 5. The parts shown in grey boxes , including therule for the non-effectful Bind statement, appear due to thesecond stage of the analysis, explained below.
The MapGet and MapUpdate rules extend the transition’ssummary Σ with the appropriate Read or Write effect, which
identifies the portion f (for field) of the contract state that is
operated on. For map accesses, f includes the name of the
map and the symbolic names of keys i𝑘 used to index into
the map. For accesses to non-map contract fields, only thename of the field is included.
Whereas contract fields can always be described, the keys
used to index into a map can be the result of a computationΓ ⊢ constr 𝑐 𝑡 𝑖 : 𝜏

Fun

Builtin

3.3

𝑏 = CanSummarise i𝑘

𝜀 = if 𝑏 then Write(i1 [i𝑘 ], 𝜏 ) else ⊤MapGet(cardinality order)
0 ⊑ 1 ⊑𝜔
(operations order) ops1 ⊑ ops2
iff ops1 ⊂ ops2
(precision order)
Exact ⊑ Inexact
0 ⊕ 𝛼 = 𝛼1 ⊕ 1 = 𝜔𝛼 ⊕ 𝜔 = 𝜔Γ ⊢ i2 : 𝜏BindΓ ⊢ app f aj : 𝜏MatchΓ ⊢ 𝑥 : 𝜏x∀𝑖, Γ𝑖 = binder (pat𝑖 ) → Γ (𝑥)∀𝑖, Γ ∪ Γ𝑖 ⊢ e𝑖 : 𝜏i
𝜏 = MatchC (x, 𝜏x , pat i , ei , 𝜏i )
Γ ⊢ match 𝑥 pat𝑖 ⇒ e𝑖 : 𝜏

Figure 7. Selected rules for statements and expressions.
and may even depend on contract state. As such, we only
assign an informative effect 𝜀 to accesses when the keys used
to index into the map are transition parameters, as they are in
Fig. 5. Moreover, for nested maps, we require that the accessis bottom-level, i.e., it touches a primitive value rather thana map. These constraints are captured by CanSummarise.
If the access cannot be summarised, the ⊤ effect is given.
Generally, an access can be statically described whenever the
keys are not dependent on the contract state, but we limit
ourselves to keys that are transition parameters to simplifytransaction dispatch, which is described in Sec. 4.3.
3.4

Contribution Types

The summaries produced so far are sufficient to enable thedisjoint state ownership sharding strategy. But, as we haveseen, we can execute in parallel even transactions with effects
over the same state, as long as the effects commute. The
second stage of the analysis annotates the effects producedby the first stage with contribution types (denoted 𝜏), which
help determining whether they commute. Concretely, forevery expression 𝑒, CoSplit computes a contribution type, anover-approximation of the set of arithmetic operations andof the set of contract state components from the beginningof the transition execution that contribute to 𝑒’s result.
The type 𝜏 (cf. Fig. 6) ascribed to an expression 𝑒 indicates,
which contribution sources, i.e., parts of the contract state

3 This can be expressed as a Write affecting the two balances, but we prefer a more informative effect since balances are treated specially by theblockchain protocol. Similar reasoning applies to SendMsg.

1332

Practical Smart Contract Sharding with Ownership and Commutativity Analysis

PLDI ’21, June 20ś25, 2021, Virtual, Canada(constraint) oc ::= Owns(f) | UserAddr(𝑥) | NoAliases( ⟨𝑥, 𝑦 ⟩) |Read(balances[_sender])Read(balances[to])Condition(balances[_sender], amount)
Write(balances[_sender], ⟨amount&balances[_sender], 1, sub⟩)Write(balances[to], ⟨amount&balances[to], 1, add⟩)
SendMsg(funds = zero; destination = to)
SendMsg(funds = zero; destination = _sender)(join)

SenderShard | ContractShard | ⊥⊎f ::= OwnOverwrite | IntMerge

EffectConstraint⊤ ∨ SendMsg(⊤)
AcceptFunds
SendMsg(_amount.𝜏 ≠ 0)
SendMsg(_recipient.𝜏 = 𝑟 )Read/Write(𝑚 [𝑥 ]), Read/Write(𝑚 [𝑦 ])Figure 8. Set of effects of the Transfer transition.
(Field f), transition parameters/constants (Const c), andfunction parameters (Formal i), flow into 𝑒’s result, what
operations are applied to those sources, and how many times
each source contributes to 𝑒’s result. The precision component 𝑝 in types records whether over-approximation of theset of operations has taken place due to joining control flows,i.e., the analysis has lost precision. This lets us answer questions like łCan the transition’s effect to field f be represented
as an addition of a constant to f’s old value?ž. If the 𝜏 ascribedto the value written to field f has as its only exact contribution Field f ↦→ (1, Builtin add), and also some constants
and transition parameters, the answer is yes.

⊥
SenderShard
ContractShard
UserAddr(𝑟 )NoAliases( ⟨𝑥, 𝑦 ⟩)Figure 9. Elements of sharding signatures (top). Translation
between effects and non-ownership constraints (bottom).
application of a Builtin function adds up the contributions
from its arguments and records an application of Builtin blt
to each contribution source, recording this in the type.
Functions are given arrow types, EFun i 𝜏, with each formal parameter constituting an artificial contribution source
Formal i. When the function is applied (rule App), the arrow type is evaluated by substituting the formal parameter’s contribution with the actual argument’s contributions,multiplying the cardinalities. Our approach supports up tosecond-order Scilla functions by expressing operations oncontribution types (⊕, ⊔, and ⊗) at the type level, and deferring normalisation until the arguments are known. For
simplicity, we do not show this in the figures. Even though
Scilla provides polymorphic functions and type applications(as in System F), they bear no significance for our analysis.
Finally, the types given to Match over-approximate thecontributions of all clauses, whose types are combined using
the MatchC operator defined as follows:

The Importance of Cardinalities. The most importantcomponent in the type is the cardinality of Field f. If f did
not show up in 𝜏, then the written value would be a constant,and different writes would not commute, as they might havepotentially different values (e.g., different transition parameters). Conversely, if f’s contribution was non-linear, i.e., its
cardinality is 𝜔 (łmanyž),4 then even though f is modified
by a commutative operation (addition), the effect would notcommute. For example, the linear function 𝑓 (𝑥) = 𝑥 + 1 commutes with 𝑔(𝑥) = 𝑥 +2, but does not with ℎ(𝑥) = 𝑥 +𝑥 +1, as𝑓 (ℎ(𝑎)) ≠ ℎ(𝑓 (𝑎)). The linearity (łused-oncež) information
attached to contribution sources lets us ensure that operations are used in ways that guarantee commutative effects.
We lift the ⊕ operation on cardinalities to types by adding
the cardinalities of matching sources and set-unioning theiroperations, ascribing to the result the ⊔ of their precisions.
For ⊗, which is defined only between a type and a single contribution, we multiply the cardinalities of the arguments andmodify the other components analogously to the ⊕ lifting.

MatchC(x, 𝜏x , pat i , ei , 𝜏i )⊔≜ 𝜏cond ⊕
𝜏i
where
𝜏cond
≜ if IsKnownOp(x, pat i , ei )then ⊥ else AdaptC 𝜏x
AdaptC ⟨cs ↦→ (_, _), _⟩≜ if SameVars(𝜏i )then ⟨cs ↦→ (0, Cond), Exact⟩
else ⟨cs ↦→ (0, Cond), Inexact⟩

The additional contribution 𝜏cond accounts for whether
matching over the scrutinee 𝑥 induces non-trivial data flow

Computing Contribution Types. The values read fromthe mutable contract state, literals, transition and contract
parameters are all contribution sources. For example, theLiteral and MapGet rules in Fig. 7 show how new contribution sources are introduced. A read into a binder i1 from alocation that was not overwritten, extends the typing context Γ by giving i1 the linear contribution type 𝜏 shown in
the rule. The type shows that the value of i1 is the value ofthe respective łpseudo-fieldž i2 [i𝑘 ] (i.e., a map entry) at the
beginning of the transition execution. Contributions frommultiple sources are combined with their cardinalities added
up point-wise via ⊕ operator (cf. Fig. 6). For example, the(in which case its contribution is determined via AdaptC), or
simply łpeels offž a constructor of an option value (in whichcase it has no contribution). The latter is a very common
special scenario, (see, e.g., lines 11ś13 of Fig. 5), and without
this machinery the analysis would lose too much precision.
3.5

Calculating Sharding Signatures

From the set of transition summaries of a given contract(one such summary is shown in Fig. 8), and provided withuser input as to what transitions to attempt to shard andwhich fields can be treated weakly for reading (cf. Sec. 4.2.3),
CoSplit derives a sharding signature, consisting of a set of
constraints oc for each transition in the contract and a join

4 Our cardinality domain is inspired by GHC’s cardinality analysis [58].

1333PLDI ’21, June 20ś25, 2021, Virtual, Canada

George Pîrlea, Amrit Kumar, and Ilya Sergey

fields that are commutatively written to might return stale
data (cf. Sec. 4.2.3), the algorithm translates effects into constraints via the mapping in Fig. 9 and by requiring ownershipof every field that is read or non-commutatively written to.

Algorithm 3.1: Derive Sharding Signature
input : effect summaries, selected transitions, weak reads
output : transition (ownership) constraints, field join operations
Σ ← effect summaries of selected transitions
wrs ← reads the user accepted might be stalefor Σ ∈ Σ docfs ← GetConstantFields(Σ)Σ ← ∀𝑓 ∈ cfs , Σ.remove(Read(𝑓 ))Σ ← Σ.MarkConstantsInTypes(cfs)lcws ← GetTransitionCommWrites(Σ)
cws, joins ← TryConsolidateJoinsGlobally(lcws)
Σ ← Σ.RemoveSpuriousReads(cws)
if joins ≠ ∅ ∧ wrs = StaleReads(Σ, joins) thenoc ← { }for Σ ∈ Σ doc ← GenEnvironmentConstraints(Σ)
foreach Read(f) ∈ Σ do c ← c ∪ Owns(f)foreach Write(f) ∈ (Σ \ cws) do c ← c ∪ Owns(f)oc ← oc ∪ creturn (oc, joins)

4 Enabling Parallelism with CoSplit
In this section, we show how the signatures inferred by
CoSplit, as described in Sec. 3, can be used to allow forparallel transaction execution in a sharded blockchain.
4.1 The Sharding Model
We integrated CoSplit with Zilliqa blockchain [67]. Zilliqa is
one of the first sharded chains in production. It implements
the Elastico protocol for secure sharding [45] and relies on an
optimised version of the Practical Byzantine Fault Tolerance(PBFT) protocol for consensus in the network [12, 61]. At
the time of writing, Zilliqa mainnet has processed 9.6 million
transactions and contained 28 types of unique smart contracts (some of them have many deployed copies). Below, weoutline the relevant parts of its architecture and transaction
processing logic, referring the reader to the corresponding
manuscripts for details (on, e.g., security and epoch-basedmining) [45, 67], which are not critical for our presentation.

operation ⊎f for each field. The top part of Fig. 9 enumerates
the constraints that summaries can impose, as well as join
operations we currently support. Constraints are static symbolic representations of conditions that must be satisfied atruntime. They refer to mutable fields or transition parameters as symbolic values, e.g., Owns(f) and UserAddr(𝑥). For
instance, the Owns(balances[_sender]) constraint denotesthat a shard executing the transition must own the _sender
portion of the balances state component, where _sender isreplaced at runtime by the actual value given by the transaction. The other constraints are imposed by the blockchain
environment, e.g., SenderShard, which must be satisfied if
the contract accepts funds, or arise as preconditions for thesoundness of our analysis, e.g., that keys used for map accesses do not alias. ⊥ corresponds to an unsatisfiable constraint, meaning that the transition cannot be executed inparallel with other transactions over the same contract.
Algorithm 3.1 shows the procedure for deriving the sharding signature. The contract developer selects a set of transitions that should be executed in parallel, and the algorithm
inspects their summaries to determine what constraints mustbe satisfied to enable parallel execution. First, it identifies
which (if any) contract fields are not written to in the selected transitions, and marks their reads as non-effectul (i.e.,
it removes them from the summary) and their contributions
as constant. Second, looking at each summary in isolation,
it identifies using the types, which writes have a commutative effect, e.g. Write(balances[to]) in Fig. 8. Then, it determines if a join operation exists for every field, i.e., the writes
across transitions are compatible, and marks reads that only
flow into commutative writes, e.g. Read(balances[to]) (sincebalances[to] does not appear in any other type), as noneffectul.5 Finally, if the developer accepts that reads from

Network Architecture. The Zilliqa network consists ofthree main components: the lookup nodes, the shards, andthe Directory Service (aka the DS committee) (cf. Fig. 10).
Lookup nodes are the entry-point to the network. Anytransaction created by a user has to be sent to the lookup
nodes, which thereupon group several transactions together
in a packet and dispatch them to one of the shards or the
DS committee for processing. Each shard (and similarly the
DS committee, which in fact is a special shard) stores thefull blockchain state and runs PBFT to reach consensus onvalidated transactions. It then proposes a MicroBlock (MB)that contains information on the transactions that it has
processed. MicroBlocks are then sent to the DS committee
together with StateDelta (SD) which encodes the changes
in the state of the accounts that were touched by the transactions within a MicroBlock. Once all the MicroBlocks andthe corresponding StateDeltas reach the DS committee, thelatter combines them all in the form of a FinalBlock (FB)
and a FinalStateDelta (FSD). The FinalBlock and FinalBlockDelta are then sent back to each shard so that all the shards
have the same view of the full global stateÐZilliqa shards
transaction execution, but not state storage.
The Default Sharding Strategy. A client-issued transaction can be processed either by one of the shards or by
the DS committee (Fig. 10). Zilliqa employs a simple deterministic transaction assignment strategy to shards to ensurethat double spends are detected within a shard without complex cross-shard communication [39]. User-to-user paymenttransactions are deterministically assigned to shards basedon the sender’s address. That is, all transactions from the

5 The Condition effect prevents removal of reads that affect control-flow.

1334

Practical Smart Contract Sharding with Ownership and Commutativity Analysis
DS Committee

tx10

MB4
SD4

MB1, MB2, MB3

MB4
SD4

nonce mechanism prevents parallel executing of transactions
with the same origin in different shards, as the total order ofnonces cannot be communicated. We notice that in practiceno applications rely on a specific order of user transactions
before they are committed by the protocol.6 Therefore, it suffices for transactions to be processed in an increasing nonce
order, without waiting for all łgapsž to be filled, treatingthem similarly to ballots in Paxos [41]. This relaxation requires a very small change in the protocol logic. With it, we
kept the aspect (b) of the nonce mechanism, while allowing
for parallel executions. For instance, this way we can executein parallel two disjoint sets of commuting transactions fromthe same user with nonces {1, 3, 5} and {2, 4}, respectively.

FB
FSD

Lookup Nodes
FB
MB1
SD1

Shard1

MB2
SD2

MB3
SD3

FSD

Shard3

Shard2tx1 tx2
tx3 tx4 tx5 tx6
tx7
tx8 tx9 tx10
tx1, tx2, tx3

MB1
SD1

tx4, tx5, tx6

MB2
SD2

tx7, tx8, tx9

MB3
SD3

Figure 10. Transaction processing in a sharded architecture.

4.2.2 Parallel Gas Accounting. Gas accounting is a mechanism to charge users for executing transactions [65]. Suchdeductions must be treated sequentially to avoid overspending. We circumvent this bottleneck to parallelism by splitting
a user’s balance across shards (with a larger fraction given to
the shard handling money transfers from that user), so gas
costs can be charged without coordinating balance changes.

same user get handled in the same shard, so any double spend
from a specific user can be detected within a single shard in
the same way it gets handled in a non-sharded architecture.
For smart contracts, Zilliqa implements a non-efficientconservative strategy. Specifically, the network statically assigns both contracts and end users to shards. Transactions to
a contract invoked by users residing in the same shard as thecontract are handled within the shard, while transactions
to a contract invoked by users from an outside shard arehandled in the DS committee. To ensure that shards and the
DS do not end up manipulating the state of the same contract concurrently, the protocol requires the DS committee
to process transactions assigned to it only after the shards
have finished processing their transactions.
Given this simple deterministic assignment, the parallelism achieved for smart contract transaction processing isquite limited. In fact, the more shards there are, the moretransactions will need to be processed by the DS committee.
4.2

PLDI ’21, June 20ś25, 2021, Virtual, Canada

4.2.3 Weak Reads. In the Transfer transition (Fig. 8), we
saw that the write into balances[to] has a commutative effect. As a result, the processing shard does not need to own
the field to execute the transition. However, allowing commutative writes means that transitions executing in a different
shard might read stale values of balances[_sender]. In our
example, this is fineÐthe sender may have more tokens that
she thinks. Yet, in general, introducing commutative writes
weakens the semantics of reads and a static analysis cannot
determine whether this is łfinež for specific contracts. As arule of thumb, a read can safely be marked as weak if thecontract semantics is łmonotonež in the corresponding value
with respect to some lattice (as in [40]), i.e., the behaviour ofthe contract is not affected if a higher value is read and othershards can increase the value, but not decrease it. Ideally,
the programming language itself would allow contract developers to mark certain reads as weak, but neither Scilla nor
Solidity, both designed with sequential semantics in mind,
currently have this feature. For now, we require that weakreads be provided as input to Algorithm 3.1.

Revising the Account-Based Blockchain Model

In order to employ the described sharding model for CoSplitenabled parallelism, we need to revise a few core aspects inthe design of Ethereum-style blockchains.
4.2.1 Relaxing the Nonce Mechanism. Ethereum’s account based model (adopted by Zilliqa and similar systems)
uses of the nonce mechanism for defining a total order on
all transactions emitted by a particular user. Nonces are calculated by counting the number of transactions sent from auser address and are digitally signed, addressing the following design aspects: (a) strict, gap-free, user-defined orderingof transactions, and (b) prevention of replay attacks. Thanks
to the nonces, the user can send many transactions withsubsequent numbers, and they are going to be processed inthis exact orderÐthe protocol will not process transaction
with a nonce 𝑛 + 1 before the one with nonce 𝑛.
Because of aspect (a), nonces pose a bottleneck to sharded
executions. While in plain Zilliqa all transactions from a single user are guaranteed to be handled in the same shard, the

4.3 CoSplit in Action
Using CoSplit assumes two modes: offline and online. In
the former, the user who is about to deploy her contract tothe blockchain, provides hints to the tool in order to choose
the most suitable sharding signature (Fig. 11). In the latter,
CoSplit is run automatically by the miners as a part of thevalidation pipeline for contracts proposed to be deployed.
6 Furthermore, the UTxO blockchain model adopted by, e.g., Bitcoin [48]promotes this kind of weak notion of consistency, in which the user cannot
predict the order in which her transactions are committed.

1335

PLDI ’21, June 20ś25, 2021, Virtual, Canada

George Pîrlea, Amrit Kumar, and Ilya Sergey

CoSplitContract
Analyser
Contract C

Transitionsummary

Sharding
Query Solver

Sharding signature(oc, ]f )<latexit sha1_base64="5lj8E5R7/RsIo8Mtisj1AZayxRI=">AAACIXicbVDLSsNAFJ3UV62vqEs3g0WoICURwS6LblxWsA9oQphMJ+3QSSbMTIQS8itu/BU3LhTpTvwZJ2kWtfXAwOGce5h7jx8zKpVlfRuVjc2t7Z3qbm1v/+DwyDw+6UmeCEy6mDMuBj6ShNGIdBVVjAxiQVDoM9L3p/e5338mQlIePalZTNwQjSMaUIyUljyz1XC49vN46oRITahKOc6yK7ikJzFLpLfwZZAGWZZdembdaloF4DqxS1IHJTqeOXdGHCchiRRmSMqhbcXKTZFQFDOS1ZxEkhjhKRqToaYRCol00+LCDF5oZQQDLvSLFCzU5USKQilnoa8niyVXvVz8zxsmKmi5KY3iRJEILz4KEgYVh3ldcEQFwYrNNEFYUL0rxBMkEFa61JouwV49eZ30rpu21bQfb+rtu7KOKjgD56ABbHAL2uABdEAXYPAC3sAH+DRejXfjy5gvRitGmTkFf2D8/ALFj6W+</latexit>

Transitions {T1 , T1 , . . .} to be sharded,
Fields for weak reads {f1, f2, …}

Figure 11. CoSplit for a contract developer (offline mode).
Offline Mode. Prior to the deployment of her contract
𝐶 (written in Scilla), the developer runs the CoSplit analysis on 𝐶’s code, producing a transition summary. Such asummary (cf. Sec. 3.2) itself is not yet useful for sharding.
The developer next sends a query (a (sub)set {T1, T2, . . .} of
𝐶’s transitions and a subset {f1, f2, . . .} of 𝐶’s fields that canbe treated weakly for reading) to the sharding solver, obtaining as a result a sharding signature: a set of ownership
constraints oc and a dictionary of per-field join functions⊎f suitable for sharding those transitions. CoSplit returns
a pair (oc, ⊎f ) of encodings, which the developer submits
along with 𝐶’s code in a contract-deploying transaction.
Validating Sharding Signatures. Each node in the shard,
upon receiving a transaction with a contract 𝐶 and its signature (oc, ⊎f ), runs CoSplit ensuring that the signature isvalid (the set of sharding transitions can be obtained from theconstraints oc). The signature is then broadcast, along withthe contract code and metadata, to all nodes in the system.
The signatures of different contracts are independent, so
the deployment of a new contract does not affect the validityof previously computed sharding signatures.
Assigning Transactions to Shards. A lookup node, uponreceiving a transaction tx = ⟨𝐶, T , 𝑥⟩ invoking a transition
T of a contract 𝐶 with inputs 𝑥, first conservatively checks
whether the transaction is indeed single-contract (i.e., nomore than one transition is invoked). If it cannot validate it
as such, the transaction is routed to the DS committee. Otherwise, the lookup node exercises the sharding strategy induced
by 𝐶’s signature (oc, ⊎f ), if such signature is available.
To do so, the lookup node invokes the dispatchoc (T , 𝑥)
procedure, which identifies a shard S that satisfies T ’s constraints, and routes tx to that shard. If no satisfying shard
exists, the transaction is routed to the DS committee.
Executing Sharded Transactions. Transactions are applied to a contract in epochs, so all nodes in all shards sharethe same contract state at each epoch’s beginning and end.
Upon receiving a transaction that invokes a transition T of
𝐶 with inputs 𝑥, a node in a shard S executes it by applying
the transition’s logic FT,𝑥 to the contract state 𝜎 at hand.
To understand why this is correct and leads to deterministic parallelism, let us think of a łlogical splitž of the state 𝜎using the per-field join operations ⊎ = ⊎f from the contract’s
sharding signature. Here, we consider the contract state 𝜎
SSS
as a join of the two states 𝜎self, and 𝜎other[44], where 𝜎self
is

1336

S
owned by the node’s shard S, while 𝜎otheris not owned, and,hence will not be affected by executing FT,𝑥 . Therefore, byrunning the contract’s transition, i.e., executing FT,𝑥 (𝜎), the′S
Snode obtains the state 𝜎 ′S = 𝜎self⊎ 𝜎other, where only theS′S
owned part has been changed from 𝜎self
to 𝜎self. Due to the
locality of FT,𝑥 with respect to the state owned by the node’s
shard (which is ensured by dispatching the transaction via
the ownership constraints), all changes done by the nodes ofthe shard S to the state of the contract can be accumulated
into the shard-specific state delta 𝜎ΔS , which only includes affected parts of the contract’s state that are łlogically disjointž
from any changes other shards have made concurrently.
The final state delta 𝜎ΔS is sent to the DS committee thatcombines the initial contract state 𝜎 with all the state deltas
by executing a three-way merge [35, 43] using the per-field
operations ⊎f from the signature. This deterministic merge
always succeeds, thanks to logical disjointness of the statedeltas from different shards. Finally, the DS committee executes all the remaining potentially conflicting transactions,obtaining the final contract state, which is broadcast systemwide to all other shards at the end of the epoch.

5 Evaluation
We implemented CoSplit in OCaml as a pluggable checker,
adding an optional phase to the existing Scilla type checking
pipeline. Put together, the analysis, query solver, transaction dispatcher, and state delta merger measure 2900 linesof OCaml code. All interaction between CoSplit and thenodes of Zilliqa network happens via JSON-RPC; that is, theapproach can be reused by any other system that provides away to serialise/deserialise the state of Scilla contracts.
In our evaluation of CoSplit, we focus on two aspectsof the tool: the quality of the analysis for sharding signatures (Sec. 5.1) and the impact of using the signatures to thesystem throughput when executing transactions to popular
contracts (Sec. 5.2) from the Zilliqa blockchain.7
5.1

Evaluating the Analysis

We are interested in quantitative answers to the following
questions with regards to the CoSplit analysis:• Is the analysis fast enough to be used for validating contractdeploying transactions (Sec. 5.1.1)?
• Is the analysis capable of inferring non-trivial sharding
signatures for real-world contracts (Sec. 5.1.2)?
To answer these questions, we have run the analysis on all
49 unique contracts from Zilliqa mainnet and testnet.
5.1.1 Analysis Performance. All Scilla contracts, upon
deployment to the blockchain, are validated by the miners that are forced to parse their code and run the typechecker. We ran the contract deployment pipeline (parsing,
7 The artefact, including CoSplit, its integration with Zilliqa, and the bench-

mark suite used for evaluation, is archived and made available [53].

Practical Smart Contract Sharding with Ownership and Commutativity Analysis
12

Cryptoman
TestSender
GoFundMi
FirstContract
Schnorr
HelloWorld
Soundario
BunkeringLog
Quizbot
LoveZilliqa
Voting
BoltAnalytics
LikeMasterUD_escrow
UD_primitive_version
UD_resolver
UD_operator_contract
Bookstore
PayRespect
HydraXSettlement
IOU
RoadDamage
FungibleToken
LUY_Cambodia
SocialPay
ZKToken
ProofIPFS
SimpleBondingCurve
OceanRumble_crate
MyRewardsToken
ProxyContract
MRToken
DinoMightyLand
SwapContract
AuctionRegistrar
OceanRumble_minion_token
Multisig
HTLC
ZeecashHybrid_Euro
OTS200Hub
DPSTokenSuperplayer_token
UD_registry
OracleMap_cornercases
DBondCelebrityNFT
XSGD
BlackjackParsing
Typechecking
Sharding analysis

PLDI ’21, June 20ś25, 2021, Virtual, Canada
●
●

10

●

8
●

4
2
0

10

●

●

6

●
●

1

●
●

●
●
●

●
●

●
●

●
●

●
●

8

●

6

●

●
●

●
●
●

●

●

●

●

●

3

5
7
9
11
13
15
Number of transitions in a contract●●

Number of maximal good enough signatures

12

Size of the largest good enough signature

4
2

●

0

●

1

17

3

5
7
9
11
13
15
Number of transitions in a contract

17(b) Maximal GE signatures(a) Largest good enough signatures

Figure 13. Statistics for Good Enough signatures.
Intuitively, a sharding signature is good enough if it allows
for the existence of a contract state, in which some 𝑘 of thetransitions can be run in parallel by different shards. Fig. 13ashows the sizes of the largest good enough signatures forour contract selection. It is worth noting that a larger GE
signature (in terms of a number 𝑘) might perform worse under real-world load than one with a smaller 𝑘, which shards
different but more frequently used transitions. The following
definition outlines the signatures worth comparing.

0

2,000

4,000

Definition 5.3 (Maximal GE signature). A GE sharding signature is maximal if its selection of transitions is not a proper
subset of some other GE signature’s selection.

6,000

Figure 12. Parsing, type checking, and analysis times (µs).

A contract might have a number of maximal signaturesof various sizes. The plot in Fig. 13b depicts those numbers
for our contracts. Computing the maximal signatures at theÍ
mining time is impractical, as it requires making 𝑛𝑘=1 𝑛𝑘
queries to the sharding solver (Fig. 11). Luckily, this computation can be done offline by a contract implementer, who
decides prior to the deployment which of the signatures topropose. The miners need to validate only that one signature.
These findings suggest that CoSplit indeed uncovers
many opportunities for parallel execution of smart contracts.

type-checking, and sharding analysis) for the contracts inour sample and measured how much time is spent in each
deployment stage. Fig. 12 shows the performance breakdownof those three components. The numbers were obtained ona PC with an Intel Core i7-8665U CPU by executing thepipeline for each contract a thousand times and averaging
the resulting time for each stage. The analysis adds a significant but acceptable overhead of around 46% to the total
contract deployment time. Since contract deployments forma very small fraction of all transactions and happen only
once during the lifetime of a contract, the analysis can be
run by the miners without affecting overall throughput.

5.2

6
5
4
3
2
1
0

5.1.2 Analysis Efficacy.
The bar chart on the rightsummarises the number oftransitions (from 1 to 18) for our 49 contracts. While it may
be more likely that a contract with a large number of transitions can be sharded efficiently, having many transitions
might also indicate having complex logic, making it difficult
to infer a useful signature. To quantify the efficacy of theanalysis, we introduce some new terminology.
1

2

3

4

5

6

7

8

9

Evaluating Sharded Executions

We evaluate the integration of CoSplit with Zilliqa by measuring the impact on throughput for five representative Scillacontracts. The chosen contracts are: (1) the most popular
contracts on Zilliqa (e.g., UD), (2) equivalent to their popularcounterparts on Ethereum currently (e.g., FungibleToken andNonfungibleToken) and in the past (e.g., Crowdfunding).

10 11 12 15 17 18

Definition 5.1 (Hogged fields). A contract’s transition T
hogs a field f in a sharding signature sg iff sg’s ownership
constraints require a shard to fully own f to execute T .

Contract

LOC #Trans Larg.GES #Max.GES

FungibleToken
Crowdfunding
NonfungibleToken
ProofIPFS
UD Registry

439
186
288
289
500

10
3
5
10
11

6
2
3
8
6

2
1
2
2
2

The table above summarises contract sizes, number of transitions, largest GE strategy, and the number of maximal GE
signatures. We set out to answer two main questions:• What throughput improvement, in terms of transactions
per second, can CoSplit help to achieve (Sec. 5.2.1)?
• What is the impact of the overheads imposed by CoSplitenabled sharding (Sec. 5.2.2)?

Definition 5.2. A sharding signature sg is good enough (GE)for its selection of 𝑘 contract transitions, iff either• 𝑘 = 1 and the selected transition does not hog fields, or• 𝑘 > 1 and any field is hogged by at most one transition.

1337

PLDI ’21, June 20ś25, 2021, Virtual, Canada

George Pîrlea, Amrit Kumar, and Ilya Sergey

Experimental Setup. To obtain the throughput figures,
we deployed small-scale testnets in various configurations on
Amazon EC2 containers. Each node runs on a t2.medium machine with 2 logical CPUs and 4GB of RAM, running Ubuntu
16.04. These specifications reflect the minimum requirements
needed to run a Zilliqa node. For our benchmarks, we fix theshard size to be 5 nodes per shard and measure the effect on
throughput of increasing the number of shards. We use thesame shard and DS gas limits as the Zilliqa mainnet.

Baseline 3 shards

CoSplit 3 shards

CoSplit 4 shards

CoSplit 5 shards

400
300
200
100
0
FT fundSelection of Sharding Signatures. We deploy each of
the five contracts in two configurations, one with no sharding
information (baseline), and one with a łreasonablež sharding
signature, informed by expected usage of the contract. For
our experiments, we make the choices as follows:

FT
CFtransfer donate

NFT
mint

NFT ProofIPFS UD
transfer register bestowUD
configFigure 14. Average TPS for different contract transitions as
a function of number of shards, over 10 epochs.

• For FungibleToken (FT, Zilliqa’s ERC20), we shard the Mint,
Transfer and TransferFrom, but not IncreaseAllowance,
Burn, or other administrative transitions.
• For NonfungibleToken (NFT, Zilliqa’s ERC-721 [59]), we
shard Mint and Transfer (which includes transfer-from
functionality), but not Burn and Approve.
• For ProofIPFS, we shard the transition that notarises ahash, but not the one that removes it from the contract.
• For the Unstoppable Domains (UD) registry, we shard
granting a new domain name and updating the record
associated with a name, but not transfers of ownership.
For the Crowdfunding contract, there is only one possible
choice, which is to shard the Donate and Claimback (if thegoal was not reached) transitions. We argue that our choicesreflect what a reasonable contract deployer would select and,as such, the measured throughput reflects probable scenarios.
We remark that we had to slightly rewrite the NFT and UD
contracts, compared to their mainnet definitions, to makethem shardable. These rewrites did not affect the semanticsof the contracts. We discuss the details of the changes, as wellas the potential to automate such modifications, in Sec. 6.
5.2.1 Measuring Throughput. After deployment, we subject the contracts, in sequence, to different workloads sustained over 10 epochs (roughly 8.5 minutes) and measure
the resulting throughput. As Fig. 14 shows, for most of theworkloads in the benchmark, we obtain a roughly linear TPS
increase as the number of shards goes up. The two exceptions
are the łFT fundž and the łProofIPFS registerž workloads.
The former transfers fungible tokens from a single source
to multiple destinations (all transactions go to the source’s
shard). The latter notarises a hash, but also keeps a list ofnotarised items for each user, and thus accesses two separate fields, which typically will be owned by different shards,
hence many transactions need to be processed by the DS
Committee. We note that for workloads that do not shardwell, performance does not degrade as compared to the baseline, and in some cases (e.g. ProofIPFS) marginally improves.

1338

The łFT transferž workload sends tokens from random
sources to random destinations. In the baseline configuration, the throughput is the same as for the single-source
workload. The CoSplit-empowered sharding strategy, on
the other hand, fully utilises the shards’ processing capacity and we get an almost linear increase in throughput as
the number of shards increases. A similar effect arises forcrowdfund donations. Interestingly, the łNFT mintž workload (which creates new tokens) is also single-source, justlike łFT fundž. However, the relevant transition does not affect state depending on the identity of the transaction sender,
but only on the identifier of the created token. As such, we
can obtain linear scaling even for a single-source workload.
This is only possible because of the changes to the accountbased model that we detailed in Sec. 4.2. Finally, Unstoppable
Domains is the most popular smart contract on the Zilliqa
mainnet, accounting for over half of the smart contract executions. We manage to shard the most popular transitions
on this contract, which account for 90% of usage, and show
linear increases in throughput for them as well.
5.2.2 Introduced Overheads. Integrating CoSplit adds
overheads to transaction dispatch and state delta merging.
Concretely, we see transaction dispatch time increase froman average 8 µs to an average 475 µs, and the state deltamerging increasing from 0.8 µs to 48.65 µs per changed state
field. This amounts to a 60x slowdown of these operations,most of it as a result of serialisation and deserialisation costs,
but this is fully justified by the resulting increase in overall system throughput. The overall performance gain comesfrom the fact that applying a delta is much faster than executing all the transactions that resulted in it. For instance,
for FungibleToken, the effects of 50 seconds of transaction
execution time can be merged in roughly 0.5 seconds.
5.2.3 Ownership versus Commutativity. In terms ofthe contribution of the two sharding strategies to the throughput improvement, we observe that contracts that manipulate
non-fungible quantities (e.g., NFTs, domains, notary) benefit
from the disjoint state ownership analysis and contracts thatmanipulate fungible quantities (e.g., FT) benefit from thecommutativity analysis. Contracts that have a mixture of
non-fungible and fungible quantities, e.g., a voting contract

Practical Smart Contract Sharding with Ownership and Commutativity Analysis

PLDI ’21, June 20ś25, 2021, Virtual, Canada

7 Related Workthat keeps track of who voted and of the total number ofvotes, can benefit from both strategies.

Sharding Contracts in Blockchains. Several industry
proposals outline approaches for smart contract sharding,yet none of them provide an efficient solution for shardingsame-contract transactions. For example, the Elrond protocol moves a smart contract to the same shard where its
static dependencies lie [23], which takes at least 5 roundsof consensus for a transaction to be finalised. Harmony [30]allows one to deploy contracts in individual shards, with nocross-shard communication allowed. Ethereum 2.0 proposesa cross-shard yanking scheme where the contract code anddata is moved into a shard at runtime [64]. The shard thenlocks the contract to block any parallel execution of othertransactions affecting it. At the time of writing, none of thesesolutions appear to be fully implemented.
The Chainspace protocol allows for sharded execution ofsmart contracts (as well as state sharding) by representing
state evolution as a directed acyclic graph [1], similar to
Bitcoin’s UTxO transaction model. In Chainspace, contracts
have to be written in a specific fashion, so their execution
happens off the chain. For an unspecified kind of transaction, the authors of Chainspace report linearly increasing
throughput of approximately 75 TPS per each two shardsof four nodes in each [1, Fig. 6]. Importantly, Chainspacedoes not address the scalability problem with same-contract
transactions (which we do): under high contention for thesame contract the rate of aborted transactions rises. This isbecause its protocol, S-BAC (a combination of PBFT [12] andTwo-Phase Commit for inter-shard communication), implements a variant of optimistic concurrency control, whereas
CoSplit allows for pessimistic (race-free) concurrency.

6 Discussion and Future Work
Handling Integer Overflows. CoSplit’s signature inference does not take possible integer overflows into account.
Overflows (and underflows) may cause a problem in the casewhen IntMerge is used to join state deltas from different
shards that individually do not cause an overflow, but do sowhen joined. At the moment, our implementation ignores
this issue. A working solution would be to modify the Scillainterpreter, providing it with information about the number 𝑁 of shards. Specifically, it should perform additional
post-hoc validation of a transaction, which will fail if thedifference between the initial (per epoch) value 𝑣 of any
affected integer-valued component and its value after thetransaction is executed exceeds ⌊ MAX_INT−𝑣⌋. The information
𝑁
about such components is already available in the sharding
signatures. Furthermore, a user might be given an option to
pay a higher gas fee, in order to reduce a risk for her transaction to be rejected due to this conservative check. Suchtransactions will be routed directly to the DS committee, and,thus, processed sequentially.
Automated Contract Repair. As mentioned in Sec. 3.3,
the analysis can describe map accesses only if the keys used
to index into the map are transition parameters. During theevaluation, we discovered a small number of contracts that
CoSplit cannot shard due to this limitation, but which canbe made shardable by a simple refactoring. For instance, an
NFT contract’s Transfer transition ensures that the transaction’s sender is authorized by the token owner to initiate thetransfer by checking for inclusion in approvals[tokenOwner],where tokenOwner is read from the contract’s state. This cannot be sharded. However, if we make tokenOwner a parameterand rewrite the transition to check that the supplied value
matches the value in the contract’s state before attempting
the transfer (akin to compare-and-swap), the transition becomes shardable. In future work, we plan to address thisusing program repair techniques, suggesting the shardable
contract version to the developer before deployment.
CoSplit and Other Blockchains. As demonstrated inSec. 3, the core analysis of CoSplit does not rely on any specific features of Scilla but is easy to implement for it due tothe language’s minimalism and restrictions (e.g., very limited
set of side effects). Should other account-based blockchains,e.g., Tezos [28] and Ethereum [65], provide a sharded architecture in the future, we believe a similar analysis could be
implemented for them as well. The key challenge of developing CoSplit for Michelson, the language of Tezos [63], isin reasoning about its stack-based executions, tracking theprovenance and cardinality of pushed and popped values.
Ethereum’s EVM could be supported through decompilation
into a high-level language [29]. The approach will most likely
have to be restricted to contracts with no external calls.

Smart Contracts and Concurrency. Dickerson et al. [18]describe a commutativity-based approach where miners execute smart contracts in parallel locally , using software transactional memory techniques [31, 32]. Unlike our approachthat detects possible transaction conflicts pessimistically bymeans of a static analysis prior to contract deployment, thework by Dickerson et al. exercises the optimistic approach,where conflicts are identified on-the-fly by the miners, withthe corresponding executions aborted. It is not clear how
to apply these ideas from optimistic concurrency for efficient sharding of general smart contracts in a Byzantine
setting, where an adversary can craft cheap (in terms of gas
costs) conflict-producing transactions that force the shards
to re-execute expensive transactions from the same batch.
A more fine-grained identification of conflicts would mostprobably require an analysis similar to ours, as conjectured
in [56]. At the same time, our solution is complementary to
Dickerson et al.’s work and other similar approaches. For
instance, one can add single-node parallelism on top of CoSplit-enabled sharding, and the analysis can help identify
which transactions are guaranteed not to require rollback
and re-execution, even within a single shard.

1339

PLDI ’21, June 20ś25, 2021, Virtual, Canada

George Pîrlea, Amrit Kumar, and Ilya Sergey

References

Recent work by Bartoletti et al. makes an observation
similar to ours that commutativity (which they dub swappability) of transactions manipulating Ethereum contracts
enables their parallel execution [6]. Their syntactic criterion
for inferring swappability is, however, more coarse-grained
than our analysis, and is based on determining disjointness oftransaction footprints, without taking into account commutativity of operations such as addition. As such, their approach
would not allow to shard individual non-conflicting updates
in an ERC20 contract as we do. Bartoletti et al.’s approachhas not been implemented in practice.
Inferring Commutativity. Reasoning about commutativity between program parts is an important problem withapplications including parallelising compilers [38, 55], speculative execution [31], and race detection [19]. Most of existing techniques for inferring commutativity are based on
analysing dynamic executions [2, 19, 26] or by solving SMT
constraints [5] and, thus, cannot be used efficiently as a partof transaction validation. Our analysis is close in spirit to
the work (in [55]) on static analysis to determine operation
commutativity for compile-time parallelisation. Our analysis
uses simpler abstractions, allowing it to be implemented in
a compositional fashion and have linear execution cost.

[1] Mustafa Al-Bassam, Alberto Sonnino, Shehar Bano, Dave Hrycyszyn,
and George Danezis. 2018. Chainspace: A Sharded Smart Contracts
Platform. In NDSS. https://doi.org/10.14722/ndss.2018.23241[2] Farhana Aleen and Nathan Clark. 2009. Commutativity analysis forsoftware parallelization: letting program transformations see the big
picture. In ASPLOS. ACM. https://doi.org/10.1145/1508244.1508273[3] Hagit Attiya, Rachid Guerraoui, Danny Hendler, Petr Kuznetsov,
Maged M. Michael, and Martin T. Vechev. 2011. Laws of order: expensive synchronization in concurrent algorithms cannot be eliminated.
In POPL. ACM, 487ś498. https://doi.org/10.1145/1925844.1926442[4] Shehar Bano, Alberto Sonnino, Mustafa Al-Bassam, Sarah Azouvi,
Patrick McCorry, Sarah Meiklejohn, and George Danezis. 2019. SoK:
Consensus in the Age of Blockchains. In Advances in Financial Technologies. ACM, 183ś198. https://doi.org/10.1145/3318041.3355458[5] Kshitij Bansal, Eric Koskinen, and Omer Tripp. 2018. Automatic Generation of Precise and Useful Commutativity Conditions. In TACAS(LNCS, Vol. 10805). Springer, 115ś132. https://doi.org/10.1007/978-3319-89960-2_7[6] Massimo Bartoletti, Letterio Galletta, and Maurizio Murgia. 2020. A
True Concurrent Model of Smart Contracts Executions. In COORDINATION (LNCS, Vol. 12134). Springer, 243ś260. https://doi.org/10.1007/
978-3-030-50029-0_16[7] Sebastian Burckhardt, Alexandro Baldassin, and Daan Leijen. 2010.
Concurrent programming with revisions and isolation types. In OOPSLA. ACM, 691ś707. https://doi.org/10.1145/1869459.1869515[8] Sebastian Burckhardt and Daan Leijen. 2011. Semantics of Concurrent
Revisions. In ESOP (LNCS, Vol. 6602). Springer, 116ś135. https://doi.
org/10.1007/978-3-642-19718-5_7[9] Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, and Hongseok
Yang. 2011. Compositional Shape Analysis by Means of Bi-Abduction.
J. ACM 58, 6 (2011), 1ś66. https://doi.org/10.1145/2049697.2049700[10] Cristiano Calcagno, Peter W. O’Hearn, and Hongseok Yang. 2007.
Local Action and Abstract Separation Logic. In LICS. IEEE, 366ś378.
https://doi.org/10.1109/lics.2007.30[11] Lásaro J. Camargos, Rodrigo Schmidt, and Fernando Pedone. 2007.
Multicoordinated Paxos. In PODC. ACM, 316ś317. https://doi.org/10.
1145/1281100.1281150[12] Miguel Castro and Barbara Liskov. 1999. Practical Byzantine Fault
Tolerance. In OSDI. USENIX Association, 173ś186.
[13] Austin T. Clements, M. Frans Kaashoek, Nickolai Zeldovich,
Robert Tappan Morris, and Eddie Kohler. 2013. The scalable commutativity rule: designing scalable software for multicore processors.
In SOSP. ACM, 1ś17. https://doi.org/10.1145/2517349.2522712[14] ConsenSys. 2018. The Inside Story of the CryptoKitties Congestion
Crisis.
[15] Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A
Unified Lattice Model for Static Analysis of Programs by Construction
or Approximation of Fixpoints. In POPL. ACM, 238ś252. https://doi.
org/10.1145/512950.512973[16] Patrick Cousot and Radhia Cousot. 1979. Systematic Design of Program
Analysis Frameworks. In POPL. ACM Press, 269ś282. https://doi.org/
10.1145/567752.567778[17] Hung Dang, Tien Tuan Anh Dinh, Dumitrel Loghin, Ee-Chien Chang,
Qian Lin, and Beng Chin Ooi. 2019. Towards Scaling Blockchain
Systems via Sharding. In SIGMOD. ACM, 123ś140. https://doi.org/10.
1145/3299869.3319889[18] Thomas D. Dickerson, Paul Gazzillo, Maurice Herlihy, and Eric Koskinen. 2017. Adding Concurrency to Smart Contracts. In PODC. ACM,
303ś312. https://doi.org/10.1145/3087801.3087835[19] Dimitar Dimitrov, Veselin Raychev, Martin T. Vechev, and Eric Koskinen. 2014. Commutativity race detection. In PLDI. ACM, 305ś315.
https://doi.org/10.1145/2594291.2594322

8 Conclusion
We presented a new approach to shard the execution of smart
contracts in an account-based blockchain model, based on
inferring ownership constraints and commutativity for statemanipulating contract operations. In our approach, smart
contracts are first processed by a static analysis tool that
produces their sharding signatures, which are then used
for shard allocation that maximises parallelism. We havedemonstrated that our approach, when integrated into thesharded production-scale blockchain, allows for linear scaling of the transaction throughput for a selection of common
smart contracts that were considered unavoidable execution
bottlenecks in existing blockchain systems.

Acknowledgments
We thank the OSDI’20 and PLDI’21 PC and AEC reviewers,
and our shepherd, Gustavo Petri, for their valuable feedback
on earlier drafts of this paper and the artefact. We thankAquinas Hobor, Yaoqi Jia, and Prateek Saxena who participated in the discussions on smart contract sharding at earlier
stages of this work. We are grateful to Haichuan Liu, Antonio Nicolas Nunez, and Jun Hao Tan, for their help in
integrating CoSplit with the Zilliqa protocol, and to Bryan
Tan for conducting preliminary experiments. We benefited a
lot from discussions and feedback on preliminary versionsof this work by Andreea Costea, Kiran Gopinathan, Jacob
Johannsen, Vaivaswatha Nagaraj, and Anton Trunov. Ilya
Sergey’s work has been supported by the grant of Singapore
NRF National Satellite of Excellence in Trustworthy Software
Systems (NSoE-TSS) and by the NUS Crystal Centre.

1340

Practical Smart Contract Sharding with Ownership and Commutativity Analysis[20] Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J.
Parkinson, and Hongseok Yang. 2013. Views: compositional reasoning
for concurrent programs. In POPL. ACM, 287ś300. https://doi.org/10.
1145/2429069.2429104[21] Dino Distefano, Manuel Fähndrich, Francesco Logozzo, and Peter W.
O’Hearn. 2019. Scaling static analyses at Facebook. Commun. ACM
62, 8 (2019), 62ś70. https://doi.org/10.1145/3338112[22] Tayfun Elmas, Shaz Qadeer, and Serdar Tasiran. 2009. A calculus of
atomic actions. In POPL. ACM, 2ś15. https://doi.org/10.1145/1480881.
1480885[23] The Elrond Team. 2019. Elrond: A Highly Scalable Public Blockchain
via Adaptive State Sharding and Secure Proof of Stake.
[24] Ethereum Foundation. 2018. ERC20 Token Standard.
[25] Ethereum Foundation. 2018. Solidity Documentation.
[26] Timon Gehr, Dimitar Dimitrov, and Martin T. Vechev. 2015. Learning
Commutativity Specifications. In CAV (LNCS, Vol. 9206). Springer.
https://doi.org/10.1007/978-3-319-21690-4_18[27] Jean-Yves Girard. 1972. Interprétation fonctionnelle et élimination descoupures de l’arithmétique d’ordre supérieur. Thèse d’État. Universitéde Paris VII, Paris, France.
[28] L.M. Goodman. 2014. TezosÐa Self-Amending Crypto-Ledger.
[29] Neville Grech, Lexi Brent, Bernhard Scholz, and Yannis Smaragdakis.
2019. Gigahorse: thorough, declarative decompilation of smart contracts. In ICSE. IEEE / ACM, 1176ś1186. https://doi.org/10.1109/icse.
2019.00120[30] Harmony Team. 2018. Harmony: Technical Whitepaper.
[31] Maurice Herlihy and Eric Koskinen. 2008. Transactional boosting: amethodology for highly-concurrent transactional objects. In PPoPP.
ACM, 207ś216. https://doi.org/10.1145/1345206.1345237[32] Maurice Herlihy, Victor Luchangco, Mark Moir, and William N. Scherer
III. 2003. Software transactional memory for dynamic-sized data structures. In PODC. ACM, 92ś101. https://doi.org/10.1145/872035.872048[33] Sungjae Hwang and Sukyoung Ryu. 2020. Gap between Theory andPractice: An Empirical Study of Security Patches in Solidity. In ICSE.
ACM, 542ś553. https://doi.org/10.1145/3377811.3380424[34] Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron
Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids andInvariants as an Orthogonal Basis for Concurrent Reasoning. In POPL.
ACM, 637ś650. https://doi.org/10.1145/2676726.2676980[35] Gowtham Kaki, Swarn Priya, K. C. Sivaramakrishnan, and Suresh Jagannathan. 2019. Mergeable replicated data types. Proc. ACM Program.
Lang. 3, OOPSLA (2019), 154:1ś154:29. https://doi.org/10.1145/3360580[36] Eleftherios Kokoris-Kogias, Philipp Jovanovic, Linus Gasser, Nicolas
Gailly, Ewa Syta, and Bryan Ford. 2018. OmniLedger: A Secure, ScaleOut, Decentralized Ledger via Sharding. In IEEE Symposium on Security
and Privacy. IEEE, 583ś598. https://doi.org/10.1109/sp.2018.000-5[37] Tim Kraska, Gene Pang, Michael J. Franklin, Samuel Madden, and Alan
Fekete. 2013. MDCC: multi-data center consistency. In EuroSys. ACM,
113ś126. https://doi.org/10.1145/2465351.2465363[38] Milind Kulkarni, Keshav Pingali, Bruce Walter, Ganesh Ramanarayanan, Kavita Bala, and L. Paul Chew. 2007. Optimistic parallelism
requires abstractions. In PLDI. ACM, 211ś222. https://doi.org/10.1145/
1250734.1250759[39] Amrit Kumar. 2018. Provisioning Sharding for Smart Contracts: A
Design for Zilliqa.
[40] Lindsey Kuper, Aaron Turon, Neelakantan R. Krishnaswami, andRyan R. Newton. 2014. Freeze after writing: quasi-deterministic
parallel programming with LVars. In POPL. ACM, 257ś270. https://doi.org/10.1145/2535838.2535842[41] Leslie Lamport. 1998. The Part-Time Parliament. ACM Trans. Comput.
Syst. 16, 2 (1998), 133ś169. https://doi.org/10.1145/279227.279229[42] Leslie Lamport. 2005. Generalized Consensus and Paxos. Technical
Report 33. Microsoft Research.

PLDI ’21, June 20ś25, 2021, Virtual, Canada[43] Daan Leijen, Manuel Fähndrich, and Sebastian Burckhardt. 2011. Prettier concurrency: purely functional concurrent revisions. In Haskell
Symposium. ACM, 83ś94. https://doi.org/10.1145/2034675.2034686[44] Ruy Ley-Wild and Aleksandar Nanevski. 2013. Subjective auxiliary
state for coarse-grained concurrency. In POPL. ACM, 561ś574. https://doi.org/10.1145/2429069.2429134[45] Loi Luu, Viswesh Narayanan, Chaodong Zheng, Kunal Baweja, SethGilbert, and Prateek Saxena. 2016. A Secure Sharding Protocol For
Open Blockchains. In CCS. ACM, 17ś30. https://doi.org/10.1145/
2976749.2978389[46] Nancy A. Lynch and Mark R. Tuttle. 1989. An Introduction to Input/Output Automata. CWI Quarterly 2 (1989), 219ś246.
[47] Iulian Moraru, David G. Andersen, and Michael Kaminsky. 2013. Thereis more consensus in Egalitarian parliaments. In SOSP. ACM, 358ś372.
https://doi.org/10.1145/2517349.2517350[48] Satoshi Nakamoto. 2008. Bitcoin: A peer-to-peer electronic cash system.
[49] Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. 1999. Principles of Program Analysis. Springer.
[50] Peter W. O’Hearn. 2007. Resources, concurrency, and local reasoning.
Theor. Comput. Sci. 375, 1-3 (2007), 271ś307. https://doi.org/10.1016/j.
tcs.2006.12.035[51] Ontology Research Team. 2019. Ontology Sharding, Draft v0.2.
[52] Prakash Prabhu, Soumyadeep Ghosh, Yun Zhang, Nick P. Johnson,
and David I. August. 2011. Commutative set: a language extension for
implicit parallel programming. In PLDI. ACM, 1ś11. https://doi.org/
10.1145/1993498.1993500[53] George Pîrlea, Amrit Kumar, and Ilya Sergey. 2021. CoSplit (PLDI 2021
Artefact). https://doi.org/10.5281/zenodo.4674301[54] John C. Reynolds. 1974. Towards a theory of type structure. In Programming Symposium (LNCS, Vol. 19). Springer, 408ś425. https://doi.org/10.1007/3-540-06859-7_148[55] Martin C. Rinard and Pedro C. Diniz. 1997. Commutativity Analysis:
A New Analysis Technique for Parallelizing Compilers. ACM Trans.
Program. Lang. Syst. 19, 6 (1997), 942ś991. https://doi.org/10.1145/
267959.269969[56] Vikram Saraph and Maurice Herlihy. 2019. An Empirical Study ofSpeculative Concurrency in Ethereum Smart Contracts. In Tokenomics(OASIcs, Vol. 71). Schloss Dagstuhl, 4:1ś4:15.
[57] Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar,
Anton Trunov, and Ken Chan Guan Hao. 2019. Safer smart contract
programming with Scilla. PACMPL 3, OOPSLA (2019), 185:1ś185:30.
https://doi.org/10.1145/3360611[58] Ilya Sergey, Dimitrios Vytiniotis, and Simon L. Peyton Jones. 2014.
Modular, higher-order cardinality analysis in theory and practice. In
POPL. ACM, 335ś348. https://doi.org/10.1145/2535838.2535861[59] Dieter Shirley. 2018. ERC-721 contract specification. http://erc721.org/.
[60] Alex Skidanov and Illia Polosukhin. 2019. Nightshade: Near Protocol
Sharding Design. https://near.org/downloads/Nightshade.pdf.
[61] Ewa Syta, Iulia Tamas, Dylan Visher, David Isaac Wolinsky, Philipp
Jovanovic, Linus Gasser, Nicolas Gailly, Ismail Khoffi, and Bryan Ford.
2016. Keeping Authorities łHonest or Bustž with Decentralized Witness Cosigning. In IEEE Symposium on Security and Privacy. IEEE
Computer Society, 526ś545. https://doi.org/10.1109/SP.2016.38[62] Nick Szabo. 1994. Smart Contracts. Online manuscript.
[63] Tezos. 2018. Michelson: the language of Smart Contracts in Tezos.
[64] Ethereum Wiki. 2020. On Sharding Blockchains.
[65] Gavin Wood. 2014. Ethereum: A Secure Decentralized Generalised
Transaction Ledger.
[66] Mahdi Zamani, Mahnush Movahedi, and Mariana Raykova. 2018.
RapidChain: Scaling Blockchain via Full Sharding. In CCS. ACM, 931ś
948. https://doi.org/10.1145/3243734.3243853[67] Zilliqa Team. 2017. The Zilliqa Technical Whitepaper.

1341