Project

General

Profile

Actions

Feature #11810

open

Check whether the same resources are passed to various related callbacks

Added by Evgeny Novikov about 2 years ago. Updated about 2 years ago.

Status:
New
Priority:
High
Category:
Testing
Target version:
-
Start date:
08/09/2022
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

#11809 demonstrates that current test cases for EMG and its specifications do not reveal cases when different resources are actually passed to callbacks of the same category. So one extra check will be pretty useful.


Related issues 7 (0 open7 closed)

Blocked by Klever - Bug #11809: Pass the same resource to probe and remove for HID driversClosedEvgeny Novikov08/09/2022

Actions
Blocked by Klever - Bug #11815: Do not pass NULL at registration of callbacksClosedEvgeny Novikov08/10/2022

Actions
Blocked by Klever - Bug #11821: Allocate memory for inode for file_operations callbacksClosedEvgeny Novikov08/12/2022

Actions
Blocked by Klever - Feature #11825: Allocate memory for tty_struct for tty_operations callbacksClosedEvgeny Novikov08/15/2022

Actions
Blocked by Klever - Feature #11839: Get rid of implicit resourcesClosedEvgeny Novikov08/23/2022

Actions
Blocked by Klever - Bug #11851: Fix issues revealed in TTY environment model specifications when checking tests using memory safetyClosedEvgeny Novikov08/24/2022

Actions
Blocked by Klever - Bug #11854: Improve error handling in test cases intended for checking TTY environment model specificationClosedEvgeny Novikov08/25/2022

Actions
Actions #1

Updated by Evgeny Novikov about 2 years ago

  • Blocks Bug #11809: Pass the same resource to probe and remove for HID drivers added
Actions #2

Updated by Evgeny Novikov about 2 years ago

I implemented the extra check in branch check-callback-resources. Indeed, it reveals both the issue with environment model specifications for HID drivers and a lot of other issues in other environment model specifications as well as in EMG test cases themselves. It has sense to fix all those issues step by step and only then enable this check (otherwise, it will fail too many times and CI will not pass tests).

Actions #3

Updated by Evgeny Novikov about 2 years ago

  • Blocks deleted (Bug #11809: Pass the same resource to probe and remove for HID drivers)
Actions #4

Updated by Evgeny Novikov about 2 years ago

  • Blocked by Bug #11809: Pass the same resource to probe and remove for HID drivers added
Actions #5

Updated by Evgeny Novikov about 2 years ago

  • Blocked by Bug #11815: Do not pass NULL at registration of callbacks added
Actions #6

Updated by Evgeny Novikov about 2 years ago

  • Blocked by Bug #11821: Allocate memory for inode for file_operations callbacks added
Actions #7

Updated by Evgeny Novikov about 2 years ago

  • Blocked by Feature #11825: Allocate memory for tty_struct for tty_operations callbacks added
Actions #8

Updated by Evgeny Novikov about 2 years ago

Actions #9

Updated by Evgeny Novikov about 2 years ago

  • Blocked by Bug #11851: Fix issues revealed in TTY environment model specifications when checking tests using memory safety added
Actions #10

Updated by Evgeny Novikov about 2 years ago

  • Target version deleted (3.7)

Eventually branch check-callback-resources contains the framework for checking callback resources. Indeed, it does more than only testing whether the same resources are passed to various related callbacks. By storing, checking and releasing resources it also verifies a correctness of an order of invoked callbacks.

In some cases it stumbles across some complicated issues with environment model specifications. For instance, it may be necessary to relate platform devices with devices passed to power management callbacks. Otherwise, Klever finds unexpected unsafes. Unfortunately, I could not do that (either environment model specifications or EMG does not support this or I did something wrong). Besides, this one as well as some other issues are actually open questions to the kernel behavior. This does not belong directly to the given issue, but it prevents its completion. You can see several blocking, already resolved issues. Several more issues should be added and fixed prior to this one can be closed.

Another point is that there are numerous timeouts for rather simple test cases after adding this framework and appropriate checks. It may be an issue in CPAchecker BAM since CPAchecker SMG can handle corresponding verification tasks very fast. Also, this can point out some extra problems with environment model specifications.

All in all, the framework and checks are useful, but more work is necessary to accept them and enable them within CI.

Actions #11

Updated by Evgeny Novikov about 2 years ago

  • Blocked by Bug #11854: Improve error handling in test cases intended for checking TTY environment model specification added
Actions

Also available in: Atom PDF