diff options
| author | Paul E. McKenney <paulmck@kernel.org> | 2023-05-11 19:12:16 -0700 |
|---|---|---|
| committer | Paul E. McKenney <paulmck@kernel.org> | 2023-07-14 15:10:56 -0700 |
| commit | 1304affd35739d83b4089a297d39ab08f1624158 (patch) | |
| tree | 3c39a66766165a5983eeac72a6fc017ee7ac8aec /tools/perf/scripts/python/export-to-sqlite.py | |
| parent | 965167e8e6c9877390bb9574f88da21dc42f03eb (diff) | |
rcu: Remove formal-verification tests
The CBMC-based formal-verification testing for SRCU was quite the thing
back in 2016, but the problem is that SRCU changes too quickly for the
scripting to keep up. In addition, more recently, SRCU's grace-period
ordering has been formally modeled by a group of Linux-kernel memory-model
litmus tests.
This commit therefore removes the pioneering formal-verification tests.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Diffstat (limited to 'tools/perf/scripts/python/export-to-sqlite.py')
0 files changed, 0 insertions, 0 deletions