The Math Behind Distributed Sytems

Scaleconf Colombia Edition

Transcript

1. The (beauty of) math behind distributed systems Verónica López @maria_fbonacci SCALECONF COLOMBIA 2018
2. whoami • Software Engineer @ Red Hat • Formerly: physics •Academia + Industry • Trying to make computers and science converge
3. Agenda • Distributed Systems • Graph Theory • Topology
4. People ask benefts of math What if I’m not good at math?
5. Math is very useful for programming and systems design, but that might not mean what you think it means.
6. Math in CS • Basic: e.g.arithmetic, geometry (frontend), logic • Specifc: e.g. linear algebra (machine learning, big data), calculus (simulations) • General: e.g. graph theory, topology
7. Math in CS • Basic: e.g.arithmetic, geometry (frontend), logic • Specifc: e.g. linear algebra (machine learning, big data), calculus (simulations) • General: e.g. graph theory, topology
8. All these concepts have connectivity in common
9. Agenda • Distributed Systems • Graph Theory • Topology
10. Famous -and overused- quote about distsys…
11. “A distributed system is one in which the failure of a computer you didn’t even know existed can render your own computer unusable” Leslie Lamport
12. Ideal Distributed Systems • Fault-Tolerant • Highly available • Recoverable • Consistent • Scalable • Predictable Performance • Secure • Etc…
13. Design for Failure We can’t have it all (at the same time), so…
14. Design for Failure Probability Connectivity
15. Probability • If the probability of something happening is one in 10^13, how often would it happen? • “Real life”: Never • Physics: All the time. • Think about servers (infrastructure) at scale.
16. Connectivity
17. Agenda • Distributed Systems • Graph Theory • Topology
18. Graph Theory • The study of graphs: the mathematical structures used to model pairwise relations between objects. • Two concepts: nodes (vertices) & lines (edges) • Might be directed or indirected
19. The paper on the Seven Bridges of Königsberg (1736, Leonard Euler) is considered the frst paper in history of graph theory.
20. Graph Theory in Distsys • Design system’s connectivity • k-connectedness: how many nodes we need for a graph to disconnect a graph • Verify points of failure • Rearrange stuf
24. Agenda • Distributed Systems • Graph Theory • Topology
25. Topology • The study of geometric properties and spatial relations unafected by the continuous change of shape or size of fgures (formal) • Interrelation (informal)
26. Topological Properties • Properties that remain invariant under continuous stretching and bending of the object • E.g. Path connectivity, higher dimensional analogs
27. The paper on the Seven Bridges of Königsberg (1736, Leonard Euler) is considered the frst paper in history of topology (too!).
28. Topologically identical objects
29. Pyramids —> Division (triangulation) —> Sphere
30. Combinatorial (Algebraic) Topology • Studies spaces that can be constructed with discretized pieces • Allows to have all the (system) perspectives (of a node) available at the same time. • Perspectives evolve with communication
31. Agenda • Distributed Systems • Graph Theory • Topology
32. Formal Verifcation of a Distributed System • Talk & Articles: check the ACM List of methods that prove properties about a system. • Very hard to get! (Expensive and/or slow) • Only a few: AWS, Verdi, etc. •
33. Verifcation of a Distributed System • Formal Specifcation Languages (defnition & correctness) <- AWS • Model Checking (execute all paths) • Composition (more than 1 method)
34. Even after being formally verifed many systems still have bugs! Although not as much as unverifed ones Also: diferent type See: An Empirical Study on the Correctness of Formally Verifed Distributed Systems (Fonseca, et al.)
35. If it’s so hard, then why are there so many successful Distributed Systems, Verónica?!
36. “Verifcation” IRL • Monitoring & Observability tools: • On-Call Engineers & paging tools • Chaos Engineering: breaking things on purpose before they break for real Prometheus, New Relic, etc Modern testing approaches: thorough e2e, production •
38. Combinatorial Topology could be used to (help) formally verify a distributed system (through algebraic expressions)
40. Representing our distributed systems as topological objects allows us to visibly describe them and study its connections by sections or “worlds”
41. Combinatorial Topology • Visibility of every partition • Placing together all the views = • Frozen representation of all possible Interleavings and failure scenarios
42. Combinatorial Topology • Invariants: connections preserved as computation unfolds. • Topological objects are subject to proofs. • Representing systems as theorems and proving them = verifed systems
43. There’s a book! Distributed Computing Through Combinatorial Topology)
44. Extra resources • Algebraic Topology and Distributed Computing, A Primer http://cs.brown.edu/~mph/HerlihyR96/sv.pdf • The Topology of Distributed Adversaries https:// link.springer.com/article/10.1007/s00446-013-0189-9 • The Topological Structure of Asynchronous Computability http://cs.brown.edu/~mph/HerlihyS99/p858-herlihy.pdf • The Verifcation of a Distributed System http:// queue.acm.org/detail.cfm?id=2889274