Bug #10896
closedReplace WRITE_ONCE macro to avoid CPAchecker hangings
0%
Description
The macro WRITE_ONCE is difficult for CPAchecker analysis. The verification tool does not analyze further paths with it, and it leads to missing real bugs. The macro was introduced quite long ago, but it is used more often in recent Linux kernel versions it is used more often. For example, it is used at INIT_LIST_HEAD function that leads to problems in many places consequently. Tests for inode operations for Linux 5.5 show it explicitly.
It is proposed to replace it with just WRITE_ONCE(x,y) == x = y or fix the CPAchecker to avoid the problem.
Updated by Evgeny Novikov over 3 years ago
This a bit strange issue. First of all, I confirm that for one particular test case it causes CPAchecker to consume a lot of computational resources (most likely nobody will care why this is the case...). It does not seem that this is a usual behavior, e.g. for Linux 5.5 driver "drivers/media/platform/renesas-ceu.ko" using "INIT_LIST_HEAD" and thus "WRITE_ONCE" there are Unsafe and Safe correspondingly for requirement specifications "memory safety" and "arch:mm:ioremap" correspondingly. That's this macro does not prevent the verification tool both to prove correctness and to report a bug.
Another observation is that source code corresponding to this macro was considerably simplified in this commit. This is approximately Linux 5.7. Using "WRITE_ONCE" for "INIT_LIST_HEAD" was added in commit that is ~Linux 4.4. Thus, all versions between 4.4 and 5.7 suffer from this complicated macro that is used not only in "INIT_LIST_HEAD".
My resume is that having a suggested model will not be redundant anyway.
Updated by Evgeny Novikov over 3 years ago
- Status changed from New to Resolved
I did this in branch write-once-model. You can read comments for 44ee135d7 for details.
Updated by Evgeny Novikov over 3 years ago
- Status changed from Resolved to Closed
I replaced weaving of calls to weaving of definition of INIT_LIST_HEAD to avoid missing of annotations for CPALockator that reports false alarms otherwise. After all CI passed, so, I merged the branch to master in 04222f7d9.