X-Git-Url: http://git.liburcu.org/?p=urcu.git;a=blobdiff_plain;f=formal-model%2Fresults%2Furcu-controldataflow-ipi-intel%2FDEFINES;fp=formal-model%2Fresults%2Furcu-controldataflow-ipi-intel%2FDEFINES;h=abea5ff8dfc230861f4d88ad7b56f40131c5482a;hp=0000000000000000000000000000000000000000;hb=f2b3a82d7569463cc9b28bdd0943f06984197b6a;hpb=f24274b95c646682a448694eb0c759311cb7a5af diff --git a/formal-model/results/urcu-controldataflow-ipi-intel/DEFINES b/formal-model/results/urcu-controldataflow-ipi-intel/DEFINES new file mode 100644 index 0000000..abea5ff --- /dev/null +++ b/formal-model/results/urcu-controldataflow-ipi-intel/DEFINES @@ -0,0 +1,18 @@ + +// Poison value for freed memory +#define POISON 1 +// Memory with correct data +#define WINE 0 +#define SLAB_SIZE 2 + +#define read_poison (data_read_first[0] == POISON || data_read_second[0] == POISON) + +#define RCU_GP_CTR_BIT (1 << 7) +#define RCU_GP_CTR_NEST_MASK (RCU_GP_CTR_BIT - 1) + +//disabled +#define REMOTE_BARRIERS + +//#define ARCH_ALPHA +#define ARCH_INTEL +//#define ARCH_POWERPC