X-Git-Url: http://git.liburcu.org/?a=blobdiff_plain;f=formal-model%2Furcu%2Furcu.spin;h=324ee3945bd21507b11b49d9ab151230dcf0f0ed;hb=a5b558b0c4655e98f7d8f43b900b6e3350a74f86;hp=5ac2f02dd9d80c3abd8d08f2b20136dd9a604635;hpb=710b09b7ba5203ea868240c1746d0ac0fc65f884;p=urcu.git diff --git a/formal-model/urcu/urcu.spin b/formal-model/urcu/urcu.spin index 5ac2f02..324ee39 100644 --- a/formal-model/urcu/urcu.spin +++ b/formal-model/urcu/urcu.spin @@ -21,15 +21,15 @@ /* Promela validation variables. */ #define NR_READERS 1 -#define NR_WRITERS 2 +#define NR_WRITERS 1 -#define NR_PROCS 3 +#define NR_PROCS 2 #define get_pid() (_pid) /* * Each process have its own data in cache. Caches are randomly updated. - * smp_wmb and smp_rmb forces cache updates (write and read), wmb_mb forces + * smp_wmb and smp_rmb forces cache updates (write and read), smp_mb forces * both. */ @@ -80,6 +80,72 @@ :: 1 -> skip \ fi; +/* + * Remote barriers tests the scheme where a signal (or IPI) is sent to all + * reader threads to promote their compiler barrier to a smp_mb(). + */ +#ifdef REMOTE_BARRIERS + +inline smp_rmb_pid(i) +{ + atomic { + CACHE_READ_FROM_MEM(urcu_gp_ctr, i); + CACHE_READ_FROM_MEM(urcu_active_readers_one, i); + CACHE_READ_FROM_MEM(generation_ptr, i); + } +} + +inline smp_wmb_pid(i) +{ + atomic { + CACHE_WRITE_TO_MEM(urcu_gp_ctr, i); + CACHE_WRITE_TO_MEM(urcu_active_readers_one, i); + CACHE_WRITE_TO_MEM(generation_ptr, i); + } +} + +inline smp_mb_pid(i) +{ + atomic { +#ifndef NO_WMB + smp_wmb_pid(i); +#endif +#ifndef NO_RMB + smp_rmb_pid(i); +#endif +#ifdef NO_WMB +#ifdef NO_RMB + ooo_mem(i); +#endif +#endif + } +} + +/* + * Readers do a simple barrier(), writers are doing a smp_mb() _and_ sending a + * signal or IPI to have all readers execute a smp_mb. + * We are not modeling the whole rendez-vous between readers and writers here, + * we just let the writer update each reader's caches remotely. + */ +inline smp_mb(i) +{ + if + :: get_pid() >= NR_READERS -> + smp_mb_pid(get_pid()); + i = 0; + do + :: i < NR_READERS -> + smp_mb_pid(i); + i++; + :: i >= NR_READERS -> break + od; + smp_mb_pid(get_pid()); + :: else -> skip; + fi; +} + +#else + inline smp_rmb(i) { atomic { @@ -107,10 +173,16 @@ inline smp_mb(i) #ifndef NO_RMB smp_rmb(i); #endif - skip; +#ifdef NO_WMB +#ifdef NO_RMB + ooo_mem(i); +#endif +#endif } } +#endif + /* Keep in sync manually with smp_rmb, wmp_wmb and ooo_mem */ DECLARE_CACHED_VAR(byte, urcu_gp_ctr, 1); /* Note ! currently only one reader */ @@ -144,16 +216,22 @@ inline ooo_mem(i) inline wait_for_reader(tmp, id, i) { - tmp = READ_CACHED_VAR(urcu_active_readers_one); - ooo_mem(i); do - :: (tmp & RCU_GP_CTR_NEST_MASK) && ((tmp ^ READ_CACHED_VAR(urcu_gp_ctr)) - & RCU_GP_CTR_BIT) - -> + :: 1 -> + tmp = READ_CACHED_VAR(urcu_active_readers_one); + ooo_mem(i); + if + :: (tmp & RCU_GP_CTR_NEST_MASK) + && ((tmp ^ READ_CACHED_VAR(urcu_gp_ctr)) + & RCU_GP_CTR_BIT) -> +#ifndef GEN_ERROR_WRITER_PROGRESS + smp_mb(i); +#else ooo_mem(i); - skip; - :: else -> +#endif + :: else -> break; + fi; od; } @@ -163,6 +241,12 @@ inline wait_for_quiescent_state(tmp, i, j) do :: i < NR_READERS -> wait_for_reader(tmp, i, j); + if + :: (NR_READERS > 1) && (i < NR_READERS - 1) + -> ooo_mem(j); + :: else + -> skip; + fi; i++ :: i >= NR_READERS -> break od; @@ -170,42 +254,73 @@ inline wait_for_quiescent_state(tmp, i, j) /* Model the RCU read-side critical section. */ -active [NR_READERS] proctype urcu_reader() +inline urcu_one_read(i, nest_i, tmp, tmp2) { - byte i; - byte tmp, tmp2; - - assert(get_pid() < NR_PROCS); - - ooo_mem(i); - tmp = READ_CACHED_VAR(urcu_active_readers_one); - ooo_mem(i); - if - :: (!(tmp & RCU_GP_CTR_NEST_MASK)) - -> - tmp2 = READ_CACHED_VAR(urcu_gp_ctr); + nest_i = 0; + do + :: nest_i < READER_NEST_LEVEL -> ooo_mem(i); - WRITE_CACHED_VAR(urcu_active_readers_one, tmp2); - :: else -> - WRITE_CACHED_VAR(urcu_active_readers_one, tmp + 1); - fi; + tmp = READ_CACHED_VAR(urcu_active_readers_one); + ooo_mem(i); + if + :: (!(tmp & RCU_GP_CTR_NEST_MASK)) + -> + tmp2 = READ_CACHED_VAR(urcu_gp_ctr); + ooo_mem(i); + WRITE_CACHED_VAR(urcu_active_readers_one, tmp2); + :: else -> + WRITE_CACHED_VAR(urcu_active_readers_one, + tmp + 1); + fi; + smp_mb(i); + nest_i++; + :: nest_i >= READER_NEST_LEVEL -> break; + od; + ooo_mem(i); - smp_mb(i); read_generation = READ_CACHED_VAR(generation_ptr); ooo_mem(i); data_access = 1; ooo_mem(i); data_access = 0; - ooo_mem(i); - smp_mb(i); - ooo_mem(i); - tmp2 = READ_CACHED_VAR(urcu_active_readers_one); - ooo_mem(i); - WRITE_CACHED_VAR(urcu_active_readers_one, tmp2 - 1); + + nest_i = 0; + do + :: nest_i < READER_NEST_LEVEL -> + smp_mb(i); + tmp2 = READ_CACHED_VAR(urcu_active_readers_one); + ooo_mem(i); + WRITE_CACHED_VAR(urcu_active_readers_one, tmp2 - 1); + nest_i++; + :: nest_i >= READER_NEST_LEVEL -> break; + od; ooo_mem(i); //smp_mc(i); /* added */ } +active [NR_READERS] proctype urcu_reader() +{ + byte i, nest_i; + byte tmp, tmp2; + + assert(get_pid() < NR_PROCS); + +end_reader: + do + :: 1 -> + /* + * We do not test reader's progress here, because we are mainly + * interested in writer's progress. The reader never blocks + * anyway. We have to test for reader/writer's progress + * separately, otherwise we could think the writer is doing + * progress when it's blocked by an always progressing reader. + */ +#ifdef READER_PROGRESS +progress_reader: +#endif + urcu_one_read(i, nest_i, tmp, tmp2); + od; +} /* Model the RCU update process. */ @@ -217,50 +332,67 @@ active [NR_WRITERS] proctype urcu_writer() assert(get_pid() < NR_PROCS); - ooo_mem(i); - atomic { - old_gen = READ_CACHED_VAR(generation_ptr); - WRITE_CACHED_VAR(generation_ptr, old_gen + 1); - } - ooo_mem(i); - do - :: 1 -> + :: (READ_CACHED_VAR(generation_ptr) < 5) -> +#ifdef WRITER_PROGRESS +progress_writer1: +#endif + ooo_mem(i); atomic { - if - :: write_lock == 0 -> - write_lock = 1; - break; - :: else -> - skip; - fi; + old_gen = READ_CACHED_VAR(generation_ptr); + WRITE_CACHED_VAR(generation_ptr, old_gen + 1); } - od; - smp_mb(i); - ooo_mem(i); - tmp = READ_CACHED_VAR(urcu_gp_ctr); - ooo_mem(i); - WRITE_CACHED_VAR(urcu_gp_ctr, tmp ^ RCU_GP_CTR_BIT); - ooo_mem(i); - //smp_mc(i); - wait_for_quiescent_state(tmp, i, j); - //smp_mc(i); + ooo_mem(i); + + do + :: 1 -> + atomic { + if + :: write_lock == 0 -> + write_lock = 1; + break; + :: else -> + skip; + fi; + } + od; + smp_mb(i); + tmp = READ_CACHED_VAR(urcu_gp_ctr); + ooo_mem(i); + WRITE_CACHED_VAR(urcu_gp_ctr, tmp ^ RCU_GP_CTR_BIT); + ooo_mem(i); + //smp_mc(i); + wait_for_quiescent_state(tmp, i, j); + //smp_mc(i); #ifndef SINGLE_FLIP - ooo_mem(i); - tmp = READ_CACHED_VAR(urcu_gp_ctr); - ooo_mem(i); - WRITE_CACHED_VAR(urcu_gp_ctr, tmp ^ RCU_GP_CTR_BIT); - //smp_mc(i); - ooo_mem(i); - wait_for_quiescent_state(tmp, i, j); + ooo_mem(i); + tmp = READ_CACHED_VAR(urcu_gp_ctr); + ooo_mem(i); + WRITE_CACHED_VAR(urcu_gp_ctr, tmp ^ RCU_GP_CTR_BIT); + //smp_mc(i); + ooo_mem(i); + wait_for_quiescent_state(tmp, i, j); #endif - ooo_mem(i); - smp_mb(i); - ooo_mem(i); - write_lock = 0; - /* free-up step, e.g., kfree(). */ - atomic { - last_free_gen = old_gen; - free_done = 1; - } + smp_mb(i); + write_lock = 0; + /* free-up step, e.g., kfree(). */ + atomic { + last_free_gen = old_gen; + free_done = 1; + } + :: else -> break; + od; + /* + * Given the reader loops infinitely, let the writer also busy-loop + * with progress here so, with weak fairness, we can test the + * writer's progress. + */ +end_writer: + do + :: 1 -> +#ifdef WRITER_PROGRESS +progress_writer2: +#endif + skip; + od; }