On Mon, 27 Apr 2020 at 17:45, Richard Henderson <[email protected]> wrote: > We *can* indicate fault from MemSingleNF for any reason whatsoever, or no > reason whatsoever. > > > // Implementation may suppress NF load for any reason > > if ConstrainUnpredictableBool(Unpredictable_NONFAULT) then > > return (bits(8*size) UNKNOWN, TRUE); > > What I'm trying to talk about above, is the third statement in MemSingleNF, > > > // Non-fault load from Device memory must not be performed externally > > if memaddrdesc.memattrs.memtype == MemType_Device then > > return (bits(8*size) UNKNOWN, TRUE); > > and the reason we can't actually test MemType_Device here. > > If you have better wording for that, I'm all ears. But I don't think there's > an actual bug here.
Oh, the comment didn't say you were relying on the operation being allowed to return 'fail' for any reason; in particular the line about "Normal memory [...] should access the bus" implies the opposite. (I also missed the distinction here between "indicate fault" and "fault".) But in that case you have the opposite problem, I think -- just because something's backed by host memory doesn't mean the guest didn't map it as Device: that case the architecture says must be indicated as 'fault' but this code won't do it. I would suggest something like: + * From this point on, all memory operations are MemSingleNF. + * + * Per the MemSingleNF pseudocode, a no-fault load from Device memory + * must not actually hit the bus -- it returns (UNKNOWN, FAULT) instead. + * + * Unfortuately we do not have access to the memory attributes from the PTE + * to tell Device memory from Normal memory. So we make a mostly + * correct check, and indicate (UNKNOWN, FAULT) for any MMIO. + * This gives the right answer for the common cases of "Normal memory, + * backed by host RAM" and "Device memory, backed by MMIO". + * The architecture allows us to suppress an NF load and return + * (UNKNOWN, FAULT) for any reason), so our behaviour (indicate + * fault) for the corner case of "Normal memory, backed by MMIO" is + * permitted. The case we get wrong is "Device memory, backed by + * host RAM", which we should return (UNKNOWN, FAULT) for but do not. + * + * Similarly, CPU_BP breakpoints would raise exceptions, and so + * return (UNKNOWN, FAULT). For simplicity, we consider gdb and + * architectural breakpoints the same. assuming my understanding is correct... thanks -- PMM
