Bug #1412
closed32_7: add atomic_dec_and_mutex_lock to the model
Added by Alexey Khoroshilov almost 13 years ago. Updated over 12 years ago.
0%
Description
As soon as not all relevant functions are in the model, 32_7 is at level 3.
Updated by Pavel Shved almost 13 years ago
- Category set to Rules and Models
- Priority changed from Normal to High
Any sample driver that yields a false positive because of this?
Updated by Pavel Shved almost 13 years ago
- Status changed from New to Open
- Assignee set to Pavel Shved
That's funny. A nice example of underestimation.
First, I added a test for model 32 with this function.
Then, I have implemented a model. Test was failing.
Then, I noticed that I missed a file in test Makefile, so I wrote a script to automatically generate it. Test was still failing.
Then, I noticed that model 32_1 and model 32_7 actually, have different files. I copied the model function to that of 32_7. Test was still failing.
Then, I noticed that atomic_dec_and_mutex_lock has, actually, two arguments, and only the second one should be rerouted. This functionality was missing from the rerouter. So, I fixed the rerouter in BLAST, adding a new option -reroute-map2. Tests kept failing.
Then, I noticed that I should also add this to RCV backend. Now the tests is passed, and the fix is being tested on LDV-git...
Updated by Pavel Shved almost 13 years ago
- Status changed from Open to Resolved
Fixed in 7aca71a. Small and model tests are passed, but watch out for nightly tests today!
The driver you supplied yields Memory limit for me, so couldn't check it properly.
Updated by Pavel Shved almost 13 years ago
This model may yield some false positives now, as the atomic counter has been modelled as an undefined value. I've launched the whole-kernel check, and we'll see tomorrow if it worked.
Updated by Alexey Khoroshilov almost 13 years ago
Pavel Shved wrote:
The driver you supplied yields Memory limit for me, so couldn't check it properly.
To which size did you try to increase memory limit?
Updated by Pavel Shved almost 13 years ago
Alexey Khoroshilov wrote:
To which size did you try to increase memory limit?
I assumed that everything you had not specified was either default or not important. Default memory limit for Git is approx. 1500 Mb.
Updated by Alexey Khoroshilov almost 13 years ago
My limits were as follows:
RCV_TIMELIMIT=6000
RCV_MEMLIMIT=3840000
Updated by Pavel Shved almost 13 years ago
- Status changed from Resolved to Open
Ok, I increased the memory limit, and found out that BLAST crashes without any useful error! Investigating...
Updated by Pavel Shved almost 13 years ago
- Status changed from Open to Resolved
Alias analysis (which was partly on!) was failing on some anonymous fields or something. Didn't want to dig up, just made it a warning instead of an error, and turned alias analysis off completely (this should save several hours, or, perhaps, even days, for a typical ldv-git run!)
The driver still yields memory limit on my machine. However, the previous version of the rule thought that there's a potential error on iteration 7431, while the new version gets as far as to iteration 8654! Definitely, something happens here. Marking as resolved.
Updated by Pavel Shved almost 13 years ago
By the way, the fixes on alias analysis have improved parsing, which made our middle tests fail today! :-)
Updated by Alexey Khoroshilov over 12 years ago
- Status changed from Resolved to Closed
UNSAFE -> Out of memory in my run as well.