3 ms·
Do you have any proofs of correctness for this at all? You claim to be able to detect almost all data race conditions, but I don't see much evidence for that in
by octo_t 14y ago
Do you have any proofs of correctness for this at all? You claim to be able to detect almost all data race conditions, but I don't see much evidence for that in the blog post.
Is all of the necessary work being offloaded to Valgrind?
- _yosefk 14y agoWell, no formal proof, but give me one counter-example and maybe we can work from there :) The post does have an informal kind of "proof" (there are various degrees of "formality"...) where I cover the various cases. What's "all of the necessary work"? You mean is there an overhead due to checking? I think very little - maybe you could count as overhead the fact that you can swap schedulers at run time, the cost here is a call through a function pointer. (I could have done it as a compile time option of course, I just don't think the tiny overhead is worth the rather large trouble to the user.)
- octo_t 14y agoBy necessary work I meant "Valgrind has associated proofs of correctness so transforming parallelisations into things valgrind can more easily diagnose". (Disclaimer: my research is on safer parallel programming)
- _yosefk 14y agoI'd be glad to discuss this over email if you like; the upshot is that I don't think there's anything formally proven anywhere along the way, but it might be interesting to discuss if it theoretically could be (that is, given a hypothetical imperative language, is fork/join code possible to fully verify as I believe or not.)