How core.async and CSP help you prove your async code works | Hacker News Reader

How core.async and CSP help you prove your async code works

reaktor.com

83 pointslarry_pi17 comments

> How can I know that my sync algorithm works?

TLA+ is one such language that can help you. It models computation at a higher level using the Temporal Logic of Actions. Essentially you define some variables to model your problem in and declare a bunch of next-state relations. You can then check your design against your correctness and liveness invariants to see if your expectations hold against all possible executions.

If you are so inclined you can even go as far as proving it correct.

I recently just grasped the proof of the strong-fairness property and it's amazing to me that we don't use predicate and temporal logic more frequently in software development.

There are other languages of course such as Event-B and Z, but I find for learning these concepts TLA+ is a great introduction.

[0] https://www.youtube.com/watch?v=iCRqE59VXT0

FWIW the linked article is just the problem description, the interesting stuff is part II which talks about CSPm (and FDR3) whose whole point is asserting properties of CSP models.

That is much better.

So the take away here is that modelling in the domain of CSP is easier because some language frameworks directly implement CSP?

I guess that's one of the challenges I'm having learning TLA+ and formal methods. I have this high-level specification of a semaphore lock that the model checker can verify and might even have a proof. How do I now implement this in code?

But that's kind of moot: a blueprint doesn't implement the building. However if we follow the blueprint, if our reasoning was sound and the mathematics hold, then the sky-scraper will stand and everyone is happy.

What's neat about FRP and functional languages like Haskell is that we can encode some of the correctness invariants into the type system; essentially having the compiler guarantee the implications for us. (Or as TFA mentions, directly synthesize our CSP program from the specification; which seems very neat but restrictive...)

And what's really cool about strong fairness is that it doesn't say anything about when a relation has to happen. It could be that your lock will be held for a thousand years before the next process gets to acquire it... but the strong fairness property guarantees it will happen.

The question may then be... well what about the implementation? How do I know it will satisfy this property without waiting for the heat-death of the universe? Computers are not theoretical machines. They are complex, physical devices with non-theoretical limitations. They won't last until the heat-death of the universe so don't worry. You can prove that every process will get a chance to acquire the lock in the implementation without saying anything about the specification.

The reason why I thought this was beautiful was because now we can reason about the soundness of our design without concerning ourselves with timers, memory limitations, network connectivity... etc, etc. The properties of those things will change over time but our specification will remain solid and useful.

All very interesting stuff and to answer the conclusion, yes I think adoption of these tools and ways of thinking can be done in practice by the wider industry. I'd even go as far as saying that it's necessary. If we want software developers to become capital-P professional software engineers we need to introduce liability and rely on tools to verify the soundness of our thinking before we go asking the world to trust our creations.

I don't think the math is terribly difficult; the problem is that thinking is hard and programmers don't seem to enjoy doing it very much. For some reason computer science is allergic to math and programmers in industry think their job is to write code. CSPm is neat but you're so close to a more general and useful language one step up.

"I have this high-level specification of a semaphore lock that the model checker can verify and might even have a proof. How do I now implement this in code?"

You do them side by side in a way that looks and behaves similarly. That's the traditional route going back to Orange Book A1-class systems. The seL4 work did something similar. Two other routes are: (a) gradually refining abstract spec into something concrete enough for code like B method does; (b) using tools like Coq that support extraction of code from specs. Also look into "abstract state machine" specification, code, generation, and so on. Much work happened under that label in both hardware and software.

Big hairy core.async go blocks like shown in these articles makes me a tad uneasy (see the sync source in the second part to this article). Because they seem to be programmed in a mostly imperative style. Almost every time I see a go block loop, I see code that could be better written with core.async/pipeline. `If` statements can be come filters, transformations can become map. And with the addition of transducers all this becomes much cleaner.

So in that sense, I think many FRP-esque libraries have something going for them, they force their users into a model that is more declarative than imperative. That sort of programming can and should be done with core.async. Go blocks are a primitive, build abstractions on top of that and keep your app code declarative.

The go blocks in here are really ugly, but to be honest I just found it difficult to refactor in this particular case. The issues were a) I wanted all the events in a single event loop to make timing issues clear and to fit the model semantics better b) core.async go blocks, because they are macros, can't be refactored like functions (>! and such need to be in a go block) and c) the sync logic otherwise was easier to reason about with all of the logic in one place. One better way to factor this would be to have a declarative format for what each action performs, but it ended up being more difficult to follow the logic when I refactored it this way. Types would help, and I think in general there is unexploited potential for types and CSP and FRP approaches. But if you have suggestions for how to make this better I'm all ears.

The only things that have been shown are that an overly simplified CSP model of what the author is actually doing might work, that the author does not have a clear understanding of concurrency, and that the author is prone to making grandiose claims like "The matching of models means that CSP can be used to solve complex problems using core.async in a way that would be more difficult using another approach like functional reactive programming or actors", without basis.

In this particular case, uniquely-identified, timestamped property updates, with last-update-wins, for named objects, would have trivially worked, in any language, without the modelling complications. Actors, FRP and CSP are all capable of doing that, without error.

Agreed, I'm not even convinced you need anything async here. In that sense you could probably write this with OS threads and you language of choice.

Generally I see the idea that "technology X makes the problems of concurrency go away" is a bad smell.

In the JVM world I am always seeing people screwing around with Actors and things like that and failing and then after days of suffering I break out some simple Executor and I have it working correctly in 10 minutes and performance tuned in another 10.

Look at the example of the LMAX Disruptor to see how adults face reality and develop real solutions instead of snake oil.

I like ReactiveX because it provides a way for thinking about these things that is cross language

The only ones I've seen that delivered [with caveats] were Concurrent Pascal, Ada's Ravenscar, Eiffel's SCOOP, and recently Rust. SCOOP got the most CompSci work with a Java port, one proving no deadlocks, one proving no livelocks, a formal verification in Maude that caught problems, and one modification to almost entirely eliminate performance penalty.

So, it can happen but does rarely enough to arouse strong skepticism. I usually don't buy it.

I admit the claim is overly grandiose, especially in this particular case where there's still a decent gap between core.async and CSPM. If one generated Haskell code directly from CSPM it might be a stronger claim for that, but I haven't had a chance to try this yet. It would be interesting to see if it would be possible to develop tools to prove correctness of e.g. core.async programs.

Having a stream of every unique action and making sure everyone gets the stream of actions and applies them in order was another approach I've thought about, if that's what you mean here. I may have to try rewriting in this style. What I think is interesting about the algorithm I was shooting for is that you can miss events and just diff with the current state. But it may be that this is just an overly complex approach. If you have any other pointers or links as to how you might implement it in your described style I would be interested.

This is a bad title. The only point at which the post even talks about FRP is in the sentence "And are there practical reasons that a library based on the CSP language is useful in ways that, say, an FRP or functional reactive programming library is not?". Doesn't mention FRP after that, not even in part II.

My bad, I just noticed that too and changed the title to reflect it. Thanks for pointing it out!

Couchbase is perfect for this use case and, in fact, a grocery list app that syncs between clients is their primary demo app.

This article doesn't talk about FRP at all. The title should be changed

Thanks for pointing it out - title changed to better fit article content.

That thing where someone calls core.async CSP and my eyelid twitches.

Reading the paper, it has very little to do with core.async.

Reply on news.ycombinator.com