v1.1.{4-5}: Sorting Propagators

28 August 2024. We perform two experiments to reduce thread divergence by sorting propagators, for the reasons mentioned in the previous post. Given a list of propagators representing constraints, we sort on the syntactic shape of the constraint:

• v1.1.4: Sort on the symbol of the outermost predicate of the formula, e.g. x < y is equal to z + y < x * x, but less than x <= y for an arbitrary ordering between < and <=.
• v1.1.5: Lexicographic sort on the first predicate symbol followed by the length of the formula, e.g. length(x < y) = 2 < 3 = length(z + y < x * x).

These are quite simple solutions to reduce divergence while avoiding spending too much time on a sorting algorithm specialized to minimize divergence. The results are not impressive, and it shows that thread divergence is perhaps not the biggest bottleneck of Turbo. Nevertheless, given how cheap this optimization is, I decided to keep it. Note that on some benchmarks where the propagators are very unsorted (e.g. gfd_schedule), sorting increases by 50% the number of nodes explored.

Results v1.1.4

Results v1.1.5