Hacker News new | ask | show | jobs
by fulafel 3180 days ago
What is the state of the art in building high assurance lock free components? Are there type systems or proof assistants that are workable?
1 comments
krenoten 3180 days ago
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.
link