Implement multithreading?

[Columbus240]

Currently, one RiscvMachine only runs one hart (RISC-V compatible hardware thread), but implementations of the RISC-V spec may support multiple harts. The interactions between harts and the restrictions on these interactions are currently not captured by this repository.

Discussing multithreading is opening a can of worms, because using multithreading, a given program can leave the processor in many different end states, depending on the order in which the instructions were executed.

This topic is similar to issue #25, where the spec allows multiple behaviors.

The following ideas came to my mind to implement multithreading.

• Try to implement the one to many step-relation of processor states.
• Choose an execution order when running a program. The ordering might be hardcoded or variable.
• Not implementing multithreading.

[threonorm]

Hi @Columbus240

The problem of generating every successor allowed is that it computationally blow up very quickly. To go in that direction I think one would need to describe it relationally - in coq for example - and never actually compute with it.

One idea at some point was to generate SAT formulas, that would represent the ISA constraints, then throw in the memory model constraints, and shake it up in a SAT solver to get the allowed behavior of a program. Usually people flatten the execution by unfolding the loop and the conditional of the program. This quickly create massive constraints system so I was not convinced into spending the time to write that. I also thought that this was problematic if one wanted to be completely honest an consider instructions loads and virtual memory loads as loads.

The part about choosing a specific execution order is fairly easy to do implementing a new instance for the riscv machine. Earlier I had made some experiments on a dual core RV32I without much trouble. But then it really become only a simulator, and I am not sure I see the interest.

One other idea, was to write a trace acceptance function:
Input : - traces of load/stores that each core would emit/receive. Kind of like taking a logic analyzer and looking at the wires between the cores and the memory.

Machine Instance : - The machine progressively eat up the trace, consuming the answer of loads as they are giving in the trace, and verifying that there are the right memory operation emitted in the trace when it tries to emit them.
For example if the trace says that next event of Core 0 is LD ADDR RETURNEDVALUE. Then the machine will:
1- Return false if the next memory operation that it is trying to do is not a load to addr ADDR
2- Otherwise use returnedvalue as the value for the load and remove the LD ADDR RETURNEDVALUE from the trace for core 0 to go to the next event.
In that perspective, we could hope to modularly check that the trace is "ISA" compliant and memory model compliant.
Output: - boolean describing if that is compliant with the RV memory model and the RV isa.

I think this is still on some todo list. It is not as easy as what it may look like beause of ctrl/data/addr dependencies in the memory model and the gazillions cases of dependencies carried or not carried through CSRs (see the memory model, there is also a fair amount of work in the A subset, that is currently handwaved in ExecuteA). So the event would need to embody more than just the kind of memory operations and their returned value/addrs, but also if they have any form of ctrl/addr/data dependencies with other events (more a graph like I think?), and the machine would need to keep track of those and ensure that the dependencies label are proper.
It also is frustrating because someone still need to come up with those traces.