Project

General

Profile

Actions

Feature #2747

open

110: Correct initialization of spin_lock

Added by Vadim Mutilin about 10 years ago. Updated over 7 years ago.

Status:
Open
Priority:
Normal
Start date:
04/13/2012
Due date:
% Done:

100%

Estimated time:
Published in build:

Description

spin_lock structure must be initialized with spin_lock_init or DEFINE_SPINLOCK before usage

Links
Sample bugfixes 90a4845, 63771f4, 9ec4f65


Related issues 1 (0 open1 closed)

Related to C Instrumentation Framework - Feature #3890: Deal with Linux kernel API macros at global scopeClosedEvgeny Novikov01/29/2013

Actions
Actions #1

Updated by Vadim Mutilin about 10 years ago

  • Tracker changed from Task to Feature
Actions #2

Updated by Vadim Mutilin about 10 years ago

  • Status changed from New to Open

rule model 110_1a
90a4845 - UNSAFE находится до, после timelimit=1800
63771f4 - до и после UNKNOWN (ошибка c большими целыми)
9ec4f65 - не исследовался, требуется правило на __SPIN_LOCK_UNLOCKED

Actions #3

Updated by Vadim Mutilin about 10 years ago

Time limit increase leads to out of mem

commit 90a4845 - after fix: Memory Limit Exceeded Time Limit: 7000 Memory Limit: 3500000

Actions #4

Updated by Vadim Mutilin about 10 years ago

  • Subject changed from Correct initialization of spin_lock (110_1) to Correct initialization of spin_lock (110_1a)
Actions #5

Updated by Alexey Khoroshilov about 10 years ago

  • Subject changed from Correct initialization of spin_lock (110_1a) to 110: Correct initialization of spin_lock
Actions #6

Updated by Evgeny Novikov about 10 years ago

  • Assignee set to Vadim Mutilin
  • Priority changed from Normal to High

There isn't any model comment in 110_1a. It's bad style, since it requires too much time to analyze error traces.

Actions #7

Updated by Evgeny Novikov about 10 years ago

Vadim Mutilin wrote:

Time limit increase leads to out of mem

commit 90a4845 - after fix: Memory Limit Exceeded Time Limit: 7000 Memory Limit: 3500000

RCV_MEMLIMIT=6000000 RCV_TIMELIMIT=7000 leads to Time_limit.

Actions #8

Updated by Evgeny Novikov about 10 years ago

Evgeny Novikov wrote:

Vadim Mutilin wrote:

Time limit increase leads to out of mem

commit 90a4845 - after fix: Memory Limit Exceeded Time Limit: 7000 Memory Limit: 3500000

RCV_MEMLIMIT=6000000 RCV_TIMELIMIT=7000 leads to Time_limit.

May be some challenge for verifiers, try CPAchecker.

Actions #9

Updated by Evgeny Novikov about 10 years ago

Some work (model development, writing model comments, big launches, etc.) is done with this model now or we should reduce its priority also?

Actions #10

Updated by Vadim Mutilin about 10 years ago

  • Priority changed from High to Normal
Actions #11

Updated by Vadim Mutilin almost 10 years ago

  • Assignee changed from Vadim Mutilin to Marina Makienko
Actions #12

Updated by Marina Makienko almost 10 years ago

  • Status changed from Open to Resolved
  • % Done changed from 0 to 100
Actions #13

Updated by Evgeny Novikov over 9 years ago

  • Status changed from Resolved to Open

Commit 2f5dc79 "Add functions in 110" to kernel-rules has duplicated aspect file content. Although it works, it isn't a good style.

Actions #14

Updated by Marina Makienko over 9 years ago

Evgeny Novikov wrote:

Commit 2f5dc79 "Add functions in 110" to kernel-rules has duplicated aspect file content. Although it works, it isn't a good style.

Fix it.

Actions #15

Updated by Marina Makienko over 9 years ago

  • Status changed from Open to Resolved
Actions #16

Updated by Evgeny Novikov over 9 years ago

  • Status changed from Resolved to Open

Please, use ability to process actual arguments of macrofunctions substituted at the global scope like in 148_7a model (implemented in #3890).

Actions #17

Updated by Vadim Mutilin over 7 years ago

  • Description updated (diff)
Actions

Also available in: Atom PDF