On Fri, Feb 01, 2019 at 08:58:34AM +0100, Christoffer Dall wrote: > 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. Thanks. Neat tool. > > > > 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. Yes, I was attempting to integrate more of the expected state of the is / will be sleeping vcpu into the analysis. I was hoping that it was provable to make stronger statements about the use of vcpu requests. I failed to do so though, both with logical arguments and I couldn't come up with a way to model outside-guest mode with the litmus test. > > 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. There's also the mode state and barriers in place that ensure the order of observation for that and requests, but as I said I couldn't model it well enough to prove anything. > > 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. Well, I don't expect the vcpu requests to solve the world (if only!), but I was hoping that they could be used with a simpler pattern. I.e. on the sending side the vcpu request is fired off (probably with a kick too) and then forgotten. On the receiving side path only a check and handler need to be added, with no concern for the order of the handlers nor of other data that we cannot observe without also observing the request. I surrender though, because I do agree there's nothing wrong with the additional barriers in this patch, only that it no longer fits my opinion of the simplest pattern. Anyway, thanks for your patience and sorry for the noise. drew
