3 ms·
Jinx can help verify mutex implementations themselves, although the example code that ships with the product is a little more advanced (lock-free stack). Some
by Kaya 16y ago
Jinx can help verify mutex implementations themselves, although the example code that ships with the product is a little more advanced (lock-free stack). Some of the underlying technology is described here: http://s3.amazonaws.com/corensic/whitepapers/DeterministicSharedMemoryMultiProcessing.pdf http://s3.amazonaws.com/corensic/whitepapers/DeterministicSh... and here: http://www.corensic.com/WhyYouNeedJinx/CorensicHasaUniqueTechnologyforFindingBugs.aspx http://www.corensic.com/WhyYouNeedJinx/CorensicHasaUniqueTec.... Because it's a hypervisor, it can aid in verifying synchronization primitives that are a mix of userspace and kernel code.
- dvyukov 16y agoI do not see anything about memory fences. If Jinx does not support them, then it's pretty much useless for verification of synchronization algorithms. I've implemented dozens of advanced synchronization algorithms, and I may say that it's crucial. Also, if it works on binary level (does not require re-compilation), then it also renders it useless, because on that level you lose information about order of memory accesses, memory fences, atomicity. For example, if you see plain x86 MOV instruction, what is it? non-atomic store? atomic relaxed store? atomic release store?