mit-plv / riscv-coq Goto Github PK

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.

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

To specify the behaviour of a risc-v processor with multiple harts, the follwing problems need to be solved.

• The harts aren’t always in the same state. This requires a restructuring of Spec.RiscvMachine.
• The harts may support different ISA extensions. (Interpretation of the spec, because the spec doesn’t specify otherwise and misa contains the capabilities of the associated hart.)
• Deal with the “parallel” execution of the harts. Because Coq has different tools to express requirements than Haskell, I believe it is possible to define a “sane” or “precise” notion of parallel execution in Coq.

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?

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

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.

• I haven’t setup automatic conversion from riscv-semantics, but I used a similar code structure. I did this because riscv-semantics doesn’t formalise many parts of the spec. For example it always assumes MXLEN=SXLEN=UXLEN and always assumes that the MXL field is implemented. And I didn’t want to configure the conversion and deal with conversion errors.
• The interface to the CSRs provided by a 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.
• riscv-semantics doesn’t formalise the fields with WPRI. I chose to do so, so that an instance of 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).
• The privileged spec describes itself as one possible specification of the privileged architecture ontop of the unprivileged ISA. Both my code and riscv-semantics don’t reflect this. It would add another layer of abstraction if we were to implement this, and because there are currently no competing privileged specifications that I know of, it would be unneccessary.
• The definition of CSRs and CSRFields were put into separate files (in my code and in riscv-semantics) so that there would be less name collisions. Because there are registers with the same name as a field, for example mscratch.
• I didn’t write down the CSRs for the debugging spec and the hypervisor stuff, because they are both still drafts.

Looking ahead

• The *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”.
• The 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.
• The privileged spec allows the 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.
• How can the current privilege level be determined? riscv-semantics lets the 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.

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

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.

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.