X-Git-Url: https://git.lttng.org/?a=blobdiff_plain;f=formal-model%2Furcu-controldataflow%2Furcu.spin;h=44bbe523e153abfe52c39ee3eac957a4b7f22f46;hb=794a737edb08278087a6628a37235d19ff68fce1;hp=f9341b4c2a7fb5b49c5654f6c7ae8521559ae754;hpb=551ac1a376f4d1e97b9026aa7436fbd0de6a5218;p=urcu.git diff --git a/formal-model/urcu-controldataflow/urcu.spin b/formal-model/urcu-controldataflow/urcu.spin index f9341b4..44bbe52 100644 --- a/formal-model/urcu-controldataflow/urcu.spin +++ b/formal-model/urcu-controldataflow/urcu.spin @@ -1,5 +1,6 @@ /* - * mem.spin: Promela code to validate memory barriers with OOO memory. + * mem.spin: Promela code to validate memory barriers with OOO memory + * and out-of-order instruction scheduling. * * This program is free software; you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by @@ -242,7 +243,6 @@ inline smp_mb(i, j) } } - #ifdef REMOTE_BARRIERS bit reader_barrier[NR_READERS]; @@ -268,32 +268,53 @@ inline smp_mb_recv(i, j) :: (reader_barrier[get_readerid()] == 1) -> smp_mb(i, j); reader_barrier[get_readerid()] = 0; - :: 1 -> skip; + :: 1 -> + /* + * Busy-looping waiting for other barrier requests are not considered as + * non-progress. + */ +#ifdef READER_PROGRESS +progress_reader2: +#endif + skip; :: 1 -> break; od; } -inline smp_mb_send(i, j) -{ - smp_mb(i, j); - i = 0; - do - :: i < NR_READERS -> - reader_barrier[i] = 1; - do - :: (reader_barrier[i] == 1) -> skip; - :: (reader_barrier[i] == 0) -> break; - od; - i++; - :: i >= NR_READERS -> - break - od; - smp_mb(i, j); +#ifdef WRITER_PROGRESS +#define PROGRESS_LABEL(progressid) progress_writer_progid_##progressid: +#else +#define PROGRESS_LABEL(progressid) +#endif + +#define smp_mb_send(i, j, progressid) \ +{ \ + smp_mb(i, j); \ + i = 0; \ + do \ + :: i < NR_READERS -> \ + reader_barrier[i] = 1; \ + do \ + :: (reader_barrier[i] == 1) -> \ + /* \ + * Busy-looping waiting for reader barrier handling is of little\ + * interest, given the reader has the ability to totally ignore \ + * barrier requests. \ + */ \ +PROGRESS_LABEL(progressid) \ + skip; \ + :: (reader_barrier[i] == 0) -> break; \ + od; \ + i++; \ + :: i >= NR_READERS -> \ + break \ + od; \ + smp_mb(i, j); \ } #else -#define smp_mb_send smp_mb +#define smp_mb_send(i, j, progressid) smp_mb(i, j) #define smp_mb_reader smp_mb #define smp_mb_recv(i, j) @@ -440,30 +461,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 */ @@ -472,17 +495,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) { @@ -516,50 +541,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: @@ -571,7 +612,7 @@ non_atomic3_end: goto non_atomic3_skip; non_atomic3: - smp_mb_recv(i, j); + smp_mb_recv(i, j); goto non_atomic3_end; non_atomic3_skip: @@ -596,9 +637,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 @@ -614,7 +663,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 */ @@ -664,12 +714,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 */ @@ -801,6 +861,11 @@ active proctype urcu_writer() byte i, j; byte tmp, tmp2, tmpa; byte old_gen; + byte cur_gp_val = 0; /* + * Keep a local trace of the current parity so + * we don't add non-existing dependencies on the global + * GP update. Needed to test single flip case. + */ wait_init_done(); @@ -842,13 +907,18 @@ progress_writer1: PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_READ_GP); PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WRITE_GP); PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT); + /* For single flip, we need to know the current parity */ + cur_gp_val = cur_gp_val ^ RCU_GP_CTR_BIT; #endif - do + do :: 1 -> + atomic { + if :: CONSUME_TOKENS(proc_urcu_writer, WRITE_PROD_NONE, WRITE_PROC_FIRST_MB) -> - smp_mb_send(i, j); + goto smp_mb_send1; +smp_mb_send1_end: PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_MB); /* first flip */ @@ -871,9 +941,15 @@ progress_writer1: ooo_mem(i); /* ONLY WAITING FOR READER 0 */ tmp2 = READ_CACHED_VAR(urcu_active_readers[0]); +#ifndef SINGLE_FLIP + /* In normal execution, we are always starting by + * waiting for the even parity. + */ + cur_gp_val = RCU_GP_CTR_BIT; +#endif if :: (tmp2 & RCU_GP_CTR_NEST_MASK) - && ((tmp2 ^ RCU_GP_CTR_BIT) & RCU_GP_CTR_BIT) -> + && ((tmp2 ^ cur_gp_val) & RCU_GP_CTR_BIT) -> PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WAIT_LOOP); :: else -> PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WAIT); @@ -887,7 +963,8 @@ progress_writer1: | WRITE_PROC_FIRST_MB, /* can be reordered before/after flips */ 0) -> #ifndef GEN_ERROR_WRITER_PROGRESS - smp_mb_send(i, j); + goto smp_mb_send2; +smp_mb_send2_end: #else ooo_mem(i); #endif @@ -902,7 +979,6 @@ progress_writer1: | WRITE_PROC_FIRST_READ_GP | WRITE_PROC_FIRST_MB, WRITE_PROC_SECOND_READ_GP) -> - //smp_mb_send(i, j); //TEST ooo_mem(i); tmpa = READ_CACHED_VAR(urcu_gp_ctr); PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_READ_GP); @@ -942,7 +1018,8 @@ progress_writer1: | WRITE_PROC_FIRST_MB, /* can be reordered before/after flips */ 0) -> #ifndef GEN_ERROR_WRITER_PROGRESS - smp_mb_send(i, j); + goto smp_mb_send3; +smp_mb_send3_end: #else ooo_mem(i); #endif @@ -959,12 +1036,15 @@ progress_writer1: | WRITE_PROC_SECOND_WRITE_GP | WRITE_PROC_FIRST_MB, WRITE_PROC_SECOND_MB) -> - smp_mb_send(i, j); + goto smp_mb_send4; +smp_mb_send4_end: PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_MB); :: CONSUME_TOKENS(proc_urcu_writer, WRITE_PROC_ALL_TOKENS, 0) -> CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_ALL_TOKENS_CLEAR); break; + fi; + } od; write_lock = 0; @@ -988,6 +1068,25 @@ progress_writer2: #endif skip; od; + + /* Non-atomic parts of the loop */ + goto end; +smp_mb_send1: + smp_mb_send(i, j, 1); + goto smp_mb_send1_end; +#ifndef GEN_ERROR_WRITER_PROGRESS +smp_mb_send2: + smp_mb_send(i, j, 2); + goto smp_mb_send2_end; +smp_mb_send3: + smp_mb_send(i, j, 3); + goto smp_mb_send3_end; +#endif +smp_mb_send4: + smp_mb_send(i, j, 4); + goto smp_mb_send4_end; +end: + skip; } /* no name clash please */