Project

General

Profile

Feature #1940

032: Locking a mutex twice or unlocking without prior locking

Added by Alexey Khoroshilov over 7 years ago. Updated over 4 years ago.

Status:
New
Priority:
Normal
Assignee:
-
Start date:
10/25/2011
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

You should not acquire or release the same mutex twice in the same process. All locked mutexes should be unlocked at finalization.

Description

There are several things you should watch for:
  1. Double-locking. Mutex-type object provides exclusive access to sections of executable code. Thus retrying to acquire the current mutex will inevitably lead to a deadlock-situation. Deadlocks should be avoided, hence no double locks should take place.
  2. Releasing an unlocked mutex.
  3. Leaving a mutex locked at finalization.

Mutex is a special case of semaphore, restricted with just one possible requestor. However, it has its own wrapping functions. To initialize a mutex, macros are often used: DECLARE_MUTEX(name) and DECLARE_MUTEX_LOCKED(name). Locking is provided via mutex_lock(), mutex_trylock() and mutex_lock_interruptible() functions; unlocking--via mutex_unlock().

Links
Sample bugfixes 4a349aa, a9e7fb5, d47b389, c1c7415, 8a9f335, 723342c


Related issues

Related to Linux Driver Verification - Bug #1412: 32_7: add atomic_dec_and_mutex_lock to the modelClosed2011-06-23

Has duplicate Linux Kernel Safety RuleDB - Feature #3324: 32: Locking a mutex twice or unlocking without prior lockingClosed2012-08-03

History

#1 Updated by Evgeny Novikov almost 7 years ago

The problem with mutex (un)locking is presented in commits 4a349aa and 8a9f335 (which are found by LDV explicitly) of the linux-stable branch.
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 #2706.

#2 Updated by Vadim Mutilin almost 7 years ago

  • c8a9f335 may lead to a race condition, because of unprotected call to arl9170_set_operating_mode
  • 4a349aa double mutex_unlock (but cannot say that it is a deadlock)

#3 Updated by Alexey Khoroshilov over 6 years ago

  • Subject changed from Locking a mutex twice or unlocking without prior locking to 032: Locking a mutex twice or unlocking without prior locking

#4 Updated by Alexey Khoroshilov over 6 years ago

A couple of instances of the bug fixed in recent kernel (3.6):
b1e1179
5be4fe6

#5 Updated by Evgeny Novikov over 6 years ago

Alexey Khoroshilov wrote:

A couple of instances of the bug fixed in recent kernel (3.6):
b1e1179
5be4fe6

And Vladimir should investigate whether these bugs can be found by LDV or not.

#6 Updated by Vadim Mutilin over 6 years ago

linux-stable commits: 4a349aa 8a9f335 c4cb1dd
d47b389 c1c7415 a9e7fb5

#7 Updated by Evgeny Novikov over 6 years ago

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:

-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:")

#8 Updated by Alexey Khoroshilov about 6 years ago

  • Tracker changed from Bug to Feature

#9 Updated by Vadim Mutilin over 4 years ago

  • Description updated (diff)

#10 Updated by Vadim Mutilin over 4 years ago

  • Description updated (diff)

#11 Updated by Vadim Mutilin over 4 years ago

  • Description updated (diff)

Also available in: Atom PDF