Project

General

Profile

Actions

Feature #1940

open

032: Locking a mutex twice or unlocking without prior locking

Added by Alexey Khoroshilov over 12 years ago. Updated over 9 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 2 (0 open2 closed)

Related to Linux Driver Verification - Bug #1412: 32_7: add atomic_dec_and_mutex_lock to the modelClosedPavel Shved06/23/2011

Actions
Has duplicate Linux Kernel Safety RuleDB - Feature #3324: 32: Locking a mutex twice or unlocking without prior lockingClosedEvgeny Novikov08/03/2012

Actions
Actions #1

Updated by Evgeny Novikov almost 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.

Actions #2

Updated by Vadim Mutilin almost 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)
Actions #3

Updated by Alexey Khoroshilov over 11 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
Actions #4

Updated by Alexey Khoroshilov over 11 years ago

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

Actions #5

Updated by Evgeny Novikov over 11 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.

Actions #6

Updated by Vadim Mutilin over 11 years ago

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

Actions #7

Updated by Evgeny Novikov over 11 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:")

Actions #8

Updated by Alexey Khoroshilov about 11 years ago

  • Tracker changed from Bug to Feature
Actions #9

Updated by Vadim Mutilin over 9 years ago

  • Description updated (diff)
Actions #10

Updated by Vadim Mutilin over 9 years ago

  • Description updated (diff)
Actions #11

Updated by Vadim Mutilin over 9 years ago

  • Description updated (diff)
Actions

Also available in: Atom PDF