Project

General

Profile

Feature #2747

110: Correct initialization of spin_lock

Added by Vadim Mutilin almost 8 years ago. Updated over 5 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

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

Actions

History

#1

Updated by Vadim Mutilin almost 8 years ago

  • Tracker changed from Task to Feature
#2

Updated by Vadim Mutilin almost 8 years ago

  • Status changed from New to Open

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

#3

Updated by Vadim Mutilin almost 8 years ago

Time limit increase leads to out of mem

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

#4

Updated by Vadim Mutilin almost 8 years ago

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

Updated by Alexey Khoroshilov almost 8 years ago

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

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

#7

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

#8

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

#9

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

#10

Updated by Vadim Mutilin almost 8 years ago

  • Priority changed from High to Normal
#11

Updated by Vadim Mutilin over 7 years ago

  • Assignee changed from Vadim Mutilin to Marina Makienko
#12

Updated by Marina Makienko over 7 years ago

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

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

#14

Updated by Marina Makienko over 7 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.

#15

Updated by Marina Makienko over 7 years ago

  • Status changed from Open to Resolved
#16

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

#17

Updated by Vadim Mutilin over 5 years ago

  • Description updated (diff)

Also available in: Atom PDF