A safe RCU implementation must never permit a grace period to complete before the completion of any RCU readers that started before the start of the grace period. This is modeled by a grace_period_state variable that can take on three states as follows:
1 #define GP_IDLE 0 2 #define GP_WAITING 1 3 #define GP_DONE 2 4 byte grace_period_state = GP_DONE; |
The grace_period() process sets this variable as it progresses through the grace-period phases, as shown below:
1 proctype grace_period() 2 { 3 byte curr; 4 byte snap; 5 6 grace_period_state = GP_IDLE; 7 atomic { 8 printf("MDLN = %d\n", MAX_DYNTICK_LOOP_NOHZ); 9 snap = dynticks_progress_counter; 10 grace_period_state = GP_WAITING; 11 } 12 do 13 :: 1 -> 14 atomic { 15 curr = dynticks_progress_counter; 16 if 17 :: (curr == snap) && ((curr & 1) == 0) -> 18 break; 19 :: (curr - snap) > 2 || (snap & 1) == 0 -> 20 break; 21 :: 1 -> skip; 22 fi; 23 } 24 od; 25 grace_period_state = GP_DONE; 26 grace_period_state = GP_IDLE; 27 atomic { 28 snap = dynticks_progress_counter; 29 grace_period_state = GP_WAITING; 30 } 31 do 32 :: 1 -> 33 atomic { 34 curr = dynticks_progress_counter; 35 if 36 :: (curr == snap) && ((curr & 1) == 0) -> 37 break; 38 :: (curr != snap) -> 39 break; 40 :: 1 -> skip; 41 fi; 42 } 43 od; 44 grace_period_state = GP_DONE; 45 }
Lines 6, 10, 25, 26, 29, and 44 update this variable (combining atomically with algorithmic operations where feasible) to allow the dyntick_nohz() process to verify the basic RCU safety property. The form of this verification is to assert that the value of the grace_period_state variable cannot jump from GP_IDLE to GP_DONE during a time period over which RCU readers could plausibly persist.
Quick Quiz E.13: Given there are a pair of back-to-back changes to grace_period_state on lines 25 and 26, how can we be sure that line 25's changes won't be lost? End Quick Quiz
The dyntick_nohz() Promela process implements this verification as shown below:
1 proctype dyntick_nohz() 2 { 3 byte tmp; 4 byte i = 0; 5 bit old_gp_idle; 6 7 do 8 :: i >= MAX_DYNTICK_LOOP_NOHZ -> break; 9 :: i < MAX_DYNTICK_LOOP_NOHZ -> 10 tmp = dynticks_progress_counter; 11 atomic { 12 dynticks_progress_counter = tmp + 1; 13 old_gp_idle = (grace_period_state == GP_IDLE); 14 assert((dynticks_progress_counter & 1) == 1); 15 } 16 atomic { 17 tmp = dynticks_progress_counter; 18 assert(!old_gp_idle || 19 grace_period_state != GP_DONE); 20 } 21 atomic { 22 dynticks_progress_counter = tmp + 1; 23 assert((dynticks_progress_counter & 1) == 0); 24 } 25 i++; 26 od; 27 }
Line 13 sets a new old_gp_idle flag if the value of the grace_period_state variable is GP_IDLE at the beginning of task execution, and the assertion at lines 18 and 19 fire if the grace_period_state variable has advanced to GP_DONE during task execution, which would be illegal given that a single RCU read-side critical section could span the entire intervening time period.
The resulting model (dyntickRCU-base-s.spin), when run with the runspin.sh script, generates 964 states and passes without errors, which is reassuring. That said, although safety is critically important, it is also quite important to avoid indefinitely stalling grace periods. The next section therefore covers verifying liveness.
Paul E. McKenney 2011-12-16