Bug #10896
closed
Replace WRITE_ONCE macro to avoid CPAchecker hangings
Added by Ilja Zakharov over 3 years ago.
Updated over 3 years ago.
Category:
Environment models
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.
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.
- Status changed from New to Resolved
I did this in branch write-once-model. You can read comments for 44ee135d7 for details.
- 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.
Also available in: Atom
PDF