Feature #2747

110: Correct initialization of spin_lock

Added by Vadim Mutilin over 5 years ago. Updated almost 3 years ago.

Status:OpenStart date:04/13/2012
Priority:NormalDue date:
Assignee:Marina Makienko% Done:

100%

Category:-
Target version:-
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 scope Closed 01/29/2013

History

#1 Updated by Vadim Mutilin over 5 years ago

  • Tracker changed from Task to Feature

#2 Updated by Vadim Mutilin over 5 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 over 5 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 over 5 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 over 5 years ago

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

#6 Updated by Evgeny Novikov over 5 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 over 5 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 over 5 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 over 5 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 over 5 years ago

  • Priority changed from High to Normal

#11 Updated by Vadim Mutilin about 5 years ago

  • Assignee changed from Vadim Mutilin to Marina Makienko

#12 Updated by Marina Makienko about 5 years ago

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

#13 Updated by Evgeny Novikov about 5 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 about 5 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 about 5 years ago

  • Status changed from Open to Resolved

#16 Updated by Evgeny Novikov over 4 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 almost 3 years ago

  • Description updated (diff)

Also available in: Atom PDF