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

Determine range constraints from fixed lookup. #2300

Merged
merged 11 commits into from
Jan 13, 2025
Merged

Conversation

chriseth
Copy link
Member

@chriseth chriseth commented Jan 2, 2025

No description provided.

@chriseth chriseth mentioned this pull request Jan 6, 2025
2 tasks
@chriseth chriseth marked this pull request as ready for review January 9, 2025 17:15
Copy link
Collaborator

@georgwiese georgwiese left a comment

Choose a reason for hiding this comment

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

Awesome! Took me while to understand but it does what I thought it would do.

executor/src/witgen/jit/affine_symbolic_expression.rs Outdated Show resolved Hide resolved
executor/src/witgen/jit/single_step_processor.rs Outdated Show resolved Hide resolved
Some(values)
});
let Some(first) = values.next() else {
// If the iterator is empty, we have no match, but it can always be answered,
Copy link
Collaborator

Choose a reason for hiding this comment

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

I'm not sure I understand this case. In this case, no match was found right? So this branch is actually impossible?

Copy link
Member Author

Choose a reason for hiding this comment

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

I mean yes, but it's not like more information about the inputs will help. As I wrote there, if we could express "invalid" in the range constraints, we should return that. We could also panic. I'll create an issue.

Copy link
Member Author

Choose a reason for hiding this comment

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

-> #2324

.iter()
.map(|is_known| {
if is_known {
// We could also copy the input range constraint.
Copy link
Collaborator

Choose a reason for hiding this comment

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

I think that would be clearer. Or add a comment that intersect with existing range constraints anyway (which it seems we do in WitgenInference::add_range_constraint), so it's no-op.

Comment on lines 285 to 312
let mut values = index
.iter()
.filter(|(key, _)| matches_range_constraint(key, &input_range_constraints))
.map(|(_, value)| {
let (_, values) = value.get()?;
Some(values)
});
let Some(first) = values.next() else {
// If the iterator is empty, we have no match, but it can always be answered,
// so this is successful.
// Unfortunately, we cannot express the "empty" range constraint.
return Some(vec![Default::default(); range_constraints.len()]);
};
// If an item (including the first) is None, it means the match was not unique.
let mut new_output_range_constraints = first?
.iter()
// min, max, mask
.map(|v| (*v, *v, v.to_integer()))
.collect_vec();
for v in values {
// If any value is None, the match was not unique.
let v = v?;
for ((min, max, mask), v) in new_output_range_constraints.iter_mut().zip_eq(v) {
*min = (*min).min(*v);
*max = (*max).max(*v);
*mask |= v.to_integer();
}
}
Copy link
Collaborator

@georgwiese georgwiese Jan 9, 2025

Choose a reason for hiding this comment

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

Suggested change
let mut values = index
.iter()
.filter(|(key, _)| matches_range_constraint(key, &input_range_constraints))
.map(|(_, value)| {
let (_, values) = value.get()?;
Some(values)
});
let Some(first) = values.next() else {
// If the iterator is empty, we have no match, but it can always be answered,
// so this is successful.
// Unfortunately, we cannot express the "empty" range constraint.
return Some(vec![Default::default(); range_constraints.len()]);
};
// If an item (including the first) is None, it means the match was not unique.
let mut new_output_range_constraints = first?
.iter()
// min, max, mask
.map(|v| (*v, *v, v.to_integer()))
.collect_vec();
for v in values {
// If any value is None, the match was not unique.
let v = v?;
for ((min, max, mask), v) in new_output_range_constraints.iter_mut().zip_eq(v) {
*min = (*min).min(*v);
*max = (*max).max(*v);
*mask |= v.to_integer();
}
}
let values = index
.iter()
.filter(|(key, _)| matches_range_constraint(key, &input_range_constraints))
.map(|(_, value)| value.get().map(|(_, values)| values))
.collect_vec();
if values.is_empty() {
// If the iterator is empty, we have no match, but it can always be answered,
// so this is successful.
// Unfortunately, we cannot express the "empty" range constraint.
return Some(vec![Default::default(); range_constraints.len()]);
};
// If any item is None, it means the match was not unique.
let values = values.into_iter().collect::<Option<Vec<_>>>()?;
let new_output_range_constraints = values
.into_iter()
// Map each row to a vector of range constraints, represented as (min, max, mask).
.map(|row| row.iter().map(|v| (*v, *v, v.to_integer())).collect_vec())
// Reduce by disjunction
.reduce(|acc, values| {
acc.into_iter()
.zip_eq(values)
.map(|((min1, max1, mask1), (min2, max2, mask2))| {
(min1.min(min2), max1.max(max2), mask1 | mask2)
})
.collect()
})
.unwrap();

What do you think of this? Should be equivalent and removes the special handling of the first element.

Copy link
Collaborator

Choose a reason for hiding this comment

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

I think it could be further improved by implementing a disjunction method in RangeConstraint and using it directly, instead of working with (T, T, T::Integer)!

Copy link
Member Author

Choose a reason for hiding this comment

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

If the range is really big, this allocates a large vector, I wanted to avoid that.

Copy link
Member Author

Choose a reason for hiding this comment

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

Disjunction is more complicated because we need to consider all combinations of which range constraint wraps.

Copy link
Member Author

Choose a reason for hiding this comment

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

Actually let me try using reduce.

Copy link
Member Author

Choose a reason for hiding this comment

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

Ah right, we would need try_reduce, but it's not stable.

@chriseth
Copy link
Member Author

Changed it to avoid advancing the iterator by the first element, but to be honest, I'm not sure it is clearer this way.

Copy link
Collaborator

@georgwiese georgwiese left a comment

Choose a reason for hiding this comment

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

I think it is clearer, thanks! Just some tiny comments left.

executor/src/witgen/machines/fixed_lookup_machine.rs Outdated Show resolved Hide resolved
}
Some(match new_range_constraints {
None => {
// The iterator was empty, i.e. there are no inputs in the index matching the
Copy link
Collaborator

Choose a reason for hiding this comment

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

I still don't understand whether this is a case that would happen in practice (for example because some branches are actually impossible), or whether hitting this path would mean we can't complete the code generation. If the latter, maybe we can at least log an error?

Copy link
Member Author

Choose a reason for hiding this comment

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

I think this can happen if we decide to branch, then derive further concrete values, do a lookup again and then discover that we do not have these values in the lookup table at all.

Copy link

@github-actions github-actions bot left a comment

Choose a reason for hiding this comment

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

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Benchmarks'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.20.

Benchmark suite Current: c13dc10 Previous: 65a2fdd Ratio
jit-benchmark/sqrt_879882356 18256 ns/iter (± 58) 2620 ns/iter (± 2) 6.97
jit-benchmark/sqrt_1882356 14032 ns/iter (± 44) 2102 ns/iter (± 2) 6.68
jit-benchmark/sqrt_1187956 13774 ns/iter (± 38) 2076 ns/iter (± 2) 6.63
jit-benchmark/sqrt_56 7163 ns/iter (± 33) 1242 ns/iter (± 1) 5.77
jit-benchmark/sort_33 388409 ns/iter (± 1506) 69275 ns/iter (± 73) 5.61
jit-benchmark/sort_100 1521434 ns/iter (± 5676) 257883 ns/iter (± 230) 5.90
jit-benchmark/sort_300 6547032 ns/iter (± 38942) 990021 ns/iter (± 1159) 6.61
jit-benchmark/sort_900 34337552 ns/iter (± 159608) 4214293 ns/iter (± 4534) 8.15
jit-benchmark/sort_2700 222478643 ns/iter (± 1281608) 20424753 ns/iter (± 158091) 10.89

This comment was automatically generated by workflow using github-action-benchmark.

georgwiese
georgwiese previously approved these changes Jan 11, 2025
@georgwiese georgwiese added this pull request to the merge queue Jan 11, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Jan 11, 2025
@georgwiese georgwiese added this pull request to the merge queue Jan 13, 2025
Merged via the queue into main with commit f6b0b7b Jan 13, 2025
16 checks passed
@georgwiese georgwiese deleted the range_from_fixed branch January 13, 2025 13:37
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.

2 participants