0xPolygonMiden / miden-vm

STARK-based virtual machine
MIT License
632 stars 161 forks source link

Memory handling of 2 reads at the same address in the same clock cycle #1561

Closed plafer closed 4 days ago

plafer commented 3 weeks ago

Closes #1560

Al-Kindi-0 commented 2 weeks ago

I would personally not treat this at the constraint system unless there is a real use case or a good reason for allowing reading the same address at the same cycles in the same context. Nevertheless, if we go with this approach, we would have to update the constraints to take into account the changes in this PR. For example the following constraints needs to be updated as the cycles need not anymore be monotonically increasing montonicaly_increasing

There could be others so we should double check all constraints which rely on assumptions changes with this PR.

bobbinth commented 2 weeks ago

we would have to update the constraints to take into account the changes in this PR. For example the following constraints needs to be updated as the cycles need not anymore be monotonically increasing

Ah - good point. I guess there are a few ways we can go:

  1. Go through with this PR and fix the constraints (either in this or a follow-up PR).
  2. Make it explicit that reading from the same address in the same cycle is not allowed (and have a proper error for this).
  3. Tackle it as a part of a bigger memory refactoring we'll do in December. For example, maybe it would make sense to introduce a "multiplicity" column for reads. This way this constraint would stay the same. Though, it may introduce more complexities.

Overall, to keep track of the things we may want to address with memory subsystem refactoring:

Al-Kindi-0 commented 2 weeks ago

we would have to update the constraints to take into account the changes in this PR. For example the following constraints needs to be updated as the cycles need not anymore be monotonically increasing

Ah - good point. I guess there are a few ways we can go:

1. Go through with this PR and fix the constraints (either in this or a follow-up PR).

2. Make it explicit that reading from the same address in the same cycle is not allowed (and have a proper error for this).

3. Tackle it as a part of a bigger memory refactoring we'll do in December. For example, maybe it would make sense to introduce a "multiplicity" column for reads. This way this constraint would stay the same. Though, it may introduce more complexities.

Makes sense! Up to you guys, I would prefer option 2 at the moment but given the work in this PR option 1 is fine as well.

Overall, to keep track of the things we may want to address with memory subsystem refactoring:

* Fix the current soundness bug for single element writes.

* Enable support for basic read-only memory.

* Potentially enable support for element-addressable memory.

* Potentially enable multiple reads from the same address at the same cycle.

* Maybe something else as well.

I think that's all

plafer commented 2 weeks ago

I would personally not treat this at the constraint system unless there is a real use case or a good reason for allowing reading the same address at the same cycles in the same context.

Ah yes you're right! Re-reading this now, it does seem like the right approach is to simply return an error in the processor, instead of changing the constraints to allow it. We currently never need to read/write the same location twice, and so it doesn't make sense to allow it.

I will update the PR accordingly.

plafer commented 2 weeks ago

Implementation changed to return an error when a memory address is accessed twice in the same clock cycle.

Interestingly the rcombine_main() test was never incrementing the clock and so was reading & writing the same memory address in the same clock cycle (now fixed).