Verifying Concurrent Programs Using Contracts (2017) [pdf]

fit.vutbr.cz

49 pointsadamnemecek5 comments

Interesting.. I've been trying/playing with a home-made modelling language to describe concurrent program flow and job conditions. Mostly in the context of queue-based-workers. The idea that a job can be split up in different parts and be run concurrently. Haven't cracked it yet :/

You might get something out of looking at lava:

https://github.com/LiveAsynchronousVisualizedArchitecture/la...

Concurrency really comes from being able to split up data in isolated chunks that have access to all their dependencies. When you think in terms of data and not tasks, things make a lot more sense.

Have you tried TLA+ and PlusCal?

Nope! But looking into it now :) Thank you sir !

Seems like the tool they developed to perform verification, has been abandoned since 2014: https://github.com/trxsys/gluon.

Reply on news.ycombinator.com