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>
This commit is contained in:
Lance Roy
Paul E. McKenney
Родитель
d85b62f18d
Коммит
418b2977b3
|
|
@ -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
|
||||||
1
tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/.gitignore
поставляемый
Normal file
1
tools/testing/selftests/rcutorture/formal/srcu-cbmc/include/linux/.gitignore
поставляемый
Normal file
|
|
@ -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
|
||||||
1
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/.gitignore
поставляемый
Normal file
1
tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/.gitignore
поставляемый
Normal file
|
|
@ -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
|
||||||
Загрузка…
Ссылка в новой задаче