On Wed, May 29, 2019 at 03:51:31PM +0200, Daniel Bristot de Oliveira wrote: > On 29/05/2019 12:20, Peter Zijlstra wrote:
> > I'm not sure I follow, IRQs disabled fully implies !preemptible. I don't > > see how the model would be more pessimistic than reality if it were to > > use this knowledge. > > Maybe I did not expressed myself well... and the example was not good either. > > "IRQs disabled fully implies !preemptible" is a "to big" step. In modeling (or > mathematical reasoning?), a good practice is to break the properties into > small > piece, and then build more complex reasoning/implications using these "small > properties." > > Doing "big steps" makes you prone "miss interpretations", creating ambiguity. > Then, -RT people are prone to be pessimist, non-RT optimistic, and so on... > and > that is what models try to avoid. You already construct the big model out of small generators, this is just one more of those little generators. > For instance, explaining this using words is contradictory:> > > Any !0 preempt_count(), which very much includes (Hard)IRQ and SoftIRQ > > counts, means non-preemptible. > > One might argue that, the preemption of a thread always takes place with > preempt_count() != 0, because __schedule() is always called with preemption > disabled, so the preemption takes place while in non-preemptive. Yeah, I know about that one; you've used it in your talks. Also, you've modeled the schedule preempt disable as a special state. If you want we can actually make it a special bit in the preempt_count word too, the patch shouldn't be too hard, although it would make no practical difference. > - WAIT But you (daniel) wants to fake the atomicity between preempt_disable > and > its tracepoint! > > Yes, I do, but this is a very straightforward step/assumption: the atomicity > is > about the real-event and the tracepoint that notifies it. It is not about two > different events. > > That is why it is worth letting the modeling rules to clarify the behavior of > system, without doing non-obvious implication in the code part, so we can > have a > model that fits better in the Linux actions/events to avoid ambiguity. You can easily build a little shim betwen the model and the tracehooks that fix this up if you don't want to stick it in the model proper. All the information is there. Heck you can even do that 3/3 thing internally I think.
