Quick Quiz .2:
What are some Promela code-style issues with this example?
Answer:
There are several:
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:
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:
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