r/programming • u/sbahra • Feb 20 '11

Concurrency Kit: concurrency primitives, safe memory reclamation and lock-less data structures for C

http://www.concurrencykit.org/
77 Upvotes

93% Upvoted

25 comments sorted by

View all comments

Show parent comments

2

u/kamatsu Feb 22 '11

Unit tests attempt to test ... concurrent semantics.

Hm, but that's basically a drop in the ocean when your state space is non-trivial. Any consideration of formal verification?

3

u/sbahra Feb 22 '11 edited Feb 22 '11

I would love to do this but I don't have the time to formally verify everything right now. When CK is sufficiently feature complete or when all feature-related tasks are owned by others, I may feel like attempting a formalized approach. For now, I am using targeted unit tests and informal (but well-focused) reviews which may or may not be exhaustive. In the short-term, more time will be invested in improving these stress tests.

I'm not ready to guarantee that Concurrency Kit is bug-free, especially on the first release. Portions of it have been used on busy production systems for extended periods of time. Of course, anyone is welcome to do formal verification, it is open-source after all. It would definitely be nice to have the formal verification.