| commit | f5f3c10d6c2ecbee420e8bc25c87d8808198c190 | [log] [tgz] |
|---|---|---|
| author | Paul E. McKenney <paulmck@linux.ibm.com> | Tue Jan 15 16:59:27 2019 -0800 |
| committer | Paul E. McKenney <paulmck@linux.ibm.com> | Tue Jan 15 17:12:02 2019 -0800 |
| tree | 1eebc48fb0eb5f4492ebfa19004487a01ba6bd50 | |
| parent | a971f375aa650c6caa184853c35364563e19fd73 [diff] |
formal: Include performance results for locking verification Verifying higher-level abstractions produces exponentially faster verifications, which this commit documents. While in the area, call out LKMM. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>