X-Git-Url: http://git.liburcu.org/?a=blobdiff_plain;f=formal-model%2Furcu%2FDEFINES;h=5d5147e7d77d417f42df675fdf1e8d6fe77e99c6;hb=1e52eccf3cb657dccb197132f7cb47b683902538;hp=4224b3238c2b0832e9072f553384ce7ea0c4ee7f;hpb=06d6106d9482f3a2805a2512ef0cda203088f2f5;p=urcu.git diff --git a/formal-model/urcu/DEFINES b/formal-model/urcu/DEFINES index 4224b32..5d5147e 100644 --- a/formal-model/urcu/DEFINES +++ b/formal-model/urcu/DEFINES @@ -1,9 +1,17 @@ + +#define read_free_race (read_generation[0] == last_free_gen) +#define read_free (free_done && data_access[0]) + +//#define TEST_SIGNAL +//#define TEST_SIGNAL_ON_READ +//#define TEST_SIGNAL_ON_WRITE + #define RCU_GP_CTR_BIT (1 << 7) #define RCU_GP_CTR_NEST_MASK (RCU_GP_CTR_BIT - 1) -#define read_free_race (read_generation == last_free_gen) -#define read_free (free_done && data_access) - #ifndef READER_NEST_LEVEL #define READER_NEST_LEVEL 1 +//#define READER_NEST_LEVEL 2 #endif + +#define REMOTE_BARRIERS