Comments (7)
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.
Related Issues (8)
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from riscv-coq.