missing speculative hazards.

[spall]

Rattle will miss speculative hazards in the case where the would be "required" command of a speculative hazard finished executing and went through hazard checking before the command became "required".

I think there are a couple of possible solutions to this:

1. When a command is "required" and has already been executed, instead of returning immediately perform a lightweight hazard checking that looks for speculative hazards.
2. When each command completes look for all speculative hazards, including those not involving the command that just completed. This might require a special case when the build is finishing; if the last command was speculated.

Thoughts?

[ndmitchell]

I would have guessed that option 1 makes most sense?

But I guess you found this because you failed to find a proof of correctness? Did you then manage to find a proof of correctness? Can we mirror the proof into executable code?

[spall]

I agree option 1 seems the best. In the model I followed something more closely to option 2, but that is just because that fit the model better, not because its the best solution.

Ok i'll work on an option 1 solution.