From 19d8de31dc92430df89d90e8ba76212b764afd44 Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Wed, 20 May 2009 00:25:17 -0400 Subject: [PATCH] Fix urcu controldataflow model remote barriers Need to split the pointer read from the data access to allow the writer to issue a memory barrier (actually more than one) to let the single flip race occur. Signed-off-by: Mathieu Desnoyers --- formal-model/urcu-controldataflow/urcu.spin | 111 +++++++++++++------- 1 file changed, 75 insertions(+), 36 deletions(-) diff --git a/formal-model/urcu-controldataflow/urcu.spin b/formal-model/urcu-controldataflow/urcu.spin index 5c377f7..484205a 100644 --- a/formal-model/urcu-controldataflow/urcu.spin +++ b/formal-model/urcu-controldataflow/urcu.spin @@ -441,30 +441,32 @@ int _proc_urcu_reader; #define READ_LOCK_NESTED_OUT (1 << 11) #define READ_PROC_READ_GEN (1 << 12) +#define READ_PROC_ACCESS_GEN (1 << 13) -/* PROCEDURE_READ_UNLOCK (NESTED) base = << 13 : 13 to 14 */ -#define READ_UNLOCK_NESTED_BASE 13 -#define READ_UNLOCK_NESTED_OUT (1 << 14) +/* PROCEDURE_READ_UNLOCK (NESTED) base = << 14 : 14 to 15 */ +#define READ_UNLOCK_NESTED_BASE 14 +#define READ_UNLOCK_NESTED_OUT (1 << 15) -#define READ_PROC_SECOND_MB (1 << 15) +#define READ_PROC_SECOND_MB (1 << 16) -/* PROCEDURE_READ_UNLOCK base = << 16 : 16 to 17 */ -#define READ_UNLOCK_BASE 16 -#define READ_UNLOCK_OUT (1 << 17) +/* PROCEDURE_READ_UNLOCK base = << 17 : 17 to 18 */ +#define READ_UNLOCK_BASE 17 +#define READ_UNLOCK_OUT (1 << 18) -/* PROCEDURE_READ_LOCK_UNROLL base = << 18 : 18 to 22 */ -#define READ_LOCK_UNROLL_BASE 18 -#define READ_LOCK_OUT_UNROLL (1 << 22) +/* PROCEDURE_READ_LOCK_UNROLL base = << 19 : 19 to 23 */ +#define READ_LOCK_UNROLL_BASE 19 +#define READ_LOCK_OUT_UNROLL (1 << 23) -#define READ_PROC_THIRD_MB (1 << 23) +#define READ_PROC_THIRD_MB (1 << 24) -#define READ_PROC_READ_GEN_UNROLL (1 << 24) +#define READ_PROC_READ_GEN_UNROLL (1 << 25) +#define READ_PROC_ACCESS_GEN_UNROLL (1 << 26) -#define READ_PROC_FOURTH_MB (1 << 25) +#define READ_PROC_FOURTH_MB (1 << 27) -/* PROCEDURE_READ_UNLOCK_UNROLL base = << 26 : 26 to 27 */ -#define READ_UNLOCK_UNROLL_BASE 26 -#define READ_UNLOCK_OUT_UNROLL (1 << 27) +/* PROCEDURE_READ_UNLOCK_UNROLL base = << 28 : 28 to 29 */ +#define READ_UNLOCK_UNROLL_BASE 28 +#define READ_UNLOCK_OUT_UNROLL (1 << 29) /* Should not include branches */ @@ -473,17 +475,19 @@ int _proc_urcu_reader; | READ_PROC_FIRST_MB \ | READ_LOCK_NESTED_OUT \ | READ_PROC_READ_GEN \ + | READ_PROC_ACCESS_GEN \ | READ_UNLOCK_NESTED_OUT \ | READ_PROC_SECOND_MB \ | READ_UNLOCK_OUT \ | READ_LOCK_OUT_UNROLL \ | READ_PROC_THIRD_MB \ | READ_PROC_READ_GEN_UNROLL \ + | READ_PROC_ACCESS_GEN_UNROLL \ | READ_PROC_FOURTH_MB \ | READ_UNLOCK_OUT_UNROLL) /* Must clear all tokens, including branches */ -#define READ_PROC_ALL_TOKENS_CLEAR ((1 << 28) - 1) +#define READ_PROC_ALL_TOKENS_CLEAR ((1 << 30) - 1) inline urcu_one_read(i, j, nest_i, tmp, tmp2) { @@ -517,50 +521,66 @@ inline urcu_one_read(i, j, nest_i, tmp, tmp2) if :: CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE, READ_LOCK_OUT | READ_LOCK_NESTED_OUT - | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT + | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL - | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) + | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT, READ_LOCK_NESTED_OUT - | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT + | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL - | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) + | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT | READ_LOCK_NESTED_OUT, - READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT + READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL - | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) + | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN, + READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT + | READ_UNLOCK_OUT + | READ_LOCK_OUT_UNROLL + | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) + || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT + | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN, READ_UNLOCK_NESTED_OUT | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL - | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) + | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT - | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT, + | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN + | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT, READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL - | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) + | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT - | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT + | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN + | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT | READ_UNLOCK_OUT, READ_LOCK_OUT_UNROLL - | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) + | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT - | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT + | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN + | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL, - READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) + READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT - | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT + | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN + | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL | READ_PROC_READ_GEN_UNROLL, + READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) + || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT + | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN + | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT + | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL + | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL, READ_UNLOCK_OUT_UNROLL) || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT - | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT + | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL - | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL, + | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL, 0) -> goto non_atomic3; non_atomic3_end: @@ -597,9 +617,17 @@ non_atomic3_skip: ooo_mem(i); read_generation[get_readerid()] = READ_CACHED_VAR(generation_ptr); + PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_GEN); + + :: CONSUME_TOKENS(proc_urcu_reader, + READ_PROC_FIRST_MB /* mb() orders reads */ + | READ_PROC_READ_GEN, + READ_PROC_ACCESS_GEN) -> + ooo_mem(i); goto non_atomic; non_atomic_end: - PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_GEN); + PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_ACCESS_GEN); + /* Note : we remove the nested memory barrier from the read unlock * model, given it is not usually needed. The implementation has the barrier @@ -615,7 +643,8 @@ non_atomic_end: :: CONSUME_TOKENS(proc_urcu_reader, - READ_PROC_READ_GEN /* mb() orders reads */ + READ_PROC_ACCESS_GEN /* mb() orders reads */ + | READ_PROC_READ_GEN /* mb() orders reads */ | READ_PROC_FIRST_MB /* mb() ordered */ | READ_LOCK_OUT /* post-dominant */ | READ_LOCK_NESTED_OUT /* post-dominant */ @@ -665,12 +694,22 @@ non_atomic_end: ooo_mem(i); read_generation[get_readerid()] = READ_CACHED_VAR(generation_ptr); + PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_GEN_UNROLL); + + :: CONSUME_TOKENS(proc_urcu_reader, + READ_PROC_READ_GEN_UNROLL + | READ_PROC_FIRST_MB /* mb() orders reads */ + | READ_PROC_SECOND_MB /* mb() orders reads */ + | READ_PROC_THIRD_MB, /* mb() orders reads */ + READ_PROC_ACCESS_GEN_UNROLL) -> + ooo_mem(i); goto non_atomic2; non_atomic2_end: - PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_GEN_UNROLL); + PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_ACCESS_GEN_UNROLL); :: CONSUME_TOKENS(proc_urcu_reader, READ_PROC_READ_GEN_UNROLL /* mb() orders reads */ + | READ_PROC_ACCESS_GEN_UNROLL /* mb() orders reads */ | READ_PROC_FIRST_MB /* mb() ordered */ | READ_PROC_SECOND_MB /* mb() ordered */ | READ_PROC_THIRD_MB /* mb() ordered */ -- 2.34.1