Keeping CALM: when distributed consistency is easy • Hacker News Board

Re: Keeping CALM: when distributed consistency is easy

#31

Post by bradleyjg » Wed, Mar 06, 2019, 8:02 PM UTC

jerf wrote: post #13

I expect that the continuing popularity and necessity of distributed programming is going to finally put an end to the idea that "programming doesn't involve mathematics". It is just so much easier if you approach it from the sort of mathematical mindset demonstrated in this paper, and exactly as discussed, this is going to be a whole-stack affair, not something that can be isolated to just the data layer, despite ou…

We aren’t there yet, but we are approaching the day when substantially everyone with the capability of rebalancing a red/black tree on a whiteboard and an inclination to program is either programming or in some other way connected to the function. If a yet higher level of mathematical ability and knowledge becomes necessary, shortages are going to become even more acute. That’s good for some of us but bad for the world. The world would be better off if we could figure out a way to lower that bar, not raise it.

Re: Keeping CALM: when distributed consistency is easy

#32

Post by [deleted] » Wed, Mar 06, 2019, 8:08 PM UTC

DanielBMarkham wrote: post #8

This is outstanding -- although in lieu of Yet Another New Programming Language (YANPL), I would suggest simply having developers learn the concepts and apply them no matter what environment they're in. This should be part of any developer's education. I have some good friends, smart people who know a lot more about good programming than I ever will, who keep saying things like "OO and FP are just different flavors.…

[deleted]

Re: Keeping CALM: when distributed consistency is easy

#33

Post by nickpsecurity » Wed, Mar 06, 2019, 8:29 PM UTC

deegles wrote: post #17

agentultra wrote: post #16

Earlier quoted context omitted.

I think this has been the case for many decades. Lamport, the Turing award winning mathematician and computer scientist who wrote seminal algorithms and papers on distributed consensus, invented TLA+ for this express purpose. A programming language is insufficiently expressive enough to specify and guarantee the safety and liveness properties of a multi-agent system. I think formal methods and program synthesis are g…

What's a good small project + stack for someone to start with formal methods and/or program synthesis?

Formal verification is really hard because you have to use mathematical proof to show that a piece of software does what it should on all inputs and paths. You have to formalize the software, the desired goals, and prove a connection. Typically, you have to do this for software written in languages that aren't designed for verification. That makes it even harder.

This led me to recommend people start with so-called lightweight, formal methods that require less upfront learning with more automation. You'll see the value of formal methods, have more fun, and maybe use it on realistic problems. The best one to start with is Design-by-Contract invented by Meyer in the 1980's based on principles from 1960's. Contracts are simply precise, declarative descriptions of a module expects from callers, does during execution, and returns to the caller. Here's an overview even a project manager can find useful:

https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b...

A number of us independently arrived at a specific use for contracts that's high ROI. You use contracts to specify intent, then automatically generate tests from them (replaces unit testing), and finally they can become runtime checks for automated testing (esp fuzzing). Contract-based tests or fuzzing with contract-based checks cause each failure to take you right to the source of the problem. Note that the test generation part has many names to Google: specification- or spec-based, model-based, and recently property-based testing. Hillel Wayne has great posts on contracts and test generation:

https://hillelwayne.com/post/contracts/

https://hillelwayne.com/post/pbt-contracts/

I recommend reading his whole blog. Anyway, the next tool is Alloy which is super-simple but with better tooling than most academic works. Hillel has examples on his blog. Davidk01 on Lobste.rs has been using it for a lot of things. He said, given its relational, he just uses it like he uses SQL:

https://lobste.rs/s/ghhcus/test_generation_from_bounded_alge...

Finally, one that will help you with protocols and concurrency is TLA+. Hillel has learntla.com up to teach you for free on top of blog examples. After a lot more time with it, he got to publish a book through Apress. I recommend it:

https://www.betterworldbooks.com/product/detail/Practical-TL...

If you want a taste of proof, the SPARK Ada language was designed to make it easier. It's used in industry. Basically uses contract-like specs and supporting functions to feed "verification conditions" into automated solvers. You only have to prove what they can't but can always use runtime checks on those. There's a nice book teaching you how to use it plus Altran/Praxis' Correct-by-Construction method for low-defect software.

https://www.betterworldbooks.com/product/detail/Building-Hig...

There's also Cleanroom: a 1980's method that combines semi-formal specs, simple use of language, hierarchical composition, and usage-based testing to cost-effectively get high quality software. Stavely has best intro to it:

http://infohost.nmt.edu/~al/cseet-paper.html

https://www.betterworldbooks.com/product/detail/Toward-Zero-...

Note: Linking to Better World Books since they're a public-benefit type of company (see History). Amazon ain't. ;)

Re: Keeping CALM: when distributed consistency is easy

#34

Post by sagichmal » Wed, Mar 06, 2019, 8:43 PM UTC

oggy wrote: post #9

kilburn wrote: post #5

Earlier quoted context omitted.

The benefits we want to obtain from building distributed systems are: 1) Increased availability 2) Ability to scale (better throughput) 3) Lower latency (get the data closer to the client) As you said, WAL + Consensus solves the consistency problem in distributed systems. It does however go against all those desirable properties: 1) You lose availability when consensus cannot be reached 2) Throughput is decreased in…

That's an excellent explanation, except for couple of points which I think can be misinterpreted. A distributed system with consensus will in practice provide higher availability than a single-node system, because it provides fault-tolerance. In fact, fault-tolerance is the primary point of using (non-Byzantine) consensus. But you are absolutely right that a distributed system using consensus has worse availability t…

> A distributed system with consensus will in practice provide higher availability than a single-node system, because it provides fault-tolerance.

I'm not sure this is true. It protects against one class of fault (node failure) but opens you up to another (network failure). As a distsys engineer I am increasingly convinced that fault tolerance is not a good selling point for distribution, the fallacies of distributed computing are real and difficult to accommodate.

Re: Keeping CALM: when distributed consistency is easy

#35

Post by strictfp » Wed, Mar 06, 2019, 9:34 PM UTC

Interesting results.

The results seem very useful when reasoning about coordination in programs, but I'm questioning how practically useful these results are when applied as methods.

In the GC example, for instance, you do need to find the garbage nodes. Any trivial way of re-formulating that search in a monotonic way would likely destroy performance. My guess is that it's no silver bullet to solving problems in distributed systems.

Re: Keeping CALM: when distributed consistency is easy

#36

Post by senderista » Wed, Mar 06, 2019, 10:16 PM UTC

mjb wrote: post #30

jerf wrote: post #19

Earlier quoted context omitted.

I'd actually suggest rather becoming fluent in modern Haskell. Formal methods are great in their own way but for a lot of programming tasks they overshoot the mark. For those that do not, by all means, bring them in. But right now, a practical engineer can't ignore just how klunky they are and how badly they scale up. One may gaze longingly at them, and dream fondly of the future date when they are more practical, bu…

Many formal methods have a much simpler mathematical foundation than Haskell. For example, for TLA+ the background includes mostly (basic) set theory, basic logic, and some additional bits of temporal logic. Some methods do require a lot more math, or different math, but I'd say your statement is false for the majority of popular formal methods.

Indeed, I heard Lamport say at a talk (in response to a question) that he saw little or no applications of functional programming to the distributed systems problems he was interested in.

Re: Keeping CALM: when distributed consistency is easy

#37

Post by steveklabnik » Wed, Mar 06, 2019, 10:30 PM UTC

jerf wrote: post #21

zzzcpan wrote: post #20

Earlier quoted context omitted.

I disagree, I think the future still holds separate data layer, but even less math because of how much easier it will be to reason about programs with DSLs built on solid foundations for distributed systems and how much harder it will be to keep doing things the old ways. Imagine a new language for databases, like SQL, but that can actually guarantee convergence and coordination freedom, where there are no transactio…

I think you'll find that if you encode these guarantees into the language level itself, that won't allow the programmers involved to stop thinking about the math. Either your language won't allow them to express the first thing they want to express, and they'll have to figure out how to do it with the proper mathematical primitives (and they'll complain up a storm about how useless your language is on the forums), or…

It’s funny; I think of Rust as freeing me from having to think of this. The compiler checks it for me, so I just don’t have to think about it at all.

Re: Keeping CALM: when distributed consistency is easy

#38

Post by mpweiher » Thu, Mar 07, 2019, 8:44 AM UTC

DanielBMarkham wrote: post #8

This is outstanding -- although in lieu of Yet Another New Programming Language (YANPL), I would suggest simply having developers learn the concepts and apply them no matter what environment they're in. This should be part of any developer's education. I have some good friends, smart people who know a lot more about good programming than I ever will, who keep saying things like "OO and FP are just different flavors.…

> OO and FP are just different flavors.

Yes, current incarnations are really just variations of the call/return architectural style. Quite limited, actually.

> Pure FP takes you places like this essay.

Bold statement. OO has taken us to...let's see...all of personal computing. And somewhat smaller, but related, to Multi Version Concurrency Control: http://publications.csail.mit.edu/lcs/pubs/pdf/MIT-LCS-TR-20...

> code at scale

"Of the candidates enumerated in 'NSB', object-oriented programming has made the biggest change, and it is a real attack on the inherent complexity itself." - Fred Brooks, No Silver Bullet Reloaded

Re: Keeping CALM: when distributed consistency is easy

#39

Post by elisharobinson » Thu, Mar 07, 2019, 10:44 AM UTC

jerf wrote: post #27

elisharobinson wrote: post #25

Earlier quoted context omitted.

I'm being honest here I don't quite understand all the math involved . But from my rough skimming of the text looks like we are sacrificing the flexibility to change any input or minor design changes for guaranteed correctness .. am I wrong

It's more like "the flexibility to change any input" produces incorrect behavior, full stop. When it comes to distributed systems, you have to be following some mathematical idea of how you're going to maintain some sort of consistency or correctness, or it just won't happen. The environment is just so much more hostile than the ones most people are used to. Most programming methodologies haven't grown up in the pres…

I respect what you are trying to say and im not denying that safety as a mathatical guarantee is a must .. but help me understand the full picture here how would such a system work with soft dev today when requirements change very quickly, sometimes small somtimes large ... for example our current sdlc looks like this

mockup --> requirement change --> design --> build --> requirement change --> mockup

rinse and repeat, the cycle time might change but this is what happens .. is this ideal I don't know .. does this work, it does sufficiently enough

and so I disagree that people in the broader software dev community are willfully ignorant about security

maybe with the rise of AI we could do the design problem with the math bits in mind and build correct software every cycle but from my perspective the only way I see the system of mathematical design which is math intensive (hence resource intensive hence time intensive) is through the waterfall model of SDLC :).

I am willing to admit that I haven't been following the formal methods space that much and what I said might be complete of the mark, in any case, please feel free to correct me, I'm here to learn thanks.

Re: Keeping CALM: when distributed consistency is easy

#40

Post by DanielBMarkham » Thu, Mar 07, 2019, 11:09 AM UTC

mpweiher wrote: post #38

DanielBMarkham wrote: post #8

This is outstanding -- although in lieu of Yet Another New Programming Language (YANPL), I would suggest simply having developers learn the concepts and apply them no matter what environment they're in. This should be part of any developer's education. I have some good friends, smart people who know a lot more about good programming than I ever will, who keep saying things like "OO and FP are just different flavors.…

> OO and FP are just different flavors. Yes, current incarnations are really just variations of the call/return architectural style. Quite limited, actually. > Pure FP takes you places like this essay. Bold statement. OO has taken us to...let's see... all of personal computing . And somewhat smaller, but related, to Multi Version Concurrency Control: http://publications.csail.mit.edu/lcs/pubs/pdf/MIT-LCS-TR-20... > c…

I think we're mixing some things up here. If I have added to that confusion, I apologize.

Yes, OO is great. It's all of modern computing. Love me some abstraction levels -- as long as they actually abstract things. Any layer that I spend more time screwing around with other than making things people want is a net negative.

And there's my point: I'm not talking about the mechanics of FP or OO. I'm also not talking about the relative successes or failures of either model. My only point was how various modes of thinking end up solving problems different ways.

I find this a recurring theme. At the end, it's all Category Theory. So we're not talking about magic sprinkles here. Whatever we put on top of the math to help us reason about problems -- OO, FP, pure FP, and so on -- has various effects on the way we reason about problems.

Hell I don't care if you program COBOL. What's fascinating to me is how some folks read essays like this and go "Of course! Very cool" and others start talking about how it's all theoretical.

I read half-assed essays everyday that could mostly be described as some version of "I learned OO and now I think of everything as objects" The natural consequences of this thing -- which is not wholly bad -- is the same as the natural consequences of poor abstraction layers in coding: the person using them spends more time thrashing around trying to keep consistency and nomenclature aligned than they do working on the important stuff. Can you do the same with FP? Sure! But that's a conversation for a different day -- because it's a different failure mode.