Feature #2747
open110: Correct initialization of spin_lock
100%
Description
Updated by Vadim Mutilin over 12 years ago
- Status changed from New to Open
rule model 110_1a
90a4845 - UNSAFE находится до, после timelimit=1800
63771f4 - до и после UNKNOWN (ошибка c большими целыми)
9ec4f65 - не исследовался, требуется правило на __SPIN_LOCK_UNLOCKED
Updated by Vadim Mutilin over 12 years ago
Time limit increase leads to out of mem
commit 90a4845 - after fix: Memory Limit Exceeded Time Limit: 7000 Memory Limit: 3500000
Updated by Vadim Mutilin over 12 years ago
- Subject changed from Correct initialization of spin_lock (110_1) to Correct initialization of spin_lock (110_1a)
Updated by Alexey Khoroshilov over 12 years ago
- Subject changed from Correct initialization of spin_lock (110_1a) to 110: Correct initialization of spin_lock
Updated by Evgeny Novikov over 12 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.
Updated by Evgeny Novikov over 12 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.
Updated by Evgeny Novikov over 12 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.
Updated by Evgeny Novikov over 12 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?
Updated by Vadim Mutilin over 12 years ago
- Priority changed from High to Normal
Updated by Vadim Mutilin over 12 years ago
- Assignee changed from Vadim Mutilin to Marina Makienko
Updated by Marina Makienko over 12 years ago
- Status changed from Open to Resolved
- % Done changed from 0 to 100
Updated by Evgeny Novikov about 12 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.
Updated by Marina Makienko about 12 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.
Updated by Marina Makienko about 12 years ago
- Status changed from Open to Resolved
Updated by Evgeny Novikov almost 12 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).