Bug #635: Add mutex_is_locked() to model of rule#32 - Linux Driver Verification - Open-Source Projects

Actions

Copy link

Bug #635

closed

Add mutex_is_locked() to model of rule#32

Added by Alexey Khoroshilov almost 14 years ago. Updated almost 14 years ago.

Status:

Closed

Priority:

High

Assignee:

Vadim Mutilin

Category:

Rules and Models

Start date:

12/21/2010

Due date:

% Done:

Estimated time:

Detected in build:

588b549

Platform:

Published in build:

4b63f97716aff56612b5252b9409b96c78846bfe

Description

Lack of the mutex_is_locked() in our model leads to false positives.

/**
 * mutex_is_locked - is the mutex locked
 * @lock: the mutex to be queried
 *
 * Returns 1 if the mutex is locked, 0 if unlocked.
 */
static inline int mutex_is_locked(struct mutex *lock)
{
        return atomic_read(&lock->count) != 1;
}

Files

mutexislocked.c (978 Bytes) mutexislocked.c

Broken regression test file

Evgeny Novikov, 01/29/2011 12:49 PM

Actions

Copy link

Updated by Alexey Khoroshilov almost 14 years ago

Drivers where false positive appears (linus-tree):
cx23885-vbi.ko
saa7134-video.ko

Actions

Copy link

Updated by Vadim Mutilin almost 14 years ago

What model do you use? 32_7?
Is it ldv-git?
Also an error trace would be preferable (link to loaded stats or file) or description of called functions and lines in files where it occurs.

Actions

Copy link

Updated by Pavel Shved almost 14 years ago

Вадим Мутилин wrote:

What model do you use? 32_7?
Is it ldv-git?
Also an error trace would be preferable (link to loaded stats or file) or description of called functions and lines in files where it occurs.

Perhaps, writing a couple of small drivers manually would be enough to test if your fix works? It would be a nice thing to do anyway.

Actions

Copy link

Updated by Vadim Mutilin almost 14 years ago

It would be a nice thing but possibly not enough because false positive may be more malicious

Actions

Copy link

Updated by Alexey Khoroshilov almost 14 years ago

Вадим Мутилин wrote:

What model do you use? 32_7?
Is it ldv-git?
Also an error trace would be preferable (link to loaded stats or file) or description of called functions and lines in files where it occurs.

32_7, ldv-git

ldv_initialize_FOREACH
IN_INTERRUPT = 1;
vbi_setup
vbi_prepare
vbi_queue
vbi_release
  cx23885_free_buffer
    videobuf_waiton(q /* q */, buf vb /* vb */, 0 /* non_blocking */, 0 /* intr */);
    {
      ret = 0;
      assert(* (vb ).magic == 537331496);
      __cil_tmp22 = 0;
      tmp___7 = __builtin_expect(__cil_tmp22 /* val */, 0 /* res */);
      {
        return val;
      }
      assert(tmp___7 == 0);
      assert(non_blocking == 0);
      assert(* (q ).ext_lock != 0);
      tmp___9 = mutex_is_locked(* (q ).ext_lock /* lock */);
      {
        tmp = atomic_read(lock foffset count /* v */);
        {
          mem_2 = v foffset counter;
          __retres3 = * (mem_2 );
          return __retres3;
        }
        assert(tmp != 1);
        __cil_tmp3 = 1;
        return __cil_tmp3;
      }
      assert(tmp___9 != 0);
      tmp___10 = 1;
      is_ext_locked = tmp___10;
      assert(is_ext_locked != 0);
      mutex_unlock_ext_lock(* (q ).ext_lock /* lock */);
      {
        assert(ldv_mutex_ext_lock != 2);
        __blast_assert();

Actions

Copy link

Updated by Vadim Mutilin almost 14 years ago

rule model 32_7

module cx23885-vbi.ko ldv_main0_plain_sorted_withcheck
Main generated for file cx23885-vbi.c
callback vbi_release->cx23885_free_buffer(cx23885-core.c)->videobuf_waiton(videobuf-core.c line 102)

module saa7134-video.ko ldv_main0_plain_sorted_withcheck
Main generated for saa7134-video.c
callback buffer_prepare->saa7134_dma_free->videobuf_waiton(videobuf-core.c line 102)

Actions

Copy link

Updated by Vadim Mutilin almost 14 years ago

Status changed from New to Feedback
Published in build set to c47eb81

fixed in c47eb81
tested on ldv-tests/regr-tests/test-sets/small/drivers/tests-model-32_7/test-mutexislocked/mutexislocked.c

Actions

Copy link

Updated by Pavel Shved almost 14 years ago

Status changed from Feedback to Resolved

Maybe it should be closed now?

Actions

Copy link

Updated by Alexey Khoroshilov almost 14 years ago

Status changed from Resolved to Closed

Actions

Copy link

#10

Updated by Alexey Khoroshilov almost 14 years ago

Status changed from Closed to Open

К сожалению, обнаружилось, что почему-то mutex_is_locked не работает. См. например:

ldv-git --force --keep-work --rule=32_7 --filter=media/video/bt8xx/bttv-vbi check

Actions

Copy link

#11

Updated by Vadim Mutilin almost 14 years ago

I forgot to update rerouting options. Fixed it in d1a476a

Actions

Copy link

#12

Updated by Evgeny Novikov almost 14 years ago

File mutexislocked.c mutexislocked.c added

Nowadays mutex_is_locked becomes completely broken! Even small regression test says it (see attachment).
Don't forget to update small regression test set after bug fixing!!!

Actions

Copy link

#13

Updated by Vadim Mutilin almost 14 years ago

Small tests fixed to find both errors old and new.
New error is fixed in 4b63f97716aff56612b5252b9409b96c78846bfe
(bug #754 in rerouting is found, which does not prevent fixing this bug)

Actions

Copy link

#14