https://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692012-04-09T10:08:17ZOpen-Source ProjectsLinux Kernel Safety RuleDB - Feature #1940: 032: Locking a mutex twice or unlocking without prior lockinghttps://forge.ispras.ru/issues/1940?journal_id=89942012-04-09T10:08:17ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>The problem with mutex (un)locking is presented in commits 4a349aa and 8a9f335 (which are found by LDV explicitly) of the linux-stable branch. <br />Our 32_1 model allows to find the problem in the commit 4a349aa with help of BLAST (CPAchecker doesn't find the given problem because of time out, but find another one, that is safe for BLAST). A bug fixed by commit 8a9f335 is found by BLAST before fix but after fix it has a memory limit even with 6Gb. CPAchecker cannot check a driver both before and after fix because of issues like described in <a class="issue tracker-4 status-3 priority-4 priority-default" title="Feature: 101: All obtained blk requests should be put after all (Resolved)" href="https://forge.ispras.ru/issues/2706">#2706</a>.</p> Linux Kernel Safety RuleDB - Feature #1940: 032: Locking a mutex twice or unlocking without prior lockinghttps://forge.ispras.ru/issues/1940?journal_id=92892012-04-25T10:22:22ZVadim Mutilinmutilin@ispras.ru
<ul></ul><ul>
<li><strong>c8a9f335</strong> may lead to a race condition, because of unprotected call to arl9170_set_operating_mode</li>
<li><strong>4a349aa</strong> double mutex_unlock (but cannot say that it is a deadlock)</li>
</ul> Linux Kernel Safety RuleDB - Feature #1940: 032: Locking a mutex twice or unlocking without prior lockinghttps://forge.ispras.ru/issues/1940?journal_id=125882012-08-07T07:06:26ZAlexey Khoroshilovkhoroshilov@ispras.ru
<ul><li><strong>Subject</strong> changed from <i>Locking a mutex twice or unlocking without prior locking</i> to <i>032: Locking a mutex twice or unlocking without prior locking</i></li></ul> Linux Kernel Safety RuleDB - Feature #1940: 032: Locking a mutex twice or unlocking without prior lockinghttps://forge.ispras.ru/issues/1940?journal_id=130702012-09-06T06:09:05ZAlexey Khoroshilovkhoroshilov@ispras.ru
<ul></ul><p>A couple of instances of the bug fixed in recent kernel (3.6):<br /><a href="http://git.kernel.org/?p=linux/kernel/git/torvalds/linux.git;a=commitdiff;h=b1e1179cea0e50ae3fead8c6bd064a985dae8f8b" class="external">b1e1179</a><br /><a href="http://git.kernel.org/?p=linux/kernel/git/torvalds/linux.git;a=commitdiff;h=5be4fe633a5ddc268afe71257e82a64773ea2f9d" class="external">5be4fe6</a></p> Linux Kernel Safety RuleDB - Feature #1940: 032: Locking a mutex twice or unlocking without prior lockinghttps://forge.ispras.ru/issues/1940?journal_id=131332012-09-07T15:26:43ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>Alexey Khoroshilov wrote:</p>
<blockquote>
<p>A couple of instances of the bug fixed in recent kernel (3.6):<br /><a href="http://git.kernel.org/?p=linux/kernel/git/torvalds/linux.git;a=commitdiff;h=b1e1179cea0e50ae3fead8c6bd064a985dae8f8b" class="external">b1e1179</a><br /><a href="http://git.kernel.org/?p=linux/kernel/git/torvalds/linux.git;a=commitdiff;h=5be4fe633a5ddc268afe71257e82a64773ea2f9d" class="external">5be4fe6</a></p>
</blockquote>
<p>And Vladimir should investigate whether these bugs can be found by LDV or not.</p> Linux Kernel Safety RuleDB - Feature #1940: 032: Locking a mutex twice or unlocking without prior lockinghttps://forge.ispras.ru/issues/1940?journal_id=132242012-09-12T14:19:47ZVadim Mutilinmutilin@ispras.ru
<ul></ul><p>linux-stable commits: 4a349aa 8a9f335 c4cb1dd<br />d47b389 c1c7415 a9e7fb5</p> Linux Kernel Safety RuleDB - Feature #1940: 032: Locking a mutex twice or unlocking without prior lockinghttps://forge.ispras.ru/issues/1940?journal_id=133782012-09-24T08:30:23ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>Commit 21a172e excluded driver "kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--serial--serial_core.c.tar.bz2" from night tests task because of it demonstrates unstable behavior:<br /><pre>
-driver=kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--serial--serial_core.c.tar.bz2;origin=external;kernel=linux-2.6.31.6;model=32_1;module=drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--serial--serial_core.c/serial_core.ko;main=ldv_main0_sequence_infinite_withcheck_stateful;verdict=unsafe
+driver=kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--serial--serial_core.c.tar.bz2;origin=external;kernel=linux-2.6.31.6;model=32_1;module=drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--serial--serial_core.c/serial_core.ko;main=ldv_main0_sequence_infinite_withcheck_stateful;verdict=unknown;RCV_status=fail;problems=Exception
ERROR(SYML)> eval: attempting to take field offset flags of expression tty@uart_shutdown whose value is Top
ERROR(SYML)> eval: attempting to take field offset info of expression state@uart_shutdown whose value is Top
block_at hits exceptionFailure("SMT sovler answer is strange: *** Fatal exception:")
Exception raised :(Failure("SMT sovler answer is strange: *** Fatal exception:")
Ack! The gremlins again!: Failure("SMT sovler answer is strange: *** Fatal exception:")
Fatal error: exception Failure("SMT sovler answer is strange: *** Fatal exception:")
</pre></p> Linux Kernel Safety RuleDB - Feature #1940: 032: Locking a mutex twice or unlocking without prior lockinghttps://forge.ispras.ru/issues/1940?journal_id=154352013-03-08T16:20:28ZAlexey Khoroshilovkhoroshilov@ispras.ru
<ul><li><strong>Tracker</strong> changed from <i>Bug</i> to <i>Feature</i></li></ul> Linux Kernel Safety RuleDB - Feature #1940: 032: Locking a mutex twice or unlocking without prior lockinghttps://forge.ispras.ru/issues/1940?journal_id=208942014-10-16T09:34:15ZVadim Mutilinmutilin@ispras.ru
<ul><li><strong>Description</strong> updated (<a title="View differences" href="/journals/20894/diff?detail_id=23196">diff</a>)</li></ul> Linux Kernel Safety RuleDB - Feature #1940: 032: Locking a mutex twice or unlocking without prior lockinghttps://forge.ispras.ru/issues/1940?journal_id=209292014-10-21T11:53:16ZVadim Mutilinmutilin@ispras.ru
<ul><li><strong>Description</strong> updated (<a title="View differences" href="/journals/20929/diff?detail_id=23225">diff</a>)</li></ul> Linux Kernel Safety RuleDB - Feature #1940: 032: Locking a mutex twice or unlocking without prior lockinghttps://forge.ispras.ru/issues/1940?journal_id=209302014-10-21T11:58:34ZVadim Mutilinmutilin@ispras.ru
<ul><li><strong>Description</strong> updated (<a title="View differences" href="/journals/20930/diff?detail_id=23226">diff</a>)</li></ul>