From 6ae334b09959594326f5d85f76e0427c03a64995 Mon Sep 17 00:00:00 2001 From: compudj Date: Thu, 19 Mar 2009 14:05:02 -0400 Subject: [PATCH] spin model : inline reader Signed-off-by: Mathieu Desnoyers --- formal-model/urcu/urcu.spin | 92 +++++++++++++++++++------------------ 1 file changed, 48 insertions(+), 44 deletions(-) diff --git a/formal-model/urcu/urcu.spin b/formal-model/urcu/urcu.spin index 2282407..570da40 100644 --- a/formal-model/urcu/urcu.spin +++ b/formal-model/urcu/urcu.spin @@ -240,6 +240,53 @@ inline wait_for_quiescent_state(tmp, i, j) /* Model the RCU read-side critical section. */ +inline urcu_one_read(i, nest_i, tmp, tmp2) +{ + nest_i = 0; + do + :: nest_i < READER_NEST_LEVEL -> + 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); + 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); + nest_i++; + :: nest_i >= READER_NEST_LEVEL -> break; + od; + + ooo_mem(i); + read_generation = READ_CACHED_VAR(generation_ptr); + ooo_mem(i); + data_access = 1; + ooo_mem(i); + data_access = 0; + + nest_i = 0; + do + :: nest_i < READER_NEST_LEVEL -> + 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++; + :: nest_i >= READER_NEST_LEVEL -> break; + od; + ooo_mem(i); + //smp_mc(i); /* added */ +} + active [NR_READERS] proctype urcu_reader() { byte i, nest_i; @@ -260,53 +307,10 @@ end_reader: #ifdef READER_PROGRESS progress_reader: #endif - nest_i = 0; - do - :: nest_i < READER_NEST_LEVEL -> - 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); - 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); - nest_i++; - :: nest_i >= READER_NEST_LEVEL -> break; - od; - - ooo_mem(i); - read_generation = READ_CACHED_VAR(generation_ptr); - ooo_mem(i); - data_access = 1; - ooo_mem(i); - data_access = 0; - - nest_i = 0; - do - :: nest_i < READER_NEST_LEVEL -> - 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++; - :: nest_i >= READER_NEST_LEVEL -> break; - od; - ooo_mem(i); - //smp_mc(i); /* added */ + urcu_one_read(i, nest_i, tmp, tmp2); od; } - /* Model the RCU update process. */ active [NR_WRITERS] proctype urcu_writer() -- 2.34.1