Feature #7783
closed
Support lightweight data races detection
Added by Evgeny Novikov over 7 years ago.
Updated over 7 years ago.
Description
Now we do need to have this support in master. Since in addition we have to merge there a still incomplete new approach for processing witnesses, please, leverage corresponding new abilities.
- Priority changed from Immediate to High
It turned out that we don't need this in master right now, so you can do this one day. Likely this should be done after or together with upcoming refactoring of VTG since it will touch some related issues.
- Priority changed from High to Urgent
This task can be implemented at last since the blocking issue #7617 was fixed. I expect you will suggest some straightforward mechanism for grabbing and reporting several witnesses that will not affect all other rule specifications anyhow.
Datarace detections needs MEA approach. How it is implemented in master?
Current code for VTG strategies and for scheduler do not properly work with BenchExec and needs to be rewriten to support MEA.
It doesn't need that approach since this comes with the completely specific rule specification and even very specific verification approach & tool. It just can leverage something from it like it was before, but it shouldn't do this. Taking into account that current master is absolutely free from any nonstandard verification task generation and processing techniques (#7617) and they are very far from it, I assume that Pavel will develop quite simple and straightforward approach for processing several witnesses and preparing corresponding reports to bring this high demanded rule specification to master at last. Perhaps later some parts of implementations can be combined but this also isn't very necessary.
Race detection do not use a specific verification tool - the tool is a cpachecker, and uses the same BenchExec tool-info module (cpachecker.py) as all the others instances of CPAchecker in SV-COMP (https://sv-comp.sosy-lab.org/2017/systems.php).
Race detection needs the same functionality as MEA and suffers from the same problems described in #7877
Nevertheless Pavel will add specific support for finding data races in several days. All considerable improvements will be made just in several months or even years.
I don't think that another crutch is the right way to go
- Status changed from New to Closed
Implemented in branch races2 that I merged to master in b48cce6. So, now everybody can try to find data races. Please refer to description of rule specification sync:race to find out proper CPAchecker version to be used for that. Keep in mind that non standard repository https://github.com/mutilin/cpachecker-ldv.git should be used.
Also available in: Atom
PDF