PeterSewell
commented
2 years ago Hi Martin,
On Sat, 5 Feb 2022 at 17:49, Martin Berger @.***> wrote:
I have a naive question which may betray my background in programming language theory: what is the intended notion Sail program equality?
None of our work so far has needed an explicit definition of program equality. For sequential uses of the instruction semantics, the most intensional thing we need is indeed the per-instruction traces of register and memory events (there is intra-instruction branching, but it's either on register/memory read values or loose-specification nondeterminism, not internal-choice nondeterminism, so I don't see any role for branching-time semantics here - though we do now work with trees instead of sets of traces for convenience). For concurrent uses, one also needs to extract the data one needs to compute the various dependency relations, which is more intensional. For relaxed virtual-memory concurrency, one needs to be able to express the absence of intra-instruction ordering between the translation-walk reads of distinct accesses (e.g. where those arise from misaligned accesses); that'll need a simple intra-instruction PAR of multiple tasks, though without interaction between the tasks; then the intra-instruction order won't be linear any more.
I know that this is a subtle issue, and not providing a clear answer might have been a choice. Anyway, the papers I have seen are a bit vague on this. The most concrete I could find was Section 4.2 ("Monadic Translation of Effects") of [1] where we find two monads discussed, the simpler state monad with nondeterminism and exceptions, and the more general free monad over an effect datatype, which looks something like [2]. I imagine that you assume a trace equivalence over those monads (finite and infinite traces).
Is this roughly right? If so I wonder how Sail program equivalence relates to the scattered remarks in the RISC-V ISA manuals about that is observable of RISC-V processors.
What is (or should be) deemed observable about the whole-system semantics is a separate question, which I don't think has ever been really carefully considered. For many purposes, that should be the external IO - but when thinking about litmus tests one is usually assuming the register and memory state can be inspected at the "end". Eyeballing the few occurrences of "observable" in the current specs, they're just assorted remarks, rather than something considered together.
Volume I: RISC-V Unprivileged ISA V20191213 p11 "2) imprecise fatal traps might be observable by software."
I've nothing to say about this one
p168 "Same-address orderings from a store to a later load, on the other hand, do not need to be enforced. As discussed in Section A.3.2, this reflects the observable behavior of implementations that forward values from buffered stores to later loads."
This is just a fact about the concurrency model - that if one did enforce that, the model wouldn't be sound w.r.t. conventional hardware.
p205 "It is observable that the Store ea can occur before the value to be stored is determined".
This is an interesting interaction between the intra-instruction semantics and the concurrency model: To be sound w.r.t. hardware, one needs to ensure for these instructions that the register write-back of the computed effective address is before (in the Sail) the register read of the data to be stored, so that later instructions dependent on that register can go ahead as early as they might. Surprisingly, it seems the case so far that one can always handle such cases by careful writing of the Sail, without needing non-sequential intra-instruction execution of it (except the address translation case above).
Peter
- A. Armstrong et al, ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS.
https://github.com/rems-project/sail/blob/sail2/src/lem_interp/sail2_impl_base.lem#L462-L475
— Reply to this email directly, view it on GitHub https://github.com/rems-project/sail/issues/163, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZTLBTTEQZABZ3OCWLDUZVPI5ANCNFSM5NUHMDIQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.
You are receiving this because you are subscribed to this thread.Message ID: @.***>
martinberger
I have a naive question which may betray my background in programming language theory: what is the intended notion of Sail program equality?
I know that this is a subtle issue, and not providing a clear answer might have been a choice, so as to give more freedom for exploration. Anyway, the papers I have seen are a bit vague on this. The most concrete I could find was Section 4.2 ("Monadic Translation of Effects") of [1] where we find two monads discussed, the simpler state monad with nondeterminism and exceptions, and the more general free monad over an effect datatype, which looks something like [2]. I imagine that you assume a trace equivalence over those monads (finite and infinite traces). Is this roughly right?
The background to my question is that I want to clarify the observables in the RISC-V Sail model, and this, I think, is best done in harmony with the related concepts in Sail.