Project

General

Profile

Actions

Bug #1412

closed

32_7: add atomic_dec_and_mutex_lock to the model

Added by Alexey Khoroshilov over 13 years ago. Updated over 13 years ago.

Status:
Closed
Priority:
High
Assignee:
Category:
Rules and Models
Start date:
06/23/2011
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

Description

As soon as not all relevant functions are in the model, 32_7 is at level 3.


Related issues 1 (1 open0 closed)

Related to Linux Kernel Safety RuleDB - Feature #1940: 032: Locking a mutex twice or unlocking without prior lockingNew10/25/2011

Actions
Actions #1

Updated by Pavel Shved over 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?

Actions #2

Updated by Alexey Khoroshilov over 13 years ago

fs/ecryptfs/mmap.ko

Actions #3

Updated by Pavel Shved over 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...

Actions #4

Updated by Pavel Shved over 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.

Actions #5

Updated by Pavel Shved over 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.

Actions #6

Updated by Alexey Khoroshilov over 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?

Actions #7

Updated by Pavel Shved over 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.

Actions #8

Updated by Alexey Khoroshilov over 13 years ago

My limits were as follows:
RCV_TIMELIMIT=6000
RCV_MEMLIMIT=3840000

Actions #9

Updated by Pavel Shved over 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...

Actions #10

Updated by Pavel Shved over 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.

Actions #11

Updated by Pavel Shved over 13 years ago

By the way, the fixes on alias analysis have improved parsing, which made our middle tests fail today! :-)

Actions #12

Updated by Alexey Khoroshilov over 13 years ago

  • Status changed from Resolved to Closed

UNSAFE -> Out of memory in my run as well.

Actions

Also available in: Atom PDF