Feature #1940
open032: Locking a mutex twice or unlocking without prior locking
0%
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:- 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.
- Releasing an unlocked mutex.
- 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
Updated by Evgeny Novikov over 12 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.
Updated by Vadim Mutilin over 12 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)
Updated by Alexey Khoroshilov over 12 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
Updated by Alexey Khoroshilov over 12 years ago
Updated by Evgeny Novikov over 12 years ago
Updated by Vadim Mutilin over 12 years ago
linux-stable commits: 4a349aa 8a9f335 c4cb1dd
d47b389 c1c7415 a9e7fb5
Updated by Evgeny Novikov about 12 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:")
Updated by Alexey Khoroshilov almost 12 years ago
- Tracker changed from Bug to Feature