https://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692011-06-24T07:17:18ZOpen-Source ProjectsLinux Driver Verification - Bug #1412: 32_7: add atomic_dec_and_mutex_lock to the modelhttps://forge.ispras.ru/issues/1412?journal_id=44512011-06-24T07:17:18ZPavel Shvedpavel.shved@gmail.com
<ul><li><strong>Category</strong> set to <i>Rules and Models</i></li><li><strong>Priority</strong> changed from <i>Normal</i> to <i>High</i></li></ul><p>Any sample driver that yields a false positive because of this?</p> Linux Driver Verification - Bug #1412: 32_7: add atomic_dec_and_mutex_lock to the modelhttps://forge.ispras.ru/issues/1412?journal_id=44742011-06-24T11:32:57ZAlexey Khoroshilovkhoroshilov@ispras.ru
<ul></ul><p>fs/ecryptfs/mmap.ko</p> Linux Driver Verification - Bug #1412: 32_7: add atomic_dec_and_mutex_lock to the modelhttps://forge.ispras.ru/issues/1412?journal_id=47272011-07-04T15:13:19ZPavel Shvedpavel.shved@gmail.com
<ul><li><strong>Status</strong> changed from <i>New</i> to <i>Open</i></li><li><strong>Assignee</strong> set to <i>Pavel Shved</i></li></ul><p>That's funny. A nice example of underestimation.</p>
<p>First, I added a test for model 32 with this function.</p>
<p>Then, I have implemented a model. Test was failing.</p>
<p>Then, I noticed that I missed a file in test Makefile, so I wrote a script to automatically generate it. Test was still failing.</p>
<p>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.</p>
<p>Then, I noticed that <code>atomic_dec_and_mutex_lock</code> 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 <code>-reroute-map2</code>. Tests kept failing.</p>
<p>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...</p> Linux Driver Verification - Bug #1412: 32_7: add atomic_dec_and_mutex_lock to the modelhttps://forge.ispras.ru/issues/1412?journal_id=47282011-07-04T16:20:42ZPavel Shvedpavel.shved@gmail.com
<ul><li><strong>Status</strong> changed from <i>Open</i> to <i>Resolved</i></li></ul><p>Fixed in <a class="changeset" title="Add script for easy makefile generation for tests with different modules (useful in model tests)." href="https://forge.ispras.ru/projects/ldv/repository/98/revisions/7aca71ae9bfaeae46250b5692753386aaecbd4ed">7aca71a</a>. Small and model tests are passed, but watch out for nightly tests today!</p>
<p>The driver you supplied yields Memory limit for me, so couldn't check it properly.</p> Linux Driver Verification - Bug #1412: 32_7: add atomic_dec_and_mutex_lock to the modelhttps://forge.ispras.ru/issues/1412?journal_id=47292011-07-04T16:55:20ZPavel Shvedpavel.shved@gmail.com
<ul></ul><p>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.</p> Linux Driver Verification - Bug #1412: 32_7: add atomic_dec_and_mutex_lock to the modelhttps://forge.ispras.ru/issues/1412?journal_id=47302011-07-05T05:56:03ZAlexey Khoroshilovkhoroshilov@ispras.ru
<ul></ul><p>Pavel Shved wrote:</p>
<blockquote>
<p>The driver you supplied yields Memory limit for me, so couldn't check it properly.</p>
</blockquote>
<p>To which size did you try to increase memory limit?</p> Linux Driver Verification - Bug #1412: 32_7: add atomic_dec_and_mutex_lock to the modelhttps://forge.ispras.ru/issues/1412?journal_id=47312011-07-05T08:56:58ZPavel Shvedpavel.shved@gmail.com
<ul></ul><p>Alexey Khoroshilov wrote:</p>
<blockquote>
<p>To which size did you try to increase memory limit?</p>
</blockquote>
<p>I assumed that everything you had not specified was either default or not important. Default memory limit for Git is approx. 1500 Mb.</p> Linux Driver Verification - Bug #1412: 32_7: add atomic_dec_and_mutex_lock to the modelhttps://forge.ispras.ru/issues/1412?journal_id=47542011-07-05T13:20:25ZAlexey Khoroshilovkhoroshilov@ispras.ru
<ul></ul><p>My limits were as follows: <br />RCV_TIMELIMIT=6000<br />RCV_MEMLIMIT=3840000</p> Linux Driver Verification - Bug #1412: 32_7: add atomic_dec_and_mutex_lock to the modelhttps://forge.ispras.ru/issues/1412?journal_id=47552011-07-05T15:10:11ZPavel Shvedpavel.shved@gmail.com
<ul><li><strong>Status</strong> changed from <i>Resolved</i> to <i>Open</i></li></ul><p>Ok, I increased the memory limit, and found out that BLAST crashes without any useful error! Investigating...</p> Linux Driver Verification - Bug #1412: 32_7: add atomic_dec_and_mutex_lock to the modelhttps://forge.ispras.ru/issues/1412?journal_id=47562011-07-05T16:25:58ZPavel Shvedpavel.shved@gmail.com
<ul><li><strong>Status</strong> changed from <i>Open</i> to <i>Resolved</i></li></ul><p>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!)</p>
<p>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.</p> Linux Driver Verification - Bug #1412: 32_7: add atomic_dec_and_mutex_lock to the modelhttps://forge.ispras.ru/issues/1412?journal_id=47592011-07-06T08:27:03ZPavel Shvedpavel.shved@gmail.com
<ul></ul><p>By the way, the fixes on alias analysis have improved parsing, which made our middle tests fail today! :-)</p> Linux Driver Verification - Bug #1412: 32_7: add atomic_dec_and_mutex_lock to the modelhttps://forge.ispras.ru/issues/1412?journal_id=52572011-08-10T05:44:49ZAlexey Khoroshilovkhoroshilov@ispras.ru
<ul><li><strong>Status</strong> changed from <i>Resolved</i> to <i>Closed</i></li></ul><p>UNSAFE -> Out of memory in my run as well.</p>