v3 client protocol machine specification

[heyitsanthony]

Specifying the etcd v3 protocol in some proof or specification language (e.g., TLA+) would open more tooling options for making etcd solid. Purposes include: documentation, code synthesis, and verification.

At minimum it should:

• Represent the rules of updating/accessing etcd v3
• Be processable by a proof system
• Cover at least watch and kv semantics

Some example rules (which don't necessarily describe the current protocol nor what it should be):

• An update between two sequential linearized reads in time should be visible by the second read.
• The mod revision for a key across two sequential serialized reads should increase if the version increases.
• A version increases after a put if its create revision does not change
• A mod revision increases after a put if the create revision is not zero
• A watch at rev=0 starts at a revision greater than or equal to the last serialized revision in time
• All puts in a transaction have the same revision once committed
• All gets in a transaction are from the same point in time, if rev=0

Related: #7597, http://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf

[xiang90]

/cc @ericavonb

[ericavonb]

@dmonay

[stale]

This issue has been automatically marked as stale because it has not had recent activity. It will be closed after 21 days if no further activity occurs. Thank you for your contributions.