mit-plv / riscv-coq Goto Github PK
View Code? Open in Web Editor NEWRISC-V Specification in Coq
License: BSD 3-Clause "New" or "Revised" License
RISC-V Specification in Coq
License: BSD 3-Clause "New" or "Revised" License
I created a branch 'doc' in my repo with some notes about the structure of the code.
I’m beginning to decipher Primitives.v
and would like to add my notes about it to this repo, so that other people can understand it more easily.
I’d like to discuss how the documentation shall be added to the repo. Should it be in coqdoc format (adding a new target to the makefile) or in files separate to src/
? Should it, if read front-to-back, touch on every aspect of the repo or only highlight major parts?
The documentation of the stdlib of Coq is relatively sparse, consisting mostly of headings and a sometimes a few lines of text. I don’t think this style would be completely adequate, because the stdlib contains well-known math, while the structure and content of this repo is unfamiliar to a new reader. But for files like Utility/Monads.v
the style of the stdlib seems okay to me.
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.
The Coq team released Coq 8.18.0
on September 7th, 2023.
The corresponding Coq Platform release 2023.10
should be released before November 30th, 2023.
It can be delayed in case of difficulties until January 15th, 2023, but this should be an exception.
This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.18.0
.
Coq Platform CI is currently testing opam package coq-riscv.0.0.4
from official repository https://coq.inria.fr/opam/released/packages/coq-riscv/coq-riscv.0.0.4/opam.
In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.
In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2023.10
, please inform us as soon as possible and before October 31st, 2023!
The working branch of Coq Platform, can be found here main.
It contains package pick ~8.18+beta1
which already supports Coq version 8.18.0
and contains already working (possibly patched / commit pinned) Coq Platform packages.
In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: coq/platform#372
The Coq team released Coq 8.17+rc1
on December 29th, 2022 and plans to release Coq 8.17.0 around March 7th, 2023.
The corresponding Coq Platform release 2023.03
should be released before April 14th, 2023.
It can be delayed in case of difficulties until June 30, 2023, but this should be an exception.
This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.17+rc1
.
Coq Platform CI is currently testing opam package coq-riscv.0.0.3
from official repository https://coq.inria.fr/opam/released/packages/coq-riscv/coq-riscv.0.0.3/opam.
In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.
In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2023.03
, please inform us as soon as possible and before March 21st, 2023!
The working branch of Coq Platform, can be found here main.
It contains package pick ~8.17~2023.03+preview1
which already supports Coq version 8.17+rc1
and contains already working (possibly patched / commit pinned) Coq Platform packages.
In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: coq/platform#335
Proofs in Minimal.v
, MinimalMMIO.v
and MetricMinimalMMIO.v
are very slow (ordered from a little slow to very slow) and make it annoying to check whether some changes are consistent with the rest of the code.
Maybe the amount of backtracking that has to be done can be reduced. The proofs use similar code of Ltac that maybe can be put in one place (Utility/Tactics.v might be good). Separating the tactics that do a lot of backtracking like _ |- _ \/ _ => left
from the ones that do very little or no backtracking might be a good idea, if it is reasonably possible. Maybe CPDT of Chlipala has some ideas.
This commit breaks the smoke test in the platform:
https://github.com/coq/platform/actions/runs/8391869140/job/22983180597
Could you offer a new test ?
I started working on a formalisation of the privileged specification, mostly the CSRs. The CSR branch on my repo contains the current code. Some splitting and reordering of the commits in the branch is necessary, but not important right now.
I’d like to describe and discuss some design decisions and problems.
RiscvMachine
has to have CSRField
granularity, because some fields appear in multiple CSRs and are required to have the same value in all ocurrences. (riscv-semantics does the same) Also properties like WARL and WPRI are defined on this granularity in the spec.RiscvMachine
can implement custom extensions to the CSRs and the values get forwarded to the programs. Also, we can now capture, whether a program actually treats the WPRI fields the way it should (preserving and ignoring).mscratch
.*XLEN
of a hart may change at runtime and may differ from eachother. The current *XLEN
can be determined by reading MXL
, SXL
and UXL
. Except, if the misa
register is not implemented (hardwired to zero). Then we have to use some “non-standard mechanism”.Extensions
field of the misa
CSR may also change at runtime. This means that which instructions are valid depends on the value of this field. So changes to decoding and execution might be necessary.misa
CSR to be hardwired to zero. In this case MXLEN
has a fixed value, but the spec says nothing about enabling or disabling extensions at runtime. To allow misa
to be zero, additional operations on RiscvMachine
would be necessary to get the equivalent of reading MXL
and Extensions
. This might create a little headache here and there, but it would represent the spec faithfully.RiscvMachine
keep track of it using additional getter/setter operations. I’m not sure whether the current privilege level can be read from a CSR. I think I can solve this myself.COQC /home/travis/build/mit-plv/riscv-coq/src/riscv/Spec/Decode.v
File "/home/travis/build/mit-plv/riscv-coq/src/riscv/Spec/Decode.v", line 24, characters 8-23:
Error: Cannot find a physical path bound to logical path matching suffix
Utility.
The Coq team released Coq 8.19.0
on January 24th, 2024.
The corresponding Coq Platform release 2024.01
should be released before April 30th, 2024.
It can be delayed in case of difficulties until May 15th, 2024, but this should be an exception.
This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (0.0.4) does not work with Coq 8.19.0
.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.
Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI appears to test this project, but has some special handling for your project which makes it difficult to retrieve the commit it tests for your project.
Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.19, preferably before March 31st, 2024?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.
In case the tag and opam package are available before March 31st, 2024, it will be included in an early Coq Platform beta release of the for Coq 8.19.0.
The working branch of Coq Platform, can be found here main.
It contains package pick ~8.19~2024.01+beta1
which already supports Coq version 8.19.0
and contains already working (possibly patched / commit pinned) Coq Platform packages.
Please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: coq/platform#405
To specify the behaviour of a risc-v processor with multiple harts, the follwing problems need to be solved.
Spec.RiscvMachine
.misa
contains the capabilities of the associated hart.)I believe, before the first two problems can be tackled, CSRs need to be implemented.
Concerning parallel execution: For Platform.Run
to work on a machine with multiple harts, it requires a structure defining the execution order of the harts. This structure consists of a sequence (in the mathematical sense, an infinite list) of hartids and a proof, that for each hartid of the machine, there is a subsequence (in the above sequence) consisting only of the given hartid (a constant sequence).
The Platform.Run
would then apply run
on the hart with id equal to the first element of the sequence and remove the first element from the sequence.
An implementation of the riscv-v ISA that behaves as if the harts were always run in the same order can be modeled with the above, by packaging the instance of Spec.RiscvMachine
with the structure containing the hart ordering.
Proofs about the behaviour of risc-v programs can thus be made either with arbitrary hart ordering or with an arbitrarily restricted hart ordering.
Was my idea about parallel execution understandable and is it reasonable?
https://content.riscv.org/wp-content/uploads/2017/05/riscv-privileged-v1.10.pdf 3.1.12:
The encoding of the MODE field is shown in Table 3.5. When MODE=Direct, all traps into
machine mode cause the pc to be set to the address in the BASE field. When MODE=Vectored,
all synchronous exceptions into machine mode cause the pc to be set to the address in the BASE
field, whereas interrupts cause the pc to be set to the address in the BASE field plus four times
the interrupt cause number. For example, a machine-mode timer interrupt (see Table 3.6) causes
the pc to be set to BASE+0x1c. Setting MODE=Vectored may impose an additional alignment
constraint on BASE, requiring up to 4 × XLEN-byte alignment.
Line 62 in 2b6e113
MODE=Vectored
.A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.