diff options
author | Lance Roy | 2017-01-01 01:33:50 +0100 |
---|---|---|
committer | Paul E. McKenney | 2017-01-25 21:54:22 +0100 |
commit | 418b2977b34378f67c46930c72a776f94e7bf903 (patch) | |
tree | 2f3f41dd02a80f237bda867211e4bb852c0c9a08 /tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/workqueues.h | |
parent | srcu: Force full grace-period ordering (diff) | |
download | kernel-qcow2-linux-418b2977b34378f67c46930c72a776f94e7bf903.tar.gz kernel-qcow2-linux-418b2977b34378f67c46930c72a776f94e7bf903.tar.xz kernel-qcow2-linux-418b2977b34378f67c46930c72a776f94e7bf903.zip |
rcutorture: Add CBMC-based formal verification for SRCU
This commit creates a formal/srcu-cbmc directory containing scripts that
pull SRCU in from the source code, filter it to remove things that CBMC
cannot handle, and run a series of verifications on it. This has a number
of shortcomings:
1. It does not yet hook into the upper-level self-test Makefiles.
2. It tests only a single scenario, store buffering.
3. There is no gcc-based syntax-error prefiltering.
Nevertheless, it does fully verify a piece of SRCU under a moderately
weak memory model (PSO).
Signed-off-by: Lance Roy <ldr709@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Diffstat (limited to 'tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/workqueues.h')
-rw-r--r-- | tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/workqueues.h | 102 |
1 files changed, 102 insertions, 0 deletions
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/workqueues.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/workqueues.h new file mode 100644 index 000000000000..e58c8dfd3e90 --- /dev/null +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/workqueues.h @@ -0,0 +1,102 @@ +#ifndef WORKQUEUES_H +#define WORKQUEUES_H + +#include <stdbool.h> + +#include "barriers.h" +#include "bug_on.h" +#include "int_typedefs.h" + +#include <linux/types.h> + +/* Stub workqueue implementation. */ + +struct work_struct; +typedef void (*work_func_t)(struct work_struct *work); +void delayed_work_timer_fn(unsigned long __data); + +struct work_struct { +/* atomic_long_t data; */ + unsigned long data; + + struct list_head entry; + work_func_t func; +#ifdef CONFIG_LOCKDEP + struct lockdep_map lockdep_map; +#endif +}; + +struct timer_list { + struct hlist_node entry; + unsigned long expires; + void (*function)(unsigned long); + unsigned long data; + u32 flags; + int slack; +}; + +struct delayed_work { + struct work_struct work; + struct timer_list timer; + + /* target workqueue and CPU ->timer uses to queue ->work */ + struct workqueue_struct *wq; + int cpu; +}; + + +static inline bool schedule_work(struct work_struct *work) +{ + BUG(); + return true; +} + +static inline bool schedule_work_on(int cpu, struct work_struct *work) +{ + BUG(); + return true; +} + +static inline bool queue_work(struct workqueue_struct *wq, + struct work_struct *work) +{ + BUG(); + return true; +} + +static inline bool queue_delayed_work(struct workqueue_struct *wq, + struct delayed_work *dwork, + unsigned long delay) +{ + BUG(); + return true; +} + +#define INIT_WORK(w, f) \ + do { \ + (w)->data = 0; \ + (w)->func = (f); \ + } while (0) + +#define INIT_DELAYED_WORK(w, f) INIT_WORK(&(w)->work, (f)) + +#define __WORK_INITIALIZER(n, f) { \ + .data = 0, \ + .entry = { &(n).entry, &(n).entry }, \ + .func = f \ + } + +/* Don't bother initializing timer. */ +#define __DELAYED_WORK_INITIALIZER(n, f, tflags) { \ + .work = __WORK_INITIALIZER((n).work, (f)), \ + } + +#define DECLARE_WORK(n, f) \ + struct workqueue_struct n = __WORK_INITIALIZER + +#define DECLARE_DELAYED_WORK(n, f) \ + struct delayed_work n = __DELAYED_WORK_INITIALIZER(n, f, 0) + +#define system_power_efficient_wq ((struct workqueue_struct *) NULL) + +#endif |