Toychain

Overview

Also Karl Palmskog in development

Master thesis of George Pîrlea

The protocol’s executions are modeled via a small-step operational semantics for asynchronous message passing, in which packages can be rearranged or duplicated.

Code extraction

Extensions

Karl Palmskog et.al.

Consistency

"when there are no inflight messages between any of the nodes, they all should agree on the local ledger, which can be, thus, thought of as a globally shared one"

citing these paper

Sebastian Burckhardt (Microsoft Research), et al.

"globally shared"

Douglas B. Terry et. al. by Xerox Palo Alto Research Center

cited by more than 1000 papers

Assumption

restricting the initial configurations to those where every node’s known peers include all addresses in the global state.

no "late joiners"

inductive for systems that start in initial configurations with a clique network topology

no crash faults nor byzantine faults

Theorem 5.1 (Consensus in a clique topology).

For 𝜎 = ⟨∆, 𝑃⟩, if Cliq(𝜎) holds, then there exists a chain 𝑐, such that for any node 𝑎 ∈ dom(𝜎), 𝑐 ≥ ledger (∆, 𝑎) and blocksFor (𝑃, 𝑎) = ∅ implies ledger (∆, 𝑎) = c

Probabilistic analysis

Kiran Gopinathan (University College London, UK), Ilya Sergey (Yale-NUS College and School of Computing, NUS, Singapore)