F.16 Chapter [*]

Quick Quiz [*].1: 
Why is there an unreached statement in locker? After all, isn't this a full state-space search?
 
Answer:
The locker process is an infinite loop, so control never reaches the end of this process. However, since there are no monotonically increasing variables, Promela is able to model this infinite loop with a small number of states.

Quick Quiz [*].2: 
What are some Promela code-style issues with this example?
 
Answer:
There are several:

  1. The declaration of sum should be moved to within the init block, since it is not used anywhere else.
  2. The assertion code should be moved outside of the initialization loop. The initialization loop can then be placed in an atomic block, greatly reducing the state space (by how much?).
  3. The atomic block covering the assertion code should be extended to include the initialization of sum and j, and also to cover the assertion. This also reduces the state space (again, by how much?).

Quick Quiz [*].3: 
Is there a more straightforward way to code the do-od statement?
 
Answer:
Yes. Replace it with if-fi and remove the two break statements.

Quick Quiz [*].4: 
Why are there atomic blocks at lines 12-21 and lines 44-56, when the operations within those atomic blocks have no atomic implementation on any current production microprocessor?
 
Answer:
Because those operations are for the benefit of the assertion only. They are not part of the algorithm itself. There is therefore no harm in marking them atomic, and so marking them greatly reduces the state space that must be searched by the Promela model.

Quick Quiz [*].5: 
Is the re-summing of the counters on lines 24-27 really necessary?
 
Answer:
Yes. To see this, delete these lines and run the model.

Alternatively, consider the following sequence of steps:

  1. One process is within its RCU read-side critical section, so that the value of ctr[0] is zero and the value of ctr[1] is two.
  2. An updater starts executing, and sees that the sum of the counters is two so that the fastpath cannot be executed. It therefore acquires the lock.
  3. A second updater starts executing, and fetches the value of ctr[0], which is zero.
  4. The first updater adds one to ctr[0], flips the index (which now becomes zero), then subtracts one from ctr[1] (which now becomes one).
  5. The second updater fetches the value of ctr[1], which is now one.
  6. The second updater now incorrectly concludes that it is safe to proceed on the fastpath, despite the fact that the original reader has not yet completed.

Quick Quiz [*].6: 
Yeah, that's just great! Now, just what am I supposed to do if I don't happen to have a machine with 40GB of main memory???
 
Answer:
Relax, there are a number of lawful answers to this question:

  1. Further optimize the model, reducing its memory consumption.
  2. Work out a pencil-and-paper proof, perhaps starting with the comments in the code in the Linux kernel.
  3. Devise careful torture tests, which, though they cannot prove the code correct, can find hidden bugs.
  4. There is some movement towards tools that do model checking on clusters of smaller machines. However, please note that we have not actually used such tools myself, courtesy of some large machines that Paul has occasional access to.

Quick Quiz [*].7: 
Why not simply increment rcu_update_flag, and then only increment dynticks_progress_counter if the old value of rcu_update_flag was zero???
 
Answer:
This fails in presence of NMIs. To see this, suppose an NMI was received just after rcu_irq_enter() incremented rcu_update_flag, but before it incremented dynticks_progress_counter. The instance of rcu_irq_enter() invoked by the NMI would see that the original value of rcu_update_flag was non-zero, and would therefore refrain from incrementing dynticks_progress_counter. This would leave the RCU grace-period machinery no clue that the NMI handler was executing on this CPU, so that any RCU read-side critical sections in the NMI handler would lose their RCU protection.

The possibility of NMI handlers, which, by definition cannot be masked, does complicate this code.

Quick Quiz [*].8: 
But if line 7 finds that we are the outermost interrupt, wouldn't we always need to increment dynticks_progress_counter?
 
Answer:
Not if we interrupted a running task! In that case, dynticks_progress_counter would have already been incremented by rcu_exit_nohz(), and there would be no need to increment it again.

Quick Quiz [*].9: 
Can you spot any bugs in any of the code in this section?
 
Answer:
Read the next section to see if you were correct.

Quick Quiz [*].10: 
Why isn't the memory barrier in rcu_exit_nohz() and rcu_enter_nohz() modeled in Promela?
 
Answer:
Promela assumes sequential consistency, so it is not necessary to model memory barriers. In fact, one must instead explicitly model lack of memory barriers, for example, as shown in Figure [*] on page [*].

Quick Quiz [*].11: 
Isn't it a bit strange to model rcu_exit_nohz() followed by rcu_enter_nohz()? Wouldn't it be more natural to instead model entry before exit?
 
Answer:
It probably would be more natural, but we will need this particular order for the liveness checks that we will add later.

Quick Quiz [*].12: 
Wait a minute! In the Linux kernel, both dynticks_progress_counter and rcu_dyntick_snapshot are per-CPU variables. So why are they instead being modeled as single global variables?
 
Answer:
Because the grace-period code processes each CPU's dynticks_progress_counter and rcu_dyntick_snapshot variables separately, we can collapse the state onto a single CPU. If the grace-period code were instead to do something special given specific values on specific CPUs, then we would indeed need to model multiple CPUs. But fortunately, we can safely confine ourselves to two CPUs, the one running the grace-period processing and the one entering and leaving dynticks-idle mode.

Quick Quiz [*].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?
 
Answer:
Recall that Promela and spin trace out every possible sequence of state changes. Therefore, timing is irrelevant: Promela/spin will be quite happy to jam the entire rest of the model between those two statements unless some state variable specifically prohibits doing so.

Quick Quiz [*].14: 
But what would you do if you needed the statements in a single EXECUTE_MAINLINE() group to execute non-atomically?
 
Answer:
The easiest thing to do would be to put each such statement in its own EXECUTE_MAINLINE() statement.

Quick Quiz [*].15: 
But what if the dynticks_nohz() process had ``if'' or ``do'' statements with conditions, where the statement bodies of these constructs needed to execute non-atomically?
 
Answer:
One approach, as we will see in a later section, is to use explicit labels and ``goto'' statements. For example, the construct:



		if
		:: i == 0 -> a = -1;
		:: else -> a = -2;
		fi;


could be modeled as something like:



		EXECUTE_MAINLINE(stmt1,
				 if
				 :: i == 0 -> goto stmt1_then;
				 :: else -> goto stmt1_else;
				 fi)
		stmt1_then: skip;
		EXECUTE_MAINLINE(stmt1_then1, a = -1; goto stmt1_end)
		stmt1_else: skip;
		EXECUTE_MAINLINE(stmt1_then1, a = -2)
		stmt1_end: skip;


However, it is not clear that the macro is helping much in the case of the ``if'' statement, so these sorts of situations will be open-coded in the following sections.

Quick Quiz [*].16: 
Why are lines 45 and 46 (the in_dyntick_irq = 0; and the i++;) executed atomically?
 
Answer:
These lines of code pertain to controlling the model, not to the code being modeled, so there is no reason to model them non-atomically. The motivation for modeling them atomically is to reduce the size of the state space.

Quick Quiz [*].17: 
What property of interrupts is this dynticks_irq() process unable to model?
 
Answer:
One such property is nested interrupts, which are handled in the following section.

Quick Quiz [*].18: 
Does Paul always write his code in this painfully incremental manner?
 
Answer:
Not always, but more and more frequently. In this case, Paul started with the smallest slice of code that included an interrupt handler, because he was not sure how best to model interrupts in Promela. Once he got that working, he added other features. (But if he was doing it again, he would start with a ``toy'' handler. For example, he might have the handler increment a variable twice and have the mainline code verify that the value was always even.)

Why the incremental approach? Consider the following, attributed to Brian W. Kernighan:

Debugging is twice as hard as writing the code in the first place. Therefore, if you write the code as cleverly as possible, you are, by definition, not smart enough to debug it.

This means that any attempt to optimize the production of code should place at least 66% of its emphasis on optimizing the debugging process, even at the expense of increasing the time and effort spent coding. Incremental coding and testing is one way to optimize the debugging process, at the expense of some increase in coding effort. Paul uses this approach because he rarely has the luxury of devoting full days (let alone weeks) to coding and debugging.

Quick Quiz [*].19: 
But what happens if an NMI handler starts running before an irq handler completes, and if that NMI handler continues running until a second irq handler starts?
 
Answer:
This cannot happen within the confines of a single CPU. The first irq handler cannot complete until the NMI handler returns. Therefore, if each of the dynticks and dynticks_nmi variables have taken on an even value during a given time interval, the corresponding CPU really was in a quiescent state at some time during that interval.

Quick Quiz [*].20: 
This is still pretty complicated. Why not just have a cpumask_t that has a bit set for each CPU that is in dyntick-idle mode, clearing the bit when entering an irq or NMI handler, and setting it upon exit?
 
Answer:
Although this approach would be functionally correct, it would result in excessive irq entry/exit overhead on large machines. In contrast, the approach laid out in this section allows each CPU to touch only per-CPU data on irq and NMI entry/exit, resulting in much lower irq entry/exit overhead, especially on large machines.

Paul E. McKenney 2011-12-16