Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Witgen: Handle machine calls with side effects #1388

Merged
merged 4 commits into from
May 21, 2024
Merged

Conversation

georgwiese
Copy link
Collaborator

@georgwiese georgwiese commented May 20, 2024

Cherry-picked ef6a72f from #1380.

With this PR, we track whether a call to a machine led to some side effect (e.g. added a block). In that case, the processed identity should count has having led to some progress, even if no values were returned to the calling machine. An example would be writing values to memory, which does not return any values and hence does not change the state of the caller.

// TODO: This would be the right thing to do, but currently leads to failing tests
// due to #1385 ("Witgen: Block machines "forget" that they already completed a block"):
// https://github.com/powdr-labs/powdr/issues/1385
// let updates = updates.report_side_effect();
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

test_data/asm/book/operations_and_links.asm fails, because there is a machine that calls the same sub-machine with multiple arguments. Because of #1385, this keeps adding new blocks. Not reporting the side effect makes this works, because then the identity is not processed again.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

is it gonna be fixed here or later?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Later, this requires fixing #1385, which is not the scope of this PR. The fix in this PR is disabled for block machines because of #1385, but IMO it makes sense to merge like this because it adds all the infrastructure to handle side effects, and it already works for other machines (crucially: memory).

@georgwiese georgwiese changed the title [WIP] Witgen: Handle machine calls with side effects Witgen: Handle machine calls with side effects May 20, 2024
@georgwiese georgwiese marked this pull request as ready for review May 20, 2024 14:04
mstore 3, 3;
mstore 4, 4;

return;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe add some assertions so we know the memory proxy is working>

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, not sure how to do this actually, because we don't have a shared memory yet (which requires #1356) ^^ So we can't access the memory from the main machine here.

If witgen didn't insert the right memory accesses into the memory machine, the permutation would fail, which is tested by the current test.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ah right

Copy link
Member

@leonardoalt leonardoalt left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

left some small comments, otherwise looks good

@leonardoalt leonardoalt added this pull request to the merge queue May 21, 2024
Merged via the queue into main with commit a3087ea May 21, 2024
6 checks passed
@leonardoalt leonardoalt deleted the side-effects branch May 21, 2024 16:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants