Add restrictions to RiscvMachine

[Columbus240]

The current definition of RiscvMachine allows some nonsensical instances, which don’t conform to the RISC-V spec. For example is it not necessary for register reads through getRegister to return a previously written value. Another sensible restriction is, that reading and writing from independent locations must commute.

A difficulty of writing the restrictions is, that they may constrain logging of program execution, depending on how logging is implemented. (I don’t understand it yet) If logging changes the internal state of the monad, then the restrictions must allow these to happen.

I’m not used to monads and am not sure how the restrictions can be formalized just-right. I’ll upload some attempts.

Concerning memory accesses:
Although the restrictions would be simpler, if the load* and store* operations would be defined in terms of byte-sized operations, it wouldn’t be sensible to do this, without riscv-semantics doing the same. A benefit the current approach is that logging can tell the difference between accesses of different size. This would be more difficult, if an instance of RiscvMachine could only provide byte-sized operations.

Edit: I learned, that I haven’t yet understood how logging works.

[Columbus240]

I tried to implement restrictions on the reservation mechanism (instructions LR and SC). I added the following lines to RiscvProgram:

makeReservation : t -> M unit;
clearReservation : t -> M unit;
checkReservation : t -> M bool;

makingReservations : forall (addr: t),
    (makeReservation addr) ;; (Return true) =
    (makeReservation addr) ;; (checkReservation addr);
clearingReservations : forall (addr: t),
    (clearReservation addr) ;; (Return true) =
    (clearReservation addr) ;; (checkReservation addr);

And I found the constraints unsatisfiable for the instance in MetricMinimal.v. The monad for MetricMinimal behaves like I expected, making this restriction impractical. I now understand logging a little better.

Does anyone have an idea for a better approach to formalise my intent, or do I wish for something impractical and impossible?

I’d like to only allow instances of RiscvMachine that conform to the RISC-V spec. If it is impossible to encode this directly in the Class, might it be more practical to develop a Hoare-Logic for the RISC-V machine language, in which the RISC-V spec can be formulated and then finally a new typeclass can be derived from RiscvMachine containing only the ones conforming to the RISC-V spec? Encoding a condition like the “guaranteed forward progress” of some loops with LR/SC could maybe be done using a Hoare/Separation-Logic.

In my repo is a branch “MemoryReservation” containing a commit with my work.

[Columbus240]

By the way: Except the trouble with the restrictions, memory reservations themselves are not problematic. I’ll rework the commit and produce an implementation of the A extension. So at least something useful will come out of this.

[Columbus240]

@samuelgruetter, is Spec.Primitives the class I’m looking for? I don’t understand what it encodes.

[samuelgruetter]

Long-ish answer on what Spec.Primitives is:

The point of the Execute*.v files is to define what each instruction does in terms of only few primitives such as get/setRegister, load/storeWord, raiseException etc, defined in riscv.Spec.Machine.RiscvProgram. The behavior of these primitives can be highly platform dependent and is not specified by the core spec. For instance, a loadWord in a range which is not memory could cause an IO event to happen if your platform does memory-mapped IO, and depending on your memory model, storing and then loading the same memory address could return a different value than what you wrote, etc.

But in order to prove anything interesting about a RiscV machine, we have to make assumptions about the behavior of these primitives. For instance, the bedrock2 compiler assumes that memory behaves like a partial map, ie. if you write and then read the same address, you get back the value you wrote. Encoding these assumptions can be done by implementing the typeclass riscv.Spec.Machine.RiscvProgram, see eg the instance riscv.Platform.Minimal, or riscv.Platform.MinimalMMIO. However, proving a compiler correct directly against such an instance is not very convenient, because the terms involved in your proof become too big, and because it would be nice to write one proof for several different instances. Therefore, I wrote riscv.Spec.Primitives, which is another way of defining what the primitives such as get/setRegister, load/storeWord do, by stating one axiom for each primitive. In order to show that theses axioms are satisfiable, I then show that the instances riscv.Platform.Minimal, or riscv.Platform.MinimalMMIO satisfy these axioms.

I realize this is not documented well enough. As you're working with this code, you'll probably learn about quite some design considerations, and if you'd be willing to write that up, that would be very welcome 😉

[Columbus240]

Thanks for the explanation. It’s very difficult understanding the relations between the different files, because I have to look into each of them and now know by heart, what each more or less does and at what level of abstraction it works. I’d very much like to see this code more documented, because the project interests me, but I don’t know if I’ll be able to find the time to do it myself. At bare minimum, our conversations document a bit what the code does.
I have to think about the format. Comments inside the files, so the extracted coqdoc is readable like literate programming, with a dependency graph showing the structure (similar to Software Foundations). Or separate files (probably markdown).

I don’t know how much time I have to offer, but there will be some opportunities throughout the year where I can lend a hand and a head. I am not yet used to collaborating with others (on GitHub or elsewhere). But I’ll try it.

[Columbus240]

Something nice about the technique of separating the functions (like in Spec.Machine.RiscvMachine) and the conditions on them (Spec.Primitives) probably inhibits problems because functional and propositional extensionality are used in the proofs of the conditions. Problems like non-constructibility of proofs leading to non-computability of functions. Because Primitives has type Prop and no computation may depend on values of this type, it completely works out, i believe. Nice.

[Columbus240]

Closing this issue because I see that you already solved this question, although I don’t yet understand the solution.