Merge branches 'doc.2017.01.15b', 'dyntick.2017.01.23a', 'fixes.2017.01.23a', 'srcu.2017.01.25a' and 'torture.2017.01.15b' into HEAD
doc.2017.01.15b: Documentation updates dyntick.2017.01.23a: Dyntick tracking consolidation fixes.2017.01.23a: Miscellaneous fixes srcu.2017.01.25a: SRCU rewrite, fixes, and verification torture.2017.01.15b: Torture-test updatestirimbino
Paul E. McKenney
8 years ago
commit
31945aa9f1
@ -0,0 +1 @@ |
||||
srcu.c |
||||
@ -0,0 +1,16 @@ |
||||
all: srcu.c store_buffering |
||||
|
||||
LINUX_SOURCE = ../../../../../..
|
||||
|
||||
modified_srcu_input = $(LINUX_SOURCE)/include/linux/srcu.h \
|
||||
$(LINUX_SOURCE)/kernel/rcu/srcu.c
|
||||
|
||||
modified_srcu_output = include/linux/srcu.h srcu.c
|
||||
|
||||
include/linux/srcu.h: srcu.c |
||||
|
||||
srcu.c: modify_srcu.awk Makefile $(modified_srcu_input) |
||||
awk -f modify_srcu.awk $(modified_srcu_input) $(modified_srcu_output)
|
||||
|
||||
store_buffering: |
||||
@cd tests/store_buffering; make
|
||||
@ -0,0 +1 @@ |
||||
srcu.h |
||||
@ -0,0 +1 @@ |
||||
#include <LINUX_SOURCE/linux/kconfig.h> |
||||
@ -0,0 +1,155 @@ |
||||
/*
|
||||
* This header has been modifies to remove definitions of types that |
||||
* are defined in standard userspace headers or are problematic for some |
||||
* other reason. |
||||
*/ |
||||
|
||||
#ifndef _LINUX_TYPES_H |
||||
#define _LINUX_TYPES_H |
||||
|
||||
#define __EXPORTED_HEADERS__ |
||||
#include <uapi/linux/types.h> |
||||
|
||||
#ifndef __ASSEMBLY__ |
||||
|
||||
#define DECLARE_BITMAP(name, bits) \ |
||||
unsigned long name[BITS_TO_LONGS(bits)] |
||||
|
||||
typedef __u32 __kernel_dev_t; |
||||
|
||||
/* bsd */ |
||||
typedef unsigned char u_char; |
||||
typedef unsigned short u_short; |
||||
typedef unsigned int u_int; |
||||
typedef unsigned long u_long; |
||||
|
||||
/* sysv */ |
||||
typedef unsigned char unchar; |
||||
typedef unsigned short ushort; |
||||
typedef unsigned int uint; |
||||
typedef unsigned long ulong; |
||||
|
||||
#ifndef __BIT_TYPES_DEFINED__ |
||||
#define __BIT_TYPES_DEFINED__ |
||||
|
||||
typedef __u8 u_int8_t; |
||||
typedef __s8 int8_t; |
||||
typedef __u16 u_int16_t; |
||||
typedef __s16 int16_t; |
||||
typedef __u32 u_int32_t; |
||||
typedef __s32 int32_t; |
||||
|
||||
#endif /* !(__BIT_TYPES_DEFINED__) */ |
||||
|
||||
typedef __u8 uint8_t; |
||||
typedef __u16 uint16_t; |
||||
typedef __u32 uint32_t; |
||||
|
||||
/* this is a special 64bit data type that is 8-byte aligned */ |
||||
#define aligned_u64 __u64 __attribute__((aligned(8))) |
||||
#define aligned_be64 __be64 __attribute__((aligned(8))) |
||||
#define aligned_le64 __le64 __attribute__((aligned(8))) |
||||
|
||||
/**
|
||||
* The type used for indexing onto a disc or disc partition. |
||||
* |
||||
* Linux always considers sectors to be 512 bytes long independently |
||||
* of the devices real block size. |
||||
* |
||||
* blkcnt_t is the type of the inode's block count. |
||||
*/ |
||||
#ifdef CONFIG_LBDAF |
||||
typedef u64 sector_t; |
||||
#else |
||||
typedef unsigned long sector_t; |
||||
#endif |
||||
|
||||
/*
|
||||
* The type of an index into the pagecache. |
||||
*/ |
||||
#define pgoff_t unsigned long |
||||
|
||||
/*
|
||||
* A dma_addr_t can hold any valid DMA address, i.e., any address returned |
||||
* by the DMA API. |
||||
* |
||||
* If the DMA API only uses 32-bit addresses, dma_addr_t need only be 32 |
||||
* bits wide. Bus addresses, e.g., PCI BARs, may be wider than 32 bits, |
||||
* but drivers do memory-mapped I/O to ioremapped kernel virtual addresses, |
||||
* so they don't care about the size of the actual bus addresses. |
||||
*/ |
||||
#ifdef CONFIG_ARCH_DMA_ADDR_T_64BIT |
||||
typedef u64 dma_addr_t; |
||||
#else |
||||
typedef u32 dma_addr_t; |
||||
#endif |
||||
|
||||
#ifdef CONFIG_PHYS_ADDR_T_64BIT |
||||
typedef u64 phys_addr_t; |
||||
#else |
||||
typedef u32 phys_addr_t; |
||||
#endif |
||||
|
||||
typedef phys_addr_t resource_size_t; |
||||
|
||||
/*
|
||||
* This type is the placeholder for a hardware interrupt number. It has to be |
||||
* big enough to enclose whatever representation is used by a given platform. |
||||
*/ |
||||
typedef unsigned long irq_hw_number_t; |
||||
|
||||
typedef struct { |
||||
int counter; |
||||
} atomic_t; |
||||
|
||||
#ifdef CONFIG_64BIT |
||||
typedef struct { |
||||
long counter; |
||||
} atomic64_t; |
||||
#endif |
||||
|
||||
struct list_head { |
||||
struct list_head *next, *prev; |
||||
}; |
||||
|
||||
struct hlist_head { |
||||
struct hlist_node *first; |
||||
}; |
||||
|
||||
struct hlist_node { |
||||
struct hlist_node *next, **pprev; |
||||
}; |
||||
|
||||
/**
|
||||
* struct callback_head - callback structure for use with RCU and task_work |
||||
* @next: next update requests in a list |
||||
* @func: actual update function to call after the grace period. |
||||
* |
||||
* The struct is aligned to size of pointer. On most architectures it happens |
||||
* naturally due ABI requirements, but some architectures (like CRIS) have |
||||
* weird ABI and we need to ask it explicitly. |
||||
* |
||||
* The alignment is required to guarantee that bits 0 and 1 of @next will be |
||||
* clear under normal conditions -- as long as we use call_rcu(), |
||||
* call_rcu_bh(), call_rcu_sched(), or call_srcu() to queue callback. |
||||
* |
||||
* This guarantee is important for few reasons: |
||||
* - future call_rcu_lazy() will make use of lower bits in the pointer; |
||||
* - the structure shares storage spacer in struct page with @compound_head, |
||||
* which encode PageTail() in bit 0. The guarantee is needed to avoid |
||||
* false-positive PageTail(). |
||||
*/ |
||||
struct callback_head { |
||||
struct callback_head *next; |
||||
void (*func)(struct callback_head *head); |
||||
} __attribute__((aligned(sizeof(void *)))); |
||||
#define rcu_head callback_head |
||||
|
||||
typedef void (*rcu_callback_t)(struct rcu_head *head); |
||||
typedef void (*call_rcu_func_t)(struct rcu_head *head, rcu_callback_t func); |
||||
|
||||
/* clocksource cycle base type */ |
||||
typedef u64 cycle_t; |
||||
|
||||
#endif /* __ASSEMBLY__ */ |
||||
#endif /* _LINUX_TYPES_H */ |
||||
@ -0,0 +1,375 @@ |
||||
#!/bin/awk -f |
||||
|
||||
# Modify SRCU for formal verification. The first argument should be srcu.h and |
||||
# the second should be srcu.c. Outputs modified srcu.h and srcu.c into the |
||||
# current directory. |
||||
|
||||
BEGIN { |
||||
if (ARGC != 5) { |
||||
print "Usange: input.h input.c output.h output.c" > "/dev/stderr"; |
||||
exit 1; |
||||
} |
||||
h_output = ARGV[3]; |
||||
c_output = ARGV[4]; |
||||
ARGC = 3; |
||||
|
||||
# Tokenize using FS and not RS as FS supports regular expressions. Each |
||||
# record is one line of source, except that backslashed lines are |
||||
# combined. Comments are treated as field separators, as are quotes. |
||||
quote_regexp="\"([^\\\\\"]|\\\\.)*\""; |
||||
comment_regexp="\\/\\*([^*]|\\*+[^*/])*\\*\\/|\\/\\/.*(\n|$)"; |
||||
FS="([ \\\\\t\n\v\f;,.=(){}+*/<>&|^-]|\\[|\\]|" comment_regexp "|" quote_regexp ")+"; |
||||
|
||||
inside_srcu_struct = 0; |
||||
inside_srcu_init_def = 0; |
||||
srcu_init_param_name = ""; |
||||
in_macro = 0; |
||||
brace_nesting = 0; |
||||
paren_nesting = 0; |
||||
|
||||
# Allow the manipulation of the last field separator after has been |
||||
# seen. |
||||
last_fs = ""; |
||||
# Whether the last field separator was intended to be output. |
||||
last_fs_print = 0; |
||||
|
||||
# rcu_batches stores the initialization for each instance of struct |
||||
# rcu_batch |
||||
|
||||
in_comment = 0; |
||||
|
||||
outputfile = ""; |
||||
} |
||||
|
||||
{ |
||||
prev_outputfile = outputfile; |
||||
if (FILENAME ~ /\.h$/) { |
||||
outputfile = h_output; |
||||
if (FNR != NR) { |
||||
print "Incorrect file order" > "/dev/stderr"; |
||||
exit 1; |
||||
} |
||||
} |
||||
else |
||||
outputfile = c_output; |
||||
|
||||
if (prev_outputfile && outputfile != prev_outputfile) { |
||||
new_outputfile = outputfile; |
||||
outputfile = prev_outputfile; |
||||
update_fieldsep("", 0); |
||||
outputfile = new_outputfile; |
||||
} |
||||
} |
||||
|
||||
# Combine the next line into $0. |
||||
function combine_line() { |
||||
ret = getline next_line; |
||||
if (ret == 0) { |
||||
# Don't allow two consecutive getlines at the end of the file |
||||
if (eof_found) { |
||||
print "Error: expected more input." > "/dev/stderr"; |
||||
exit 1; |
||||
} else { |
||||
eof_found = 1; |
||||
} |
||||
} else if (ret == -1) { |
||||
print "Error reading next line of file" FILENAME > "/dev/stderr"; |
||||
exit 1; |
||||
} |
||||
$0 = $0 "\n" next_line; |
||||
} |
||||
|
||||
# Combine backslashed lines and multiline comments. |
||||
function combine_backslashes() { |
||||
while (/\\$|\/\*([^*]|\*+[^*\/])*\**$/) { |
||||
combine_line(); |
||||
} |
||||
} |
||||
|
||||
function read_line() { |
||||
combine_line(); |
||||
combine_backslashes(); |
||||
} |
||||
|
||||
# Print out field separators and update variables that depend on them. Only |
||||
# print if p is true. Call with sep="" and p=0 to print out the last field |
||||
# separator. |
||||
function update_fieldsep(sep, p) { |
||||
# Count braces |
||||
sep_tmp = sep; |
||||
gsub(quote_regexp "|" comment_regexp, "", sep_tmp); |
||||
while (1) |
||||
{ |
||||
if (sub("[^{}()]*\\{", "", sep_tmp)) { |
||||
brace_nesting++; |
||||
continue; |
||||
} |
||||
if (sub("[^{}()]*\\}", "", sep_tmp)) { |
||||
brace_nesting--; |
||||
if (brace_nesting < 0) { |
||||
print "Unbalanced braces!" > "/dev/stderr"; |
||||
exit 1; |
||||
} |
||||
continue; |
||||
} |
||||
if (sub("[^{}()]*\\(", "", sep_tmp)) { |
||||
paren_nesting++; |
||||
continue; |
||||
} |
||||
if (sub("[^{}()]*\\)", "", sep_tmp)) { |
||||
paren_nesting--; |
||||
if (paren_nesting < 0) { |
||||
print "Unbalanced parenthesis!" > "/dev/stderr"; |
||||
exit 1; |
||||
} |
||||
continue; |
||||
} |
||||
|
||||
break; |
||||
} |
||||
|
||||
if (last_fs_print) |
||||
printf("%s", last_fs) > outputfile; |
||||
last_fs = sep; |
||||
last_fs_print = p; |
||||
} |
||||
|
||||
# Shifts the fields down by n positions. Calls next if there are no more. If p |
||||
# is true then print out field separators. |
||||
function shift_fields(n, p) { |
||||
do { |
||||
if (match($0, FS) > 0) { |
||||
update_fieldsep(substr($0, RSTART, RLENGTH), p); |
||||
if (RSTART + RLENGTH <= length()) |
||||
$0 = substr($0, RSTART + RLENGTH); |
||||
else |
||||
$0 = ""; |
||||
} else { |
||||
update_fieldsep("", 0); |
||||
print "" > outputfile; |
||||
next; |
||||
} |
||||
} while (--n > 0); |
||||
} |
||||
|
||||
# Shifts and prints the first n fields. |
||||
function print_fields(n) { |
||||
do { |
||||
update_fieldsep("", 0); |
||||
printf("%s", $1) > outputfile; |
||||
shift_fields(1, 1); |
||||
} while (--n > 0); |
||||
} |
||||
|
||||
{ |
||||
combine_backslashes(); |
||||
} |
||||
|
||||
# Print leading FS |
||||
{ |
||||
if (match($0, "^(" FS ")+") > 0) { |
||||
update_fieldsep(substr($0, RSTART, RLENGTH), 1); |
||||
if (RSTART + RLENGTH <= length()) |
||||
$0 = substr($0, RSTART + RLENGTH); |
||||
else |
||||
$0 = ""; |
||||
} |
||||
} |
||||
|
||||
# Parse the line. |
||||
{ |
||||
while (NF > 0) { |
||||
if ($1 == "struct" && NF < 3) { |
||||
read_line(); |
||||
continue; |
||||
} |
||||
|
||||
if (FILENAME ~ /\.h$/ && !inside_srcu_struct && |
||||
brace_nesting == 0 && paren_nesting == 0 && |
||||
$1 == "struct" && $2 == "srcu_struct" && |
||||
$0 ~ "^struct(" FS ")+srcu_struct(" FS ")+\\{") { |
||||
inside_srcu_struct = 1; |
||||
print_fields(2); |
||||
continue; |
||||
} |
||||
if (inside_srcu_struct && brace_nesting == 0 && |
||||
paren_nesting == 0) { |
||||
inside_srcu_struct = 0; |
||||
update_fieldsep("", 0); |
||||
for (name in rcu_batches) |
||||
print "extern struct rcu_batch " name ";" > outputfile; |
||||
} |
||||
|
||||
if (inside_srcu_struct && $1 == "struct" && $2 == "rcu_batch") { |
||||
# Move rcu_batches outside of the struct. |
||||
rcu_batches[$3] = ""; |
||||
shift_fields(3, 1); |
||||
sub(/;[[:space:]]*$/, "", last_fs); |
||||
continue; |
||||
} |
||||
|
||||
if (FILENAME ~ /\.h$/ && !inside_srcu_init_def && |
||||
$1 == "#define" && $2 == "__SRCU_STRUCT_INIT") { |
||||
inside_srcu_init_def = 1; |
||||
srcu_init_param_name = $3; |
||||
in_macro = 1; |
||||
print_fields(3); |
||||
continue; |
||||
} |
||||
if (inside_srcu_init_def && brace_nesting == 0 && |
||||
paren_nesting == 0) { |
||||
inside_srcu_init_def = 0; |
||||
in_macro = 0; |
||||
continue; |
||||
} |
||||
|
||||
if (inside_srcu_init_def && brace_nesting == 1 && |
||||
paren_nesting == 0 && last_fs ~ /\.[[:space:]]*$/ && |
||||
$1 ~ /^[[:alnum:]_]+$/) { |
||||
name = $1; |
||||
if (name in rcu_batches) { |
||||
# Remove the dot. |
||||
sub(/\.[[:space:]]*$/, "", last_fs); |
||||
|
||||
old_record = $0; |
||||
do |
||||
shift_fields(1, 0); |
||||
while (last_fs !~ /,/ || paren_nesting > 0); |
||||
end_loc = length(old_record) - length($0); |
||||
end_loc += index(last_fs, ",") - length(last_fs); |
||||
|
||||
last_fs = substr(last_fs, index(last_fs, ",") + 1); |
||||
last_fs_print = 1; |
||||
|
||||
match(old_record, "^"name"("FS")+="); |
||||
start_loc = RSTART + RLENGTH; |
||||
|
||||
len = end_loc - start_loc; |
||||
initializer = substr(old_record, start_loc, len); |
||||
gsub(srcu_init_param_name "\\.", "", initializer); |
||||
rcu_batches[name] = initializer; |
||||
continue; |
||||
} |
||||
} |
||||
|
||||
# Don't include a nonexistent file |
||||
if (!in_macro && $1 == "#include" && /^#include[[:space:]]+"rcu\.h"/) { |
||||
update_fieldsep("", 0); |
||||
next; |
||||
} |
||||
|
||||
# Ignore most preprocessor stuff. |
||||
if (!in_macro && $1 ~ /#/) { |
||||
break; |
||||
} |
||||
|
||||
if (brace_nesting > 0 && $1 ~ "^[[:alnum:]_]+$" && NF < 2) { |
||||
read_line(); |
||||
continue; |
||||
} |
||||
if (brace_nesting > 0 && |
||||
$0 ~ "^[[:alnum:]_]+[[:space:]]*(\\.|->)[[:space:]]*[[:alnum:]_]+" && |
||||
$2 in rcu_batches) { |
||||
# Make uses of rcu_batches global. Somewhat unreliable. |
||||
shift_fields(1, 0); |
||||
print_fields(1); |
||||
continue; |
||||
} |
||||
|
||||
if ($1 == "static" && NF < 3) { |
||||
read_line(); |
||||
continue; |
||||
} |
||||
if ($1 == "static" && ($2 == "bool" && $3 == "try_check_zero" || |
||||
$2 == "void" && $3 == "srcu_flip")) { |
||||
shift_fields(1, 1); |
||||
print_fields(2); |
||||
continue; |
||||
} |
||||
|
||||
# Distinguish between read-side and write-side memory barriers. |
||||
if ($1 == "smp_mb" && NF < 2) { |
||||
read_line(); |
||||
continue; |
||||
} |
||||
if (match($0, /^smp_mb[[:space:]();\/*]*[[:alnum:]]/)) { |
||||
barrier_letter = substr($0, RLENGTH, 1); |
||||
if (barrier_letter ~ /A|D/) |
||||
new_barrier_name = "sync_smp_mb"; |
||||
else if (barrier_letter ~ /B|C/) |
||||
new_barrier_name = "rs_smp_mb"; |
||||
else { |
||||
print "Unrecognized memory barrier." > "/dev/null"; |
||||
exit 1; |
||||
} |
||||
|
||||
shift_fields(1, 1); |
||||
printf("%s", new_barrier_name) > outputfile; |
||||
continue; |
||||
} |
||||
|
||||
# Skip definition of rcu_synchronize, since it is already |
||||
# defined in misc.h. Only present in old versions of srcu. |
||||
if (brace_nesting == 0 && paren_nesting == 0 && |
||||
$1 == "struct" && $2 == "rcu_synchronize" && |
||||
$0 ~ "^struct(" FS ")+rcu_synchronize(" FS ")+\\{") { |
||||
shift_fields(2, 0); |
||||
while (brace_nesting) { |
||||
if (NF < 2) |
||||
read_line(); |
||||
shift_fields(1, 0); |
||||
} |
||||
} |
||||
|
||||
# Skip definition of wakeme_after_rcu for the same reason |
||||
if (brace_nesting == 0 && $1 == "static" && $2 == "void" && |
||||
$3 == "wakeme_after_rcu") { |
||||
while (NF < 5) |
||||
read_line(); |
||||
shift_fields(3, 0); |
||||
do { |
||||
while (NF < 3) |
||||
read_line(); |
||||
shift_fields(1, 0); |
||||
} while (paren_nesting || brace_nesting); |
||||
} |
||||
|
||||
if ($1 ~ /^(unsigned|long)$/ && NF < 3) { |
||||
read_line(); |
||||
continue; |
||||
} |
||||
|
||||
# Give srcu_batches_completed the correct type for old SRCU. |
||||
if (brace_nesting == 0 && $1 == "long" && |
||||
$2 == "srcu_batches_completed") { |
||||
update_fieldsep("", 0); |
||||
printf("unsigned ") > outputfile; |
||||
print_fields(2); |
||||
continue; |
||||
} |
||||
if (brace_nesting == 0 && $1 == "unsigned" && $2 == "long" && |
||||
$3 == "srcu_batches_completed") { |
||||
print_fields(3); |
||||
continue; |
||||
} |
||||
|
||||
# Just print out the input code by default. |
||||
print_fields(1); |
||||
} |
||||
update_fieldsep("", 0); |
||||
print > outputfile; |
||||
next; |
||||
} |
||||
|
||||
END { |
||||
update_fieldsep("", 0); |
||||
|
||||
if (brace_nesting != 0) { |
||||
print "Unbalanced braces!" > "/dev/stderr"; |
||||
exit 1; |
||||
} |
||||
|
||||
# Define the rcu_batches |
||||
for (name in rcu_batches) |
||||
print "struct rcu_batch " name " = " rcu_batches[name] ";" > c_output; |
||||
} |
||||
@ -0,0 +1,16 @@ |
||||
#ifndef ASSUME_H |
||||
#define ASSUME_H |
||||
|
||||
/* Provide an assumption macro that can be disabled for gcc. */ |
||||
#ifdef RUN |
||||
#define assume(x) \ |
||||
do { \
|
||||
/* Evaluate x to suppress warnings. */ \
|
||||
(void) (x); \
|
||||
} while (0) |
||||
|
||||
#else |
||||
#define assume(x) __CPROVER_assume(x) |
||||
#endif |
||||
|
||||
#endif |
||||
@ -0,0 +1,41 @@ |
||||
#ifndef BARRIERS_H |
||||
#define BARRIERS_H |
||||
|
||||
#define barrier() __asm__ __volatile__("" : : : "memory") |
||||
|
||||
#ifdef RUN |
||||
#define smp_mb() __sync_synchronize() |
||||
#define smp_mb__after_unlock_lock() __sync_synchronize() |
||||
#else |
||||
/*
|
||||
* Copied from CBMC's implementation of __sync_synchronize(), which |
||||
* seems to be disabled by default. |
||||
*/ |
||||
#define smp_mb() __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence", \ |
||||
"WWcumul", "RRcumul", "RWcumul", "WRcumul") |
||||
#define smp_mb__after_unlock_lock() __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence", \ |
||||
"WWcumul", "RRcumul", "RWcumul", "WRcumul") |
||||
#endif |
||||
|
||||
/*
|
||||
* Allow memory barriers to be disabled in either the read or write side |
||||
* of SRCU individually. |
||||
*/ |
||||
|
||||
#ifndef NO_SYNC_SMP_MB |
||||
#define sync_smp_mb() smp_mb() |
||||
#else |
||||
#define sync_smp_mb() do {} while (0) |
||||
#endif |
||||
|
||||
#ifndef NO_READ_SIDE_SMP_MB |
||||
#define rs_smp_mb() smp_mb() |
||||
#else |
||||
#define rs_smp_mb() do {} while (0) |
||||
#endif |
||||
|
||||
#define ACCESS_ONCE(x) (*(volatile typeof(x) *) &(x)) |
||||
#define READ_ONCE(x) ACCESS_ONCE(x) |
||||
#define WRITE_ONCE(x, val) (ACCESS_ONCE(x) = (val)) |
||||
|
||||
#endif |
||||
@ -0,0 +1,13 @@ |
||||
#ifndef BUG_ON_H |
||||
#define BUG_ON_H |
||||
|
||||
#include <assert.h> |
||||
|
||||
#define BUG() assert(0) |
||||
#define BUG_ON(x) assert(!(x)) |
||||
|
||||
/* Does it make sense to treat warnings as errors? */ |
||||
#define WARN() BUG() |
||||
#define WARN_ON(x) (BUG_ON(x), false) |
||||
|
||||
#endif |
||||
@ -0,0 +1,13 @@ |
||||
#include <config.h> |
||||
|
||||
/* Include all source files. */ |
||||
|
||||
#include "include_srcu.c" |
||||
|
||||
#include "preempt.c" |
||||
#include "misc.c" |
||||
|
||||
/* Used by test.c files */ |
||||
#include <pthread.h> |
||||
#include <stdlib.h> |
||||
#include <linux/srcu.h> |
||||
@ -0,0 +1,27 @@ |
||||
/* "Cheater" definitions based on restricted Kconfig choices. */ |
||||
|
||||
#undef CONFIG_TINY_RCU |
||||
#undef __CHECKER__ |
||||
#undef CONFIG_DEBUG_LOCK_ALLOC |
||||
#undef CONFIG_DEBUG_OBJECTS_RCU_HEAD |
||||
#undef CONFIG_HOTPLUG_CPU |
||||
#undef CONFIG_MODULES |
||||
#undef CONFIG_NO_HZ_FULL_SYSIDLE |
||||
#undef CONFIG_PREEMPT_COUNT |
||||
#undef CONFIG_PREEMPT_RCU |
||||
#undef CONFIG_PROVE_RCU |
||||
#undef CONFIG_RCU_NOCB_CPU |
||||
#undef CONFIG_RCU_NOCB_CPU_ALL |
||||
#undef CONFIG_RCU_STALL_COMMON |
||||
#undef CONFIG_RCU_TRACE |
||||
#undef CONFIG_RCU_USER_QS |
||||
#undef CONFIG_TASKS_RCU |
||||
#define CONFIG_TREE_RCU |
||||
|
||||
#define CONFIG_GENERIC_ATOMIC64 |
||||
|
||||
#if NR_CPUS > 1 |
||||
#define CONFIG_SMP |
||||
#else |
||||
#undef CONFIG_SMP |
||||
#endif |
||||
@ -0,0 +1,31 @@ |
||||
#include <config.h> |
||||
|
||||
#include <assert.h> |
||||
#include <errno.h> |
||||
#include <inttypes.h> |
||||
#include <pthread.h> |
||||
#include <stddef.h> |
||||
#include <string.h> |
||||
#include <sys/types.h> |
||||
|
||||
#include "int_typedefs.h" |
||||
|
||||
#include "barriers.h" |
||||
#include "bug_on.h" |
||||
#include "locks.h" |
||||
#include "misc.h" |
||||
#include "preempt.h" |
||||
#include "percpu.h" |
||||
#include "workqueues.h" |
||||
|
||||
#ifdef USE_SIMPLE_SYNC_SRCU |
||||
#define synchronize_srcu(sp) synchronize_srcu_original(sp) |
||||
#endif |
||||
|
||||
#include <srcu.c> |
||||
|
||||
#ifdef USE_SIMPLE_SYNC_SRCU |
||||
#undef synchronize_srcu |
||||
|
||||
#include "simple_sync_srcu.c" |
||||
#endif |
||||
@ -0,0 +1,33 @@ |
||||
#ifndef INT_TYPEDEFS_H |
||||
#define INT_TYPEDEFS_H |
||||
|
||||
#include <inttypes.h> |
||||
|
||||
typedef int8_t s8; |
||||
typedef uint8_t u8; |
||||
typedef int16_t s16; |
||||
typedef uint16_t u16; |
||||
typedef int32_t s32; |
||||
typedef uint32_t u32; |
||||
typedef int64_t s64; |
||||
typedef uint64_t u64; |
||||
|
||||
typedef int8_t __s8; |
||||
typedef uint8_t __u8; |
||||
typedef int16_t __s16; |
||||
typedef uint16_t __u16; |
||||
typedef int32_t __s32; |
||||
typedef uint32_t __u32; |
||||
typedef int64_t __s64; |
||||
typedef uint64_t __u64; |
||||
|
||||
#define S8_C(x) INT8_C(x) |
||||
#define U8_C(x) UINT8_C(x) |
||||
#define S16_C(x) INT16_C(x) |
||||
#define U16_C(x) UINT16_C(x) |
||||
#define S32_C(x) INT32_C(x) |
||||
#define U32_C(x) UINT32_C(x) |
||||
#define S64_C(x) INT64_C(x) |
||||
#define U64_C(x) UINT64_C(x) |
||||
|
||||
#endif |
||||
@ -0,0 +1,220 @@ |
||||
#ifndef LOCKS_H |
||||
#define LOCKS_H |
||||
|
||||
#include <limits.h> |
||||
#include <pthread.h> |
||||
#include <stdbool.h> |
||||
|
||||
#include "assume.h" |
||||
#include "bug_on.h" |
||||
#include "preempt.h" |
||||
|
||||
int nondet_int(void); |
||||
|
||||
#define __acquire(x) |
||||
#define __acquires(x) |
||||
#define __release(x) |
||||
#define __releases(x) |
||||
|
||||
/* Only use one lock mechanism. Select which one. */ |
||||
#ifdef PTHREAD_LOCK |
||||
struct lock_impl { |
||||
pthread_mutex_t mutex; |
||||
}; |
||||
|
||||
static inline void lock_impl_lock(struct lock_impl *lock) |
||||
{ |
||||
BUG_ON(pthread_mutex_lock(&lock->mutex)); |
||||
} |
||||
|
||||
static inline void lock_impl_unlock(struct lock_impl *lock) |
||||
{ |
||||
BUG_ON(pthread_mutex_unlock(&lock->mutex)); |
||||
} |
||||
|
||||
static inline bool lock_impl_trylock(struct lock_impl *lock) |
||||
{ |
||||
int err = pthread_mutex_trylock(&lock->mutex); |
||||
|
||||
if (!err) |
||||
return true; |
||||
else if (err == EBUSY) |
||||
return false; |
||||
BUG(); |
||||
} |
||||
|
||||
static inline void lock_impl_init(struct lock_impl *lock) |
||||
{ |
||||
pthread_mutex_init(&lock->mutex, NULL); |
||||
} |
||||
|
||||
#define LOCK_IMPL_INITIALIZER {.mutex = PTHREAD_MUTEX_INITIALIZER} |
||||
|
||||
#else /* !defined(PTHREAD_LOCK) */ |
||||
/* Spinlock that assumes that it always gets the lock immediately. */ |
||||
|
||||
struct lock_impl { |
||||
bool locked; |
||||
}; |
||||
|
||||
static inline bool lock_impl_trylock(struct lock_impl *lock) |
||||
{ |
||||
#ifdef RUN |
||||
/* TODO: Should this be a test and set? */ |
||||
return __sync_bool_compare_and_swap(&lock->locked, false, true); |
||||
#else |
||||
__CPROVER_atomic_begin(); |
||||
bool old_locked = lock->locked; |
||||
lock->locked = true; |
||||
__CPROVER_atomic_end(); |
||||
|
||||
/* Minimal barrier to prevent accesses leaking out of lock. */ |
||||
__CPROVER_fence("RRfence", "RWfence"); |
||||
|
||||
return !old_locked; |
||||
#endif |
||||
} |
||||
|
||||
static inline void lock_impl_lock(struct lock_impl *lock) |
||||
{ |
||||
/*
|
||||
* CBMC doesn't support busy waiting, so just assume that the |
||||
* lock is available. |
||||
*/ |
||||
assume(lock_impl_trylock(lock)); |
||||
|
||||
/*
|
||||
* If the lock was already held by this thread then the assumption |
||||
* is unsatisfiable (deadlock). |
||||
*/ |
||||
} |
||||
|
||||
static inline void lock_impl_unlock(struct lock_impl *lock) |
||||
{ |
||||
#ifdef RUN |
||||
BUG_ON(!__sync_bool_compare_and_swap(&lock->locked, true, false)); |
||||
#else |
||||
/* Minimal barrier to prevent accesses leaking out of lock. */ |
||||
__CPROVER_fence("RWfence", "WWfence"); |
||||
|
||||
__CPROVER_atomic_begin(); |
||||
bool old_locked = lock->locked; |
||||
lock->locked = false; |
||||
__CPROVER_atomic_end(); |
||||
|
||||
BUG_ON(!old_locked); |
||||
#endif |
||||
} |
||||
|
||||
static inline void lock_impl_init(struct lock_impl *lock) |
||||
{ |
||||
lock->locked = false; |
||||
} |
||||
|
||||
#define LOCK_IMPL_INITIALIZER {.locked = false} |
||||
|
||||
#endif /* !defined(PTHREAD_LOCK) */ |
||||
|
||||
/*
|
||||
* Implement spinlocks using the lock mechanism. Wrap the lock to prevent mixing |
||||
* locks of different types. |
||||
*/ |
||||
typedef struct { |
||||
struct lock_impl internal_lock; |
||||
} spinlock_t; |
||||
|
||||
#define SPIN_LOCK_UNLOCKED {.internal_lock = LOCK_IMPL_INITIALIZER} |
||||
#define __SPIN_LOCK_UNLOCKED(x) SPIN_LOCK_UNLOCKED |
||||
#define DEFINE_SPINLOCK(x) spinlock_t x = SPIN_LOCK_UNLOCKED |
||||
|
||||
static inline void spin_lock_init(spinlock_t *lock) |
||||
{ |
||||
lock_impl_init(&lock->internal_lock); |
||||
} |
||||
|
||||
static inline void spin_lock(spinlock_t *lock) |
||||
{ |
||||
/*
|
||||
* Spin locks also need to be removed in order to eliminate all |
||||
* memory barriers. They are only used by the write side anyway. |
||||
*/ |
||||
#ifndef NO_SYNC_SMP_MB |
||||
preempt_disable(); |
||||
lock_impl_lock(&lock->internal_lock); |
||||
#endif |
||||
} |
||||
|
||||
static inline void spin_unlock(spinlock_t *lock) |
||||
{ |
||||
#ifndef NO_SYNC_SMP_MB |
||||
lock_impl_unlock(&lock->internal_lock); |
||||
preempt_enable(); |
||||
#endif |
||||
} |
||||
|
||||
/* Don't bother with interrupts */ |
||||
#define spin_lock_irq(lock) spin_lock(lock) |
||||
#define spin_unlock_irq(lock) spin_unlock(lock) |
||||
#define spin_lock_irqsave(lock, flags) spin_lock(lock) |
||||
#define spin_unlock_irqrestore(lock, flags) spin_unlock(lock) |
||||
|
||||
/*
|
||||
* This is supposed to return an int, but I think that a bool should work as |
||||
* well. |
||||
*/ |
||||
static inline bool spin_trylock(spinlock_t *lock) |
||||
{ |
||||
#ifndef NO_SYNC_SMP_MB |
||||
preempt_disable(); |
||||
return lock_impl_trylock(&lock->internal_lock); |
||||
#else |
||||
return true; |
||||
#endif |
||||
} |
||||
|
||||
struct completion { |
||||
/* Hopefuly this won't overflow. */ |
||||
unsigned int count; |
||||
}; |
||||
|
||||
#define COMPLETION_INITIALIZER(x) {.count = 0} |
||||
#define DECLARE_COMPLETION(x) struct completion x = COMPLETION_INITIALIZER(x) |
||||
#define DECLARE_COMPLETION_ONSTACK(x) DECLARE_COMPLETION(x) |
||||
|
||||
static inline void init_completion(struct completion *c) |
||||
{ |
||||
c->count = 0; |
||||
} |
||||
|
||||
static inline void wait_for_completion(struct completion *c) |
||||
{ |
||||
unsigned int prev_count = __sync_fetch_and_sub(&c->count, 1); |
||||
|
||||
assume(prev_count); |
||||
} |
||||
|
||||
static inline void complete(struct completion *c) |
||||
{ |
||||
unsigned int prev_count = __sync_fetch_and_add(&c->count, 1); |
||||
|
||||
BUG_ON(prev_count == UINT_MAX); |
||||
} |
||||
|
||||
/* This function probably isn't very useful for CBMC. */ |
||||
static inline bool try_wait_for_completion(struct completion *c) |
||||
{ |
||||
BUG(); |
||||
} |
||||
|
||||
static inline bool completion_done(struct completion *c) |
||||
{ |
||||
return c->count; |
||||
} |
||||
|
||||
/* TODO: Implement complete_all */ |
||||
static inline void complete_all(struct completion *c) |
||||
{ |
||||
BUG(); |
||||
} |
||||
|
||||
#endif |
||||
@ -0,0 +1,11 @@ |
||||
#include <config.h> |
||||
|
||||
#include "misc.h" |
||||
#include "bug_on.h" |
||||
|
||||
struct rcu_head; |
||||
|
||||
void wakeme_after_rcu(struct rcu_head *head) |
||||
{ |
||||
BUG(); |
||||
} |
||||
@ -0,0 +1,58 @@ |
||||
#ifndef MISC_H |
||||
#define MISC_H |
||||
|
||||
#include "assume.h" |
||||
#include "int_typedefs.h" |
||||
#include "locks.h" |
||||
|
||||
#include <linux/types.h> |
||||
|
||||
/* Probably won't need to deal with bottom halves. */ |
||||
static inline void local_bh_disable(void) {} |
||||
static inline void local_bh_enable(void) {} |
||||
|
||||
#define MODULE_ALIAS(X) |
||||
#define module_param(...) |
||||
#define EXPORT_SYMBOL_GPL(x) |
||||
|
||||
#define container_of(ptr, type, member) ({ \ |
||||
const typeof(((type *)0)->member) *__mptr = (ptr); \
|
||||
(type *)((char *)__mptr - offsetof(type, member)); \
|
||||
}) |
||||
|
||||
#ifndef USE_SIMPLE_SYNC_SRCU |
||||
/* Abuse udelay to make sure that busy loops terminate. */ |
||||
#define udelay(x) assume(0) |
||||
|
||||
#else |
||||
|
||||
/* The simple custom synchronize_srcu is ok with try_check_zero failing. */ |
||||
#define udelay(x) do { } while (0) |
||||
#endif |
||||
|
||||
#define trace_rcu_torture_read(rcutorturename, rhp, secs, c_old, c) \ |
||||
do { } while (0) |
||||
|
||||
#define notrace |
||||
|
||||
/* Avoid including rcupdate.h */ |
||||
struct rcu_synchronize { |
||||
struct rcu_head head; |
||||
struct completion completion; |
||||
}; |
||||
|
||||
void wakeme_after_rcu(struct rcu_head *head); |
||||
|
||||
#define rcu_lock_acquire(a) do { } while (0) |
||||
#define rcu_lock_release(a) do { } while (0) |
||||
#define rcu_lockdep_assert(c, s) do { } while (0) |
||||
#define RCU_LOCKDEP_WARN(c, s) do { } while (0) |
||||
|
||||
/* Let CBMC non-deterministically choose switch between normal and expedited. */ |
||||
bool rcu_gp_is_normal(void); |
||||
bool rcu_gp_is_expedited(void); |
||||
|
||||
/* Do the same for old versions of rcu. */ |
||||
#define rcu_expedited (rcu_gp_is_expedited()) |
||||
|
||||
#endif |
||||
@ -0,0 +1,92 @@ |
||||
#ifndef PERCPU_H |
||||
#define PERCPU_H |
||||
|
||||
#include <stddef.h> |
||||
#include "bug_on.h" |
||||
#include "preempt.h" |
||||
|
||||
#define __percpu |
||||
|
||||
/* Maximum size of any percpu data. */ |
||||
#define PERCPU_OFFSET (4 * sizeof(long)) |
||||
|
||||
/* Ignore alignment, as CBMC doesn't care about false sharing. */ |
||||
#define alloc_percpu(type) __alloc_percpu(sizeof(type), 1) |
||||
|
||||
static inline void *__alloc_percpu(size_t size, size_t align) |
||||
{ |
||||
BUG(); |
||||
return NULL; |
||||
} |
||||
|
||||
static inline void free_percpu(void *ptr) |
||||
{ |
||||
BUG(); |
||||
} |
||||
|
||||
#define per_cpu_ptr(ptr, cpu) \ |
||||
((typeof(ptr)) ((char *) (ptr) + PERCPU_OFFSET * cpu)) |
||||
|
||||
#define __this_cpu_inc(pcp) __this_cpu_add(pcp, 1) |
||||
#define __this_cpu_dec(pcp) __this_cpu_sub(pcp, 1) |
||||
#define __this_cpu_sub(pcp, n) __this_cpu_add(pcp, -(typeof(pcp)) (n)) |
||||
|
||||
#define this_cpu_inc(pcp) this_cpu_add(pcp, 1) |
||||
#define this_cpu_dec(pcp) this_cpu_sub(pcp, 1) |
||||
#define this_cpu_sub(pcp, n) this_cpu_add(pcp, -(typeof(pcp)) (n)) |
||||
|
||||
/* Make CBMC use atomics to work around bug. */ |
||||
#ifdef RUN |
||||
#define THIS_CPU_ADD_HELPER(ptr, x) (*(ptr) += (x)) |
||||
#else |
||||
/*
|
||||
* Split the atomic into a read and a write so that it has the least |
||||
* possible ordering. |
||||
*/ |
||||
#define THIS_CPU_ADD_HELPER(ptr, x) \ |
||||
do { \
|
||||
typeof(ptr) this_cpu_add_helper_ptr = (ptr); \
|
||||
typeof(ptr) this_cpu_add_helper_x = (x); \
|
||||
typeof(*ptr) this_cpu_add_helper_temp; \
|
||||
__CPROVER_atomic_begin(); \
|
||||
this_cpu_add_helper_temp = *(this_cpu_add_helper_ptr); \
|
||||
__CPROVER_atomic_end(); \
|
||||
this_cpu_add_helper_temp += this_cpu_add_helper_x; \
|
||||
__CPROVER_atomic_begin(); \
|
||||
*(this_cpu_add_helper_ptr) = this_cpu_add_helper_temp; \
|
||||
__CPROVER_atomic_end(); \
|
||||
} while (0) |
||||
#endif |
||||
|
||||
/*
|
||||
* For some reason CBMC needs an atomic operation even though this is percpu |
||||
* data. |
||||
*/ |
||||
#define __this_cpu_add(pcp, n) \ |
||||
do { \
|
||||
BUG_ON(preemptible()); \
|
||||
THIS_CPU_ADD_HELPER(per_cpu_ptr(&(pcp), thread_cpu_id), \
|
||||
(typeof(pcp)) (n)); \
|
||||
} while (0) |
||||
|
||||
#define this_cpu_add(pcp, n) \ |
||||
do { \
|
||||
int this_cpu_add_impl_cpu = get_cpu(); \
|
||||
THIS_CPU_ADD_HELPER(per_cpu_ptr(&(pcp), this_cpu_add_impl_cpu), \
|
||||
(typeof(pcp)) (n)); \
|
||||
put_cpu(); \
|
||||
} while (0) |
||||
|
||||
/*
|
||||
* This will cause a compiler warning because of the cast from char[][] to |
||||
* type*. This will cause a compile time error if type is too big. |
||||
*/ |
||||
#define DEFINE_PER_CPU(type, name) \ |
||||
char name[NR_CPUS][PERCPU_OFFSET]; \
|
||||
typedef char percpu_too_big_##name \
|
||||
[sizeof(type) > PERCPU_OFFSET ? -1 : 1] |
||||
|
||||
#define for_each_possible_cpu(cpu) \ |
||||
for ((cpu) = 0; (cpu) < NR_CPUS; ++(cpu)) |
||||
|
||||
#endif |
||||
@ -0,0 +1,78 @@ |
||||
#include <config.h> |
||||
|
||||
#include "preempt.h" |
||||
|
||||
#include "assume.h" |
||||
#include "locks.h" |
||||
|
||||
/* Support NR_CPUS of at most 64 */ |
||||
#define CPU_PREEMPTION_LOCKS_INIT0 LOCK_IMPL_INITIALIZER |
||||
#define CPU_PREEMPTION_LOCKS_INIT1 \ |
||||
CPU_PREEMPTION_LOCKS_INIT0, CPU_PREEMPTION_LOCKS_INIT0 |
||||
#define CPU_PREEMPTION_LOCKS_INIT2 \ |
||||
CPU_PREEMPTION_LOCKS_INIT1, CPU_PREEMPTION_LOCKS_INIT1 |
||||
#define CPU_PREEMPTION_LOCKS_INIT3 \ |
||||
CPU_PREEMPTION_LOCKS_INIT2, CPU_PREEMPTION_LOCKS_INIT2 |
||||
#define CPU_PREEMPTION_LOCKS_INIT4 \ |
||||
CPU_PREEMPTION_LOCKS_INIT3, CPU_PREEMPTION_LOCKS_INIT3 |
||||
#define CPU_PREEMPTION_LOCKS_INIT5 \ |
||||
CPU_PREEMPTION_LOCKS_INIT4, CPU_PREEMPTION_LOCKS_INIT4 |
||||
|
||||
/*
|
||||
* Simulate disabling preemption by locking a particular cpu. NR_CPUS |
||||
* should be the actual number of cpus, not just the maximum. |
||||
*/ |
||||
struct lock_impl cpu_preemption_locks[NR_CPUS] = { |
||||
CPU_PREEMPTION_LOCKS_INIT0 |
||||
#if (NR_CPUS - 1) & 1 |
||||
, CPU_PREEMPTION_LOCKS_INIT0 |
||||
#endif |
||||
#if (NR_CPUS - 1) & 2 |
||||
, CPU_PREEMPTION_LOCKS_INIT1 |
||||
#endif |
||||
#if (NR_CPUS - 1) & 4 |
||||
, CPU_PREEMPTION_LOCKS_INIT2 |
||||
#endif |
||||
#if (NR_CPUS - 1) & 8 |
||||
, CPU_PREEMPTION_LOCKS_INIT3 |
||||
#endif |
||||
#if (NR_CPUS - 1) & 16 |
||||
, CPU_PREEMPTION_LOCKS_INIT4 |
||||
#endif |
||||
#if (NR_CPUS - 1) & 32 |
||||
, CPU_PREEMPTION_LOCKS_INIT5 |
||||
#endif |
||||
}; |
||||
|
||||
#undef CPU_PREEMPTION_LOCKS_INIT0 |
||||
#undef CPU_PREEMPTION_LOCKS_INIT1 |
||||
#undef CPU_PREEMPTION_LOCKS_INIT2 |
||||
#undef CPU_PREEMPTION_LOCKS_INIT3 |
||||
#undef CPU_PREEMPTION_LOCKS_INIT4 |
||||
#undef CPU_PREEMPTION_LOCKS_INIT5 |
||||
|
||||
__thread int thread_cpu_id; |
||||
__thread int preempt_disable_count; |
||||
|
||||
void preempt_disable(void) |
||||
{ |
||||
BUG_ON(preempt_disable_count < 0 || preempt_disable_count == INT_MAX); |
||||
|
||||
if (preempt_disable_count++) |
||||
return; |
||||
|
||||
thread_cpu_id = nondet_int(); |
||||
assume(thread_cpu_id >= 0); |
||||
assume(thread_cpu_id < NR_CPUS); |
||||
lock_impl_lock(&cpu_preemption_locks[thread_cpu_id]); |
||||
} |
||||
|
||||
void preempt_enable(void) |
||||
{ |
||||
BUG_ON(preempt_disable_count < 1); |
||||
|
||||
if (--preempt_disable_count) |
||||
return; |
||||
|
||||
lock_impl_unlock(&cpu_preemption_locks[thread_cpu_id]); |
||||
} |
||||
@ -0,0 +1,58 @@ |
||||
#ifndef PREEMPT_H |
||||
#define PREEMPT_H |
||||
|
||||
#include <stdbool.h> |
||||
|
||||
#include "bug_on.h" |
||||
|
||||
/* This flag contains garbage if preempt_disable_count is 0. */ |
||||
extern __thread int thread_cpu_id; |
||||
|
||||
/* Support recursive preemption disabling. */ |
||||
extern __thread int preempt_disable_count; |
||||
|
||||
void preempt_disable(void); |
||||
void preempt_enable(void); |
||||
|
||||
static inline void preempt_disable_notrace(void) |
||||
{ |
||||
preempt_disable(); |
||||
} |
||||
|
||||
static inline void preempt_enable_no_resched(void) |
||||
{ |
||||
preempt_enable(); |
||||
} |
||||
|
||||
static inline void preempt_enable_notrace(void) |
||||
{ |
||||
preempt_enable(); |
||||
} |
||||
|
||||
static inline int preempt_count(void) |
||||
{ |
||||
return preempt_disable_count; |
||||
} |
||||
|
||||
static inline bool preemptible(void) |
||||
{ |
||||
return !preempt_count(); |
||||
} |
||||
|
||||
static inline int get_cpu(void) |
||||
{ |
||||
preempt_disable(); |
||||
return thread_cpu_id; |
||||
} |
||||
|
||||
static inline void put_cpu(void) |
||||
{ |
||||
preempt_enable(); |
||||
} |
||||
|
||||
static inline void might_sleep(void) |
||||
{ |
||||
BUG_ON(preempt_disable_count); |
||||
} |
||||
|
||||
#endif |
||||
@ -0,0 +1,50 @@ |
||||
#include <config.h> |
||||
|
||||
#include <assert.h> |
||||
#include <errno.h> |
||||
#include <inttypes.h> |
||||
#include <pthread.h> |
||||
#include <stddef.h> |
||||
#include <string.h> |
||||
#include <sys/types.h> |
||||
|
||||
#include "int_typedefs.h" |
||||
|
||||
#include "barriers.h" |
||||
#include "bug_on.h" |
||||
#include "locks.h" |
||||
#include "misc.h" |
||||
#include "preempt.h" |
||||
#include "percpu.h" |
||||
#include "workqueues.h" |
||||
|
||||
#include <linux/srcu.h> |
||||
|
||||
/* Functions needed from modify_srcu.c */ |
||||
bool try_check_zero(struct srcu_struct *sp, int idx, int trycount); |
||||
void srcu_flip(struct srcu_struct *sp); |
||||
|
||||
/* Simpler implementation of synchronize_srcu that ignores batching. */ |
||||
void synchronize_srcu(struct srcu_struct *sp) |
||||
{ |
||||
int idx; |
||||
/*
|
||||
* This code assumes that try_check_zero will succeed anyway, |
||||
* so there is no point in multiple tries. |
||||
*/ |
||||
const int trycount = 1; |
||||
|
||||
might_sleep(); |
||||
|
||||
/* Ignore the lock, as multiple writers aren't working yet anyway. */ |
||||
|
||||
idx = 1 ^ (sp->completed & 1); |
||||
|
||||
/* For comments see srcu_advance_batches. */ |
||||
|
||||
assume(try_check_zero(sp, idx, trycount)); |
||||
|
||||
srcu_flip(sp); |
||||
|
||||
assume(try_check_zero(sp, idx^1, trycount)); |
||||
} |
||||
@ -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 |
||||
@ -0,0 +1 @@ |
||||
*.out |
||||
@ -0,0 +1,11 @@ |
||||
CBMC_FLAGS = -I../.. -I../../src -I../../include -I../../empty_includes -32 -pointer-check -mm pso
|
||||
|
||||
all: |
||||
for i in ./*.pass; do \
|
||||
echo $$i ; \
|
||||
CBMC_FLAGS="$(CBMC_FLAGS)" sh ../test_script.sh --should-pass $$i > $$i.out 2>&1 ; \
|
||||
done
|
||||
for i in ./*.fail; do \
|
||||
echo $$i ; \
|
||||
CBMC_FLAGS="$(CBMC_FLAGS)" sh ../test_script.sh --should-fail $$i > $$i.out 2>&1 ; \
|
||||
done
|
||||
@ -0,0 +1 @@ |
||||
test_cbmc_options="-DASSERT_END" |
||||
@ -0,0 +1 @@ |
||||
test_cbmc_options="-DFORCE_FAILURE" |
||||
@ -0,0 +1 @@ |
||||
test_cbmc_options="-DFORCE_FAILURE_2" |
||||
@ -0,0 +1 @@ |
||||
test_cbmc_options="-DFORCE_FAILURE_3" |
||||
@ -0,0 +1,72 @@ |
||||
#include <src/combined_source.c> |
||||
|
||||
int x; |
||||
int y; |
||||
|
||||
int __unbuffered_tpr_x; |
||||
int __unbuffered_tpr_y; |
||||
|
||||
DEFINE_SRCU(ss); |
||||
|
||||
void rcu_reader(void) |
||||
{ |
||||
int idx; |
||||
|
||||
#ifndef FORCE_FAILURE_3 |
||||
idx = srcu_read_lock(&ss); |
||||
#endif |
||||
might_sleep(); |
||||
|
||||
__unbuffered_tpr_y = READ_ONCE(y); |
||||
#ifdef FORCE_FAILURE |
||||
srcu_read_unlock(&ss, idx); |
||||
idx = srcu_read_lock(&ss); |
||||
#endif |
||||
WRITE_ONCE(x, 1); |
||||
|
||||
#ifndef FORCE_FAILURE_3 |
||||
srcu_read_unlock(&ss, idx); |
||||
#endif |
||||
might_sleep(); |
||||
} |
||||
|
||||
void *thread_update(void *arg) |
||||
{ |
||||
WRITE_ONCE(y, 1); |
||||
#ifndef FORCE_FAILURE_2 |
||||
synchronize_srcu(&ss); |
||||
#endif |
||||
might_sleep(); |
||||
__unbuffered_tpr_x = READ_ONCE(x); |
||||
|
||||
return NULL; |
||||
} |
||||
|
||||
void *thread_process_reader(void *arg) |
||||
{ |
||||
rcu_reader(); |
||||
|
||||
return NULL; |
||||
} |
||||
|
||||
int main(int argc, char *argv[]) |
||||
{ |
||||
pthread_t tu; |
||||
pthread_t tpr; |
||||
|
||||
if (pthread_create(&tu, NULL, thread_update, NULL)) |
||||
abort(); |
||||
if (pthread_create(&tpr, NULL, thread_process_reader, NULL)) |
||||
abort(); |
||||
if (pthread_join(tu, NULL)) |
||||
abort(); |
||||
if (pthread_join(tpr, NULL)) |
||||
abort(); |
||||
assert(__unbuffered_tpr_y != 0 || __unbuffered_tpr_x != 0); |
||||
|
||||
#ifdef ASSERT_END |
||||
assert(0); |
||||
#endif |
||||
|
||||
return 0; |
||||
} |
||||
@ -0,0 +1,102 @@ |
||||
#!/bin/sh |
||||
|
||||
# This script expects a mode (either --should-pass or --should-fail) followed by |
||||
# an input file. The script uses the following environment variables. The test C |
||||
# source file is expected to be named test.c in the directory containing the |
||||
# input file. |
||||
# |
||||
# CBMC: The command to run CBMC. Default: cbmc |
||||
# CBMC_FLAGS: Additional flags to pass to CBMC |
||||
# NR_CPUS: Number of cpus to run tests with. Default specified by the test |
||||
# SYNC_SRCU_MODE: Choose implementation of synchronize_srcu. Defaults to simple. |
||||
# kernel: Version included in the linux kernel source. |
||||
# simple: Use try_check_zero directly. |
||||
# |
||||
# The input file is a script that is sourced by this file. It can define any of |
||||
# the following variables to configure the test. |
||||
# |
||||
# test_cbmc_options: Extra options to pass to CBMC. |
||||
# min_cpus_fail: Minimum number of CPUs (NR_CPUS) for verification to fail. |
||||
# The test is expected to pass if it is run with fewer. (Only |
||||
# useful for .fail files) |
||||
# default_cpus: Quantity of CPUs to use for the test, if not specified on the |
||||
# command line. Default: Larger of 2 and MIN_CPUS_FAIL. |
||||
|
||||
set -e |
||||
|
||||
if test "$#" -ne 2; then |
||||
echo "Expected one option followed by an input file" 1>&2 |
||||
exit 99 |
||||
fi |
||||
|
||||
if test "x$1" = "x--should-pass"; then |
||||
should_pass="yes" |
||||
elif test "x$1" = "x--should-fail"; then |
||||
should_pass="no" |
||||
else |
||||
echo "Unrecognized argument '$1'" 1>&2 |
||||
|
||||
# Exit code 99 indicates a hard error. |
||||
exit 99 |
||||
fi |
||||
|
||||
CBMC=${CBMC:-cbmc} |
||||
|
||||
SYNC_SRCU_MODE=${SYNC_SRCU_MODE:-simple} |
||||
|
||||
case ${SYNC_SRCU_MODE} in |
||||
kernel) sync_srcu_mode_flags="" ;; |
||||
simple) sync_srcu_mode_flags="-DUSE_SIMPLE_SYNC_SRCU" ;; |
||||
|
||||
*) |
||||
echo "Unrecognized argument '${SYNC_SRCU_MODE}'" 1>&2 |
||||
exit 99 |
||||
;; |
||||
esac |
||||
|
||||
min_cpus_fail=1 |
||||
|
||||
c_file=`dirname "$2"`/test.c |
||||
|
||||
# Source the input file. |
||||
. $2 |
||||
|
||||
if test ${min_cpus_fail} -gt 2; then |
||||
default_default_cpus=${min_cpus_fail} |
||||
else |
||||
default_default_cpus=2 |
||||
fi |
||||
default_cpus=${default_cpus:-${default_default_cpus}} |
||||
cpus=${NR_CPUS:-${default_cpus}} |
||||
|
||||
# Check if there are two few cpus to make the test fail. |
||||
if test $cpus -lt ${min_cpus_fail:-0}; then |
||||
should_pass="yes" |
||||
fi |
||||
|
||||
cbmc_opts="-DNR_CPUS=${cpus} ${sync_srcu_mode_flags} ${test_cbmc_options} ${CBMC_FLAGS}" |
||||
|
||||
echo "Running CBMC: ${CBMC} ${cbmc_opts} ${c_file}" |
||||
if ${CBMC} ${cbmc_opts} "${c_file}"; then |
||||
# Verification successful. Make sure that it was supposed to verify. |
||||
test "x${should_pass}" = xyes |
||||
else |
||||
cbmc_exit_status=$? |
||||
|
||||
# An exit status of 10 indicates a failed verification. |
||||
# (see cbmc_parse_optionst::do_bmc in the CBMC source code) |
||||
if test ${cbmc_exit_status} -eq 10 && test "x${should_pass}" = xno; then |
||||
: |
||||
else |
||||
echo "CBMC returned ${cbmc_exit_status} exit status" 1>&2 |
||||
|
||||
# Parse errors have exit status 6. Any other type of error |
||||
# should be considered a hard error. |
||||
if test ${cbmc_exit_status} -ne 6 && \ |
||||
test ${cbmc_exit_status} -ne 10; then |
||||
exit 99 |
||||
else |
||||
exit 1 |
||||
fi |
||||
fi |
||||
fi |
||||
Loading…
Reference in new issue