Specification of the Byzantine tolerant RSM Sample Clauses

Specification of the Byzantine tolerant RSM. ≤ − The replicated state machine is composed of n replicas, which start in the initial empty state s0. Among them, up to f (n 1)/3 replicas may exhibit Byzantine failures. The RSM exposes two operations, update and read, such that the update operation with command cmd modifies the current state s of the RSM by applying cmd to s but does not return any value, while the read operation returns the current state of the RSM. The state of the RSM at time t is a set of update commands applied to the initial state s0 until time t. Note that being the RSM commutative the order in which updates are applied does not matter. Clients may trigger an infinite number of read and update operations. We assume that each command is unique (which can be easily done by tagging it with the identifier of the client and a sequence number). We do not make any assumptions regarding clients behavior: they can exhibit arbitrary behaviors (e.g., invoke an update operation with some arbitrary command, or modify the read and update code). We do not limit the number of Byzantine clients. Hence, to prevent Byzantine clients from jeopardizing the state of the RSM through arbitrary commands, commands are locally executed by clients: the RSM provides clients with a set of updates and clients locally execute them. For readibility reasons, the value returned by the execution of a set of commands is equal to the set of commands. The following properties formalise the behavior of read and update operations during any execution run by correct clients: • Liveness Any update and read operation completes;