summaryrefslogtreecommitdiffstats
path: root/tools/testing/selftests/rcutorture/formal
Commit message (Expand)AuthorAgeFilesLines
* rcu: Remove formal-verification testsPaul E. McKenney2023-07-1440-1600/+0
* rcu: Fix various typos in commentsIngo Molnar2021-05-121-1/+1
* .gitignore: add SPDX License IdentifierMasahiro Yamada2020-03-253-0/+3
* block: remove CONFIG_LBDAFChristoph Hellwig2019-04-061-4/+0
* rcutorture/formal: Replace synchronize_sched() with synchronize_rcu()Paul E. McKenney2018-12-011-2/+2
* Merge branch 'linus' into locking/core, to resolve conflictsIngo Molnar2017-11-0720-0/+20
|\
| * License cleanup: add SPDX GPL-2.0 license identifier to files with no licenseGreg Kroah-Hartman2017-11-0220-0/+20
* | locking/atomics, rcutorture/formal: Prepare for ACCESS_ONCE() removalMark Rutland2017-10-251-3/+2
|/
* srcu-cbmc: Use /usr/bin/awk instead of /bin/awkPriyalee Kushwaha2017-06-081-1/+1
* rcutorture: Add CBMC-based formal verification for SRCULance Roy2017-01-2540-0/+1582