4 ms·
Well, 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 de
by _yosefk 14y ago
Well, 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.)