Add restrictions to `RiscvMachine` about riscv-coq HOT 7 CLOSED

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.

from riscv-coq.

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.

from riscv-coq.

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

from riscv-coq.

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 😉

from riscv-coq.

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.

from riscv-coq.

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.

from riscv-coq.

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

from riscv-coq.