News for hackers. Stuff that matters.

A comment on Fear and Loathing in Lock-Free Programming.

Re:Fear and Loathing in Lock-Free Programming by fulafel on Monday October 09, 2017 @02:08PM (#15436086)
What is the state of the art in building high assurance lock free components? Are there type systems or proof assistants that are workable?
[ Parent | on HN ]
Re:Fear and Loathing in Lock-Free Programming by krenoten on Monday October 09, 2017 @02:41PM (#15436341)
SPIN is a nice tool for modeling them. You can extract code from a coq model. You can go into the world of dynamic instrumentation to try to verify invariants in implementations.
[ Parent | on HN ]