Re: [RFC 2/3] preempt_tracer: Disable IRQ while starting/stopping due to a preempt_counter change

[Peter Zijlstra]

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.