Abstracting and Verifying Decentralised Systems in CSP

Interest in decentralised systems such as blockchains and network computers has increased in the last few years, with increasing globalisation and distrust of centralised authorities. These systems typically comprise a loosely coupled population of both honest and malevolent (Byzantine) agents, communicating with each other using message passing. A significant issue in the design of decentralised systems is ensuring predictable (i.e. correct) behaviour despite malevolent agents being present. This paper uses CSP to formalise the programming of assemblies of distributed agents to operate as sequential state machines, or consensus machines, to achieve predictable outcomes. Such consensus machines may be live (guaranteed to complete, or total) or subject to deadlock (fail to complete, or partial), depending on the assumed proportion of malign agents in the assembly. An assembly of agents forming a consensus machine can be modelled in CSP in several alternative styles. This paper concentrates on how multiple consensus machines (whose agent sets may intersect) can mimic parallel threads communicating via single-writer shared variables, which may sometimes act as signals. Examples included are an application to a blockchain consensus protocol and a mutual exclusion algorithm. The effect of different communication assumptions on the implementation of shared variables is also analysed.