It would be great if trying to execute an instruction from an address that was written to after the last FENCE.I instruction was executed was undefined behavior. I am requesting this because I realized that the kami case study cpu does not satisfy this specification because writes to instruction memory are not reflected in instruction execution (and FENCE.I happens to be not supported). As this processor is roughly microcontroller-class, uses a very simple traditional RISC pipeline, and does not do anything funny with memory coherence, perhaps we can avoid the discussion of the more general weak memory tarpit.
However, if I understand correctly, this is the first instance of specifying something as undefined behavior in this repository, so we will figure out a way to do that. Naive suggestion: set a "bad" bit in the processor state and refuse all further instructions?
It would be great if trying to execute an instruction from an address that was written to after the last
FENCE.Iinstruction was executed was undefined behavior. I am requesting this because I realized that the kami case study cpu does not satisfy this specification because writes to instruction memory are not reflected in instruction execution (andFENCE.Ihappens to be not supported). As this processor is roughly microcontroller-class, uses a very simple traditional RISC pipeline, and does not do anything funny with memory coherence, perhaps we can avoid the discussion of the more general weak memory tarpit.However, if I understand correctly, this is the first instance of specifying something as undefined behavior in this repository, so we will figure out a way to do that. Naive suggestion: set a "bad" bit in the processor state and refuse all further instructions?