Project

General

Profile

Actions
Copy link

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:
Vadim Mutilin
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
Copy link

Also available in: Atom PDF