On Thu, Jan 31, 2019 at 06:06:09PM +0100, Andrew Jones wrote:
> On Thu, Jan 31, 2019 at 02:52:11PM +0000, Marc Zyngier wrote:
> > On 31/01/2019 12:57, Andrew Jones wrote:
> > > On Thu, Jan 31, 2019 at 12:51:56PM +0100, Christoffer Dall wrote:
> >
> > [...]
> >
> > >> I don't think there's anything very unconventional here.
> > >
> > > Normally if a thread observes a change to vcpu->requests, then we ensure a
> > > change to some accompanying data is also observable. We're reversing that
> > > here, which adds a need for additional barriers and a strict request
> > > checking order.
> > >
> > >>
> > >> Let's try this: If you have a better way of implementing this, how
> > >> about you write a patch?
> > >
> > > It would just be this patch minus the unnecessary barriers. I can send it
> > > if you like, but I wouldn't want to change the authorship for such a small
> > > change.
> >
> > Having these barriers makes it explicit (at least to me) what data we
> > expect to be visible in other threads and in which order. You keep
> > saying that order doesn't matter and we disagree on this. Yes, you've
> > listed cases where we can survive things coming in out of order, but
> > that's not a proof that we don't need them.
> >
> > So at the end of the day, and unless you can prove that the barriers are
> > not necessary by providing the same form of validation tool, I'm
> > inclined to go with the verified approach.
>
> I don't know how to compile and run the litmus test, but I'd be happy to
> try if given some pointers.
You can look in tools/memory-model/README as a start.
> If I did know how, I would add vcpu->mode to
> the P1 inputs and some additional lines that look similar to what's in
> "Ensuring Requests Are Seen" of Documentation/virtual/kvm/vcpu-requests.rst
> Even without the litmus test please allow me to try again to describe why
> I think the barriers may be removed.
>
> Any vcpu we're attempting to power on must be on its way to sleep with a
> SLEEP request, or already be sleeping. This means that it's outside guest
> mode, or will be shortly. If the vcpu observes power_off=false in
> vcpu_req_sleep(), whether it was awaken or never even got to sleep, we
> know that observation is taking place with vcpu->mode != IN_GUEST_MODE.
>
> We now no longer need to be concerned with the relationship between
> power_off and the RESET vcpu request.
I disagree. That argument requires more explanation.
If you set power_off = false before posting the reset
request, then if the VCPU thread is awoken (for any reason) it can run
the VCPU without observing the reset request and that's the problem.
If you are making assumptions about only being woken up as a result of a
reset request, or the interaction with the pause flag, or setting the
sleep request to prevent the guest from executing again, that is a more
complex argument (which you haven't made yet!) and I add that it's a
brittle construction.
What we have here are three pieces of state:
reset_state->reset
vcpu->requests
vcpu->arch.power_state
They must be written to, and the writes must be observed, in that
particular order without any additional assumptions.
You keep arguing that you can enforce an ordering between these three
states with a single barrier which is clearly not possible.
So this boils down to you making additional assumptions (see above,
brittle) without explaining what they are. I suspect you want this to
fit in your mental model of how vcpu requests solve the world, otherwise
I'm not sure what your concern with this patch, which we all agree is
correct, really is.
Thanks,
Christoffer
_______________________________________________
kvmarm mailing list
kvmarm@xxxxxxxxxxxxxxxxxxxxx
https://lists.cs.columbia.edu/mailman/listinfo/kvmarm
