Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
-#define NR_READERS 1
-#define NR_WRITERS 1
-
-#define NR_PROCS 2
-
#define read_free_race (read_generation[0] == last_free_gen)
#define read_free (free_done && data_access[0])
#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
+//#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)
#ifndef READER_NEST_LEVEL
#define READER_NEST_LEVEL 1
#define RCU_GP_CTR_BIT (1 << 7)
#define RCU_GP_CTR_NEST_MASK (RCU_GP_CTR_BIT - 1)
#ifndef READER_NEST_LEVEL
#define READER_NEST_LEVEL 1
+//#define READER_NEST_LEVEL 2
#endif
#define REMOTE_BARRIERS
#endif
#define REMOTE_BARRIERS
/* All signal readers have same PID and uses same reader variable */
#ifdef TEST_SIGNAL_ON_WRITE
/* All signal readers have same PID and uses same reader variable */
#ifdef TEST_SIGNAL_ON_WRITE
-#define get_pid() ((_pid < 1) -> 0 : 1)
+
+#define NR_READERS 1 /* the writer is also a signal reader */
+#define NR_WRITERS 1
+
+#define NR_PROCS 1
+
+#define get_pid() (0)
+
#elif defined(TEST_SIGNAL_ON_READ)
#elif defined(TEST_SIGNAL_ON_READ)
#define get_pid() ((_pid < 2) -> 0 : 1)
#define get_pid() ((_pid < 2) -> 0 : 1)
+
+#define NR_READERS 1
+#define NR_WRITERS 1
+
+#define NR_PROCS 2
+
+
+#define NR_READERS 1
+#define NR_WRITERS 1
+
+#define NR_PROCS 2
+
#endif
#define get_readerid() (get_pid())
#endif
#define get_readerid() (get_pid())
* We are not modeling the whole rendez-vous between readers and writers here,
* we just let the writer update each reader's caches remotely.
*/
* 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_writer(i, j)
- if
- :: get_pid() >= NR_READERS ->
- smp_mb_pid(get_pid(), j);
- i = 0;
- do
- :: i < NR_READERS ->
- smp_mb_pid(i, j);
- i++;
- :: i >= NR_READERS -> break
- od;
- smp_mb_pid(get_pid(), j);
- :: else -> skip;
- fi;
+ smp_mb_pid(get_pid(), j);
+ i = 0;
+ do
+ :: i < NR_READERS ->
+ smp_mb_pid(i, j);
+ i++;
+ :: i >= NR_READERS -> break
+ od;
+ smp_mb_pid(get_pid(), j);
+}
+
+inline smp_mb_reader(i, j)
+{
+ skip;
+inline smp_mb_writer(i, j)
+{
+ smp_mb(i, j);
+}
+
+inline smp_mb_reader(i, j)
+{
+ smp_mb(i, j);
+}
+
#endif
/* Keep in sync manually with smp_rmb, wmp_wmb, ooo_mem and init() */
#endif
/* Keep in sync manually with smp_rmb, wmp_wmb, ooo_mem and init() */
&& ((tmp2 ^ READ_CACHED_VAR(urcu_gp_ctr))
& RCU_GP_CTR_BIT) ->
#ifndef GEN_ERROR_WRITER_PROGRESS
&& ((tmp2 ^ READ_CACHED_VAR(urcu_gp_ctr))
& RCU_GP_CTR_BIT) ->
#ifndef GEN_ERROR_WRITER_PROGRESS
/* Model the RCU read-side critical section. */
/* Model the RCU read-side critical section. */
+#ifndef TEST_SIGNAL_ON_WRITE
+
inline urcu_one_read(i, j, nest_i, tmp, tmp2)
{
nest_i = 0;
inline urcu_one_read(i, j, nest_i, tmp, tmp2)
{
nest_i = 0;
WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
tmp + 1);
fi;
WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
tmp + 1);
fi;
dispatch_sighand_read_exec();
nest_i++;
:: nest_i >= READER_NEST_LEVEL -> break;
dispatch_sighand_read_exec();
nest_i++;
:: nest_i >= READER_NEST_LEVEL -> break;
nest_i = 0;
do
:: nest_i < READER_NEST_LEVEL ->
nest_i = 0;
do
:: nest_i < READER_NEST_LEVEL ->
dispatch_sighand_read_exec();
tmp2 = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
ooo_mem(i);
dispatch_sighand_read_exec();
tmp2 = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
ooo_mem(i);
* progress when it's blocked by an always progressing reader.
*/
#ifdef READER_PROGRESS
* progress when it's blocked by an always progressing reader.
*/
#ifdef READER_PROGRESS
- /* Only test progress of one random reader. They are all the
- * same. */
- if
- :: get_readerid() == 0 ->
#endif
urcu_one_read(i, j, nest_i, tmp, tmp2);
od;
}
#endif
urcu_one_read(i, j, nest_i, tmp, tmp2);
od;
}
+#endif //!TEST_SIGNAL_ON_WRITE
+
#ifdef TEST_SIGNAL
/* signal handler reader */
#ifdef TEST_SIGNAL
/* signal handler reader */
WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
tmp + 1);
fi;
WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
tmp + 1);
fi;
nest_i++;
:: nest_i >= READER_NEST_LEVEL -> break;
od;
nest_i++;
:: nest_i >= READER_NEST_LEVEL -> break;
od;
nest_i = 0;
do
:: nest_i < READER_NEST_LEVEL ->
nest_i = 0;
do
:: nest_i < READER_NEST_LEVEL ->
tmp2 = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
ooo_mem(i);
WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2 - 1);
tmp2 = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
ooo_mem(i);
WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2 - 1);
* progress when it's blocked by an always progressing reader.
*/
#ifdef READER_PROGRESS
* progress when it's blocked by an always progressing reader.
*/
#ifdef READER_PROGRESS
- /* Only test progress of one random reader. They are all the
- * same. */
- if
- :: get_readerid() == 0 ->
#endif
urcu_one_read_sig(i, j, nest_i, tmp, tmp2);
od;
#endif
urcu_one_read_sig(i, j, nest_i, tmp, tmp2);
od;
dispatch_sighand_write_exec();
tmp = READ_CACHED_VAR(urcu_gp_ctr);
ooo_mem(i);
dispatch_sighand_write_exec();
tmp = READ_CACHED_VAR(urcu_gp_ctr);
ooo_mem(i);
dispatch_sighand_write_exec();
wait_for_quiescent_state(tmp, tmp2, i, j);
#endif
dispatch_sighand_write_exec();
wait_for_quiescent_state(tmp, tmp2, i, j);
#endif
dispatch_sighand_write_exec();
write_lock = 0;
/* free-up step, e.g., kfree(). */
dispatch_sighand_write_exec();
write_lock = 0;
/* free-up step, e.g., kfree(). */