Project

General

Profile

Actions

Feature #3986

open

Common kernel core model for current and atomic_*

Added by Alexey Khoroshilov over 11 years ago. Updated about 10 years ago.

Status:
New
Priority:
Normal
Assignee:
Start date:
03/01/2013
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

UNSAFE detected by CPAchecker SeqComb in fs/btrfs/btrfs.ko (linux-3.8-rc1) on rule '32_7a' is a false positive because lack of common kernel core model for current and atomic_* inline functions that are implemented in assembler.

I believe a model for these functions will be useful for all rules.

current can be modeled as a pointer to a global variable that is initialized by some proper values.
More correct design is to have two global variables and nondeterministically switch between them in main function between call of different handlers.

atomic_functions modes obviously are just nonatomic counterparts in C.

Actions #1

Updated by Evgeny Novikov over 11 years ago

  • Project changed from Linux Driver Verification to Linux Kernel Safety RuleDB
  • Assignee set to Ilya Shchepetkov

Models should be added and tested as well as for pointer error processing functions. But this feature request isn't critical, I guess.

Actions #2

Updated by Evgeny Novikov about 10 years ago

  • Assignee changed from Ilya Shchepetkov to Vadim Mutilin

New students can try to implement and to experiment with this.

Actions

Also available in: Atom PDF