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

Some new performance features #14

Merged
merged 3 commits into from
May 21, 2024
Merged

Some new performance features #14

merged 3 commits into from
May 21, 2024

Conversation

ericeil
Copy link
Collaborator

@ericeil ericeil commented May 16, 2024

While doing some Prover performance work, I found the following to be useful:

  • Add mapReduce and parallelMapReduce methods on TreapSet, TreapMap, and TreapList. These do what you think they do, and are useful for the obvious reasons.

  • Allow TreapMap.updateValues (and parallelUpdateValues) to change the type of the values. This makes a straightforward mapping of values to different types an O(N) operation instead of O(N log N).

I also simplified the TreapMap.updateEntry signature a bit (it had some extraneous nullability annotations).

@ericeil ericeil changed the title A couple of new features and a bugfix Some new performance features May 16, 2024
@ericeil ericeil requested a review from jtoman May 16, 2024 22:19
Copy link

@jtoman jtoman left a comment

Choose a reason for hiding this comment

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

Nits and requests for comment

Comment on lines +359 to +368
private fun <R : Any> mapReduceImpl(map: (K, V) -> R, reduce: (R, R) -> R): R {
val (left, middle, right) = fork(
self,
{ left?.mapReduceImpl(map, reduce) },
{ shallowMapReduce(map, reduce) },
{ right?.mapReduceImpl(map, reduce) }
)
val leftAndMiddle = left?.let { reduce(it, middle) } ?: middle
return right?.let { reduce(leftAndMiddle, it) } ?: leftAndMiddle
}
Copy link

Choose a reason for hiding this comment

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

is there a compelling reason to not just go ahead and make this an erased types implementation too? It seems like we always go back and do this for performance anyway so...

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Static typing is good. :)

Comment on lines +159 to +177
override fun <R : Any> mapReduce(map: (E) -> R, reduce: (R, R) -> R): R =
notForking(self) { mapReduceImpl(map, reduce) }

override fun <R : Any> parallelMapReduce(map: (E) -> R, reduce: (R, R) -> R, parallelThresholdLog2: Int): R =
maybeForking(self, threshold = { it.isApproximatelySmallerThanLog2(parallelThresholdLog2) }) {
mapReduceImpl(map, reduce)
}

context(ThresholdForker<S>)
private fun <R : Any> mapReduceImpl(map: (E) -> R, reduce: (R, R) -> R): R {
val (left, middle, right) = fork(
self,
{ left?.mapReduceImpl(map, reduce) },
{ shallowMapReduce(map, reduce) },
{ right?.mapReduceImpl(map, reduce) }
)
val leftAndMiddle = left?.let { reduce(it, middle) } ?: middle
return right?.let { reduce(leftAndMiddle, it) } ?: leftAndMiddle
}
Copy link

Choose a reason for hiding this comment

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

just so I'm not crazy: this is the same implementation as the map case right?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Yes, I think it's just the map lambda type that's different.

Comment on lines +22 to +29
override fun <R : Any> updateValues(
transform: (K, V) -> R?
): TreapMap<K, R> = treapMapOf()

override fun <U> updateEntry(key: K, value: U?, merger: (V?, U?) -> V?): TreapMap<K, V> =
override fun <R : Any> parallelUpdateValues(
parallelThresholdLog2: Int,
transform: (K, V) -> R?
): TreapMap<K, R> = treapMapOf()
Copy link

Choose a reason for hiding this comment

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

can't you return this and just unsafe cast it? That's ultimately what treapMapOf is doing right? I'm not suggesting we do this, just making sure I understand what the code is doing.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Yes, this is just a nicer-looking way of doing that.

Comment on lines +284 to +291
override fun <R : Any> shallowMapReduce(map: (K, V) -> R, reduce: (R, R) -> R): R {
var result: R? = null
forEachPair {
val mapped = map(it.key, it.value)
result = result?.let { result -> reduce(result, mapped) } ?: mapped
}
return result!!
}
Copy link

Choose a reason for hiding this comment

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

is the type bound on R here just so we have nullability of result? I'm trying to think of a way to relax this, but I think you can only use, e.g., lateinit on non-null types.

Probably not worth it.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

We depend on this constraint in mapReduceImpl, where it's a bigger deal. It avoids needing to allocate a result holder for each step of the traversal.


internal tailrec fun <E> TreapListNode<E>?.isApproximatelySmallerThanLog2(sizeLog2: Int): Boolean = when {
this == null -> true
sizeLog2 <= 0 -> false
Copy link

Choose a reason for hiding this comment

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

when could this ever be less than zero? Seems like we should throw on this behavior?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Good point!

Comment on lines +37 to +39
public fun <R : Any> updateValues(
transform: (K, V) -> R?
): TreapMap<K, R>
Copy link

Choose a reason for hiding this comment

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

So this is a change in the public API right? If V was a nullable type, you could use this function to update the values of the map. But now you can't, updatedValues is unusable for nullable types. Maybe that was a bug, as I suspect that we removed entries for which transform returned null, but still, it means part of the API is unusable depending on your type parameter.

Copy link

Choose a reason for hiding this comment

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

I think I'm favor of this change, as it makes explicit that null values are filtered out, where as previously you could write:

 treapMapOf("foo" to 3, "bar" to null).updateValues { _, v -> v }

and have this return a map without "bar" (and no null keys) but this wasn't reflected in the return type of updateValues

Copy link

Choose a reason for hiding this comment

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

Can we document this behavior a bit more explicitly though?

Copy link
Collaborator Author

@ericeil ericeil May 17, 2024

Choose a reason for hiding this comment

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

You can definitely write this, before and after this change:

var map = treapMapOf("foo" to 3, "bar" to null).updateValues { _, v -> v }

In both cases the result is a map without the entries that had null values. With this change, the result will be typed as TreapMap<String, Int> instead of TreapMap<String, Int?>.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I will add some comments.

@ericeil ericeil requested a review from jtoman May 17, 2024 20:21
@ericeil ericeil merged commit 840d5eb into Certora:main May 21, 2024
1 check passed
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