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

Re:How core.async and CSP help you prove your async code works by ghusbands on Thursday February 25, 2016 @11:06AM (#11175291)

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.

[ Parent | on HN ]

Re:How core.async and CSP help you prove your async code works by hoodunit on Thursday February 25, 2016 @11:49AM (#11175671)

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.

[ Parent | on HN ]

Re:How core.async and CSP help you prove your async code works by _halgari on Thursday February 25, 2016 @11:11AM (#11175344)

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.

[ Parent | on HN ]

Re:How core.async and CSP help you prove your async code works by PaulHoule on Thursday February 25, 2016 @11:38AM (#11175572)

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

[ Parent | on HN ]

Re:How core.async and CSP help you prove your async code works by nickpsecurity on Thursday February 25, 2016 @06:03PM (#11178562)

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.

[ Parent | on HN ]