From: Mathieu Desnoyers Date: Wed, 25 Feb 2009 01:58:55 +0000 (-0500) Subject: Add independent reader and writer progress checks X-Git-Tag: v0.1~275 X-Git-Url: https://git.liburcu.org/?p=urcu.git;a=commitdiff_plain;h=89674313b5ff1209dc090e3b2c48680d222e81cd Add independent reader and writer progress checks Signed-off-by: Mathieu Desnoyers --- diff --git a/formal-model/urcu/Makefile b/formal-model/urcu/Makefile index 7b395cb..c52c4ba 100644 --- a/formal-model/urcu/Makefile +++ b/formal-model/urcu/Makefile @@ -27,6 +27,9 @@ default: make urcu_free_no_wmb | tee urcu_free_no_wmb.log make urcu_free_no_mb | tee urcu_free_no_mb.log make urcu_free_single_flip | tee urcu_free_single_flip.log + make urcu_progress_writer | tee urcu_progress_writer.log + make urcu_progress_reader | tee urcu_progress_reader.log + make urcu_progress_writer_error | tee urcu_progress_writer_error.log make asserts | tee asserts.log make summary @@ -36,7 +39,7 @@ default: summary: @echo @echo "Verification summary" - @grep error *.log + @grep errors: *.log asserts: clean cat DEFINES > .input.spin @@ -86,6 +89,54 @@ urcu_free_ltl: cat .input.define >> pan.ltl spin -f "!(`cat urcu_free.ltl | grep -v ^//`)" >> pan.ltl +# Progress checks + +urcu_progress_writer: clean urcu_progress_writer_ltl \ + urcu_progress_writer_define run_weak_fair + cp .input.spin $@.spin.input + -cp .input.spin.trail $@.spin.input.trail + +urcu_progress_writer_define: + cp urcu_progress_writer.define .input.define + +urcu_progress_writer_ltl: + touch .input.define + cat DEFINES > pan.ltl + cat .input.define >> pan.ltl + spin -f "!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl + +urcu_progress_reader: clean urcu_progress_reader_ltl \ + urcu_progress_reader_define run_weak_fair + cp .input.spin $@.spin.input + -cp .input.spin.trail $@.spin.input.trail + +urcu_progress_reader_define: + cp urcu_progress_reader.define .input.define + +urcu_progress_reader_ltl: + touch .input.define + cat DEFINES > pan.ltl + cat .input.define >> pan.ltl + spin -f "!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl + +urcu_progress_writer_error: clean urcu_progress_writer_error_ltl \ + urcu_progress_writer_error_define run_weak_fair + cp .input.spin $@.spin.input + -cp .input.spin.trail $@.spin.input.trail + +urcu_progress_writer_error_define: + cp urcu_progress_writer_error.define .input.define + +urcu_progress_writer_error_ltl: + touch .input.define + cat DEFINES > pan.ltl + cat .input.define >> pan.ltl + spin -f "!(`cat urcu_progress.ltl | grep -v ^//`)" >> pan.ltl + + +run_weak_fair: pan + ./pan -a -f -v -c1 -X -m10000 -w20 + run: pan ./pan -a -v -c1 -X -m10000 -w20 diff --git a/formal-model/urcu/urcu.spin b/formal-model/urcu/urcu.spin index 5ac2f02..e9271f8 100644 --- a/formal-model/urcu/urcu.spin +++ b/formal-model/urcu/urcu.spin @@ -21,9 +21,9 @@ /* 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) @@ -144,16 +144,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) - -> - ooo_mem(i); + :: 1 -> + ooo_mem(i); + tmp = READ_CACHED_VAR(urcu_active_readers_one); + 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 skip; - :: else -> +#endif + :: else -> break; + fi; od; } @@ -177,33 +183,48 @@ active [NR_READERS] proctype urcu_reader() 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); +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 ooo_mem(i); - WRITE_CACHED_VAR(urcu_active_readers_one, tmp2); - :: else -> - WRITE_CACHED_VAR(urcu_active_readers_one, tmp + 1); - fi; - 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); - ooo_mem(i); - //smp_mc(i); /* added */ + 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; + 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); + ooo_mem(i); + //wakeup_all(i); + //smp_mc(i); /* added */ + od; } @@ -217,50 +238,70 @@ 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); } + ooo_mem(i); + + do + :: 1 -> + atomic { + if + :: write_lock == 0 -> + write_lock = 1; + break; + :: else -> + skip; + fi; + } + 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); + #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); + #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; + } + :: else -> break; 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); -#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); + /* + * 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 - 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; - } + skip; + od; } diff --git a/formal-model/urcu/urcu_free_single_flip.define b/formal-model/urcu/urcu_free_single_flip.define new file mode 100644 index 0000000..5e642ef --- /dev/null +++ b/formal-model/urcu/urcu_free_single_flip.define @@ -0,0 +1 @@ +#define SINGLE_FLIP diff --git a/formal-model/urcu/urcu_progress.ltl b/formal-model/urcu/urcu_progress.ltl new file mode 100644 index 0000000..8718641 --- /dev/null +++ b/formal-model/urcu/urcu_progress.ltl @@ -0,0 +1 @@ +([] <> !np_) diff --git a/formal-model/urcu/urcu_progress_reader.define b/formal-model/urcu/urcu_progress_reader.define new file mode 100644 index 0000000..ff3f783 --- /dev/null +++ b/formal-model/urcu/urcu_progress_reader.define @@ -0,0 +1 @@ +#define READER_PROGRESS diff --git a/formal-model/urcu/urcu_progress_writer.define b/formal-model/urcu/urcu_progress_writer.define new file mode 100644 index 0000000..1e4417f --- /dev/null +++ b/formal-model/urcu/urcu_progress_writer.define @@ -0,0 +1 @@ +#define WRITER_PROGRESS diff --git a/formal-model/urcu/urcu_progress_writer_error.define b/formal-model/urcu/urcu_progress_writer_error.define new file mode 100644 index 0000000..8d304f5 --- /dev/null +++ b/formal-model/urcu/urcu_progress_writer_error.define @@ -0,0 +1,2 @@ +#define WRITER_PROGRESS +#define GEN_ERROR_WRITER_PROGRESS