[agentultra]

> 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

[masklinn]

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.

[agentultra]

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.

[nickpsecurity]

"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.