Ideas about implementing multiple harts

[Columbus240]

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?

[andres-erbsen]

this makes sense overall. I think it should be possible to have run nondeterministically pick a hart without materializing the oracle sequence, though -- bedrock2 uses a similar semantic style, and there the exec.interact rule picks a non-deterministic return values for external calls without any oracle.