Feature #11799


Develop models and tests for list API

Added by Evgeny Novikov 10 days ago. Updated 8 days ago.

Environment models
Target version:
Start date:
Due date:
% Done:


Estimated time:
Published in build:


It is pretty strange that we don't have models for such the important API while related issues exist for a long time. Surprisingly, there is no many false alarms (~5% of all false alarms). From the other side, it may be a tip of an iceberg. Adding models may be pretty dangerous, since the list API is widely used and some unexpected degradations can be found when using models. Nevertheless, let's give a chance for models.

Actions #1

Updated by Evgeny Novikov 9 days ago

  • Status changed from New to Resolved

I implemented models and tests for the list API in branch list-models-and-tests. Most related false alarms, that were obtained at verification of Linux 5.19-rc7 against memory safety, became either safes or unknowns. In some cases there are still unsafes, but they are either quite complicated (it is not clear whether list operations are responsible for them) or they have other error traces than before. Let's carefully test these models as they quite vital.

Actions #2

Updated by Evgeny Novikov 9 days ago

  • Status changed from Resolved to Open

CI revealed numerous degradations due to old versions of the Linux kernel do not have the header included by the new model. Moreover, there are some transitions to be carefully studied.

Actions #3

Updated by Evgeny Novikov 9 days ago

  • Status changed from Open to Resolved

I fixed inclusion of headers so that everything seems to work well for all considered versions of the Linux kernel. Moreover, I scrutinized transitions. They correspond to positive regressions thanks to models of the list API. Let's see on CI results one more time and, more important, let's evaluate how these models affect verification of a bunch of drivers against various requirement specifications.

Actions #4

Updated by Evgeny Novikov 8 days ago

  • Status changed from Resolved to Closed

I was very wondered, that adding models for the list API resulted in several positive, expected regressions, but nothing changed considerably. It is the case both for checking memory safety and drivers:clk2 requirements specification. So I merged the branch to master in 40c9ccc3e.


Also available in: Atom PDF